Tuesday, March 31, 2009

Hand-writing derivations

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

1 comment:

Richard Cobbe said...

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.)