February 8th, 2008

beartato phd

(no subject)

Had a meeting with chrisamaphone. Her senior thesis is lookin' good! TeX does wonders for that kind of thing, and so does, er, having proofs. Math is fun! Let's not go shopping.

In lambda calculus Statman basically finished off the proof that all the difficulty in checking βη equality of simply typed terms is already present at type (o → o → o) → o → o, the type of binary trees. This went by first reducing everything to the type
Λ = ((o → o) → o) → (o → o → o) → o
which I desperately wanted him to call what it is, namely the type of untyped lambda expressions! Maybe not everyone in the class already had an intuition for HOAS, but some did, and I think explaining it would have been easier than thinking of the two arguments (o → o) → o and o → (o → o) as being injections and outjections of a function type into o. The latter intuition worked well enough for Scott, but it feels very old fasioned.

But armed with the former intuition, we can go ahead and do the same construction we would anyway, which is to name the free variables lam : ((o → o) → o) and app : (o → o → o)) and make the type-inductive definitions of UA : o → A and VA : A → o as follows:

Uo = Vo = λ x . x
UA → B = λ x . λ y . UB (app x (VA y))
VA → B = λ x . lam (λ y . VB (x (UA y)))

(but Statman gave a "dot-dot-dot" style definition, which I claimed to wjl was probably necessary if he was doing it that way, but I was totally wrong, as apparently I usually am when I make these sort of claims)

And then
T =(λM.λlam.λapp.VA M)
is a term of type A → Λ that is injective in the sense that M =βη N iff T M =βηT N. Why? Here's where the HOAS intuition comes in handy and makes a one-line proof of what otherwise took a whole class-period of futzing with head-variables and reductions and so on:
because T M is the HOAS representation inside the type Λ of the canonical (η-long, β-normal form) of M.

The proof after that point was showing how to eliminate binding from Λ. First you ask for a type that has two binary operators, one unary, and one leaf, call it:
Ω = (o → o → o) → (o → o → o) → (o → o) → o → o

and do this funny trick

(λ e : Λ. λ g f u z . e (λ b . g (u (b z)) (b (u (b z)))) f) : Λ → Ω

The easy part is that the binary operation of application just gets interpreted homomorphically as one of the two binary operators in Ω, called here by the ariable name "f". The cute thing is that you turn binding into a binary operator g, where the left branch is the name of the variable and the right branch is the term; but way you guarantee freshness of the variable's "name" is by making it the whole body of the lambda-abstraction! Except the body is open, so you have to ground it somehow, which you do by plugging in the leaf z: b z is the name of the variable. Except it isn't. We also want to wrap this whole business in the unary function symbol u just to make sure that an irrelevant function body and a single occurrence of a variable don't get confused: okay, so u (b z) is the name of the variable. We want to substitute this for every occurrence of the variable, so HOAS lets us carry this substitution out by application: b (u (b z)). Now just slap g and the "nominal" u (b z) on it and we're done.

To convert back to plain binary trees is then an easy matter of "tagging". Just make up three distinct tags and put them in the left branch, and put the rest of your tree down the right:

(λ w : Ω. λ node . &lambda . leaf .
 (λ x y . node t1 (node x y))
 (λ x y . node t2 (node x y))
 (λ x . node t3 x)
 leaf) : Ω → (o → o → o) → o → o

where, like, t1 = leaf, t2 = node leaf leaf, and t3 = node (node leaf leaf) leaf