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
10 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
Good to read this webpage, and I used to pay a visit this web site. greatt
I am reading articles online and this is one of the best, Thankyou for providing this.
I’m happy I read this. It is very well written, great Keep doing it. Thanks
Hi! this nice article you shared with great information. Keep sharing.
This article is Really contains lot more information about This Topic. Its a great blog
I have read this excellent post. This is a great job. Keep what you're doing, thanks.
I will bookmark this blog of yours, its so good. Waiting for your next updates
Its really fun to read this. I enjoyed a lot. Great Article its really informative.
Post a Comment