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 picalculus  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 namefree accounts of lambda, e.g. SKI, while proposals for namefree 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 higherorder 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 sidesteps 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 higherorder 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 alphaequivalence 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 urprogram. 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 placeholder to drop in a program frozen in a name. This is not terribly magical in lambda  which is already higherorder  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 betareduction 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 higherorder  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 namefree, 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 20061223 01:55  LtU Forum  previous forum topic  next forum topic  other blogs  8874 reads

Browse archivesActive forum topics 
Recent comments
1 week 6 days ago
11 weeks 18 hours ago
11 weeks 3 days ago
12 weeks 6 days ago
12 weeks 6 days ago
13 weeks 9 hours ago
14 weeks 4 days ago
14 weeks 6 days ago
14 weeks 6 days ago
15 weeks 12 hours ago