Lambda Calculus

Posted on May 1, 2023


  • Variables: {$a..z$}, commonly $x$ first
  • Terms: {$A..Z$}, commonly M first. Either a variable, abstraction or application; respectively, $M ::= x | (\lambda x.M) | (M M)$
    • May also be denoted as $e$, expression: $e ::= x | (\lambda x.e) | (e e)$
  • Application associates leftwise, and binds tighter than abstraction.

$\lambda$ binds a variable to the scope that comes after the dot. In $\lambda x. (\lambda y. M)$, the scope of $x$’s binding is over $(\lambda y. M)$. Unbound variables are called free.

Note: we can omit unnessecary parethesis when associating leftwise. $\lambda x. (\lambda y. M)$ = $\lambda x y. M$


$[N/x]M$ means “replace free variable x with N in M”. eg:

  • $[z/y]\lambda x. y = \lambda x. z$
  • $[N/x]\lambda x. M = \lambda x. M$, since x is bound (freshness)
  • $[N/x](P Q) = ([N/x]P )([N/x]Q)$, since substitution is distributive

$\alpha$ Equivalence

If we can convert an expression to another and back using only substitution, they are $\alpha$ equivalent.

  • $[a/x][b/y][c/z](\lambda x y z. x x y y) = (\lambda a b c. a a b b)$
  • $[x/a][y/b][z/c](\lambda a b c. a a b b) = (\lambda x y z. x x y y)$
  • $\therefore (\lambda x y z. x x y y) \rightarrow_{\alpha} (\lambda a b c. a a b b)$

$\beta$ Reduction

“Applying an argument”; substituting an argument to an abstraction.

  • $(\lambda x.M )N \longrightarrow [N/x]M$

We say A evaluates to B if we can transform A into B through some number of $\beta$ reductions: $A \Rightarrow B \equiv A \longrightarrow^{*} B$. Sometimes, evaluating results in divergence, where evaluation gets stuck in a loop.

$\eta$ Reduction

For when we can simplify an expression without performing a full $\beta$ reduction: $(\lambda x. Mx) \longrightarrow_{\eta} M$

  • $(\lambda y. \lambda x. y x) \longrightarrow_{\eta} (\lambda y. y) \longrightarrow_{\eta} ()$

Evaluation order

We can choose which order to evaluate redexes. Assuming $M \Rightarrow M\prime$, $N \Rightarrow N\prime$:

  • Eager (Normal order): Reduce leftmost redex first. Evaluate operands first.
    • $(\lambda x.M )N \Rightarrow (\lambda x.M )N\prime \rightarrow_{\alpha} [N\prime /x]M$
  • Lazy (Applicative order): Reduce rightmost redex first. $\beta$ reduce only when nessecary, always $\alpha$ reduce first.
    • $(\lambda x.M )N \rightarrow_{\alpha} [N/x]M$
  • “Optimising”: Evaluate functions first.
    • $(\lambda x.M )N \Rightarrow (\lambda x.M\prime )N \rightarrow_{\alpha} [N /x]M\prime$

Normal forms

Recall expression definition: $e ::= x | (\lambda x.e) | (e e)$ Introduce:

  • Normal form expression: $E ::= \lambda x.E | x E_1 … E_n$
  • Weak normal form expression: $E ::= \lambda x.e | x E_1 … E_n$
    • Function “contents” may be any expression
  • Head normal form expression: $E ::= \lambda x.E | x e_1 … e_n$
    • Function “operands” may be any expression
  • Weak Head normal form: $E ::= \lambda x.e | x e_1 … e_n$

De Bruijn representation

Refer to bound variables by the number of scopes since they were bound.

  • $(\lambda x.x (\lambda y.x y x (\lambda z.y z x ))x)$ is represented as $(\lambda 1 (\lambda 2 1 2 (\lambda 2 1 3 )) 1)$
  • Free variables use locally nameless terms, i.e. the next available number not used anywhere else in the expression
    • $(\lambda x. \lambda y. z x (\lambda u. u x)) (\lambda x. w x) $ becomes $(\lambda \lambda 4 2 (\lambda 1 3)) (\lambda 5 1)$, noting that $z$ and $w$ are free variables


6 important closed (context-free) expressions.

  • $I=\lambda x. x$ (Identity)
  • $K=\lambda x y. x$ (Constant)
  • $Y=\lambda f. (\lambda x. f(x x)) (\lambda x. f(x x))$
  • $S=\lambda x y z. x z (y z)$
  • $B=\lambda x y z. x (y z)$
  • $T=\lambda x y. y x$

Any closed lambda expression, including other combinators, can be expressed using only S and K.

Church encodings


  • True: $\mathcal{T} = \lambda x y. x$ (= K combinator); choose first input
  • False: $\mathcal{F} = \lambda x y. y$; choose second input
  • If: $\mathcal{I} = \lambda p x y. p x y$
    • $\mathcal{I} \mathcal{T} x y \Rightarrow x$
    • $\mathcal{I} \mathcal{F} x y \Rightarrow y$
  • And: $\mathcal{A} = \lambda p q. p q p$
  • Or: $\mathcal{O} = \lambda p q. p p q$
  • Not: $\mathcal{N} = \lambda p a b. p b a$


  • $0 = \lambda f x. x$
  • $1 = \lambda f x. f x$
  • $\mathtt{add} = \lambda i j f x. (i f) (j f x)$
    • $\mathtt{add}$ 1 1 $\Rightarrow \lambda f x. f (f x) = 2$

Return to Index ⟶