The Lambda Calculus and Its Racket Implementation

The lambda calculus (also written as λ-calculus) is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. The calculus is a universal machine: a model of computation that can be used to simulate any Turing machine. Alonzo Church introduced it in the 1930s as part of his research into the foundations of mathematics. Racket implements it directly: lambda is the abstraction, and (f a) is the application.

1. Overview

A lambda term is a variable, an abstraction, or an application. Its syntax is given by the grammar

where variables range over an infinite set of names. A term is valid when it can be obtained by repeated application of those three rules. Since the calculus has no store and no machine state, computation is substitution. Racket writes a variable as an identifier, and the three forms below map onto lambda and on the application form (f a).

Abstraction. The term \(\lambda x.\, M\) is the function of one parameter \(x\) with body \(M\). The dot separates the parameter from the body, and the body extends to the right until a parenthesis closes it, so \(\lambda x.\, \lambda y.\, x\) means \(\lambda x.\, (\lambda y.\, x)\). An abstraction is a value: it has no name, and it can be created where it is needed, passed as an argument, and returned as a result. Racket’s lambda is the same form, and the identity function is written in both notations as follows.

(define identity (lambda (x) x))
(identity 'a)   ; => 'a

Application. The term \(M\, N\) applies the operator \(M\) to the operand \(N\). Application associates to the left, so \(M\, N\, P\) means \((M\, N)\, P\), and the operator position may hold any term, including another application. Racket writes application as a parenthesized list whose first element is the operator; the core form is #%app.

(define K (lambda (x) (lambda (y) x)))
((K 'kept) 'ignored)   ; => 'kept

Currying. An abstraction binds exactly one parameter, so a function of two parameters is a nest of abstractions: the function \(x \mapsto y \mapsto x^{2} + y^{2}\) returns a function of \(y\), and the second application supplies \(y\). That transformation is currying, and it is why one-parameter abstraction suffices for any number of inputs. The uncurried function of the pair \((5, 2)\) and the curried version both yield 29; the curried one takes two β-reduction steps.

(define curried-add (lambda (x) (lambda (y) (+ x y))))
((curried-add 4) 9)   ; => 13

Free and bound variables. An occurrence of \(x\) is free when no enclosing abstraction binds it, and bound when it lies in the body of an enclosing \(\lambda x\). In \(\lambda x.\, x\, y\) the occurrence of \(x\) is bound and \(y\) is free. The free variables of a term are defined by induction, which makes the informal account precise:

A term with no free variables is closed, and a closed term denotes a function of its arguments and nothing else. Racket resolves the same distinction when a program is expanded: a free identifier is looked up in the enclosing scope, and one with no binding at all is an error.

(define y 10)
(define add-y (lambda (x) (+ x y)))
(add-y 1)                  ; => 11
(let ([y 100]) (add-y 1))  ; => 11, the free y is the outer one

Substitution. The notation \(M[x := N]\) replaces every free occurrence of \(x\) in \(M\) by \(N\), and it is defined by cases over the structure of \(M\). A variable is replaced when its name matches, so \(x[x := N] = N\) and \(y[x := N] = y\) for \(y \neq x\). An application distributes the substitution to both subterms, so \((M_1\, M_2)[x := N] = (M_1[x := N])\, (M_2[x := N])\). An abstraction whose binder is \(x\) is unchanged, since the inner binder hides the outer \(x\); an abstraction whose binder \(y\) is distinct becomes \(\lambda y.\, (M[x := N])\), except that when \(y \in \mathrm{FV}(N)\) the binder is renamed first. Substitution is the only operation that computes, which is why it is defined so carefully.

α-conversion. The name chosen for a bound variable does not matter. If \(y \notin \mathrm{FV}(M)\), then \(\lambda x.\, M\) and \(\lambda y.\, M[x := y]\) are α-equivalent, written \(\lambda x.\, M \equiv_{\alpha} \lambda y.\, M[x := y]\), and the relation is the smallest congruence generated by that rule. So (lambda (x) x) and (lambda (z) z) denote the same function. α-renaming is a property of the notation rather than a step a program performs: in Racket the inner parameter is a distinct binding, so no capture arises in the first place. De Bruijn’s 1972 notation makes the equivalence syntactic by writing a variable as the number of abstractions between the use and its binder.

(define y 'free)
(define f (lambda (x) (lambda (y) (list x y))))
((f y) 'bound)   ; => '(free bound)

β-reduction. A β-redex is an application of the form \((\lambda x.\, t)\, s\), and β-reduction rewrites it to \(t[x := s]\). The subterm that is rewritten is the redex, and the term it reduces to is its reduct. For example, \((\lambda x.\, x)\, s \rightarrow s\) shows that \(\lambda x.\, x\) is the identity, and \((\lambda x.\, y)\, s \rightarrow y\) shows that \(\lambda x.\, y\) is the constant function returning \(y\). Racket evaluates a redex by entering the body with the parameter bound to the evaluated operand, which is the machine counterpart of the same substitution.

((lambda (x) (+ x 1)) 41)   ; => 42

β-normal form. A term with no β-redex is a β-normal form, and it is unique when it exists: by the Church-Rosser theorem, any two reduction sequences that terminate from the same term produce the same normal form, up to α-conversion. The untyped calculus is nevertheless neither strongly nor weakly normalising, because there are terms with no normal form at all. The smallest is \(\Omega = \omega\, \omega\), where \(\omega = \lambda x.\, x\, x\): one reduction substitutes \(\omega\) for \(x\) and returns \(\Omega\) again. A Racket binding evaluates its right-hand side, so the cycle is written under a lambda and diverges only when it is called.

(define (omega) ((lambda (x) (x x)) (lambda (x) (x x))))

η-conversion. The rule \(\lambda x.\, f\, x \rightarrow f\), valid when \(x\) is not free in \(f\), expresses extensionality: two functions are the same when they agree on every argument. It is a conversion rather than a reduction rule for computation, and Racket leaves (lambda (x) (f x)) as a procedure instead of replacing it by f. The term is a β-normal form and is η-equivalent to f.

Evaluation order. β-reduction says a redex may be contracted; it does not say which one to contract first. That choice is the evaluation strategy, and every strategy answers two questions.

1. Is the argument reduced before it is passed? Yes means the argument is evaluated at the call site. No means it is passed as a computation and evaluated by the body, only if and when the body uses it.
2. Is the body of an abstraction reduced before the abstraction is called? Yes reduces under the binder. No stops at the binder, and the term is only evaluated when it is applied to an argument.

The four common strategies are the four combinations of those answers.

Normal order passes the argument as a computation, and it reduces the body of an abstraction before the abstraction is called. Because the argument is passed unevaluated, the body decides whether to evaluate it, which is why (lambda (x) (lambda (y) y)) applied to \(\Omega\) returns \(\lambda y.\, y\). Because it reduces under the binder, it reaches a full β-normal form whenever one exists.

#lang lazy
(define (const-first x) (lambda (y) x))
(define (omega) ((lambda (x) (x x)) (lambda (x) (x x))))
((const-first 'kept) (omega))   ; => 'kept, the argument is never evaluated

Call by name is normal order without reduction under the binder. Everything outside an abstraction is reduced exactly as normal order reduces it; the body of an abstraction is not touched until the abstraction is applied.

That single difference is visible on one term: \(\lambda x.\, \Omega\). Normal order reduces the body, so it starts the cycle of \(\Omega\) and never returns. Call by name stops at the binder, so it returns the abstraction with the cycle still inside it, and the cycle only begins if someone applies that abstraction.

(define (omega) ((lambda (x) (x x)) (lambda (x) (x x))))

;; call by name: the body is not reduced, so this returns a procedure
(define by-name (lambda (x) (omega)))
(procedure? by-name)   ; => #t

The same term under normal order is written by forcing the body first, and it does not return:

(define (omega) ((lambda (x) (x x)) (lambda (x) (x x))))
(define by-normal-order (let ([body (omega)]) (lambda (x) body)))   ; does not return

The two consequences follow from the same rule. An argument that is passed as a computation is evaluated only when the body uses it, so an unused argument never runs, and an argument used twice runs twice because nothing is shared. The counter below shows both:

(define calls 0)
(define (tick) (set! calls (add1 calls)) 'v)

(define (ignore th) 'done)
(ignore (lambda () (tick)))   ; => 'done
calls                         ; => 0, the argument never ran

(define (twice th) (list (th) (th)))
(twice (lambda () (tick)))    ; => '(v v)
calls                         ; => 2, once per use, not once per call

Applicative order evaluates the argument at the call site, and it reduces the body of an abstraction before the abstraction is called. Because the argument is evaluated first, a divergent argument is evaluated even when the body would drop it, so this strategy can fail on a term that has a normal form.

(define log '())
(define (note tag v) (set! log (cons tag log)) v)
(define (ignore y) 'done)

(ignore (note 'arg 1))            ; => 'done
(reverse log)                     ; => '(arg), the argument ran before the body

Call by value is applicative order without reduction under the binder. The argument is evaluated at the call site, so an argument the body never uses is still evaluated, and a used argument is evaluated once. The result of a call is a value: a procedure or a datum in Racket. This is the rule of Racket, Scheme, Standard ML, and OCaml. Racket evaluates the operator, then the operands from left to right, and then enters the body; only special forms such as if, cond, and lambda decide for themselves which subexpressions to evaluate.

(define (say tag v) (displayln tag) v)
(list (say 'first 1) (say 'second 2) (say 'third 3))   ; prints first, second, third

(define (const-first x y) x)
(const-first 'kept (error "operand evaluated"))        ; raises the error

Call by need is call by name that remembers the first result. The argument is passed as a computation, as in call by name, but once the body demands it the value is stored and later uses read that value. An unused argument is still never evaluated; a used argument is evaluated once. Haskell’s non-strict functions use this strategy, and so does #lang lazy.

(define count 0)
(define p (delay (begin (set! count (add1 count)) 1)))
(+ (force p) (force p))   ; => 2
count                     ; => 1, evaluated once and then shared

Separating the four. Each of the two questions above halves the four strategies, so two test terms together identify which one is in use. The first term has a diverging argument that the body discards, which tests whether the argument is reduced first. The second term holds a redex inside the body of an abstraction, which tests whether reduction goes under a binder.

The first column separates the strategies that evaluate the argument first from those that pass it as a computation. The second separates the strategies that reduce under a binder from those that stop at it. The four rows are therefore all different, and each row states which combination of the two answers it implements.

Full β-reduction is not a strategy but the relation itself: any redex may be contracted at any time. It matters for the confluence result, which says that any two complete sequences end at the same β-normal form, while the strategies above govern which of those sequences a concrete evaluator follows.

(define (square x) (* x x))
(+ (square 2) (square 3))   ; => 13, whichever redex is contracted first

Call-by-value fixed point. Because call by value reduces the operand first, the combinator \(Y = \lambda g.\, (\lambda x.\, g\, (x\, x))\, (\lambda x.\, g\, (x\, x))\) diverges: its argument is a self-application. The repair is the combinator \(Z\), which delays that self-application under an extra abstraction, an η-expansion of \(x\, x\):

(define Z
  (lambda (g)
    ((lambda (x) (g (lambda (v) ((x x) v))))
     (lambda (x) (g (lambda (v) ((x x) v)))))))

Section 3 develops the fixed-point equation, the reduction that establishes it, and the use of \(Y\) and \(Z\) to define factorial, summation, and Fibonacci.

Typing. A type discipline changes which terms are admitted. The calculus may be untyped or typed, and the typed calculi are strictly weaker in what they can express. In the simply typed lambda calculus the self-application \(x\, x\) has no type, because the operator would have to be a function that accepts itself, so the fixed-point combinator cannot be expressed and general recursion is added as a primitive. Every reduction sequence of a simply typed term is finite, whereas an untyped reduction sequence may be infinite. Typed Racket applies the same restriction to Racket, rejecting the self-application with a type error.

2. Encoding data

The calculus has no data. Booleans, numerals, and pairs are encoded by the way a term uses its arguments. Because functions are first-class values, a datum can be represented as a function that selects or iterates, and the encodings below are the standard ones.

The Church Booleans are the two selectors:

The encoding is not an arbitrary trick. It follows from one specification, the meaning a conditional must have: an expression that chooses between a then-branch and an else-branch returns the then-branch when the condition is true and the else-branch when it is false. In the calculus the only way to choose between two things is to be applied to them, so the condition must be a term that takes the two branches as arguments and returns one of them. TRUE returns the first, and FALSE returns the second. That requirement determines both constants, and it also determines the conditional itself: applying the condition to the two branches is the conditional, so no if operator is needed.

The connectives then follow by reading each one as a conditional. NOT \(p\) is “if \(p\) then FALSE else TRUE”, which is \(p\) applied to FALSE and TRUE. AND \(p\, q\) is “if \(p\) then \(q\) else FALSE”, which is \(p\) applied to \(q\) and FALSE. OR \(p\, q\) is “if \(p\) then TRUE else \(q\)”.

The shorthand forms in the table above replace the constant in the unused branch by \(p\) itself. In AND \(p\, q\), the else branch is reached only when \(p\) is false, so any false term serves there, and \(p\) is false at that point; writing \(p\) instead of FALSE gives \(p\, q\, p\). In OR \(p\, q\), the then branch is reached only when \(p\) is true, so any true term serves, and \(p\) is true there; writing \(p\) gives \(p\, p\, q\). The substitutions are valid and shorter, which is why the standard forms use them.

(define ctrue (lambda (x) (lambda (y) x)))
(define cfalse (lambda (x) (lambda (y) y)))

(define (cif p) (lambda (a) (lambda (b) ((p a) b))))
(define (cnot p) ((p cfalse) ctrue))
(define (cand-by-if p q) ((p q) cfalse))
(define (cor-by-if p q) ((p ctrue) q))
(define (cand p) (lambda (q) ((p q) p)))
(define (cor p) (lambda (q) ((p p) q)))
(define (to-bool b) ((b #t) #f))

AND TRUE FALSE reduces to TRUE FALSE TRUE and then to FALSE. Every branch of that reduction is a β-step on a term, and the value of the encoding is that the table of connectives follows from the selectors alone.

A pair encapsulates two values as an abstraction that expects a handler. PAIR applies the handler to both components, and the selectors supply a handler that keeps one of them:

(define (pair x) (lambda (y) (lambda (sel) ((sel x) y))))
(define (pfirst p) (p (lambda (x) (lambda (y) x))))
(define (psecond p) (p (lambda (x) (lambda (y) y))))

(define pair1 ((pair 'a) 'b))
(pfirst pair1)    ; => 'a
(psecond pair1)   ; => 'b

A linked list is either the empty list or a pair of an element and a smaller list, so the pair encoding already carries the structure of a list.

A Church numeral is a higher-order function. It takes a function \(f\) and returns the \(n\)-th composition of \(f\):

Repeated composition obeys two laws of exponents, \(f^{(m)} \circ f^{(n)} = f^{(m+n)}\) and \((f^{(n)})^{(m)} = f^{(m \cdot n)}\), and those laws are why the numerals can do arithmetic:

(define zero (lambda (f) (lambda (x) x)))
(define (succ n) (lambda (f) (lambda (x) (f ((n f) x)))))
(define (plus m) (lambda (n) (lambda (f) (lambda (x) ((m f) ((n f) x))))))
(define (mult m) (lambda (n) (lambda (f) (m (n f)))))
(define (pow b) (lambda (n) (n b)))

(define (church->int n) ((n add1) 0))
(define (int->church k)
  (if (zero? k) zero (succ (int->church (sub1 k)))))

The numeral two is written as two applications of succ to zero, not as a pre-written tower. church->int applies the numeral to add1 and to 0, and the Racket procedure supplies both the iteration and the arithmetic.

The predecessor is the involved case. It is specified by two equations, \(\mathrm{PRED}\, (\mathrm{SUCC}\, n) = n\) and \(\mathrm{PRED}\, 0 = 0\), and the standard term uses the shifting function \(T = \lambda g.\, \lambda h.\, h\, (g\, f)\):

(define (pred n)
  (lambda (f)
    (lambda (x)
      (((n (lambda (g) (lambda (h) (h (g f))))) (lambda (u) x))
       (lambda (u) u)))))
(define (iszero n) ((n (lambda (_) cfalse)) ctrue))

(define two (int->church 2))
(define three (int->church 3))

iszero and pred reuse ctrue and cfalse from the Boolean definitions above.

Predecessor of zero is zero. The term threads the shifting function through the iterator; on zero that function is never applied, and the result is the numeral zero. The zero test is the most fundamental predicate: it applies the numeral to a function that discards its argument and returns FALSE, with TRUE as the base case, so a numeral of zero applications returns TRUE.

3. Recursion and the Y combinator

Recursion is the ingredient that completes the calculus. Without it, terms express only what a fixed finite tower of abstraction and application can write down; with it, they express every function that a Turing machine computes, because a loop in the machine becomes a recursive definition in the calculus. The fixed-point combinator supplies recursion without adding a recursive binding to the language.

The pure calculus has no names for terms. A variable refers to a parameter of an enclosing abstraction and to nothing else, so an abstraction cannot mention itself. A recursive definition such as \(F(n) = n \times F(n-1)\) therefore has no direct term: the body would have to contain the term that is being defined, which would make the term infinitely large. The calculus recovers recursion by passing a function to itself.

Start from the functional that closes over the recursive call as a parameter \(r\):

If \(r\) were \(F\), then \(G\, F\) would also be \(F\), since \(G\, F\) is the function that multiplies \(n\) by \(F(n-1)\). The equation \(F = G\, F\) says that \(F\) is a fixed point of \(G\). A fixed-point combinator is a term \(Y\) that produces such a fixed point for any functional: it satisfies

so \(Y\, G\) is the recursive function, and every occurrence of \(r\) in the body of \(G\) becomes a call to \(Y\, G\) again. The standard term is

The self-application \(x\, x\) is what supplies the term to itself. Reducing \(Y\, G\) shows how it works:

The reduction ends at \(G\, (Y\, G)\), which is what the equation requires: the argument that \(G\) receives is again the whole fixed point. The term therefore has no normal form in the strict sense, and the recursion unfolds one step at a time as the body demands it.

Self-application without a combinator. A single recursive function can be written without a combinator by performing the self-application at the definition site. The term \(E\) receives itself as its first argument, and each recursive call becomes \(s\, s\):

(define (fact-self-application n)
  ((lambda (self) (self self n))
   (lambda (self k) (if (zero? k) 1 (* k (self self (sub1 k)))))))

(fact-self-application 5)   ; => 120

The difference from \(Y\) is that the rewrite is repeated by hand at every call site. \(Y\) performs it once, at the moment the fixed point is built, so the body of \(G\) needs no self-application.

\(Y\) under non-strict evaluation. Under normal order, \(Y\) works as written, because the operand \((x\, x)\) is substituted before it is reduced and the body of \(g\) decides when it is needed. #lang lazy implements that behavior, and the three classic recursive functions follow from their functionals without any change to the combinator:

#lang lazy
(define Y (lambda (g) ((lambda (x) (g (x x))) (lambda (x) (g (x x))))))

(define fact-gen (lambda (self) (lambda (n) (if (= n 0) 1 (* n (self (- n 1)))))))
(define sum-gen  (lambda (self) (lambda (n) (if (= n 0) 0 (+ n (self (- n 1)))))))
(define fib-gen  (lambda (self) (lambda (n) (if (< n 2) n (+ (self (- n 1)) (self (- n 2)))))))

((Y fact-gen) 5)    ; => 120
((Y sum-gen) 10)    ; => 55
((Y fib-gen) 10)    ; => 55

Each functional receives its own fixed point as self, so (self k) is a call to the function being defined. The fixed-point equation holds as an identity on the two terms: Y g and g (Y g) give the same results on every input.

#lang lazy
(define Y (lambda (g) ((lambda (x) (g (x x))) (lambda (x) (g (x x))))))
(define g (lambda (self) (lambda (n) n)))
(equal? (map (Y g) '(0 1 2)) (map (g (Y g)) '(0 1 2)))   ; => #t

\(Y\) under call by value. Racket’s default language evaluates the operand first, so the argument \((x\, x)\) is reduced before it is passed to \(g\), and that reduction reproduces the same argument indefinitely. The definition of fact as (Y fact-gen) does not terminate under #lang racket.

The repair is to delay the self-application behind an abstraction. The combinator \(Z\) passes \(g\) a function that performs the self-application only when it is called:

The inner \(\lambda v.\, x\, x\, v\) is an η-expansion of \(x\, x\): an abstraction whose body applies \(x\) to \(x\) and then applies the result to \(v\). Since an abstraction is a value, the argument of \(g\) is a value, and \(g\) can be entered before the recursion is unfolded. The recursive call then happens when \(v\) is supplied.

(define Z
  (lambda (g)
    ((lambda (x) (g (lambda (v) ((x x) v))))
     (lambda (x) (g (lambda (v) ((x x) v)))))))

(define fact-gen (lambda (self) (lambda (n) (if (= n 0) 1 (* n (self (- n 1)))))))
(define sum-gen  (lambda (self) (lambda (n) (if (= n 0) 0 (+ n (self (- n 1)))))))
(define fib-gen  (lambda (self) (lambda (n) (if (< n 2) n (+ (self (- n 1)) (self (- n 2)))))))

(map (Z fact-gen) '(0 1 2 3 4 5))     ; => '(1 1 2 6 24 120)
((Z sum-gen) 100)                     ; => 5050
(map (Z fib-gen) '(0 1 2 3 4 5 6 7 8 9 10))   ; => '(0 1 1 2 3 5 8 13 21 34 55)

The functionals are identical to the ones used with \(Y\) under #lang lazy. Only the combinator changes, because only the evaluation order changes.

What a language provides instead. A Racket definition needs no combinator, because the binding is in scope in the body and the name refers to the procedure being defined:

(define (fact n) (if (zero? n) 1 (* n (fact (sub1 n)))))
(fact 5)   ; => 120

All three forms compute the same function. The difference is where the recursion lives: in a hand-written self-application, in a term that rebuilds itself through \(Y\) or \(Z\), or in a binding that the language creates before the body runs. define is the language’s answer to the fixed-point combinator, and Racket’s internal definitions are specified to behave as if the bound names were in scope throughout the body.

The distinction is visible in the surface forms. A let binding is not in scope in its own right-hand side, which is exactly the restriction that makes the non-recursive let an application of an abstraction. A module that refers to the name there does not compile:

(let ([f (lambda (k) (f k))]) (f 1))   ; f: unbound identifier

letrec extends the scope to the right-hand sides, which is what a recursive definition needs, and it is the direct analogue of \(Z\): the binding exists before any right-hand side is evaluated.

(letrec ([f (lambda (k) (if (zero? k) 1 (* k (f (sub1 k)))))]) (f 5))   ; => 120

4. Combinators and abstraction elimination

Certain terms have commonly accepted names. They are closed terms, and they form a notation in which variables are eliminated entirely.

\(S K K\) reduces to the identity. Expanding gives \((K\, z)\, (K\, z)\), and \(K\, z\) is the constant function that returns \(z\), so the whole term returns \(z\).

(define I (lambda (x) x))
(define K (lambda (x) (lambda (y) x)))
(define S (lambda (x) (lambda (y) (lambda (z) ((x z) (y z))))))
(define B (lambda (x) (lambda (y) (lambda (z) (x (y z))))))
(define C (lambda (x) (lambda (y) (lambda (z) ((x z) y)))))
(define W (lambda (x) (lambda (y) ((x y) y))))

(((S K) K) 'a)       ; => 'a
(((B I) I) 'b)       ; => 'b
(((C K) 'c) 'k)      ; => 'k
((W K) 'ignored)     ; => 'ignored

\(S\) and \(K\) together form a complete basis: every lambda term is equivalent to a term built from \(S\) and \(K\) alone, applied to each other, with no variables. \(B\), \(C\), \(K\), and \(W\) form an alternative basis. The construction is abstraction elimination: a term \(N\) without abstractions is transformed into a term \(T(x, N)\) equivalent to \(\lambda x.\, N\), by three rules.

A term \(T(x, N)\, P\) then reduces by having \(I\), \(K\), or \(S\) take the argument \(P\), exactly as the β-reduction of \((\lambda x.\, N)\, P\) would. \(I\) returns \(P\), \(K\, N\) discards it, and \(S\) passes it to both subterms. Adding the rule \(T(x,\, N\, x) = N\) when \(x\) is not free in \(N\) expresses η-conversion, since \((\lambda x.\, N\, x)\, P\) and \(N\, P\) agree.

Combinatory logic is the notation that results: a system of terms built from \(S\) and \(K\) with application, no variables, and no substitution rule beyond the reductions of the combinators themselves. It is equivalent in power to the lambda calculus, which is why the calculus can be presented without variables at all.

5. Closures and execution frames

The calculus substitutes an argument into the body of an abstraction, so the body is evaluated with the parameter replaced by the argument term. A Racket program does not rewrite its body; it records the parameter’s value in an environment, and it records where evaluation is to continue. A closure and an execution frame are the two structures that carry out the substitution rule at run time.

The substitution model. For a closed application, the two accounts agree. Applying \((\lambda x.\, (+ x 1))\) to 41 substitutes 41 for \(x\) in the body and leaves \((+ 41)\), which evaluates to 42. The value of a function in this model is the abstraction itself, and there is no state.

((lambda (x) (+ x 1)) 41)   ; => 42

Closure. An abstraction with a free variable cannot be evaluated by substitution alone, because the free variable has no value inside the term. The value of such an abstraction is a closure: its code (the parameter and body), together with the environment in which the abstraction was evaluated. Applying the closure extends that stored environment with a binding of the parameter, and evaluates the body in the extended environment. The closure’s environment therefore supplies exactly the values that substitution would have copied into the body.

(define (make-adder n) (lambda (x) (+ x n)))
(define add2 (make-adder 2))
(add2 5)   ; => 7

add2 holds a closure whose stored environment binds n to 2. The body of the inner lambda contains the free n, and the closure supplies it at each call. Two calls to make-adder return two closures with the same code and different environments, which is why two of them behave differently:

(define (make-adder n) (lambda (x) (+ x n)))
(define add2 (make-adder 2))
(define add5 (make-adder 5))
(list (add2 1) (add5 1))   ; => '(3 6)

Capture is decided where the closure is created. Because the environment is stored at the abstraction, a free variable takes its value from that environment, not from the environment of the caller. A caller that rebinds the name cannot change what the closure sees, which is the run-time form of the lexical-scope rule that α-conversion protects.

(define x 'outer)
(define (show) x)
(define (shadowed) (define x 'inner) (show))
(shadowed)   ; => 'outer

The stored environment is shared, so a closure can carry state. The environment is a set of locations, not a copy of values, so a closure that assigns its free variable mutates the location that every invocation of that closure reads. The two closures returned by two calls to make-counter hold distinct environments, and each count advances independently.

(define (make-counter)
  (define n 0)
  (lambda () (set! n (add1 n)) n))

(define c1 (make-counter))
(define c2 (make-counter))
(list (c1) (c1) (c2))   ; => '(1 2 1)

State is outside the pure calculus. The substitutions of section 1 cannot observe it, and this is the point at which an environment machine and a substitution machine describe different objects: the substitution machine copies values into a term, while the environment machine names a location that can be assigned.

Execution frame. Evaluating a call needs more than the new bindings: it must also record where the result is to be used. An execution frame holds both parts, the environment for the body and the continuation, the pending computation of the caller. Racket allocates a frame for each active call. Entering the body of a closure pushes a frame that binds the parameters and points to the rest of the expression; returning from the call pops it and hands the value to the continuation.

Frames and the continuation. A frame’s continuation is the rest of the computation in the calculus sense, the term that surrounds the application. A non-tail call keeps the frame alive because its continuation has more work to do; a tail call replaces the current frame, because the continuation of the callee is the continuation of the caller. That is why a loop written as a tail call runs in constant space, while a non-tail recursion of the same depth builds a frame per level. Racket requires tail calls to be safe for space in this sense.

(define (loop n) (if (zero? n) 'done (loop (sub1 n))))
(loop 1000000)   ; => 'done, in constant space

call/cc reifies a frame’s continuation. The continuation of a call is usually implicit in the frame. call/cc captures it as an ordinary procedure, so the rest of the computation becomes a value that the program can call, store, or discard.

(define (safe-div a b)
  (call/cc (lambda (escape) (if (zero? b) (escape 'undefined) (/ a b)))))
(safe-div 6 0)   ; => 'undefined

Recursive frames. A recursive definition needs a frame in which the name is already bound. letrec creates one environment for all the right-hand sides and evaluates each in it, which is what the extra abstraction in \(Z\) achieves inside a pure term: the recursive value exists before it is applied.

(letrec ([fact (lambda (n) (if (zero? n) 1 (* n (fact (sub1 n)))))])
  (fact 5))   ; => 120

Deferred evaluation. A frame is also the device that postpones work. A thunk is a nullary closure whose body is evaluated when the thunk is called, so an argument can be passed as a frame rather than as a value. #lang lazy uses this to evaluate an argument only when the body demands it, which is the non-strict rule from section 1.

#lang lazy
(define (const-first x) (lambda (y) x))
(define (omega) ((lambda (x) (x x)) (lambda (x) (x x))))
((const-first 'kept) (omega))   ; => 'kept

Effects and mutable state sit outside the calculus. Substitution of a term that prints or writes a cell can observe which redex was contracted, and the confluence of the pure calculus does not extend unchanged to a language with assignment.

6. References

• Structure and Interpretation of Computer Programs — Harold Abelson and Gerald Jay Sussman, with Julie Sussman. 2nd ed. MIT Press, 1996.
• The Little Schemer — Daniel P. Friedman and Matthias Felleisen. 4th ed. MIT Press, 1996.