IA014: Advanced Functional
Programming
2. Untyped Lambda Calculus
Jan Obdržálek obdrzalek@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
IA014 2. Untyped Lambda Calculus 1
Formal development
IA014 2. Untyped Lambda Calculus 2
Syntax
The set of λ-terms is defined by the following BNF grammar:
M ::= x variable
| MM application
| λx.M abstraction
• where x, y, z, . . . are variables from a countable set Var
• we use uppercase letters M, N, . . . to denote λ-terms
• (, ) are used whenever the meaning is not clear
examples
I ≡ λx.x K ≡ λx.(λy.x)
ω ≡ λx.(x x) S ≡ λx.(λy.(λz.((x z)(y z))))
Ω ≡ ω ω ≡ (λx.(x x))(λx.(x x))
IA014 2. Untyped Lambda Calculus 3
Syntactic conventions
• λx1x2 . . . xn.M means λx1.(λx2.(. . . (λxn.M) . . .))
• M1M2M3 . . . Mn means (. . . ((M1M2)M3) . . .)
application associates to the left
• λx.x y means λx.(x y)
function application takes precedence
• spaces have no meaning
Examples
simplified
λx.(x y z) λx.x y z
(λx.x) y (λx.x) y
λx.(λy.x) λxy.x
λx.(λy.(λz.((x z) (y z))) λxyz.(x z) (y z)
IA014 2. Untyped Lambda Calculus 4
Variable binding
In a term λx.M the variable x is bound in the body M.
• λ is an abstraction operator and M is its scope.
• occurrence of a variable is free if it is not bound
Formally The set of free variables, FV (M), in a λ-term M is
defined as:
FV (x) = x
FV (MN) = FV (M) ∪ FV (N)
FV (λx.M) = FV (M) \ {x}
If FV (M) = ∅, then M is called a closed term or a combinator.
IA014 2. Untyped Lambda Calculus 5
Binding examples
term free bound
λx.x y y x
(λx.x y) x x, y x
λxy.x − − x, y
(λx.x x)(λx.x x) − − x
Convention we will use: the names of free and bound variables
will always be different.
IA014 2. Untyped Lambda Calculus 6
Substitution
M[x := N] – the substitution of N for the free occurrences of x
in M, is defined as:
x[x := N] = N
y[x := N] = y if y = x
(M1M2)[x := N] = (M1[x := N])(M2[x := N])
(λx.M)[x := N] = λx.M
(λy.M)[x := N] = λy.(M[x := N]) if x = y
provided y ∈ FV (N)
In the last case, if y ∈ FV (N) we say that y is fresh for N.
IA014 2. Untyped Lambda Calculus 7
Substitution II
comments
The freshness requirement is absolutely crucial:
λy.x[x := y] = λy.y name capture
Our substitution is capture-avoiding.
Alternative definition of substitution (only the last case):
(λy.M)[x := N] = λz.M[y := z][x := N]
provided x = y and z ∈ FV (M) ∪ FV (N) ∪ {x}
examples
(λy.x)[y := x] = λy.x
(λy.x)[x := y] = λz.y
(λx.(λy.y z) (λw.w) z x)[y := z] = . . .
IA014 2. Untyped Lambda Calculus 8
α-conversion and equivalence
Observation: The terms λx.x and λy.y are, for all practical
purposes, equivalent.
The α-equivalence relation, =α, is defined by the following
rules:
M[x := z] =α N[y := z] z ∈ FV (M) ∪ FV (N)
λx.M =α λy.N
x =α x
M1 =α M2 N1 =α N2
M1N1 =α M2N2
Renaming bound variables is often called α-conversion.
Compare with the previous slide!
IA014 2. Untyped Lambda Calculus 9
β-reduction
The idea of function application is expressed by the following
equational axiom:
(λx.M)N = M[x := N] (β)
In computational context, this can be though of as a single
computation step, called β-reduction step:
(λx.M)N → M[x := N]
In this context, (λx.M)N is called a redex (reducible
expression).
IA014 2. Untyped Lambda Calculus 10
Full β-reduction
• a redex can appear anywhere in a term M
• Full β-reduction is then given by the following set of rules:
(λx.M)N →β M[x := N]
M1 →β M2
λx.M1 →β λx.M2
M1 →β M2
M1N →β M2N
N1 →β N2
MN1 →β MN2
We also define a reflexive transitive closure →∗
β of →β:
M →∗
β N iff either M = N or there is a sequence
M →β M1 →β M2 →β . . . →β N
• We will often drop the index β from →β.
• We will work modulo α-equivalence.
IA014 2. Untyped Lambda Calculus 11
β-reduction – examples
(λx.λy.yx)(λz.u) → λy.y(λz.u)
(λx.xx)(λz.u) → (λz.u)(λz.u)
(λy.y a)((λx.x)(λz.(λu.u) z)) → (λy.y a)(λz.(λu.u) z)
(λy.y a)((λx.x)(λz.(λu.u) z)) → (λy.y a)((λx.x)(λz.z))
(λy.y a)((λx.x)(λz.(λu.u) z)) → ((λx.x)(λz.(λu.u)z))a
Ω ≡ (λx.x x)(λx.x x) → (λx.x x)(λx.x x) → . . .
KaΩ ≡ (λxy.x) a Ω
KaΩ → a
KaΩ → KaΩ → a
KaΩ → KaΩ → KaΩ → a
(λx.x x)((λy.y)z) → (λx.x x)z → z z
(λx.x x)((λy.y)z) → ((λy.y)z)((λy.y)z) →2
z z
IA014 2. Untyped Lambda Calculus 12
Normal form, Questions
Normal form
Term M is in β-normal form iff it contains no β-redexes.
Q1: Can a term have more than one normal form?
Q2: Does a β-reduction always terminate?
Q3: Does the order of evaluation matter?
Q4: In which order should we select the redexes?
IA014 2. Untyped Lambda Calculus 13
Confluence
Q1: Can a term have more than one normal form?
Theorem (Church-Rosser)
Let M be a λ-term. If M →∗ M1 and M →∗ M2, then there is N
such that M1 →∗ N and M2 →∗ N
N
M1
*
M2
*
M
* *
(λx.x x)((λy.y)z) → (λx.x x)z → z z
(λx.x x)((λy.y)z) → ((λy.y)z)((λy.y)z) →2
z z
IA014 2. Untyped Lambda Calculus 14
Non-termination
Q2: Does a β-reduction always terminate?
• This is called strong normalization property.
• Untyped λ-calculus is not strongly normalizing:
Ω ≡ (λx.x x)(λx.x x) → (λx.x x)(λx.x x) → (λx.x x)(λx.x x) → . . .
• Simply-typed λ-calculus is strongly normalizing.
• What does that mean?
• . . . it is decidable whether program halts . . .
• Then it is not Turing complete! (computationally universal)
IA014 2. Untyped Lambda Calculus 15
Nondeterminism
Q3: Does the order of evaluation matter?
Compare
(λx.z)((λw.www)(λw.www)) →
(λx.z)((λw.www)(λw.www)(λw.www)) →
(λx.z)((λw.www)(λw.www)(λw.www)(λw.www)) →
. . .
with
(λx.z)((λw.www)(λw.www)) → z
The choice of evaluation (reduction) strategy matters!
IA014 2. Untyped Lambda Calculus 16
Evaluation Strategies
Q4: In which order should we select the redexes?
• Full β-reduction
• Any redex can be selected.
• As defined on slide 11
• Applicative order
• form of strict/eager evaluation
• leftmost innermost
• evaluate arguments (left to right) before applying function
• Normal order
• form of non-strict evaluation
• leftmost outermost
• applying function before evaluating arguments
• complete – if there is a normal form, it would be eventually
reached
IA014 2. Untyped Lambda Calculus 17
Call-By-Value semantics of λ
• strict/eager evaluation strategy
• unlike applicative order, does not reduce the body of the
function before applying the function
• used, e.g., by ML
M ::= x variable
| MM application
| λx.M abstraction
V ::= λx.M abstraction value
(λx.M)V →β M[x := V ]
M1 →β M2
M1N →β M2N
N1 →β N2
V N1 →β V N2
IA014 2. Untyped Lambda Calculus 18
β-equivalence
β-reduction is directional. However, we can also use it
“bidirectionally”
β-equivalence
Two terms M and N are said to be β-equivalent (written as
M =β N) if either:
1 M ≡ N, or
2 there is a sequence of terms M = M0, M1, . . . Mk = N s.t.
for all 1 ≤ i ≤ k either
• Mi−1 → Mi, or
• Mi → Mi−1
(i.e. =β is a reflexive, symmetric and transitive closure of →β)
From Church-Rosser, two normalizing terms are β-equivalent iff
their normal forms are equal.
IA014 2. Untyped Lambda Calculus 19
η-conversion (reduction)
Let us assume we have the following term:
N ≡ λx.M x
and that x is not free in M.
Observation: (λx.M x)N →β MN
η-reduction rule:
x ∈ FV (M)
(λx.M x) →η M
• removes redundant λ-abstractions
• we can define →βη-reduction
• →βη-reduction is (again) confluent
IA014 2. Untyped Lambda Calculus 20
Encoding Mathematics in
λ-calculus
IA014 2. Untyped Lambda Calculus 21
Booleans
truth values
• true := λx.λy.x
• false := λx.λy.y
true tf
= (λx.λy.x)tf
→ (λy.t)f
→ t
false tf
= (λx.λy.y)tf
→ (λy.y)f
→ f
conditional statement
• if := λxyz.xyz
IA014 2. Untyped Lambda Calculus 22
Boolean operators
truth values
• true := λx.λy.x
• false := λx.λy.y
operators
• and := λxy.x y x
• or := λxy.x x y
• not := λxyz.x z y
Check that the operators behave as expected!
IA014 2. Untyped Lambda Calculus 23
Pairs
Desired behaviour:
fst(pair x y) →∗
β x
snd(pair x y) →∗
β y
Idea: use Booleans for projections
• pair := λxyf.f x y
• fst := λp.p true
• snd := λp.p false
Check that the operators behave as expected!
IA014 2. Untyped Lambda Calculus 24
Church numerals
How do we construct natural numbers?
• 0, succ(0), succ(succ(0)), . . .
• the same idea is behind the Church numerals
• function, which takes 0 and succ as parameters
• 0 := λf.λx.x
• 1 := λf.λx.f x
• 2 := λf.λx.f (f x)
• 3 := λf.λx.f (f (f x))
• . . .
• n := f(f . . . (f
n-times
(x) . . .) = λf.λx.fn(x)
IA014 2. Untyped Lambda Calculus 25
Arithmetic operations
n := λf.λx.fn
(x)
• successor
succ := λn.λf.λx.f (n f x)
• addition
plus := λm.λn.λf.λx.m f (n f x) or
plus := λm.λn.m succ n
• multiplication
times := λm.λn.λf.m (n f) or
using plus (exercise)
• exponentiation
(exercise)
• subtraction (assuming a predecessor)
minus := λm.λn.n pred m
IA014 2. Untyped Lambda Calculus 26
Predecessor function
n := λf.λx.fn
(x)
• To compute predecessor, you have to remove one f.
• But there is no “empty” λ-term!
Wisdom tooth trick
• you count up to n, remembering also the previous number
• pairs are ideal:
(0, 0), (0, 1), (1, 2), (2, 3), (3, 4) . . .
λ-calculus encoding
step := λp. pair (snd p) (succ(snd p))
pred := λn. fst(n step (pair 0 0))
IA014 2. Untyped Lambda Calculus 27
Lists – exercise
Define lists and functions operating on them:
• nil – empty list
• null – test for emptiness
• cons – prepends element to a list
• hd – head of the list
• tl – tail of the list
Desired behaviour:
null nil →∗
true hd(cons x l) →∗
x
null (cons x l) →∗
false tl(cons x l) →∗
l
IA014 2. Untyped Lambda Calculus 28
Recursion
IA014 2. Untyped Lambda Calculus 29
Recursive functions
• As we have seen, many functions are λ-definable.
• What about the factorial?
F(n) =
1 if n = 0
n ∗ F(n − 1) otherwise
• Problem: in λ-calculus, functions are anonymous:
fact ≡ λn. if n = 0 then 1 else n ∗ fact(n − 1)
Q: No self-reference in λ-calculus?
Luckily not: ω y = (λx.x x) y → y y
IA014 2. Untyped Lambda Calculus 30
Manual recursion
Idea: recursive function f takes a definition of itself as first
argument, and passes it to the subsequent calls
G := λf.λn. if n = 0 then 1 else n ∗ (f f (n − 1))
fact := G G = (λx.x x) G
Works as intended (TRY IT!)
problem: every recursive call needs to be rewritten as
self-application
IA014 2. Untyped Lambda Calculus 31
More natural recursion
G := λf.λn. if n = 0 then 1 else n ∗ (f f (n − 1))
fact := G G = (λx.x x) G
problem: every recursive call needs to be rewritten as
self-application
Our goal: write just
G := λf.λn. if n = 0 then 1 else n ∗ (f (n − 1))
• Naturally, we want Gfx = fx to hold.
• I.e. Gf = f . . . we are looking for a fixed point F of G!
• We would like to do this automatically.
Find a function FIX such that F = G(FIX G) = FIX G
Does such a function exist?
IA014 2. Untyped Lambda Calculus 32
Factorial using FIX
Let us assume we have such a function FIX and take
G := λf.λn. if n = 0 then 1 else n ∗ (f (n − 1))
fact := FIX G = G (FIX G)
Let’s compute the factorial of 2:
fact 2 = (FIX G)2 = G(FIX G)2 =
λf.λn. if n = 0 then 1 else n ∗ (f(n − 1))(FIX G)2 →β
λn. if n = 0 then 1 else n ∗ ((FIX G)(n − 1))2 →β
if 2 = 0 then 1 else 2 ∗ ((FIX G)(2 − 1)) →δ
if 2 = 0 then 1 else 2 ∗ ((FIX G)1) →δ
2 ∗ ((FIX G)1) = 2 ∗ (G(FIX G)1) =
2 ∗ (λf.λn. if n = 0 then 1 else n ∗ (f(n − 1))(FIX G)1) →β
2 ∗ (λn. if n = 0 then 1 else n ∗ ((FIX G)(n − 1))1) →β
2 ∗ (if 1 = 0 then 1 else 1 ∗ ((FIX G)(1 − 1))) →δ
2 ∗ (if 1 = 0 then 1 else 1 ∗ ((FIX G)0)) →δ
2 ∗ (1 ∗ ((FIX G)0))
IA014 2. Untyped Lambda Calculus 33
Y combinator (Church)
Y := λf.(λx.f(x x)) (λx.f(x x))
Theorem
Y g = g(Y g)
Proof.
Y g = (λf.(λx.f(x x)) (λx.f(x x))) g
→ (λx.g(x x)) (λx.g(x x))
→ g((λx.g(x x))(λx.g(x x)))
← g(λf.((λx.f(x x)) (λx.f(x x))) g)
= g(Y g)
Note: Y g →∗ g(Y g)
IA014 2. Untyped Lambda Calculus 34
Θ combinator (Turing)
Θ := (λxf.f(x x f))(λxf.f(x x f))
Theorem
Θ g →∗ g(Θ g)
Proof.
Θ g = (λxf.f(x x f)) (λxf.f(x x f)) g
→ (λh.h ((λxf.f(x x f)) (λxf.f(x x f)) h)) g
→ g((λxf.f(x x f)) (λxf.f(x x f)) g)
= g(Θ g)
IA014 2. Untyped Lambda Calculus 35
From λ-calculus to functional
programming I
IA014 2. Untyped Lambda Calculus 36
Applied λ-calculi
applied λ-calculus = λ-calculus + constants (+ operations)
But we have just seen that we can do everything with pure
λ-calculus!?
Why applied λ-calculi?
• efficiency
• reliability
• convenience
IA014 2. Untyped Lambda Calculus 37
Formally
syntax
The set of lambda terms with constants Λ(C) is defined by:
M ::= x | M M | λx.M | C
Where C ∈ C for some set of constants C.
Different applied λ-calculi arise by a different choice of the set
C.
IA014 2. Untyped Lambda Calculus 38
δ-reduction
Let
• X ⊆ Λ(C) be a set of closed normal forms
(usually we take X ⊆ C)
• δ ∈ C a special constant
• f : X → Λ(C) externally defined function
Then the following δ-contraction rules are added to those of the
(pure) λ-calculus:
δM1 . . . Mk → f(M1 . . . Mk)
for M1, . . . Mk in X.
IA014 2. Untyped Lambda Calculus 39
δ-rule examples I
Booleans
C = true, false, not, and, or, ite
δ-rules
not true → false ite true → true(≡ λxy.x)
not false → true ite false → false(≡ λxy.y)
and true true → true or true true → true
and true false → false or true false → true
and false true → false or false true → true
and false false → false or false false → false
IA014 2. Untyped Lambda Calculus 40
δ-rule examples II
Integers
C = {n|n ∈ Z} ∪ plus, minus, times, divide, equal
δ-rule schemas
plus m n → m + n
minus m n → m − n
times m n → m ∗ n
divide m n → m ÷ n for n = 0
divide m 0 → error
equal m m → true
equal m n → false for m = n
IA014 2. Untyped Lambda Calculus 41
βδ-reduction
The “combined” reduction of the “new” calculus is called
βδ-reduction, written as →βδ (→∗
βδ).
Theorem
Let f be a function on closed normal forms. Then the resulting
notion of reduction →∗
βδ satisfies the Church-Rosser property.
The notion of normal form also generalizes.
IA014 2. Untyped Lambda Calculus 42
Syntactic sugar
Definition (Syntactic sugar)
Programming language construct, which can be removed from
the language without any effect on:
• functionality
• expressive power
Why do we need sugar?
To make language sweeter for humans. Can e.g.
• improve readability
• be more concise
• more natural to some
IA014 2. Untyped Lambda Calculus 43
Sugar I – functions
• binary arithmetic operators (+, −, ∗, . . .) in infix notation
4 + 5 =⇒ + 4 5 =⇒ plus 4 5
• comparison operators (<, ≤, =, =, . . .) in infix notation
4 < 5 =⇒ < 4 5
• if-then-else
if p then x else y =⇒ ite p x y
IA014 2. Untyped Lambda Calculus 44
Sugar II – local declarations
let x = M in N =⇒ (λx.N)M
recursive declarations
letrec x = M in N =⇒ (λx.N) (Y λx.M)
example:
letrec f = lambda n.if n=1 then 1
else n * (f(n-1))
in f 5
is desugared to
(λf.f 5) (Y λf.λn. if (= n 1)1(∗ n (f (− n 1))))
IA014 2. Untyped Lambda Calculus 45
Sugar III – function declarations
let f x1 . . . xn = M in N
=⇒ let fλx1 . . . λxn.M in N
=⇒ (λf.N)(x1 . . . λxn.M)
and similarly
letrec f x1 . . . xn = M in N
=⇒ letrec fλx1 . . . λxn.M in N
IA014 2. Untyped Lambda Calculus 46