User loginNavigation |
Quotation and evaluation -- or, how pure is the pure lambda calculus?By now theories of computation are a dime a dozen. What makes any such theory interesting, at this stage of the game, is the perspective such a theory offers on computation. One aspect of algebraic theories -- like the lambda or the pi-calculus -- that has long intrigued me is that they are typically predicated on a theory of names. They'll tell you what a computation is as long as you are willing to pony up some notion of a name. Moreover, this notion of name has got to come equipped with a notion of equality to effect things like substitution in lambda and pi or synchronization in pi. And, since having an infinite set of atomic entities over which you specify an equality leads to too much computational power, a notion of name, equipped with an equality, sneaks in a notion of computation -- the very thing the algebraic theory is attempting to give an account of. In this light, even the 'pure' lambda calculus doesn't seem so pure. Of course, the process calculi suffer this critique more severely than lambda does because there are natural name-free accounts of lambda, e.g. SKI, while proposals for name-free accounts of pi are turgid at best and it is unclear whether they extend naturally to variants like ambients. Further, i would argue that SKI loses much of the flavor of lambda and, more importantly, doesn't set up the theory of computation to extend well to other programming notions, like reference and mutability especially in higher-order situations. This may be a matter of taste, more than anything else, but as i argued above, theories of computation are cheap, at this point, and taste and sensibility seems to be the essential differentiating factor amongst them. With this little preamble, let me give you, dear reader, a taste of a treatment of a reflective account of computation that side-steps this little conundrum about names. The presentation below presents a reflective account of lambda that is derived from a reflective account of pi, published in a workshop at ETAPS in 2005. The reason i went back to treat lambda after giving an account of pi is that it turns out that such an account for lambda is a wee bit trickier because lambda is implicitly higher-order while plain vanilla pi is not. An account that gives a lambda calculus emerging just out of term constructors in which there is a kind of alternation of name constructors and program constructors -- a feature whose rationale we will visit at the end of this little note -- turns out to be fairly tightly constrained and therefore may be of some interest to this community. So, without further ado, here's the syntax:
Two things to note about this grammar immediately: 1. There's a production for names! Names are quoted programs. As usual, we calculate bound occurrences of names recursively, via
Next, we whack this set of terms down by the usual alpha-equivalence plus ^*x^ == x Note, we could have achieved the same effect by moving *x from the production for P into the production for M,N; but, for uniformity (especially with the ETAPS presentation for a reflective pi) it was more natural to leave dequote (a.k.a. drop) among the program ctors -- because it is one. Before giving the operational semantics, let me also point out the relationship between L -- another departure from the standard presentation of lambda -- and quotation. It turns out to get names to emerge just out of quoted programs you have to have a base, atomic program. In pi this is straightforward, it's the null process, 0. In lambda the choice of the base program turns out to be somewhat interesting; but, apart from it's dynamics, you have to have one and L is our base, atomic program. It's the first or ur-program. From the first program one can form the first name, ^L^. With this name one can form the first abstraction, λ^L^.L . With this one can form another name ^λ^L^.L^, evidently distinct from ^L^ and you're off to the races. You've got -- at least -- the terms of a lambda calculus where the variables are a bit funny, but no funnier than deBruijn numbers, to my taste, anyway. Equipped with a set of (equivalence classes of) terms over which to compute, lets' write down the operational semantics. We have the usual beta reduction (λx.M)N -> M[N/x] but with a catch M[N/x] denotes semantic substitution, which we give now. x[N/x] := N all bog standard, so far, but now we get to the fresh tofu *x[N/x] := *x (N not a name, i.e. of the form ^M^) The upshot of these rules is that a dropped name is a place-holder to drop in a program frozen in a name. This is not terribly magical in lambda -- which is already higher-order -- but it is very powerful in pi and ultimately gives rise to a mechanism for interpreting the fresh name generator. Ok, so we've got beta-reduction sorted, but we also have other terms, in particular, L, that have to be given semantics. It turns out there are a lot of possibilities for the dynamics of L, but here is one that seems very natural: it's a lambda constructor. I.e., L^M^N -> λ^M^.N Note that some care must be exercised here. If we were to have the rule LMN -> λ^M^.N then because names are terms -- lambda is implicitly higher-order -- you could form L^M^N which would reduce to λ^^M^^.N defeating the strict alternation of name constructors and program constructors. Finally, we add a minimal context rule M -> M' => MN -> M'N which makes our calculus reasonably lazy. So, this gives you a calculus into which you can embed the lambda calculus (built over the name set of your choice) by the obvious translation scheme. But, this calculus is pure. It doesn't demand its user to pony up a set of names. It's a complete theory in and of itself. A notion of name equality can be built, recursively, using the notions of computational equality and straightforward syntactic equality of the finite set of term constructors. Another perspective on these same statements is that we have a 'machine code'. Expressions in this calculus are completely closed with no need for dereferencing of symbols. It is name-free, like SKI, and could be used to build a different sort of virtual machine that is in many ways like the categorical abstract machine, but still retains much of traditional stack machine shape. But there is another intriguing possibility. First, i leave it as an exercise to the reader to write down an encoding of this calculus into binary. But, here's an open question: is there an arithmetic formula that corresponds to the reduction rule? More formally, is there a binary encoding B : M -> {0,1}* and a function R : {0,1}* x {0,1}* -> {0,1}* s.t. R(B(M),B(N)) = B(D) whenever MN ->* D and D doesn't reduce? If such a function did exist it might be the basis for a really, really fast implementation of lambda. Finally, let me point out an intriguing connection with games semantics that gives some support for the alternation of name constructor and program constructor as desiderata. i discovered this when thinking about adding quotation to set theory. The basic idea is that you can interpret program constructor as question and name constructor as answer and role of player versus opponent as the dividing line between program and environment. It's these connections and questions, apart from any real affection for 'purity', that make an account of this shape interesting to me and i hope to others as well. By Lucius Gregory Meredith at 2006-12-23 01:55 | LtU Forum | previous forum topic | next forum topic | other blogs | 11064 reads
|
Browse archives
Active forum topics |
Recent comments
20 weeks 6 days ago
20 weeks 6 days ago
20 weeks 6 days ago
43 weeks 18 hours ago
47 weeks 2 days ago
48 weeks 6 days ago
48 weeks 6 days ago
51 weeks 4 days ago
1 year 4 weeks ago
1 year 4 weeks ago