These web pages provide a practical introduction to lambda reduction, with a few pointers to more esoteric issues. I'm a linguist, and I have linguists in mind for my audience, so linguistic issues will be emphasized (e.g., a discussion of the interaction of lambda with other binding operators such as "exists" and "forall").
Goal: Church's -calculus provides a convenient way of representing meanings, whether meanings of programs or of expressions in English or some other natural language. As a result, it is ubiquitous in computer science, logic, and formal approaches to the semantics of natural language. The -calculus consists of two things: a formal language and an associated notion of REDUCTION (roughly equivalent to "computation"). In the context of the lambda calculus, reduction is specifically called -reduction. What these pages will attempt to do is teach you how to perform -reduction accurately and confidently.
Other sources: I recommend Hankin's Lambda Calculi : A Guide for Computer Scientists (Oxford) for a readable survey, and Barendregt's The Lambda Calculus (Elsevier) for a more complete reference work. Barendregt and Barendsen's shorter introduction to the lambda calculus is also excellent, and accessible electronically for free (if the citeseer link ceases to work, I've cached a copy here; note for some mysterious reason pages 2, 3 and 4 are blank). Selinger has an excellent set of lecture notes covering many logical and computational aspects of the lambda calculus here. For a more linguistic perspective, chapter 2 of Carpenter's Type-Logical Semantics (MIT Press) presents a -calculus within a framework for describing natural language. The following is too fun not to mention: David Keenan, To dissect a mockingbird: a graphical notation for the lambda calculus with animated reduction .
Acknowledgements: Saber Ben Salem made a number of helpful suggestions.
is a binding operator, just like backwards E ("∃") or upside down A ("∀"). Consequently, it always binds something (a variable), taking scope over some expression that (usually) contains occurrences of the bound variable. More practically, always occurs in the following configuration:
Freedom is always relative to a particular expression. If the preceding expression is embedded within a larger one, the free variables can come to be bound:
The key notion of the -calculus is that it is possible to arrive at a logically equivalent expression by means of a process called -reduction. In the usual case, -reduction is actually a combination of three distinct reduction operations, each of which is discussed below. The key operation, the one that does the heavy lifting, is called -reduction, and that is operation we will discuss first.
By the way, some people say "-conversion" instead of -reduction; others reserve "-conversion" to refer specifically to a single step in a series of reductions. This tutorial is trying not to be overly pedantic, so for present purposes I don't care.
Nothing happens until a -binding form occurs in construction with an argument, thus:
The main idea of -reduction is to replace every free occurrence of the variable "var" in "body" with "argument". For instance, in the form below, both occurrences of "var" in the body are free.
Unfortunately, applying -reduction indiscriminately can cause trouble when the body contains binding operators. Consider:
But consider what happens in this closely parallel but slightly different situation:
|(( x ( y (x y))) y)||-reduction: substitute "y" in for "x" in the body "( y (x y))" ==>|
|( y (y y))|
The solution is to make use of alphabetic variants. Roughly, two expressions are "alphabetic variants" if they are identical except perhaps for the choice of variable symbols. For instance, the following expressions are alphabetic variants of one another:
Some examples of alphabetic variants:
|1.||(( x x) x)||-reduction on "( x x)", substituting "y1" for "x" ==>|
|(( y1 y1) x)||2.||(( x x)( x (x x)))||-reduction on "( x x)", substituting "y1" for "x" ==>|
|(( y1 y1)( x (x x)))|
|3.||( x ( x (x x)))||-reduction on "( x ( x (x x)))", substituting "y1" for "x" ==>|
|( y1 ( x (x x)))|
The third example may look surprising; the key fact is that -reduction specifically targets only free occurrences of the variable in question (free relative to the body). Since the second binds the last two occurrences of "x", performing -reduction on the larger form won't touch them.
Now, back to the original problem. The way to deal with "(( x ( y (x y))) y)", then, is to first take an alphabetic variant. Because alphabetic variants are guaranteed to be logically equivalent, we can substitute variants in place of the original sub expressions. If we do this cleverly, the "y" and the "z"'s don't interact in the pernicious manner shown above.
|1.||(( x ( y (x y))) y)||-reduction on "( y (x y))", substituting "y1" for "y" ==>|
|2.||(( x ( y1 (x y1))) y)||-reduction, substituting "y" for "x" ==>|
|3.||( y1 (y y1))|
Equivalent steps are taken automatically by the -reduction program:
It usually takes some practice to know when it is necessary to use an alphabetic variant. The safest strategy is to automatically apply -reduction to every binding operator before each application of -reduction. See if you can work out the right result for this form before clicking on the "Reduce" button; you will need three applications of -reduction and at least one application of -reduction:
(Warning:) I have modified the characterization of -reduction and of -reduction somewhat in the interests of simplicity. The simplified versions are perfectly sound, and provide the full expressive power of the -calculus. If you're interested in the traditional elaboration, consult either the Hankin book or Berendregt book mentioned above.
-reduction says that an expression of the form "( x (P x))" is guaranteed to be equivalent to "P" alone, where "P" is any expression (in which x does not occur free). This equivalence is obvious enough, but -reduction and -reduction alone do not guarantee it. However, few practical applications of -reduction bother to implement -reduction. In particular, the programs given on this page do not:
Some examples (try to guess the result before clicking):
Some more linguistically-related practice. Once again, try writing
down the anticipated result before clicking "Reduce":
Now for something a little more difficult. Find an expression that you can use to replace "X" so that the result is "(John sleeps)" (you will have to type it into the input window in place of "X" to try it):
Here's a harder problem: If the input is "((D man) sleep)", and the result is "(∃ x ((man x) & (sleep x)))", what is "D"? (Hint: the answer is an approximation of the meaning of the determiner "some", as in "Some man sleeps". The symbol "∃" is supposed to show up as a backwards E, and is usually read "there exists"; in any case, the program expects you to type it in to the window as the symbol "exists".)
It takes some practice to match up 's with the correct argument. Does the following form evaluate to "(2 3)" or "(3 2)"?
In fact, when a form contains more than one that can be reduced, it does not matter which one is reduced first, the result will be the same. (This is known as the Church-Rosser property, or, informally, as the diamond property---see Hankin or Berendregt for lengthy discussion.) For instance, for the last example, we could either apply -reduction to the innermost first, thus:
|(( x (( y (x y)) 2)) 3)||-reduction on "(( y (x y)) 2)", substituting "2" for "y" in the body "(x y)" ==>|
|(( x (x 2)) 3)||-reduction, substituting "3" for "x" in the body "(x 2)" ==>|
|(( x (( y (x y)) 2)) 3)||-reduction on "(( x (( y (x y)) 2)) 3)", substituting "3" for "x" in the body "(( y (x y)) 2)" ==>|
|(( y (3 y)) 2)||-reduction, substituting "2" for "y" in the body "(3 y)" ==>|
That is, when the reduction converges at all---some expressions can't be simplified (e.g., "(( x (x x))( x (x x)))", which reduces to itself, or more pathological examples, such as this (DON'T CLICK ON "REDUCE"!):
I have been writing predicates and their arguments inside parentheses, thus: "(pred arg)". Often in logic and linguistics, such an expression would be written "pred(arg)", for instance, "f(x)" (as in "f(x) = y"). I have chosen the first, more LISP-like notation because it significantly simplifies the design of the program for automating -reduction.
Often, instead of "( x ( y (x y)))", people write " x y . x y". For some reason, these people hate to draw parentheses, and they hate to draw 's. The dot shows where the list of bound variables stops and the (innermost) body begins. Because the scope of the operator(s) is not explicitly marked, sloppy use of this abbreviatory convention often leads to expressions that are ambiguous; this in turn often causes beginners tremendous frustration.
The complexities of -reduction arise from trying to provide a set of syntactic transformations that are guaranteed to preserve meaning. That is, two expressions that are related by some combination of , , and reduction are guaranteed to mean the same thing. In fact, although -reduction is sound, it does not capture the full meaning of the -operator.
A simpler, more direct, and more complete way to understand is to consider its meaning.
The following rule completely characterizes the meaning of the -operator. First, let "[*]^g" mean "the denotation of `*' with respect to the assignment function g", where an assignment function is a function mapping variable symbols onto values, and g[u/v] is that assignment function exactly like g except that it maps the variable v onto the value u.
(define (reduce f) ; 1 ((lambda (value) (if (equal? value f) f (reduce value))) ; 2 (let r ((f f) (g ())) ; 3 (cond ((not (pair? f)) ; 4 (if (null? g) f (if (eq? f (car g)) (cadr g) (r f (caddr g))))) ; 5 ((and (pair? (car f)) (= 2 (length f)) (eq? 'lambda (caar f))) ; 6 (r (caddar f) (list (cadar f) (r (cadr f) g) g))) ; 7 ((and (not (null? g)) (= 3 (length f)) (eq? 'lambda (car f))) ; 8 (cons 'lambda (r (cdr f) (list (cadr f) (delay (cadr f)) g)))) ; 9 (else (map (lambda (x) (r x g)) f)))))) ;10
(reduce '(((lambda x (lambda y (x y))) 2) 3)) ;Value: (2 3) (reduce '((lambda x (lambda y (x y))) 2)) ;Value: (lambda #[promise 2] (2 #[promise 2]))Comments: f is the form to be evaluated, and g is the local assignment function; g has the structure (variable value g2), where g2 contains the rest of the assignments. The named let function r executes one pass through a form. The arguments to r are a form f, and an assignment function g. Line 2: continue to process the form until there are no more conversions left. Line 4 (substitution): If f is atomic [or if it is a promise], check to see if matches any variable in g and if so replace it with the new value. Line 6 (beta reduction): if f has the form ((lambda variable body) argument), it is a lambda form being applied to an argument, so perform lambda conversion. Remember to evaluate the argument too! Line 8 (alpha reduction): if f has the form (lambda variable body), replace the variable and its free occurences in the body with a unique object to prevent accidental variable collision. [In this implementation a unique object is constructed by building a promise. Note that the identity of the original variable can be recovered if you ever care by forcing the promise.] Line 10: recurse down the subparts of f.