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
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded