I've come to prefer one particular approach to writing out a derivation tree by hand. I used to try to draw the tree by stacking up rules with horizontal separators à la Gentzen, but I could never judge how much space I would need--I'm not accustomed to filling a page bottom to top--and one page never seemed to be enough anyway.
I've found that writing judgments top to bottom, indenting to represent nesting, is much more scalable. E.g.:
⊢ (λ f.f 1) (λ x.x) : int
⊢ (λ f.f 1) : (int → int) → int
f : int → int ⊢ f 1 : int
f : int → int ⊢ f : int → int
f : int → int ⊢ 1 : int
⊢ (λ x.x) : int → int
x : int ⊢ x : int
2 comments:
Yeah, I developed a similar technique of my own. In addition to the reasons that you mention, writing the trees out Gentzen-style has one other serious problem: the proof tree very quickly gets much wider than any reasonable sheet of paper. (Especially with PL type rules, which tend to have many more antecedents than do the inference rules in, say, classical logic.)
Good to become visiting your weblog again, it has been months for me. Nicely this article that i've been waited for so long. I will need this post to total my assignment in the college, and it has exact same topic together with your write-up. Thanks, good share. cheap custom term paper
Post a Comment