7 min read
On this page

Lambda Calculus

Untyped Lambda Calculus

Syntax

The lambda calculus has three term forms:

M, N ::= x          (variable)
        | lambda x. M   (abstraction)
        | M N        (application)

Application is left-associative: M N P = (M N) P. Abstraction extends as far right as possible: lambda x. M N = lambda x. (M N).

Alpha-Equivalence

Alpha-conversion: Renaming bound variables preserves meaning. lambda x. x =_alpha lambda y. y. Terms are considered equal up to alpha-equivalence, forming equivalence classes.

Formally, lambda x. M =_alpha lambda y. M[x := y] provided y is not free in M (avoiding capture). This is the simplest notion of equivalence and is typically treated as syntactic identity.

Beta-Reduction

Beta-reduction is the fundamental computation rule:

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

where M[x := N] denotes capture-avoiding substitution. The term (lambda x. M) N is called a beta-redex (reducible expression).

Capture-avoiding substitution requires renaming bound variables to avoid free variables of N being captured:

  • x[x := N] = N
  • y[x := N] = y (y != x)
  • (M1 M2)[x := N] = M1[x := N] M2[x := N]
  • (lambda y. M)[x := N] = lambda z. M[y := z][x := N] where z is fresh

Eta-Reduction

Eta-reduction: lambda x. M x ->_eta M, provided x is not free in M.

Eta expresses extensionality: two functions are equal if they produce the same result on all inputs. Beta-eta equivalence gives the finest congruence compatible with extensional function equality.

The Church-Rosser Theorem

Theorem (Church-Rosser, 1936): If M ->_beta N1 and M ->_beta N2, then there exists P such that N1 ->_beta P and N2 ->_beta P.

Corollary (Uniqueness of normal forms): If M has a normal form, it is unique up to alpha-equivalence.

Proof approaches:

  • Tait-Martin-Lof: Define parallel reduction (=>), where multiple redexes are contracted simultaneously. Show => satisfies the diamond property. Since ->_beta equals =>, Church-Rosser follows.
  • Takahashi: Use the "complete development" (contracting all redexes at once) as the joining term.

Church-Rosser does NOT guarantee that a normal form exists, nor that every reduction strategy finds it.

Normalization

A term is in normal form if it contains no beta-redexes. A term is:

  • Weakly normalizing: Some reduction sequence reaches a normal form
  • Strongly normalizing: Every reduction sequence terminates (reaches a normal form)

Not all terms normalize: Omega = (lambda x. x x)(lambda x. x x) ->_beta Omega (infinite loop).

Reduction strategies:

  • Normal-order (leftmost-outermost): Always reduces the leftmost outermost redex. Guaranteed to find the normal form if one exists (by the Standardization Theorem).
  • Applicative-order (leftmost-innermost): Evaluates arguments before substitution. May diverge even when a normal form exists.
  • Call-by-value: Reduces only when the argument is a value (abstraction). Models strict evaluation.
  • Call-by-need: Memoizes call-by-name. Models lazy evaluation.

Church Encodings

The untyped lambda calculus is Turing-complete. Data can be encoded as functions:

Booleans: TRUE = lambda t f. t, FALSE = lambda t f. f Church numerals: n = lambda f x. f^n(x). So 0 = lambda f x. x, 1 = lambda f x. f x, etc. Pairs: PAIR = lambda a b p. p a b, FST = lambda p. p TRUE, SND = lambda p. p FALSE Lists: Using right folds or Scott encodings

Arithmetic: SUCC = lambda n f x. f (n f x), PLUS = lambda m n f x. m f (n f x), MULT = lambda m n f. m (n f)

Predecessor is surprisingly nontrivial: PRED = lambda n f x. n (lambda g h. h (g f)) (lambda u. x) (lambda u. u). This uses the pairing trick: iterate (a, b) -> (b, b+1) starting from (0, 0).

Scott Encodings

Scott encodings represent data by their elimination form (pattern matching), unlike Church encodings (fold/iteration):

For natural numbers: 0 = lambda z s. z, SUCC n = lambda z s. s n

Scott encodings allow O(1) predecessor (just apply the destructor), while Church encodings require O(n) steps for predecessor.

Fixed-Point Combinators

Since lambda calculus has no built-in recursion, fixed-point combinators enable recursive definitions:

Y combinator (Curry): Y = lambda f. (lambda x. f (x x))(lambda x. f (x x))

  • Y f ->_beta f (Y f) -- under normal-order reduction

Theta combinator (Turing): Theta = (lambda x y. y (x x y))(lambda x y. y (x x y))

  • Theta f ->_beta f (Theta f) -- works under any strategy

Call-by-value Y: Z = lambda f. (lambda x. f (lambda v. x x v))(lambda x. f (lambda v. x x v))

De Bruijn Indices

De Bruijn indices replace variable names with natural numbers indicating binding distance:

  • 0 refers to the nearest enclosing binder
  • k refers to the binder k levels up

Example: lambda x. lambda y. x = lambda. lambda. 1

Benefits: Alpha-equivalence becomes syntactic equality. No need for fresh variable generation during substitution.

Substitution with de Bruijn indices requires shifting: when substituting under a binder, free variable indices in the substituted term must be incremented.

shift(k, c, n) = n if n < c, n + k if n >= c

This is used in formal proof assistants and implementations.

Combinatory Logic (SKI)

Combinatory logic eliminates variables entirely, using combinators:

  • S = lambda x y z. x z (y z) -- "generalized application"
  • K = lambda x y. x -- "constant"
  • I = lambda x. x = S K K -- "identity"

Theorem: {S, K} is a complete basis. Every lambda term can be translated to an SKI expression via bracket abstraction:

[x] x = I [x] M = K M (if x not free in M) [x] M N = S ([x] M) ([x] N)

BCKW basis: B = lambda x y z. x (y z) (composition), C = lambda x y z. x z y (flip), K (constant), W = lambda x y. x y y (duplication). This basis often produces more compact translations.

Categorical Combinatory Logic

Combinatory logic corresponds to Cartesian closed categories (CCCs). The SKI combinators model the internal language of CCCs, connecting lambda calculus to category theory. Curry-Howard-Lambek extends this: types = objects, terms = morphisms, reduction = equality of morphisms.

Simply Typed Lambda Calculus

Types

A, B ::= alpha        (base type)
        | A -> B       (function type)

Church-Style (Explicit Types)

Terms carry type annotations: lambda x:A. M. Typing is syntax-directed:

Gamma, x:A |- x : A                       (Var)
Gamma, x:A |- M : B
----------------------------               (Abs)
Gamma |- (lambda x:A. M) : A -> B
Gamma |- M : A -> B    Gamma |- N : A
----------------------------               (App)
Gamma |- M N : B

Curry-Style (Implicit Types)

Terms are untyped; types are assigned externally. Type inference asks: given M, find A and Gamma such that Gamma |- M : A. For the simply typed lambda calculus, type inference is decidable via unification (Hindley, 1969; Milner, 1978).

Principal type property: Every typable term has a most general type (principal type scheme).

Strong Normalization

Theorem (Tait, 1967): Every well-typed term in the simply typed lambda calculus is strongly normalizing.

Proof (Tait's method of logical relations / reducibility candidates):

Define, for each type A, a set RED_A of "reducible" terms:

  • RED_alpha = {M : M is strongly normalizing} for base types
  • RED_{A -> B} = {M : for all N in RED_A, M N in RED_B}

Show:

  1. Every reducible term is strongly normalizing (by induction on types)
  2. Every well-typed term is reducible (by induction on typing derivations)
  3. Therefore, every well-typed term is strongly normalizing

This technique is fundamental and extends to System F (Girard's proof), dependent types, and beyond.

Curry-Howard Correspondence

The simply typed lambda calculus corresponds to intuitionistic propositional logic:

| Lambda Calculus | Logic | |---|---| | Type | Proposition | | Term | Proof | | A -> B | Implication A implies B | | Application | Modus ponens | | Abstraction | Implication introduction | | Beta-reduction | Proof normalization (cut elimination) | | Normal form | Cut-free proof |

This extends to richer type systems: products = conjunction, sums = disjunction, dependent types = quantifiers, etc.

Expressivity Limitations

The simply typed lambda calculus is not Turing-complete: all programs terminate. The class of functions representable is exactly the extended polynomials (Schwichtenberg, 1976) -- a strict subset of primitive recursive functions. Adding recursion (fix : (A -> A) -> A) or general recursive types restores Turing completeness at the cost of termination guarantees.