September 23rd, 2008

beartato phd

(no subject)

ICFP day two. I have a wretched cold: it is not fun.

The invited talk was again very good. Olivier Danvy is a great, animated speaker. I missed a couple of jokes through the haze of French accent, but there were plenty of zingers left. He talked a lot about some known facts that are apparently quite old, but new to me in their given form, and quite appealing.

The short version is basically this story:

John Reynolds grabs you by the wrist one fine day and shows you a definitional interpreter of the lambda calculus, implemented in a straightforward way in your favorite functional programming language, and asks you, "is this interpreter Call-by-Name or Call-by-Value?". It turns out it's a trick question! Because of the utterly transparent way the interpreter is written*, it's CBN if your favorite language is, and CBV if your favorite language is.

The next neat thing is if you defunctionalize and CPS convert this definitional interpeter, you get a standard stack machine semantics --- actually, one of two rather standard stack machine semantics, depending on whether you take the CBN or CBV version of the CPS transform.

The moral I take away from this is that if you're looking for the ultimate origin of the interesting stuff, the stack machines that actually tell us how to do computation, well, their meaning is hidden away in the CPS and defunctionalization transformations. For the datum that these transformations are applied to, namely the definitional interpreter, has no real meaning unto itself. It basically just says "translate app as app, var as var, lam as lam".

What I want to know is: what does this tell us about HOAS, the epitome, if anything is, of making mountains out of meta-mountains? If we vary the meaning of β-reduction, or of variables, (in some way more drastic than just making them substructral or modal or something) what might this do to our encodings?

* Which was called the "Scott-Tarski interpreter" by Danvy, alluding to Dana Scott because it implements a solution of the domain equation D = D → D, and Tarski because of Girard's habitual complaining about "Mr. Meta-Tarski" defining first-order logic in an equally "transparent" way by saying "|= A v B holds if, you know, either |= A or |= B holds", relying on our natural-language intuitions (or perhaps classicalitions?) of the meaning of disjunction.