Jason (jcreed) wrote,

Randy Pollack gave a very curious talk about lambda-term representation. I thought I had already heard basically everything there was to hear on the subject, but there's this Sato-Pollack paper that points out that there do exist reasonable canonical (i.e. alpha-equivalence classes have exactly one canonical form) representations of lambda terms that are nonetheless named, in the sense that there are real identifiers sitting at the lambdas, and variables point to their binder by using that same identifier, not via some deBruijn mumbo-jumbo, be it deBruijn indices (counting up) or deBruijn levels (counting down).

There are in fact three very nice properties that characterize well-behaved "height functions", which are the things that tell you what to call a bound variable when you bind it.

Stepping back, the whole process I guess is like someone handing me a lambda term like

(\x.\y.x) (\z.\z.z)

and my job is to come up with a canonical alpha-equivalent lambda-term --- according to one height function Pollack mentioned, (on page 8 of http://homepages.inf.ed.ac.uk/rpollack/export/SatoPollack09.pdf) it would come out:

(\1.\0.1) (\0.\1.1)

where I'm using numbers as bound variables, but unlike deBruijn, they occur at binding positions too.

This labelling process I'm tasked with can be done in a very nice substitution-compatible way; for this particular height function, every occurrence of a subterm like \z.z will always become \1.1, every subterm like \x.\y.x will always be \1.\0.1, and so on.
Tags: binding, hoas, math, talks

  • (no subject)

    Cat vs. Fence. WHO WILL WIN? Cat is very agile, but... In other news, Lulu copy of thesis just arrived today, and it looks great! Score one more…

  • (no subject)

    Ok, kids, if you want to blow $40+shipping on a color* copy of my thesis I'm not stopping you. *The cover is color no matter what, but this version…

  • (no subject)

    Recently constructed things: First attempt at Lulu-ing thesis. I have ordered a copy for myself to make sure it looks ok. Made a song with tom7…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded