The untyped lambda calculus has only variables, abstraction, and application. Despite that tiny syntax, it can express data, control, and general computation. Just as importantly for us, it provides a compact setting in which to reason about binding and program transformation precisely.

The central challenge is not arithmetic. It is substitution: replacing a variable while preserving which declarations bind which references.

Learning objectives

After working through this note, you should be able to:

  • parse a lambda-calculus expression using the standard associativity rules;
  • compute the free variables of an expression;
  • determine whether two expressions are alpha-equivalent;
  • perform capture-avoiding substitution;
  • use beta reduction to justify an equational calculation;
  • state the side condition for eta reduction;
  • distinguish an equality in the pure calculus from an evaluation rule in a call-by-value programming language; and
  • implement and test a small reducer in Racket.

Syntax and parsing conventions

Lambda-calculus expressions are generated by:

Expression ::= Variable
             | (lambda (Variable) Expression)
             | (Expression Expression)

On paper, lambda is often written with the Greek letter λ and some parentheses are omitted:

λx. x
λx. λy. x
f x y

Two conventions recover the missing parentheses:

  • application associates to the left, so f x y means ((f x) y); and
  • a lambda body extends as far right as possible, so λx. f x means λx. (f x).

Therefore:

λx. λy. x y z

means:

(lambda (x)
  (lambda (y)
    ((x y) z)))

Application has no built-in notion of “two arguments.” A two-argument function is represented as a function that returns another function.

Free and bound variables

In (lambda (x) body), the declaration of x binds the free references to x in body. A reference is free if no enclosing lambda declares its name.

The free-variable function is defined structurally:

FV(x)             = {x}
FV(M N)           = FV(M) union FV(N)
FV(lambda x. M)   = FV(M) minus {x}

For example:

(lambda (x)
  ((f x) y))

has free variables f and y. The occurrence of x is bound.

Free and bound are properties of occurrences, not names in isolation. In:

(x (lambda (x) x))

the first occurrence of x is free and the last is bound.

Alpha-equivalence

The spelling of a bound variable is not part of a lambda expression’s essential binding structure. These expressions are alpha-equivalent:

(lambda (x)
  (lambda (y)
    (x y)))

(lambda (first)
  (lambda (second)
    (first second)))

But this expression is different:

(lambda (first)
  (lambda (second)
    (second second)))

Alpha-renaming is not an unscoped search-and-replace. The new name must not capture a free reference, and a nested declaration of the old name begins a new binding region.

One reliable test converts bound references to lexical addresses. A bound reference is represented by the number of binders between it and its declaration; a free reference retains its name. Alpha-equivalent terms then have identical addressed forms.

Capture-avoiding substitution

Write M[x := N] for “replace the free occurrences of x in M with N.” The word free is essential.

The easy cases are:

x[x := N] = N
y[x := N] = y                         when y != x
(M1 M2)[x := N] = (M1[x := N] M2[x := N])

At a lambda, three cases matter:

(lambda x. M)[x := N]
  = lambda x. M

(lambda y. M)[x := N]
  = lambda y. M[x := N]
    when y != x and y is not free in N

If y is free in N, descending directly would capture that reference. First alpha-rename y to a genuinely fresh name.

Why naïve substitution is wrong

Consider:

(lambda y. x)[x := y]

Replacing text directly produces lambda y. y. The originally free y has become bound, so the program’s meaning changed. Capture-avoiding substitution instead chooses a fresh name:

(lambda y. x)[x := y]
  =alpha lambda y_0. x
  ->      lambda y_0. y

The resulting y remains free.

Beta reduction

A lambda applied to an argument forms a beta redex:

(lambda x. M) N

Contracting the redex substitutes the argument for the formal parameter:

((lambda x. M) N) ->beta M[x := N]

Example:

((lambda x. (x x)) (lambda z. z))
-> ((lambda z. z) (lambda z. z))
-> lambda z. z

Beta conversion treats the two sides as equal in the pure lambda calculus. Beta reduction directs that equality from the application toward the substituted body, giving us a way to calculate.

A capture-sensitive reduction trace

Reduce:

(((lambda x. lambda y. x) y) z)

The first redex asks for (lambda y. x)[x := y]. Because y is free in the argument, rename the bound y before substituting:

(((lambda x. lambda y. x) y) z)
=alpha (((lambda x. lambda y_0. x) y) z)
->beta ((lambda y_0. y) z)
->beta y

A naïve substitution would have produced (lambda y. y), followed by z. That wrong result is evidence of variable capture.

The binding invariant for substitution is:

Substitution may replace free occurrences, but it must not change which declarations bind any other occurrences.

Eta equivalence

Eta equivalence captures an extensional idea: a function that does nothing but pass its argument to another function behaves like that function.

lambda x. (M x) =eta M       when x is not free in M

The side condition is necessary. Reducing lambda x. (x x) to x would remove the declaration that binds both occurrences and create a free variable.

Eta can also be used in the expanding direction. For example, f can be eta-expanded to lambda x. (f x) when a transformation needs an explicit lambda.

An executable reducer

The program below implements:

  • free-variable and all-name analysis;
  • alpha-equivalence through lexical addresses;
  • deterministic fresh-name generation;
  • capture-avoiding substitution;
  • one leftmost-outermost beta step and normalization with fuel; and
  • top-level eta contraction.

It is intentionally small rather than fast. Its purpose is to make the binding invariants executable.

The argument order follows our course convention:

(substitute replacement target expression)

This computes [target := replacement] expression.

#lang racket

(require racket/set)

(define (free-vars expr)
  (match expr
    [(? symbol? name)
     (set name)]
    [`(lambda (,(? symbol? name)) ,body)
     (set-remove (free-vars body) name)]
    [`(,operator ,operand)
     (set-union (free-vars operator)
                (free-vars operand))]
    [bad-expression
     (error 'free-vars "bad lambda expression: ~v" bad-expression)]))

(define (all-names expr)
  (match expr
    [(? symbol? name)
     (set name)]
    [`(lambda (,(? symbol? name)) ,body)
     (set-add (all-names body) name)]
    [`(,operator ,operand)
     (set-union (all-names operator)
                (all-names operand))]
    [bad-expression
     (error 'all-names "bad lambda expression: ~v" bad-expression)]))

(define (fresh-like base avoid)
  (let loop ([number 0])
    (define candidate
      (string->symbol
       (format "~a_~a" base number)))
    (if (set-member? avoid candidate)
        (loop (add1 number))
        candidate)))

(define (substitute replacement target expression)
  (match expression
    [(? symbol? reference)
     (if (eqv? reference target)
         replacement
         reference)]

    [`(lambda (,(? symbol? parameter)) ,lambda-body)
     (cond
       ;; This inner declaration shadows the name being replaced.
       [(eqv? parameter target)
        expression]

       ;; Descending is safe when the binder cannot capture the replacement.
       [(not (set-member? (free-vars replacement) parameter))
        `(lambda (,parameter)
           ,(substitute replacement target lambda-body))]

       ;; Rename the binder before descending.
       [else
        (define avoid
           (set-add
            (set-union (all-names lambda-body)
                       (all-names replacement))
           target))
        (define fresh
          (fresh-like parameter avoid))
        (define renamed-body
          (substitute fresh parameter lambda-body))
        `(lambda (,fresh)
           ,(substitute replacement target renamed-body))])]

    [`(,operator ,operand)
     `(,(substitute replacement target operator)
       ,(substitute replacement target operand))]

    [bad-expression
     (error 'substitute "bad lambda expression: ~v" bad-expression)]))

(define (alpha-view expr [binders '()])
  (match expr
    [(? symbol? name)
     (define depth
       (index-of binders name eqv?))
     (if depth
         `(bound ,depth)
         `(free ,name))]

    [`(lambda (,(? symbol? name)) ,body)
     `(lambda ,(alpha-view body (cons name binders)))]

    [`(,operator ,operand)
     `(apply ,(alpha-view operator binders)
             ,(alpha-view operand binders))]

    [bad-expression
     (error 'alpha-view "bad lambda expression: ~v" bad-expression)]))

(define (alpha-equivalent? left right)
  (equal? (alpha-view left)
          (alpha-view right)))

(define (beta-step expr)
  (match expr
    ;; Contract a redex before searching its subexpressions.
    [`((lambda (,(? symbol? name)) ,body) ,argument)
     (values (substitute argument name body) #t)]

    [`(lambda (,(? symbol? name)) ,body)
     (define-values (next-body changed?)
       (beta-step body))
     (values `(lambda (,name) ,next-body) changed?)]

    [`(,operator ,operand)
     (define-values (next-operator operator-changed?)
       (beta-step operator))
     (if operator-changed?
         (values `(,next-operator ,operand) #t)
         (let-values ([(next-operand operand-changed?)
                       (beta-step operand)])
           (values `(,operator ,next-operand) operand-changed?)))]

    [(? symbol?)
     (values expr #f)]

    [bad-expression
     (error 'beta-step "bad lambda expression: ~v" bad-expression)]))

(define (normalize expr [fuel 100])
  (define-values (next changed?)
    (beta-step expr))
  (cond
    [(not changed?)
     expr]
    [(zero? fuel)
     (error 'normalize "fuel exhausted; the term may diverge")]
    [else
     (normalize next (sub1 fuel))]))

(define (eta-contract expr)
  (match expr
    [`(lambda (,(? symbol? name))
        (,function ,(? symbol? argument)))
     #:when (and (eqv? name argument)
                 (not (set-member? (free-vars function) name)))
     function]
    [_ #f]))

(module+ test
  (require rackunit)

  (check-equal?
   (free-vars '(lambda (x) ((f x) y)))
   (set 'f 'y))

  (check-true
   (alpha-equivalent?
    '(lambda (x) (lambda (y) (x y)))
    '(lambda (first) (lambda (second) (first second)))))

  (check-false
   (alpha-equivalent?
    '(lambda (x) (lambda (y) (x y)))
    '(lambda (x) (lambda (y) (y y)))))

  ;; The replacement's free y must not be captured.
  (check-equal?
   (substitute 'y 'x '(lambda (y) x))
   '(lambda (y_0) y))

  ;; Substitution stops at a declaration that shadows x.
  (check-equal?
   (substitute 'replacement 'x '(lambda (x) (x z)))
   '(lambda (x) (x z)))

  (check-equal?
   (normalize
    '((lambda (x) (x x))
      (lambda (z) z)))
   '(lambda (z) z))

  ;; Fuel counts permitted contractions, not visits to normal forms.
  (check-equal?
   (normalize 'already-normal 0)
   'already-normal)

  (check-equal?
   (normalize '((lambda (x) x) y) 1)
   'y)

  (check-exn
   #rx"fuel exhausted"
   (lambda ()
     (normalize '((lambda (x) x) y) 0)))

  ;; The capture-sensitive worked example normalizes to free y.
  (check-equal?
   (normalize
    '(((lambda (x) (lambda (y) x)) y) z))
   'y)

  (check-equal?
   (eta-contract '(lambda (x) (f x)))
   'f)

  (check-false
   (eta-contract '(lambda (x) (x x)))))

What the lexical-address test records

For example:

(alpha-view
 '(lambda (x)
    (lambda (y)
      (x y))))

produces the conceptual shape:

'(lambda
   (lambda
     (apply (bound 1)
            (bound 0))))

The names x and y have disappeared. bound 0 refers to the nearest lambda; bound 1 crosses one lambda to reach the next. A free variable would retain its symbol, because renaming a free variable is not alpha-equivalence.

Equality is not automatically an evaluation strategy

Equational reasoning in the pure lambda calculus and evaluation in a concrete programming language answer related but different questions.

Consider the divergent term:

Omega = (lambda x. x x) (lambda x. x x)

Then:

(lambda ignored. result) Omega

has a beta contraction to result if we choose the outermost redex first. A call-by-value evaluator instead tries to evaluate Omega before applying the lambda and therefore does not return.

Similarly, eta equivalence expresses extensional equality in a pure setting. In a language with effects, errors, divergence, procedure identity, or a strict value restriction, replacing M with lambda x. M x may change when M is evaluated or whether an error occurs.

Keep these levels distinct:

  • alpha, beta, and eta conversion describe equations on pure terms;
  • a reduction strategy chooses which allowed redex to contract next; and
  • a programming-language evaluator fixes evaluation order and may include effects or errors absent from the pure calculus.

Functions as data encodings

The lambda calculus needs no primitive Boolean values. A Boolean can choose one of two alternatives:

(define true
  (lambda (then-value)
    (lambda (else-value)
      then-value)))

(define false
  (lambda (then-value)
    (lambda (else-value)
      else-value)))

(define choose
  (lambda (boolean)
    (lambda (then-value)
      (lambda (else-value)
        ((boolean then-value) else-value)))))

(((choose true) 'yes) 'no)    ; => 'yes
(((choose false) 'yes) 'no)   ; => 'no

This example illustrates the calculus’s universality without changing its syntax: data is represented by the behavior of functions that consume it. Church numerals, pairs, and lists apply the same idea on a larger scale.

Supervised practice

Work through these without using the reducer first.

Binding and alpha-equivalence

(lambda (x)
  ((lambda (x)
     (x y))
   x))
  1. Mark every declaration, bound reference, and free reference.
  2. Rename the inner declaration to z without changing meaning.
  3. Can the outer declaration also be renamed to y? Justify your answer using free-variable information.

Capture-avoiding reduction

((lambda x. lambda y. x y) y)
  1. Identify the redex, body, formal parameter, and argument.
  2. Explain why direct textual replacement captures a variable.
  3. Choose a fresh name and perform one correct beta step.
  4. List the free variables before and after the step. They should agree.

Reduction order

(lambda x. z) ((lambda y. y) w)
  1. Show a leftmost-outermost reduction sequence.
  2. Show a sequence that reduces the argument first.
  3. Do both terminate at the same normal form?
  4. Replace the argument with Omega. Which sequence still reaches z?

Common mistakes

  • Reading application as right-associative. f x y means ((f x) y), not (f (x y)).
  • Stopping a lambda body too early. The body extends rightward unless parentheses say otherwise.
  • Calling a name globally free or bound. Free and bound classify variable occurrences in an expression.
  • Renaming only some bound references. Alpha-renaming changes one declaration and exactly the occurrences it binds.
  • Choosing a fresh name that already occurs. A safely fresh name avoids every name relevant to the substitution.
  • Substituting beneath a shadowing declaration. (lambda (x) body) blocks a substitution for free x inside body.
  • Ignoring capture. A replacement’s free variables must remain free unless the original program already bound them.
  • Omitting the eta side condition. lambda x. M x contracts only when x is not free in M.
  • Confusing convertibility with call-by-value evaluation. An equation may permit several transformations even though an evaluator commits to one order.
  • Assuming every term has a normal form. Omega reduces forever.

Summary

  • Lambda-calculus syntax consists only of variables, abstraction, and application.
  • Alpha-equivalence ignores the spelling of bound variables while preserving binding structure.
  • Capture-avoiding substitution replaces free occurrences without rebinding other variables.
  • Beta reduction applies a lambda by substitution.
  • Eta equivalence identifies a function with a wrapper that merely forwards an argument, subject to a free-variable side condition.
  • Lexical addresses give a direct executable test for alpha-equivalence.
  • Fresh-name generation is a semantic necessity, not cosmetic formatting.
  • Pure equational laws must be related carefully to a concrete language’s evaluation order and effects.

Self-check questions

  1. How do you parenthesize f x y z?
  2. What are the free variables of lambda x. (f (x y))?
  3. Why are lambda x. x and lambda y. y alpha-equivalent?
  4. Why are lambda x. y and lambda y. y not alpha-equivalent?
  5. When must substitution alpha-rename a lambda parameter?
  6. What invariant does capture-avoiding substitution preserve?
  7. What is the beta contractum of (lambda x. x x) N?
  8. What side condition permits eta contraction?
  9. Why can normal-order reduction return when call-by-value evaluation does not?
  10. Why does the reducer use fuel even though some inputs normalize quickly?

Updated: