3 min read
On this page

Lambda Calculus Applied

The Lambda Cube

Untyped Lambda Calculus Review

Syntax

e ::= x          (variable)
    | λx. e      (abstraction)
    | e1 e2      (application)

Convention: application is left-associative, abstraction extends as far right as possible.

Beta Reduction

(λx. e1) e2 -> e1[e2/x] (capture-avoiding substitution)

Alpha equivalence: λx. e ≡_α λy. e[y/x] when y is fresh. Practically handled via de Bruijn indices or locally nameless representations.

Eta Reduction

λx. e x -> e when x is not free in e. Establishes extensional equality of functions.

Church Encodings

Lambda calculus is Turing-complete. Data is represented as functions.

Booleans

true  = λt. λf. t
false = λt. λf. f
and   = λa. λb. a b false
or    = λa. λb. a true b
not   = λa. a false true
if    = λc. λt. λf. c t f    (redundant: c itself acts as if)

Church Numerals

0 = λf. λx. x
1 = λf. λx. f x
2 = λf. λx. f (f x)
n = λf. λx. f^n x

succ  = λn. λf. λx. f (n f x)
plus  = λm. λn. λf. λx. m f (n f x)
times = λm. λn. λf. m (n f)
iszero = λn. n (λx. false) true

Predecessor is harder: requires a pairing trick. pred = λn. λf. λx. n (λg. λh. h (g f)) (λu. x) (λu. u).

Pairs and Lists

pair  = λa. λb. λf. f a b
fst   = λp. p true
snd   = λp. p false
nil   = λc. λn. n                   (Church/Scott encoding)
cons  = λh. λt. λc. λn. c h (t c n)

Scott encoding is an alternative that allows constant-time pattern matching but does not directly support folds.

Fixed-Point Combinators

Recursion without self-reference: a fixed-point combinator F satisfies F g = g (F g).

Y Combinator (Call-by-Name)

Y = λf. (λx. f (x x)) (λx. f (x x))

Reduction: Y g -> (λx. g (x x)) (λx. g (x x)) -> g ((λx. g (x x)) (λx. g (x x))) = g (Y g).

Does not work under call-by-value because x x is eagerly evaluated, causing divergence.

Z Combinator (Call-by-Value)

Z = λf. (λx. f (λv. x x v)) (λx. f (λv. x x v))

The eta-expansion λv. x x v delays the self-application until actually called. Essential for strict languages.

Turing's Combinator

Θ = (λx. λf. f (x x f)) (λx. λf. f (x x f))

Another fixed-point combinator; Θ f = f (Θ f) in one step.

Practical Recursion

fact = Y (λf. λn. if (iszero n) 1 (times n (f (pred n))))

In real languages, letrec/let rec provides recursive binding without explicit combinators, typically implemented via mutable references or backpatching.

Reduction Strategies

Call-by-Value (CBV)

Reduce arguments to values before substitution. The leftmost-outermost redex whose argument is a value is reduced first.

(λx. e) v -> e[v/x]     (v is a value)

Used by: ML, Scheme, most imperative languages. Predictable evaluation order; easy to reason about effects.

Call-by-Name (CBN)

Substitute arguments unevaluated; the leftmost-outermost redex is reduced first.

(λx. e1) e2 -> e1[e2/x]  (e2 may not be a value)

Arguments evaluated each time they are used (can duplicate work). If an argument is unused, it is never evaluated.

Call-by-Need (Lazy Evaluation)

Like call-by-name but with memoization: each thunk is evaluated at most once. Used by Haskell.

Implementation requires a heap to store thunks and update them with their values after first evaluation.

Confluence (Church-Rosser)

If e ->* e1 and e ->* e2, then there exists e3 such that e1 ->* e3 and e2 ->* e3.

Consequence: if a normal form exists, it is unique (regardless of reduction strategy). However, not all strategies find it; CBN/CBNeed find it whenever it exists (normalizing strategies).

Standardization

The standard reduction (leftmost-outermost) finds a normal form whenever one exists. CBV may diverge even when a normal form exists: (λx. λy. y) (Ω) diverges under CBV but reduces to λy. y under CBN.

Abstract Machines

Abstract machines make evaluation strategies explicit by defining transitions on machine states (configurations).

SECD Machine (Landin, 1964)

State: (S, E, C, D) - Stack, Environment, Control, Dump.

Components:
  S = value stack
  E = environment (variable bindings)
  C = control (list of instructions)
  D = dump (saved continuations)

Key transitions:
  (S, E, VAR(x).C, D)         -> (lookup(E,x).S, E, C, D)
  (S, E, LAM(x,body).C, D)    -> (Closure(x,body,E).S, E, C, D)
  (S, E, APP.C, D)             -> ([], E', body, (S,E,C,D))
      where top of S has arg v and Closure(x,body,E')
      E' extended with x=v
  (v.S, E', [], (S',E,C,D))   -> (v.S', E, C, D)    (return)

Historical importance: first abstract machine for lambda calculus. Basis for early Lisp and ML implementations.

CEK Machine

State: (C, E, K) - Control (current expression), Environment, Continuation.

(x, E, K)             -> (E(x), E, K)           (lookup)
(λx.e, E, K)          -> (Closure(x,e,E), E, K)  (value reached, apply K)
(e1 e2, E, K)         -> (e1, E, ArgK(e2,E,K))  (evaluate function first)
(v, E, ArgK(e,E',K))  -> (e, E', FunK(v,K))     (function done, eval arg)
(v, E, FunK(Clo(x,e,E'),K)) -> (e, E'[x->v], K) (apply function)

Implements left-to-right CBV. The continuation K makes control flow explicit. Directly corresponds to defunctionalized continuation-passing style.

Krivine Machine

Implements call-by-name. State: (C, E, S) - Control, Environment, Stack (of closures).

(x, E, S)             -> (e, E', S)       where E(x) = (e, E')
(λx.e, E, c.S)        -> (e, E[x->c], S)  (pop arg, extend env)
(e1 e2, E, S)         -> (e1, E, (e2,E).S) (push argument closure)

No reduction of arguments before binding. Extends to call-by-need by adding a heap and update markers (lazy Krivine machine).

Relationships

Definitional interpreter
    |-- CPS transform --> continuation-based interpreter
    |-- defunctionalize --> CEK machine
    |-- further transforms --> SECD, Krivine variants

Danvy and Filinski showed systematic derivation: CPS transformation + defunctionalization connects interpreters to abstract machines. Each machine corresponds to a specific evaluation strategy and representation choice.

Summary

| Concept | Key Idea | |---|---| | Church encodings | Data as functions (universality of lambda calculus) | | Fixed-point combinators | Recursion without built-in recursion | | Reduction strategies | Different evaluation orders, different properties | | Confluence | Normal forms are unique when they exist | | Abstract machines | Explicit, mechanized evaluation; bridge theory and implementation |

The lambda calculus remains the foundational model for functional programming languages and the theoretical basis for compiler intermediate representations, type theory, and program analysis.