λ-Calculus Church Encodings
λ-Calculus
Dr. Liam O’Connor
University of Edinburgh LFCS UNSW, Term 3 2020
1
λ-Calculus
Church Encodings
λ-Calculus
The term language we defined for Higher Order Abstract Syntax is almost a full featured programming language.
Just enrich the syntax slightly:
t ::= Symbol
| x
| t1 t2
| λx. t
(variables) (application) (λ-abstraction)
There is just one rule to evaluate terms, called β-reduction: (λx. t) u →β t[x := u]
Just as in Haskell, (λx. t) denotes a function that, given an argument for x, will return
t. 2
λ-Calculus
Church Encodings
Syntax Concerns
Function application is left associative:
f abc = ((f a)b)c
λ-abstraction extends as far as possible:
λa.f ab = λa.(f ab)
All functions are unary, like Haskell. Multiple argument functions are modelled with nested λ-abstractions:
λx.λy. x + y
3
λ-Calculus
Church Encodings
β-reduction is a congruence:
β-reduction
(λx. t) u →β t[x := u]
t→β t′ s→β s′ t→β t′
st→β st′ st→β s′ t λx.t→β λx.t′
This means we can pick any reducible subexpression (called a redex) and perform β-reduction.
4
λ-Calculus
Church Encodings
β-reduction is a congruence:
β-reduction
(λx. t) u →β t[x := u]
t→β t′ s→β s′ t→β t′
st→β st′ st→β s′ t λx.t→β λx.t′
This means we can pick any reducible subexpression (called a redex) and perform β-reduction.
Example:
(λx. λy. f (y x)) 5 (λx. x)
5
λ-Calculus
Church Encodings
β-reduction is a congruence:
β-reduction
(λx. t) u →β t[x := u]
t→β t′ s→β s′ t→β t′
st→β st′ st→β s′ t λx.t→β λx.t′
This means we can pick any reducible subexpression (called a redex) and perform β-reduction.
Example:
(λx.λy.f (y x))5(λx.x) →β (λy.f (y 5))(λx.x)
6
λ-Calculus
Church Encodings
β-reduction is a congruence:
β-reduction
(λx. t) u →β t[x := u]
t→β t′ s→β s′ t→β t′
st→β st′ st→β s′ t λx.t→β λx.t′
This means we can pick any reducible subexpression (called a redex) and perform β-reduction.
Example:
(λx.λy.f (y x))5(λx.x) →β (λy.f (y 5))(λx.x) →β f ((λx. x) 5)
7
λ-Calculus
Church Encodings
β-reduction is a congruence:
β-reduction
(λx. t) u →β t[x := u]
t→β t′ s→β s′ t→β t′
st→β st′ st→β s′ t λx.t→β λx.t′
This means we can pick any reducible subexpression (called a redex) and perform β-reduction.
Example:
(λx.λy.f (y x))5(λx.x) →β (λy.f (y 5))(λx.x) →β f ((λx. x) 5)
→β f5
8
λ-Calculus
Church Encodings
Confluence
Supposing we arrive via one reduction path to an expression that cannot be reduced further (called a normal form), then any other reduction path will result in the same normal form.
λ-Calculus
Church Encodings
Confluence
Supposing we arrive via one reduction path to an expression that cannot be reduced further (called a normal form), then any other reduction path will result in the same normal form.
(λa. a) ((λy. f y) 5)
(λy. f y) 5
f5
λ-Calculus
Church Encodings
Confluence
Supposing we arrive via one reduction path to an expression that cannot be reduced further (called a normal form), then any other reduction path will result in the same normal form.
(λa. a) ((λy. f y) 5)
(λy.f y)5
(λa.a)(f 5)
f5
11
λ-Calculus
Church Encodings
Equivalence
Confluence means we can define another notion of equivalence, which equates more than α-equivalence. Two terms are αβ-equivalent, written s ≡αβ t if they β-reduce to α-equivalent normal forms.
12
λ-Calculus
Church Encodings
Equivalence
Confluence means we can define another notion of equivalence, which equates more than α-equivalence. Two terms are αβ-equivalent, written s ≡αβ t if they β-reduce to α-equivalent normal forms.
η
There is also another equation that cannot be proven from β-equivalence alone, called η-reduction:
(λx. f x) →η f
Adding this reduction to the system preserves confluence and uniqueness of normal forms, so we have a notion of αβη-equivalence also.
13
λ-Calculus
Church Encodings
Does every term in λ-calculus have a normal form?
Normal Forms
14
λ-Calculus
Church Encodings
Does every term in λ-calculus have a normal form? (λx. x x)(λx. x x)
Try to β-reduce this! (the answer is that it doesn’t have a normal form)
Normal Forms
15
λ-Calculus
Church Encodings
Why learn this stuff?
λ-calculus is a Turing-complete programming language.
λ-calculus is the foundation for every functional programming language and some
non-functional ones.
λ-calculus is the foundation of Higher Order Logic and Type Theory, the two main foundations used for mathematics in interactive proof assistants.
λ-calculus is the smallest example of a usable programming language, so it’s good for teaching about programming languages.
16
λ-Calculus
Church Encodings
Making λ-Calculus Usable
In order to demonstrate that λ calculus is actually a usable programming language, we will demonstrate how to encode booleans and natural numbers as λ-terms, along with their operations.
General Idea
We transform a data type into the type of its eliminator. In other words, we make a function that can serve the same purpose as the data type at its use sites.
17
λ-Calculus
Church Encodings
How do we use booleans?
Booleans
18
λ-Calculus
Church Encodings
Booleans
How do we use booleans? To choose between two results!
19
λ-Calculus
Church Encodings
Booleans
How do we use booleans? To choose between two results!
So, a boolean will be a function that, given two arguments, returns the first one if it is
true and the second one if it is false:
True ≡ λa. λb. a False ≡ λa. λb. b
How do we write conjunction? to board
20
λ-Calculus
Church Encodings
Booleans
How do we use booleans? To choose between two results!
So, a boolean will be a function that, given two arguments, returns the first one if it is
true and the second one if it is false:
True ≡ λa. λb. a False ≡ λa. λb. b
How do we write conjunction? to board
And ≡ λp.λq.pqp
21
λ-Calculus
Church Encodings
Booleans
How do we use booleans? To choose between two results!
So, a boolean will be a function that, given two arguments, returns the first one if it is
true and the second one if it is false:
True ≡ λa. λb. a False ≡ λa. λb. b
How do we write conjunction? to board
And ≡ λp.λq.pqp
Example (Test it out!)
Try β-normalising And True False.
22
λ-Calculus
Church Encodings
Booleans
How do we use booleans? To choose between two results!
So, a boolean will be a function that, given two arguments, returns the first one if it is
true and the second one if it is false:
True ≡ λa. λb. a False ≡ λa. λb. b
How do we write conjunction? to board
And ≡ λp.λq.pqp
Example (Test it out!)
Try β-normalising And True False. What about Or?
23
λ-Calculus
Church Encodings
Natural Numbers
How do we use natural numbers?
24
λ-Calculus
Church Encodings
Natural Numbers
How do we use natural numbers? To do something n times!
25
λ-Calculus
Church Encodings
Natural Numbers
How do we use natural numbers? To do something n times!
So, a natural number will be a function that takes a function f and a value x, and
applies the function f to x that number of times:
How do we write Suc?
Zero ≡ λf.λx.x
One ≡λf.λx.fx Two ≡ λf.λx.f(fx) …
26
λ-Calculus
Church Encodings
Natural Numbers
How do we use natural numbers? To do something n times!
So, a natural number will be a function that takes a function f and a value x, and
applies the function f to x that number of times:
How do we write Suc?
Zero ≡ λf.λx.x
One ≡λf.λx.fx Two ≡ λf.λx.f(fx) …
Suc ≡ λn.λf.λx.f (nf x)
27
λ-Calculus
Church Encodings
Natural Numbers
How do we use natural numbers? To do something n times!
So, a natural number will be a function that takes a function f and a value x, and
applies the function f to x that number of times:
How do we write Suc? How do we write Add?
Zero ≡ λf.λx.x
One ≡λf.λx.fx Two ≡ λf.λx.f(fx) …
Suc ≡ λn.λf.λx.f (nf x)
28
λ-Calculus
Church Encodings
Natural Numbers
How do we use natural numbers? To do something n times!
So, a natural number will be a function that takes a function f and a value x, and
applies the function f to x that number of times:
How do we write Suc?
How do we write Add?
Zero ≡ λf.λx.x
One ≡λf.λx.fx Two ≡ λf.λx.f(fx) …
Suc ≡ λn.λf.λx.f (nf x) Add ≡ λm.λn.λf.λx.mf (nf x)
29
λ-Calculus
Church Encodings
Natural Numbers
How do we use natural numbers? To do something n times!
So, a natural number will be a function that takes a function f and a value x, and
applies the function f to x that number of times:
How do we write Suc?
How do we write Add?
Zero ≡ λf.λx.x
One ≡λf.λx.fx Two ≡ λf.λx.f(fx) …
Suc ≡ λn.λf.λx.f (nf x) Add ≡ λm.λn.λf.λx.mf (nf x)
30
λ-Calculus
Church Encodings
Natural Number Practice
Example
Try β-normalising Suc One. Example
Try writing a different λ-term for defining Suc.
Example
Try writing a λ-term for defining Multiply.
31