13 Lambda Calculus

Before lambda calculus, the dominant model of computation was the Turing Machine — an abstract device consisting of an infinite tape of symbols, a read/write head, and a control unit that tracks a finite state. The machine reads a symbol, consults a transition table, writes a new symbol, moves the head, and transitions to a new state. This process repeats until a halt state is reached.

The Turing Machine gives us one precise, mechanical account of computation. But in the 1930s, mathematician Alonzo Church (born in Washington, DC) proposed a completely different formalism: the lambda calculus (λ-calculus). Rather than thinking in terms of tape operations and states, Church’s system is built entirely on functions and substitution.

Despite looking nothing like a Turing Machine, the lambda calculus is provably Turing complete — it can compute anything a Turing Machine can. This equivalence (known as the Church–Turing thesis) deepened our understanding of what it means for a problem to be computable at all.

13.1.1 What is Lambda Calculus?🔗

Lambda calculus is a formal system — a mathematical framework with precise syntax and rules — originally designed to investigate functions and recursion. Church used it to explore the foundations of mathematics in the 1930s.

Today, lambda calculus is used for two main purposes:

Investigating computability — which problems can and cannot be solved by any algorithm
As the basis of functional programming languages — including Lisp, Scheme, ML, OCaml, and Haskell

13.1.2 Why Study Lambda Calculus?🔗

Lambda calculus is a "core" language: it is extraordinarily small — just three syntactic forms — yet it is Turing complete. This makes it the ideal lens through which to study general ideas in programming languages:

Language features — what do different constructs mean, and how can they be expressed?
Semantics — how do we assign precise meanings to programs?
Proof systems — how do we reason formally about program behavior?
Algorithms — how do evaluation strategies (eager vs. lazy) affect computation?

Because lambda calculus is so minimal, insights gained here apply broadly. Any language feature you want to understand — higher-order functions, closures, recursion, variable binding — can be analyzed cleanly in the lambda calculus.

13.2 Lambda Calculus Syntax🔗

A lambda calculus expression (also called a term) is defined by the following grammar:

\begin{array}{rcll} e & ::= & x & \textit{variable} \\ & \mid & \lambda x.\, e & \textit{abstraction (function definition)} \\ & \mid & e \; e & \textit{application (function call)} \end{array}

That is all. The entire language has exactly three constructs:

Variable (x): a name that stands for some expression. Variables are bound by abstractions, just like function parameters.
Abstraction (λx.e): a function that takes x as input and returns the expression e as output. This is exactly like (fun x -> e) in OCaml. The variable x is the parameter, and e is the body.
Application (e1 e2): calling the function e1 with argument e2. This is written with juxtaposition — no parentheses required — just like OCaml’s function application syntax f x.

Note that the lambda calculus has no built-in numbers, booleans, conditionals, or recursion. Everything must be encoded using only these three forms. As we will see, this is surprisingly powerful.

13.3 Parsing Conventions🔗

Because lambda calculus expressions can be ambiguous, two conventions govern how they are parsed:

13.3.1 Convention 1: Scope of λ Extends as Far Right as Possible🔗

The body of a λ extends as far to the right as possible, subject only to boundaries set by explicit parentheses. For example:

λx. λy.x y is the same as λx.(λy.(x y)) — the outer λ’s body is the entire λy.x y, and the inner λ’s body is x y.

This means that when you see λx.e, the expression e is everything to the right unless parentheses cut it short.

13.3.2 Convention 2: Function Application is Left-Associative🔗

When multiple applications appear in a row, they group from the left. For example:

x y z is the same as (x y) z — apply x to y first, then apply the result to z.

This is the same rule as OCaml, where f x y means (f x) y.

Quiz: Applying the Conventions
Consider the term λx.x a b. Which of the following is it equivalent to?
(λx.x) (a b)
(((λx.x) a) b)
λx.(x (a b))
(λx.((x a) b))

Answer: (λx.((x a) b)). Apply the two conventions step by step: λ scope extends as far right as possible, so λx.x a b → λx.(x a b); then application is left-associative, so x a b → (x a) b; combined: λx.((x a) b). Note: (((λx.x) a) b) looks plausible but is wrong — it treats (λx.x) as the outermost function rather than keeping the full lambda body intact.

13.4 Lambda Calculus Semantics🔗

13.4.1 Evaluation via Substitution🔗

The only computational step in the lambda calculus is applying a function to an argument. Given the application (λx.e1) e2, we evaluate e1 with x replaced by e2.

This operation is called beta-reduction and is written:

(\lambda x.\, e_1)\; e_2 \;\to\; e_1[x {:=} e_2]

The notation e1[x:=e2] means: in the expression e1, substitute every free occurrence of the variable x with the expression e2.

Beta-reduction corresponds exactly to function call evaluation. When OCaml runs (fun x -> e1) e2, it replaces x with e2 in e1 — that is precisely what beta-reduction does.

13.4.2 Beta Reduction Example🔗

Consider the expression:

(λx.λz.x z) y

Step through the reduction:

The outermost function is λx.λz.x z, applied to argument y.
Substitute y for x in the body λz.x z: every x becomes y.
Result: λz.y z

(λx.λz.x z) y  →  λz.y z

The equivalent OCaml code makes this concrete:

(fun x -> (fun z -> (x z))) y  →  fun z -> (y z)

The result is still a function — a partially applied curried function waiting for its second argument z.

13.5 Beta Reductions: Call-by-Value (CBV)🔗

13.5.1 Simple Examples🔗

Here are several basic beta reductions under call-by-value (eager) evaluation, where all arguments are values (cannot be reduced further) before substitution:

(λx.x) z  →  z

 (λx.y) z  →  y

 (λx.x y) z  →  z y

Explanations:

(λx.x) z: the identity function applied to z. Body is x; substitute z for x → z.
(λx.y) z: a constant function that always returns y, ignoring its argument. Body is y; x does not appear → y.
(λx.x y) z: a function that applies its argument to y. Body is x y; substitute z for x → z y.

13.5.2 Multi-Step Examples🔗

Reductions sometimes require multiple steps:

Example 1:

(λx.x y)(λz.z)  →  (λz.z) y  →  y

Step 1: Apply λx.x y to λz.z: substitute λz.z for x in x y → (λz.z) y
Step 2: Apply the identity λz.z to y: substitute y for z in z → y

Example 2: A curried function of two arguments that applies its first to its second:

(λx.λy.x y) z  →  λy.z y

Substitute z for x in λy.x y: every x becomes z → λy.z y
The result is a new function waiting for its second argument.

Example 3: A longer chain:

(λx.λy.x y)(λz.zz) x
  →  (λy.(λz.zz) y) x
  →  (λz.zz) x
  →  x x

Step 1: Substitute λz.zz for x in λy.x y → λy.(λz.zz) y
Step 2: Apply λy.(λz.zz) y to x: substitute x for y in (λz.zz) y → (λz.zz) x
Step 3: Apply λz.zz to x: substitute x for z in zz → x x

13.6 Evaluation Strategies: Eager vs. Lazy🔗

Lambda calculus does not specify when arguments must be evaluated — only what the result of substitution is. This gives rise to two distinct evaluation strategies.

13.6.1 Eager Evaluation (Call-by-Value, CBV)🔗

In eager (call-by-value) evaluation, the argument e2 is evaluated to a value before performing the beta-reduction. This is the strategy used by OCaml.

The evaluation judgment e ⇓ v (read "e evaluates to v") is defined by two rules:

Abstraction is already a value: \frac{} {(\lambda x.\, e_1) \;\Downarrow\; (\lambda x.\, e_1)}

Application (eager): \frac{e_1 \;\Downarrow\; (\lambda x.\, e_3) \qquad e_2 \;\Downarrow\; e_4 \qquad e_3[x {:=} e_4] \;\Downarrow\; e_5} {e_1 \; e_2 \;\Downarrow\; e_5}

The key is the middle premise: e2 ⇓ e4 — the argument is fully evaluated to e4 before it is substituted into the body.

13.6.2 Lazy Evaluation (Call-by-Name, CBN)🔗

In lazy (call-by-name) evaluation, the argument is substituted as-is, without being evaluated first. This is the strategy used by Haskell.

Abstraction is already a value: (same rule) \frac{} {(\lambda x.\, e_1) \;\Downarrow\; (\lambda x.\, e_1)}

Application (lazy): \frac{e_1 \;\Downarrow\; (\lambda x.\, e_3) \qquad e_3[x {:=} e_2] \;\Downarrow\; e_4} {e_1 \; e_2 \;\Downarrow\; e_4}

Notice: there is no premise e2 ⇓ e4. The unevaluated expression e2 is substituted directly into e3.

13.6.3 CBV vs. CBN: A Comparison🔗

Consider the term (λz.z)((λy.y) x):

CBV (eager): evaluate the argument (λy.y) x first:

(λz.z)((λy.y) x)  →  (λz.z) x  →  x

CBN (lazy): substitute the unevaluated argument directly:

(λz.z)((λy.y) x)  →  (λy.y) x  →  x

Both strategies produce the same final result (x), but take different intermediate steps. CBV evaluates (λy.y) x to x before passing it to λz.z, while CBN passes (λy.y) x directly and evaluates it only when the body needs it.

Key differences:

CBV (eager): Arguments are evaluated exactly once, before the call. Can loop if the argument diverges even when the body doesn’t need it. Used by OCaml, Scheme, most imperative languages.
CBN (lazy): Arguments may be evaluated zero or more times (once per use). Can avoid non-termination when the body doesn’t use the argument. Used by Haskell.

13.7 Beta Reductions: Call-by-Name (CBN)🔗

Under CBN, we substitute the argument expression as-is without evaluating it first. Here are two worked examples:

Example 1:

(λx.x (λy.y)) (u r)  →  (u r) (λy.y)

Under CBN, we do not evaluate (u r) first.
Substitute (u r) for x in the body x (λy.y): every x becomes (u r).
Result: (u r) (λy.y).

Example 2:

(λx.(λw. x w)) (y z)  →  λw. (y z) w

Under CBN, we do not evaluate (y z) first.
Substitute (y z) for x in the body (λw. x w): every x becomes (y z).
Result: λw. (y z) w — a function waiting for argument w, which will apply (y z) to it.

Example 3: CBN terminates where CBV diverges

Recall the omega combinator Ω = (λx.x x)(λx.x x), which reduces to itself forever. Now consider applying a constant function to Ω:

(λx.y) Ω

CBV (eager) — diverges:

(λx.y) Ω
  =  (λx.y) ((λx.x x)(λx.x x))    [expand Ω]
  →  (λx.y) ((λx.x x)(λx.x x))    [Ω →  Ω, loops forever]
  →  ...                           [never reaches the body]

Under CBV we must evaluate the argument before the call. Since Ω never reduces to a value, the whole expression diverges.

CBN (lazy) — terminates:

(λx.y) Ω
  →  y                             [substitute Ω for x in body y; x ∉ FV(y), done]

Under CBN we substitute Ω for x in the body y without evaluating it. Since x does not appear in y, the substitution produces y immediately and Ω is never evaluated.

This is the key advantage of lazy evaluation: arguments that are never used by the body are never computed, even if they would loop forever.

Quiz: Beta-Reduction Result
(λx.y) z can be beta-reduced to which of the following?
y
y z
z
cannot be reduced

Answer: y. The body is y and the parameter is x. Substituting z for x in y leaves y unchanged since x does not appear in y. This is the constant function — it ignores its argument and always returns y.

Quiz: Which Expression Reduces to λz.z?
Which of the following reduces to λz.z?
(λy. λz. x) z
(λz. λx. z) y
(λy. y) (λx. λz. z) w
(λy. λx. z) z (λz. z)

Answer: (λy. y) (λx. λz. z) w. Trace through:

(λy. y) (λx. λz. z) w
  →  (λx. λz. z) w        [apply identity (λy.y) to (λx.λz.z)]
  →  λz. z                [apply (λx.λz.z) to w: x not in body, result is λz.z]

Why the others fail:

a) (λy. λz. x) z → λz. x — the free variable x remains; result is not λz.z.
b) (λz. λx. z) y → λx. y — substitutes y for z in λx.z → λx.y, not λz.z.
d) (λy. λx. z) z (λz. z) → (λx. z)(λz. z) → z — free variable z, not a lambda abstraction.

13.8 Static Scoping and Alpha Conversion🔗

13.8.1 Static Scoping🔗

Lambda calculus uses static (lexical) scoping: each variable refers to the nearest enclosing λ that binds it. When a lambda parameter shares a name with an outer one, the inner binding shadows the outer.

Example:

(λx.x (λx.x)) z

The outer λx binds the first x.
The inner λx creates a new binding that shadows the outer one within (λx.x).
Applying to z: substitute z for the outer x only → z (λx.x).
The inner λx.x is left unchanged — its x is bound by the inner lambda.

13.8.2 Alpha Conversion (Renaming Bound Variables)🔗

The names of bound variables are irrelevant — only their binding structure matters. Two terms that differ only in the names of their bound variables are considered alpha-equivalent:

λx.x  =  λy.y  =  λz.z

All three are the identity function. Renaming a bound variable consistently throughout a term is called alpha conversion. For example:

λx.x (λx.x)  ≡  λx.x (λy.y)

The inner λx.x is alpha-converted to λy.y — same function, different name. Alpha conversion is essential for avoiding variable capture during substitution (see the next section).

13.9 Substitution: Formal Rules🔗

Beta-reduction is defined in terms of substitution: (λx.e1) e2 → e1[x:=e2]. The notation e[x:=e’] means "replace all free occurrences of x in e with e’." The formal definition breaks into cases:

13.9.1 Case 1: Variable🔗

x[x := e]  =  e          (x matches the substituted variable)
y[x := e]  =  y          (y ≠ x, so leave it alone)

13.9.2 Case 2: Application🔗

(e0 e1)[x := e]  =  (e0[x := e]) (e1[x := e])

Substitution distributes over both sides of an application.

13.9.3 Case 3: Abstraction — Shadowing🔗

If the lambda binds the same variable being substituted, do nothing — the inner binding shadows the substitution:

(λx.e')[x := e]  =  λx.e'

The x inside e’ refers to the lambda parameter, not the outer x, so substituting e for x would incorrectly reach inside the binding.

13.9.4 Case 4: Abstraction — No Capture🔗

If the lambda binds a different variable y and y is not free in e, substitution proceeds into the body normally:

(λy.e')[x := e]  =  λy.(e'[x := e])     (if y ∉ FV(e)  and  y ≠ x)

13.9.5 Case 5: Abstraction — Variable Capture (Requires Alpha Conversion)🔗

The tricky case: if the lambda binds y and y is free in e, direct substitution would capture y, giving the wrong meaning.

Problem example:

(λy.x y)[x := y]
  Wrong naive result:  λy.y y   ❌   (the y in e was captured!)

Correct approach — alpha-convert the lambda first, replacing y with a fresh variable w:

(λy.x y)[x := y]
  →  alpha-convert to (λw.x w)
  →  (λw.x w)[x := y]
  =  λw.y w              ✓

Formal rule (using a fresh variable w not free in either e’ or e):

(λy.e')[x := e]  =  λw.((e'[y := w])[x := e])   (w is a fresh variable)

13.10 Free Variables🔗

A variable is free in an expression if it is not bound by any enclosing λ. The set of free variables FV(e) is defined recursively:

FV(x)      = {x}
FV(e1 e2)  = FV(e1) ∪ FV(e2)
FV(λx.e)   = FV(e) - {x}

Examples:

FV(λx.x)    = FV(x) - {x} = {x} - {x} = {}
FV(λx.x y)  = FV(x y) - {x} = ({x} ∪ {y}) - {x} = {y}

Free variables matter for substitution: e1[x:=e2] only replaces free occurrences of x in e1. Bound occurrences (inside a λx) are left alone.

13.11 Lambda Calculus in OCaml🔗

13.11.1 AST Representation🔗

Lambda calculus expressions map directly to an OCaml algebraic data type:


type id = string

type exp =
  | Var of id        (* x *)
  | Lam of id * exp  (* λx.e *)
  | App of exp * exp (* e1 e2 *)

13.11.2 Substitution Implementation🔗

The substitution subst m y e computes m[y:=e] — replacing free occurrences of variable y in m with expression e:


let rec subst m y e =
  match m with
  | Var x ->
      if y = x then e else m
  | App (e1, e2) ->
      App (subst e1 y e, subst e2 y e)
  | Lam (x, e0) ->
      if y = x then m                           (* shadowing: stop here *)
      else if not (List.mem x (fvs e)) then
        Lam (x, subst e0 y e)                   (* safe: x not free in e *)
      else
        let z = newvar () in                    (* x would be captured: rename *)
        let e0' = subst e0 x (Var z) in
        Lam (z, subst e0' y e)

The three cases mirror the formal rules: shadowing stops the substitution; if the bound variable is not free in e it is safe to recurse; otherwise, generate a fresh name to avoid capture.

13.11.3 Reduction Strategy (CBV)🔗

The CBV reduction function repeatedly finds and fires the leftmost outermost redex (a beta-reducible application):


let rec reduce e =
  match e with
  | App (Lam (x, e1), e2) -> subst e1 x e2      (* fire the redex *)
  | App (e1, e2) ->
      let e1' = reduce e1 in
      if e1' != e1 then App (e1', e2)            (* reduce function first *)
      else App (e1, reduce e2)                   (* then reduce argument *)
  | Lam (x, e) -> Lam (x, reduce e)             (* reduce under lambda *)
  | _ -> e                                       (* variable: already normal *)

13.12 Encoding Programming Constructs🔗

Lambda calculus has no built-in booleans, numbers, or pairs — but all of these can be encoded using only abstractions and applications. These encodings, known as Church encodings, demonstrate that lambda calculus is computationally universal.

13.12.1 Let Bindings🔗

A let x = e1 in e2 expression is just syntactic sugar for an immediately applied lambda:

let x = e1 in e2  =  (λx.e2) e1

Example:

let x = (λy.y) in x x
  =  (λx.x x) (λy.y)
  →  (λy.y) (λy.y)
  →  λy.y

13.12.2 Booleans (Church Encoding)🔗

Church booleans encode true and false as functions that choose between two arguments:

true  = λx.λy.x    (take x and y, return the first)
false = λx.λy.y    (take x and y, return the second)

An if-then-else expression is then just application — the boolean selects the correct branch:

if a then b else c  =  a b c

Verification:

true b c = (λx.λy.x) b c → (λy.b) c → b ✓
false b c = (λx.λy.y) b c → (λy.y) c → c ✓

13.12.3 Boolean Operations🔗

Using Church booleans, the standard boolean operations are:

not = λx.x false true
and = λx.λy.x y false
or  = λx.λy.x true y

For example, not true = true false true = false ✓, and and true false = true false false = false ✓.

13.13 Pairs🔗

A pair (a, b) is encoded as a function that, given a boolean selector, returns either the first or second component:

(a, b)  =  λx.if x then a else b
          =  λx.x a b

The projection functions use Church booleans as selectors:

fst = λf.f true
snd = λf.f false

Verification:

fst (a, b) = (λf.f true) (λx.x a b) → (λx.x a b) true → true a b → a ✓
snd (a, b) = (λf.f false) (λx.x a b) → (λx.x a b) false → false a b → b ✓

13.14 Church Numerals🔗

Natural numbers are encoded as Church numerals: the number n is a higher-order function that applies a given function f exactly n times to a starting value y:

0 = λf.λy.y           (apply f zero times)
1 = λf.λy.f y          (apply f once)
2 = λf.λy.f (f y)      (apply f twice)
3 = λf.λy.f (f (f y))  (apply f three times)

In general, the Church numeral for n is:

n = λf.λy. f applied n times to y

This encoding elegantly captures the essence of counting: a number is the act of iterating a function a certain number of times.

13.15 Arithmetic on Church Numerals🔗

13.15.1 Successor🔗

The successor function adds one application of f:

succ = λz.λf.λy.f (z f y)

Given numeral z (which applies f n times to y), succ z applies f one additional time: f (z f y).

13.15.2 isZero🔗

iszero = λz.z (λy.false) true

z applies (λy.false) some number of times to true. If z = 0, no applications occur and the result is true. If z ≥ 1, at least one application fires, returning false.

13.15.3 Addition🔗

+ = λM.λN.λf.λy.M f (N f y)

N f y applies f n times to y; then M f applies f m more times, giving m+n total applications.

13.15.4 Multiplication🔗

* = λM.λN.λf.λy.M (N f) y

N f is a function that applies f n times; M (N f) y iterates that m times, giving m \times n total applications of f.

13.15.5 Example: 1 + 1 = 2🔗

1 + 1
= (λM.λN.λf.λy.M f (N f y)) 1 1
→ λf.λy.1 f (1 f y)
→ λf.λy.f (f y)
= 2  ✓

13.16 Recursion and Looping🔗

13.16.1 Infinite Loop🔗

Lambda calculus can express non-termination. Define:

D = λx.x x

Then applying D to itself diverges:

D D = (λx.x x)(λx.x x) → (λx.x x)(λx.x x) → ...  (infinite loop)

This is the simplest non-terminating lambda term.

13.16.2 The Y Combinator (Fixed-Point Combinator)🔗

General recursion requires a fixed-point combinator. The Y combinator, discovered by Church, enables recursion without any built-in mechanism:

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

Key property: Y F = F (Y F) for any F.

Proof:

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

This means Y F is a fixed point of F: applying F to Y F gives back Y F. This is how recursion works — each reduction of Y F expands into F (Y F), which can call F again with Y F as the recursive reference.

13.17 Factorial via the Y Combinator🔗

Factorial can be expressed as the fixed point of a non-recursive step function. Define:

fact = λf.λn. if n = 0 then 1 else n * (f (n-1))

Here f is the recursive reference — the function to call for the smaller input. The actual recursive factorial is Y fact:

(Y fact) n

Because Y fact = fact (Y fact), each call to (Y fact) n expands to fact (Y fact) n, which either returns 1 (base case) or computes n * ((Y fact)(n-1)).

Example:

(Y fact) 4  →  4 * (Y fact) 3
            →  4 * 3 * (Y fact) 2
            →  4 * 3 * 2 * (Y fact) 1
            →  4 * 3 * 2 * 1 * (Y fact) 0
            →  4 * 3 * 2 * 1 * 1
            =  24

13.18 Limitations of Untyped Lambda Calculus🔗

Untyped lambda calculus is theoretically universal but practically cumbersome:

Slow: Church numeral arithmetic requires a number of reductions proportional to the values involved. For example, 10000 + 1 requires thousands of beta-reductions.
Large: Encoded terms for even simple programs are enormous.
Hard to read: Abstractions nested several levels deep are difficult to follow.
No type safety: Nothing prevents nonsensical applications.

13.19 The Need for Types🔗

Untyped lambda calculus has no way to distinguish different kinds of values. For example, Church’s encoding makes false and 0 identical:

false = λx.λy.y
0     = λx.λy.y

They are the same term! This means expressions like false 0 are syntactically valid and reduce to a result — but the result is meaningless:

false 0  =  (λx.λy.y)(λx.λy.y)  →  λy.y   (nonsense, but no error)

Types solve this by partitioning terms into kinds and statically rejecting programs that mix them incorrectly.

13.20 Simply-Typed Lambda Calculus (STLC)🔗

The Simply-Typed Lambda Calculus (STLC) adds a type system to lambda calculus. The syntax is extended to require type annotations on lambda parameters:

e ::= n | x | λx:t.e | e e

t ::= int | t → t

13.20.1 Type Annotations on Abstractions🔗

Every λ parameter now carries an explicit type: λx:t.e means "x has type t." Function types are written t1 → t2 (the function takes a t1 and returns a t2).

13.20.2 Key Properties of STLC🔗

Prevents invalid programs: An expression like true 0 (applying a boolean to a number) is now a type error, caught before runtime.
Strong normalization: Every well-typed STLC program always terminates — it reaches a normal form (irreducible term) after a finite number of reductions.
Less expressive: The Y combinator cannot be typed in STLC because λx.x x would require x to have a type t such that t = t → ?, which is impossible in a finite type system.

13.20.3 The Termination Trade-Off🔗

STLC’s strong normalization is both a strength and a limitation. It guarantees no infinite loops — but it also means STLC is not Turing complete. You cannot express arbitrary recursion. In contrast, untyped lambda calculus (with the Y combinator) is Turing complete but can loop forever.

Practical typed languages (OCaml, Haskell) escape this by adding recursive types or explicit fix constructs that permit general recursion while retaining most type-safety benefits.

13.21 Summary🔗

Lambda calculus is a minimal yet universal formal model of computation built entirely on three constructs: variables, abstractions, and applications.

Core mechanics:

Beta-reduction: (λx.e1) e2 → e1[x:=e2] — the single computation step
Substitution: must handle shadowing and avoid variable capture (alpha conversion)
Free variables: determine which xs in a body are affected by substitution

Evaluation strategies:

CBV (eager): evaluate the argument first — used by OCaml, Scheme
CBN (lazy): substitute the unevaluated argument — used by Haskell

Church encodings show lambda calculus can represent everything:

Booleans: true = λx.λy.x, false = λx.λy.y, if a then b else c = a b c
Natural numbers: n = λf.λy.(f applied n times to y)
Arithmetic: successor, addition, multiplication, iszero
Pairs: (a,b) = λx.x a b, with fst = λf.f true, snd = λf.f false
Recursion: Y combinator Y = λf.(λx.f(x x))(λx.f(x x))

Types (STLC) add structure: they prevent nonsense programs and guarantee termination, at the cost of ruling out general recursion.

13.22 Lambda Calculus Code Example🔗

In-class Example Code (lambda.zip)

Simplified version. To run:

ocaml main.ml

Output:

Lambda Expression: λx.x y
AST: Lam(x,App(Var x,Var y))
unparsed AST: λx. x y
Example: if expression

if true then 1 else 2 = 1

if false then 1 else 2 = 2

Example: Addition
3 + 2 = 5

Example: Multiplication
5 * 4 = 20
(5 + 4) * 20 = 180

Example: Integer Division
succ(3)/2 =  2

Example: Recursion: Factorial
fact(3) = 6

lambda-simple/main.ml

(*
open Lambda
open Pp
*)
#use "lambda.ml"
#use "pp.ml"
let r = Lam ("x", App (Var "x", Var "y"));;

Printf.printf "Lambda Expression: λx.x y\n";;
Printf.printf "AST: %s\n" (lambda_exp_2_str r);;
Printf.printf "unparsed AST: ";;
print_lambda r;;

Printf.printf "\nExample: if expression\n"

(* and true true  *)
let e = App (App (myand, mytrue), mytrue);;

(*  if e then 1 else 2 *)
let e2 = App (App (App (myif, e), one), two)
let e2 = reduce_multi e2
let () = Printf.printf "\nif true then 1 else 2 = %d\n" (to_int e2)

(*Example 2 *)

(* and true false  *)
let e = App (App (myand, mytrue), myfalse)

(*   e2 = if e then 1  else 2 *)
let e2 = App (App (App (myif, e), one), two)
let e2 = reduce_multi e2;;
let () = Printf.printf "\nif false then 1 else 2 = %d\n" (to_int e2)
;;
(* Example 3: Addition
   3 + 2
*)
Printf.printf "\nExample: Addition\n"
let e1 = App (App (plus, three), two)
let e2 = reduce_multi e1;;
let () = Printf.printf "3 + 2 = %d\n" (to_int e2);;

(* Example 4  Multiplication
   let e1 = 3 + 2
   let e2 = 3 + 1
   let e3 = e1 * e2
*)
Printf.printf "\nExample: Multiplication\n"
let e1 = App (App (plus, three), two)
let e2 = App (succ, three)
let e3 = App (App (mult, e1), e2)
let e4 = reduce_multi e3
let () = Printf.printf "5 * 4 = %d\n" (to_int e4)

(* let e5 = (e3+e2) * e4
            (5 + 4 ) * 20
*)
let e5 = App (App (mult, App (App (plus, e1), e2)), e4)
let e6 = reduce_multi e5
let () = Printf.printf "(5 + 4) * 20 = %d\n" (to_int e6);;

Printf.printf "\nExample: Integer Deivision\n"

(*   4 / 2  *)
let e = App(App(div,App(succ,three)),two);;
Printf.printf "succ(3)/2 =  %d\n" (to_int (reduce_multi e));;

Printf.printf "\nExample: Recursion: Factorial\n";;
(*
   Y = \f.(\x. f (x x)) (\x. f (x x))
  fact = \f.\n. if n = 0 then 1 else n * (f (n -1))
 *)

(* Example 4
   fact(3)
*)

let if2 (a, b, c) = App (App (App (myif, a), b), c)

let fact1 =
  Lam
    ( "f",
      Lam
        ( "n",
          if2
            ( App (iszero, Var "n"),
              (* condition *)
              one,
              (* if branch *)
              App (App (mult, Var "n"), App (Var "f", App (mypred, Var "n")))
              (* else *) ) ) )

(* calculate factorial of 3  *)
let e = App (App (yfix, fact1), three)

(* print the factorial 3 as int *)
let x = to_int (reduce_multi e) (*  6 *);;

Printf.printf "fact(3) = %d\n" x;;


(* calculate factorial of 4  *)

(*
let four = reduce_multi (App(succ,three));;
let e  = App(App(yfix, fact1), four);;

let x = to_int (reduce_multi e)   (*  6 *)
;;
Printf.printf "fact(4) = %d\n" x;;
*)

lambda-simple/lambda.ml

                                                                                                                                                                                                                                                                                   

href="#cb1-1" aria-hidden="true" tabindex="-1">type var = string class="kw">type exp = Var of var | Lam of var * exp | App of exp * exp an> class="co">(* generates a fresh variable name *) class="kw">let newvar = let x = ref 0 in fun () -> let c = !x in incr x; "v" ^ string_of_int c span> class="co">(* computes the free (non-bound) variables in e *) class="kw">let rec fvs e = match e with | Var x -> [ x ] | Lam (x, e) -> List.filter (fun y -> x <> y) (fvs e) | App (e1, e2) -> fvs e1 @ fvs e2 span> class="co">(* substitution: subst e y m means class="co">   "substitute occurrences of variable y with m in the expression e" *) class="kw">let rec subst e y m = match e with | Var x -> if y = x then m (* replace x with m *) else e (* variables don't match: leave x alone *) | App (e1, e2) -> App (subst e1 y m, subst e2 y m) | Lam (x, e) -> if y = x then (* don't substitute under the variable binder *) Lam (x, e) else if not (List.mem x (fvs m)) then (* no need to alpha convert *) Lam (x, subst e y m) else (* need to alpha convert *) let z = newvar () in (* assumed to be "fresh" *) let e' = subst e x (Var z) in (* replace x with z in e *) Lam (z, subst e' y m) span> class="kw">let rec reduce e = (*let _= Printf.printf "reducing ...\n" in *) match e with | App (Lam (x, e), e2) -> subst e x e2 (* direct beta rule *) | App (e1, e2) -> let e1' = reduce e1 in (* try to reduce a term in the lhs *) if e1' != e1 then App (e1', e2) else App (e1, reduce e2) (* didn't work; try rhs *) | Lam (x, e) -> Lam (x, reduce e) (* reduce under the lambda (!) *) | _ -> e (* no opportunity to reduce *) span> class="kw">let rec reduce_multi e1 = let e2 = reduce e1 in if e2 = e1 then e1 else reduce_multi e2 span> class="co">(* Church Encodings*) span> class="kw">let zero = Lam ("f", Lam ("x", Var "x")) class="kw">let one = Lam ("f", Lam ("x", App (Var "f", Var "x"))) class="kw">let two = Lam ("f", Lam ("x", App (Var "f", App (Var "f", Var "x")))) span> class="kw">let three = Lam ("f", Lam ("x", App (Var "f", App (Var "f", App (Var "f", Var "x"))))) class="co">(* "λf. λx. f (f (f x))" *) span> class="kw">let succ = Lam ( "n", Lam ("f", Lam ("x", App (Var "f", App (App (Var "n", Var "f"), Var "x")))) ) class="co">(*"λn. λf. λx. f (n f x)" *) span> class="kw">let plus = Lam ( "m", Lam ( "n", Lam ( "f", Lam ( "x", App ( App (Var "m", Var "f"), App (App (Var "n", Var "f"), Var "x") ) ) ) ) ) class="co">(* λm. λn. λf. λx. m f (n f x) *) span> class="kw">let mult = Lam ("m", Lam ("n", Lam ("f", App (Var "m", App (Var "n", Var "f"))))) span> class="co">(* "λm. λn. λf. m (n f)"*) class="kw">let mytrue = Lam ("x", Lam ("y", Var "x")) (* "λx. λy. x" *) class="kw">let myfalse = Lam ("x", Lam ("y", Var "y")) (* λx. λy. y *) class="kw">let myif = Lam ("a", Lam ("b", Lam ("c", App (App (Var "a", Var "b"), Var "c")))) class="co">(* λa. λb. λc. a b c *) span> class="kw">let mynot = Lam ("b", Lam ("x", Lam ("y", App (App (Var "b", Var "y"), Var "x")))) class="co">(* "λb. λx. λy.  b y x" *) span> class="kw">let myand = Lam ( "a", Lam ( "b", Lam ( "x", Lam ( "y", App ( App (Var "b", App (App (Var "a", Var "x"), Var "y")), Var "y" ) ) ) ) ) class="co">(* λa. λb. λx. λy. b (a x y) y *)  class="kw">let myor = Lam ( "a", Lam ( "b", Lam ( "x", Lam ( "y", App ( App (Var "b", Var "x"), App (App (Var "a", Var "x"), Var "y") ) ) ) ) ) class="co">(* λa. λb. λx. λy.  b x (a x y) *)  class="kw">let iszero = Lam ( "n", App ( App (Var "n", Lam ("x", Lam ("x", Lam ("y", Var "y")))), Lam ("x", Lam ("y", Var "x")) ) ) class="co">(* λn. n (λx. (λx.λy. y)) (λx. λy. x) *)  class="kw">let mypred = Lam ( "n", Lam ( "f", Lam ( "x", App ( App ( App ( Var "n", Lam ( "g", Lam ("h", App (Var "h", App (Var "g", Var "f"))) ) ), Lam ("u", Var "x") ), Lam ("u", Var "u") ) ) ) ) class="co">(* λn. λf. λx. n (λg.  λh.  h (g f)) (λu.x) (λu. u) *)  class="kw">let minus = Lam ( "m", Lam ( "n", App ( App ( Var "n", Lam ( "n", Lam ( "f", Lam ( "x", App ( App ( App ( Var "n", Lam ( "g", Lam ( "h", App ( Var "h", App (Var "g", Var "f") ) ) ) ), Lam ("u", Var "x") ), Lam ("u", Var "u") ) ) ) ) ), Var "m" ) ) ) class="co">(* λm. λn. (n λn. λf. λx. n (λg.  λh.  h (g f)) (λu.x) (λu. u)) m *)  class="kw">let div = Lam ( "n", App ( App ( Lam ( "f", App ( Lam ("x", App (Var "x", Var "x")), Lam ("x", App (Var "f", App (Var "x", Var "x"))) ) ), Lam ( "c", Lam ( "n", Lam ( "m", Lam ( "f", Lam ( "x", App ( Lam ( "d", App ( App ( App ( Lam ( "n", App ( App ( Var "n", Lam ( "x", Lam ( "a", Lam ( "b", Var "b" ) ) ) ), Lam ( "a", Lam ( "b", Var "a" ) ) ) ), Var "d" ), App ( App ( Lam ( "f", Lam ("x", Var "x") ), Var "f" ), Var "x" ) ), App ( Var "f", App ( App ( App ( App ( Var "c", Var "d" ), Var "m" ), Var "f" ), Var "x" ) ) ) ), App ( App ( Lam ( "m", Lam ( "n", App ( App ( Var "n", Lam ( "n", Lam ( "f", Lam ( "x", App ( App (  App (  Var "n", Lam (  "g", Lam (  "h", App (  Var "h", App (  Var "g", Var "f" ) ) ) ) ), Lam (  "u", Var "x" ) ), Lam (  "u", Var "u" ) ) ) ) ) ), Var "m" ) ) ), Var "n" ), Var "m" ) ) ) ) ) ) ) ), App ( Lam ( "n", Lam ( "f", Lam ( "x", App (Var "f", App (App (Var "n", Var "f"), Var "x")) ) ) ), Var "n" ) ) )  class="co">(* Y combinator *) class="kw">let yfix = Lam ( "f", App ( Lam ("x", App (Var "f", App (Var "x", Var "x"))), Lam ("x", App (Var "f", App (Var "x", Var "x"))) ) ) class="co">(*  "λf.(λx. f (x x)) (λx. f (x x))" *)

lambda-simple/pp.ml

(* open Lambda *)
open Format

let ident = Printf.printf "%s" (*print_string*)
let kwd = Printf.printf "%s" (*print_string*)

let rec print_exp0 = function
  | Var s -> ident s
  | lam ->
      open_hovbox 1;
      kwd "(";
      print_lambda lam;
      kwd ")";
      close_box ()

and print_app = function
  | e ->
      open_hovbox 2;
      print_other_applications e;
      close_box ()

and print_other_applications f =
  match f with
  | App (f, arg) ->
      print_app f;
      Printf.printf " ";
      print_exp0 arg
  | f -> print_exp0 f

and 
 print_lambda = function
  | Lam (s, lam) ->
      open_hovbox 1;
      kwd "λ";
      ident s;
      kwd ".";
      Printf.printf " ";
      print_lambda lam;
      close_box ()
  | e -> print_app e

let rec lambda_exp_2_str e =
  match e with
  | Var x -> "Var " ^ x
  | App (e1, e2) ->
      "App(" ^ lambda_exp_2_str e1 ^ "," ^ lambda_exp_2_str e2 ^ ")"
  | Lam (x, e) -> "Lam(" ^ x ^ "," ^ lambda_exp_2_str e ^ ")"

  let p = print_lambda ;;

  let rec to_int e =
  match e with
  | App (x, y) -> 1 + to_int x + to_int y
  | Lam (_a, b) -> to_int b
  | _ -> 0

contents ← prev up next →

1	Introduction
2	Functional Programming with OCaml
3	Imperative Programming with OCaml
4	Property-Based Randomized Testing (PBT)
5	Regular Expressions
6	Finite Automata
7	Context Free Grammars
8	Parsing
9	Operational Semantics
10	Type System
11	Memory Management and Garbage Collection
12	Rust
13	Lambda Calculus
14	Software Security
15	Exercises

13.1	Introduction to Lambda Calculus
13.2	Lambda Calculus Syntax
13.3	Parsing Conventions
13.4	Lambda Calculus Semantics
13.5	Beta Reductions: Call-by-Value (CBV)
13.6	Evaluation Strategies: Eager vs. Lazy
13.7	Beta Reductions: Call-by-Name (CBN)
13.8	Static Scoping and Alpha Conversion
13.9	Substitution: Formal Rules
13.10	Free Variables
13.11	Lambda Calculus in OCaml
13.12	Encoding Programming Constructs
13.13	Pairs
13.14	Church Numerals
13.15	Arithmetic on Church Numerals
13.16	Recursion and Looping
13.17	Factorial via the Y Combinator
13.18	Limitations of Untyped Lambda Calculus
13.19	The Need for Types
13.20	Simply-Typed Lambda Calculus (STLC)
13.21	Summary
13.22	Lambda Calculus Code Example