COMP2022: Formal Languages and Logic – 2018, Semester 2, Week 3
COMP2022: Formal Languages and Logic
2018, Semester 2, Week 3
Joseph Godbehere
16th August, 2018
COMMONWEALTH OF AUSTRALIA
Copyright Regulations 1969
WARNING
This material has been reproduced and communicated to you by or
on behalf of the University of Sydney pursuant to part VB of the
Copyright Act 1968 (the Act).
The material in this communication may be subject to copyright
under the Act. Any further copying or communication of this
material by you may be subject of copyright protect under the Act.
Do not remove this notice.
Revision Combinators Encodings Functional programming Review
outline
▶ Revision – Lambda Calculus
▶ Y Combinator
▶ Encodings
▶ numbers (a different way)
▶ pairs
▶ lists
▶ Functional Programming
3/60
Revision Combinators Encodings Functional programming Review
When are α-reductions required?
If they never change the meaning, why bother?
▶ Readability
▶ β-reduction assumes all variables have different labels
▶ Usually it doesn’t matter…
▶ … except when it does!
▶ … even worse – it’s not enough to only look at the subformula
being reduced
4/60
Revision Combinators Encodings Functional programming Review
WRONG
λx .(λyx .y)x
= λx .(λx .x )
(mistake!)
= λx .(λy .y)
= λxy .y
= FALSE
▶ Where is the error?
▶ Why is it a mistake?
▶ x was bound to the first λ, but on line 2 it is not! Free
variables in N should not become bound in M [x := N ]
5/60
Revision Combinators Encodings Functional programming Review
WRONG
λx .(λyx .y)x
= λx .(λx .x ) (mistake!)
= λx .(λy .y)
= λxy .y
= FALSE
▶ Where is the error?
▶ Why is it a mistake?
▶ x was bound to the first λ, but on line 2 it is not! Free
variables in N should not become bound in M [x := N ]
5/60
Revision Combinators Encodings Functional programming Review
WRONG
λx .(λyx .y)x
= λx .(λx .x ) (mistake!)
= λx .(λy .y)
= λxy .y
= FALSE
▶ Where is the error?
▶ Why is it a mistake?
▶ x was bound to the first λ, but on line 2 it is not! Free
variables in N should not become bound in M [x := N ]
5/60
Revision Combinators Encodings Functional programming Review
CORRECT
λx .(λyx .y)x
= λx .(λyz .y)x (α)
= λx .(λz .x ) (β)
= λxz .x
= TRUE
Rule of thumb: always perform α reductions before β reductions.
▶ sometimes it’s necessary
▶ usually makes the formula easier to read too
6/60
Revision Combinators Encodings Functional programming Review
η-reduction (Eta)
If x is not free in M , then we can write:
λx .Mx = M
Idea: any input applied to this will simply be applied to M
▶ If x is not free in M , then (λx .Mx )N = Mx [x := N ] = MN
▶ Identical to applying N to M directly.
Uses:
▶ It can simplify some arguments a little
▶ e.g. λx .(λy .y)x = λy .y
▶ It can help to convert expressions to ’point free’ form (where
they do not label their variables).
▶ Point-free programs can be easier to reason about, but are
often difficult to read.
7/60
Revision Combinators Encodings Functional programming Review
η-reduction (Eta)
If x is not free in M , then we can write:
λx .Mx = M
Idea: any input applied to this will simply be applied to M
▶ If x is not free in M , then (λx .Mx )N = Mx [x := N ] = MN
▶ Identical to applying N to M directly.
Uses:
▶ It can simplify some arguments a little
▶ e.g. λx .(λy .y)x = λy .y
▶ It can help to convert expressions to ’point free’ form (where
they do not label their variables).
▶ Point-free programs can be easier to reason about, but are
often difficult to read.
7/60
Revision Combinators Encodings Functional programming Review
η-reduction (Eta)
If x is not free in M , then we can write:
λx .Mx = M
Idea: any input applied to this will simply be applied to M
▶ If x is not free in M , then (λx .Mx )N = Mx [x := N ] = MN
▶ Identical to applying N to M directly.
Uses:
▶ It can simplify some arguments a little
▶ e.g. λx .(λy .y)x = λy .y
▶ It can help to convert expressions to ’point free’ form (where
they do not label their variables).
▶ Point-free programs can be easier to reason about, but are
often difficult to read.
7/60
Revision Combinators Encodings Functional programming Review
outline
▶ Revision – Lambda Calculus
▶ Y Combinator
▶ Encodings
▶ numbers (a different way)
▶ pairs
▶ lists
▶ Functional Programming
8/60
Revision Combinators Encodings Functional programming Review
Necessary Logical Notation: Quantifiers
▶ “for all possible values of X …” denoted ∀X
▶ “there exists a value of X such that …” denoted ∃X
Examples (for all positive rational numbers)
▶ “∀x (x ∗ 1 = x )” is true
▶ “∃x (x + 1 = 4)” is true (choose x = 3)
▶ “∀x (x + 1 = 4)” is false (e.g. false on x = 1)
▶ “∃x∀y (xy = 0)” is true (choose x = 0)
▶ “∃x∀y (xy = 1)” is false (whatever we choose for x , we’ll be
able to find a y that doesn’t work)
▶ “∀x∃y (xy = 1)” is true (for any x , we can choose y = 1
x
)
9/60
Revision Combinators Encodings Functional programming Review
Combinators
A combinator is any expression M which contains no free variables.
Example:
▶ λxy .xyz is not a combinator (z is free)
▶ λxy .xyy is a combinator (all variables bound)
Combinators combine values into expressions without relying on
quantifiers or explicitly defining variables.
10/60
Revision Combinators Encodings Functional programming Review
Combinators
A combinator is any expression M which contains no free variables.
Example:
▶ λxy .xyz is not a combinator (z is free)
▶ λxy .xyy is a combinator (all variables bound)
Combinators combine values into expressions without relying on
quantifiers or explicitly defining variables.
10/60
Revision Combinators Encodings Functional programming Review
Combinators
A combinator is any expression M which contains no free variables.
Example:
▶ λxy .xyz is not a combinator (z is free)
▶ λxy .xyy is a combinator (all variables bound)
Combinators combine values into expressions without relying on
quantifiers or explicitly defining variables.
10/60
Revision Combinators Encodings Functional programming Review
Combinators
A combinator is any expression M which contains no free variables.
Example:
▶ λxy .xyz is not a combinator (z is free)
▶ λxy .xyy is a combinator (all variables bound)
Combinators combine values into expressions without relying on
quantifiers or explicitly defining variables.
10/60
Revision Combinators Encodings Functional programming Review
Combinator examples
Standard combinators:
▶ I = λx .x (identity)
▶ K = λxy .x (true)
▶ K∗ = λxy .y (false)
▶ S = λxyz .xz (yz ) (generalisation of application)
We can easily deduce (by using β reduction):
▶ IM = M
▶ KMN = M
▶ K∗MN = N
▶ SMNL = ML(NL)
Interestingly, these λ-free combinators are sufficient to make
expressions equal to any λ term. We will not talk about that
further today though.
11/60
Revision Combinators Encodings Functional programming Review
Combinator examples
Standard combinators:
▶ I = λx .x (identity)
▶ K = λxy .x (true)
▶ K∗ = λxy .y (false)
▶ S = λxyz .xz (yz ) (generalisation of application)
We can easily deduce (by using β reduction):
▶ IM = M
▶ KMN = M
▶ K∗MN = N
▶ SMNL = ML(NL)
Interestingly, these λ-free combinators are sufficient to make
expressions equal to any λ term. We will not talk about that
further today though.
11/60
Revision Combinators Encodings Functional programming Review
Combinator examples
Standard combinators:
▶ I = λx .x (identity)
▶ K = λxy .x (true)
▶ K∗ = λxy .y (false)
▶ S = λxyz .xz (yz ) (generalisation of application)
We can easily deduce (by using β reduction):
▶ IM = M
▶ KMN = M
▶ K∗MN = N
▶ SMNL = ML(NL)
Interestingly, these λ-free combinators are sufficient to make
expressions equal to any λ term. We will not talk about that
further today though.
11/60
Revision Combinators Encodings Functional programming Review
Solving simple equations
∃G ∀X GX = XXX
(Where X , F are expressions in the lambda calculus)
“There exists some G such that for all X it’s true that
GC = XXX ”
Proof:
▶ Let G = λx .xxx
▶ Then GX = (λx .xxx )X = XXX
That was easy… But what if we need to reason about a recursive
function?
12/60
Revision Combinators Encodings Functional programming Review
Solving simple equations
∃G ∀X GX = XXX
(Where X , F are expressions in the lambda calculus)
“There exists some G such that for all X it’s true that
GC = XXX ”
Proof:
▶ Let G = λx .xxx
▶ Then GX = (λx .xxx )X = XXX
That was easy… But what if we need to reason about a recursive
function?
12/60
Revision Combinators Encodings Functional programming Review
Solving simple equations
∃G ∀X GX = XXX
(Where X , F are expressions in the lambda calculus)
“There exists some G such that for all X it’s true that
GC = XXX ”
Proof:
▶ Let G = λx .xxx
▶ Then GX = (λx .xxx )X = XXX
That was easy… But what if we need to reason about a recursive
function?
12/60
Revision Combinators Encodings Functional programming Review
Solving simple equations
∃G ∀X GX = XXX
(Where X , F are expressions in the lambda calculus)
“There exists some G such that for all X it’s true that
GC = XXX ”
Proof:
▶ Let G = λx .xxx
▶ Then GX = (λx .xxx )X = XXX
That was easy… But what if we need to reason about a recursive
function?
12/60
Revision Combinators Encodings Functional programming Review
Solving simple equations
∃G ∀X GX = XXX
(Where X , F are expressions in the lambda calculus)
“There exists some G such that for all X it’s true that
GC = XXX ”
Proof:
▶ Let G = λx .xxx
▶ Then GX = (λx .xxx )X = XXX
That was easy… But what if we need to reason about a recursive
function?
12/60
Revision Combinators Encodings Functional programming Review
Fixed Point Combinators
A fixed point combinator is a combinator which has a fixed point.
We say F has a fixed point if ∃X (FX = X )
i.e. some input X exists which, when applied to F , outputs X
again.
13/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (i)
Theorem:
∀F ∃X FX = X
“For all F , there exists some X such that FX = X ”
▶ i.e. all functions have a fixed point
Proof:
Let W = λx .F (xx ) and X = WW . Then:
X = WW (def. of X)
= (λx .F (xx ))W (def. of W)
= F (WW ) (β-reduction)
= FX (def. of X)
14/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (i)
Theorem:
∀F ∃X FX = X
“For all F , there exists some X such that FX = X ”
▶ i.e. all functions have a fixed point
Proof:
Let W = λx .F (xx ) and X = WW . Then:
X = WW (def. of X)
= (λx .F (xx ))W (def. of W)
= F (WW ) (β-reduction)
= FX (def. of X)
14/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (i)
Theorem:
∀F ∃X FX = X
“For all F , there exists some X such that FX = X ”
▶ i.e. all functions have a fixed point
Proof:
Let W = λx .F (xx ) and X = WW . Then:
X =
WW (def. of X)
= (λx .F (xx ))W (def. of W)
= F (WW ) (β-reduction)
= FX (def. of X)
14/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (i)
Theorem:
∀F ∃X FX = X
“For all F , there exists some X such that FX = X ”
▶ i.e. all functions have a fixed point
Proof:
Let W = λx .F (xx ) and X = WW . Then:
X = WW (def. of X)
=
(λx .F (xx ))W (def. of W)
= F (WW ) (β-reduction)
= FX (def. of X)
14/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (i)
Theorem:
∀F ∃X FX = X
“For all F , there exists some X such that FX = X ”
▶ i.e. all functions have a fixed point
Proof:
Let W = λx .F (xx ) and X = WW . Then:
X = WW (def. of X)
= (λx .F (xx ))W (def. of W)
=
F (WW ) (β-reduction)
= FX (def. of X)
14/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (i)
Theorem:
∀F ∃X FX = X
“For all F , there exists some X such that FX = X ”
▶ i.e. all functions have a fixed point
Proof:
Let W = λx .F (xx ) and X = WW . Then:
X = WW (def. of X)
= (λx .F (xx ))W (def. of W)
= F (WW ) (β-reduction)
=
FX (def. of X)
14/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (i)
Theorem:
∀F ∃X FX = X
“For all F , there exists some X such that FX = X ”
▶ i.e. all functions have a fixed point
Proof:
Let W = λx .F (xx ) and X = WW . Then:
X = WW (def. of X)
= (λx .F (xx ))W (def. of W)
= F (WW ) (β-reduction)
= FX (def. of X)
14/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (ii)
There is a fixed point combinator (the “Y Combinator”)
Y = λf .
(
λx .f (xx )
)(
λx .f (xx )
)
such that
∀F F (YF ) = YF
Proof:
YF =
(
λf .
(
λx .f (xx )
)(
λx .f (xx )
))
F (defn. of Y )
=
(
λx .F (xx )
)(
λx .F (xx )
)
(β − reduction)
= F
((
λx .F (xx )
)(
λx .F (xx )
))
(by pf. of theorem (i))
= F (YF ) (by equality above)
15/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (ii)
There is a fixed point combinator (the “Y Combinator”)
Y = λf .
(
λx .f (xx )
)(
λx .f (xx )
)
such that
∀F F (YF ) = YF
Proof:
YF =
(
λf .
(
λx .f (xx )
)(
λx .f (xx )
))
F (defn. of Y )
=
(
λx .F (xx )
)(
λx .F (xx )
)
(β − reduction)
= F
((
λx .F (xx )
)(
λx .F (xx )
))
(by pf. of theorem (i))
= F (YF ) (by equality above)
15/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (ii)
There is a fixed point combinator (the “Y Combinator”)
Y = λf .
(
λx .f (xx )
)(
λx .f (xx )
)
such that
∀F F (YF ) = YF
Proof:
YF =
(
λf .
(
λx .f (xx )
)(
λx .f (xx )
))
F (defn. of Y )
=
(
λx .F (xx )
)(
λx .F (xx )
)
(β − reduction)
=
F
((
λx .F (xx )
)(
λx .F (xx )
))
(by pf. of theorem (i))
= F (YF ) (by equality above)
15/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (ii)
There is a fixed point combinator (the “Y Combinator”)
Y = λf .
(
λx .f (xx )
)(
λx .f (xx )
)
such that
∀F F (YF ) = YF
Proof:
YF =
(
λf .
(
λx .f (xx )
)(
λx .f (xx )
))
F (defn. of Y )
=
(
λx .F (xx )
)(
λx .F (xx )
)
(β − reduction)
= F
((
λx .F (xx )
)(
λx .F (xx )
))
(by pf. of theorem (i))
=
F (YF ) (by equality above)
15/60
Revision Combinators Encodings Functional programming Review
Fixed point theorem (ii)
There is a fixed point combinator (the “Y Combinator”)
Y = λf .
(
λx .f (xx )
)(
λx .f (xx )
)
such that
∀F F (YF ) = YF
Proof:
YF =
(
λf .
(
λx .f (xx )
)(
λx .f (xx )
))
F (defn. of Y )
=
(
λx .F (xx )
)(
λx .F (xx )
)
(β − reduction)
= F
((
λx .F (xx )
)(
λx .F (xx )
))
(by pf. of theorem (i))
= F (YF ) (by equality above)
15/60
Revision Combinators Encodings Functional programming Review
Y Combinator
So, uh… Why is this interesting?
1. Good news: it allows us to write self recursive functions
▶ it effectively lets us define variables
2. Bad news: it leads to Curry’s Paradox, and the
incompleteness of lamdba calculus
▶ not all valid expressions can be proved / computed
16/60
Revision Combinators Encodings Functional programming Review
Y Combinator
So, uh… Why is this interesting?
1. Good news: it allows us to write self recursive functions
▶ it effectively lets us define variables
2. Bad news: it leads to Curry’s Paradox, and the
incompleteness of lamdba calculus
▶ not all valid expressions can be proved / computed
16/60
Revision Combinators Encodings Functional programming Review
Y Combinator
So, uh… Why is this interesting?
1. Good news: it allows us to write self recursive functions
▶ it effectively lets us define variables
2. Bad news: it leads to Curry’s Paradox, and the
incompleteness of lamdba calculus
▶ not all valid expressions can be proved / computed
16/60
Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f (n) = if (n == 0) then 1 else n ∗ f (n − 1)
We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n(x )
▶ This notation, indicating n repetitions of f (…) is a little
dangerous (but convenient)
▶ Be aware that Church numerals have the form:
λfz .f (f (f (f (fz )))) ̸= λfz .fffffz
17/60
Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f (n) = if (n == 0) then 1 else n ∗ f (n − 1)
We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n(x )
▶ This notation, indicating n repetitions of f (…) is a little
dangerous (but convenient)
▶ Be aware that Church numerals have the form:
λfz .f (f (f (f (fz )))) ̸= λfz .fffffz
17/60
Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f (n) = if (n == 0) then 1 else n ∗ f (n − 1)
We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n(x )
▶ This notation, indicating n repetitions of f (…) is a little
dangerous (but convenient)
▶ Be aware that Church numerals have the form:
λfz .f (f (f (f (fz )))) ̸= λfz .fffffz
17/60
Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f (n) = if (n == 0) then 1 else n ∗ f (n − 1)
We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n(x )
▶ ISZERO := λn.n (λx .FALSE ) TRUE
▶ Returns TRUE if the argument is a Church zero, FALSE if it’s
any other Church numeral
18/60
Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f (n) = if (n == 0) then 1 else n ∗ f (n − 1)
We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n(x )
▶ ISZERO := λn.n (λx .FALSE ) TRUE
▶ Returns TRUE if the argument is a Church zero, FALSE if it’s
any other Church numeral
18/60
Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
=
(λn.n (λx .FALSE ) TRUE ) ZERO (def. ISZERO)
=
ZERO (λx .FALSE ) TRUE (β)
=
(λfz .z ) (λx .FALSE ) TRUE (def .ZERO)
=
(λz .z ) TRUE (β)
=
TRUE (β)
19/60
Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= (λn.n (λx .FALSE ) TRUE ) ZERO (def. ISZERO)
=
ZERO (λx .FALSE ) TRUE (β)
=
(λfz .z ) (λx .FALSE ) TRUE (def .ZERO)
=
(λz .z ) TRUE (β)
=
TRUE (β)
19/60
Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= (λn.n (λx .FALSE ) TRUE ) ZERO (def. ISZERO)
= ZERO (λx .FALSE ) TRUE (β)
=
(λfz .z ) (λx .FALSE ) TRUE (def .ZERO)
=
(λz .z ) TRUE (β)
=
TRUE (β)
19/60
Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= (λn.n (λx .FALSE ) TRUE ) ZERO (def. ISZERO)
= ZERO (λx .FALSE ) TRUE (β)
= (λfz .z ) (λx .FALSE ) TRUE (def .ZERO)
=
(λz .z ) TRUE (β)
=
TRUE (β)
19/60
Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= (λn.n (λx .FALSE ) TRUE ) ZERO (def. ISZERO)
= ZERO (λx .FALSE ) TRUE (β)
= (λfz .z ) (λx .FALSE ) TRUE (def .ZERO)
= (λz .z ) TRUE (β)
=
TRUE (β)
19/60
Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= (λn.n (λx .FALSE ) TRUE ) ZERO (def. ISZERO)
= ZERO (λx .FALSE ) TRUE (β)
= (λfz .z ) (λx .FALSE ) TRUE (def .ZERO)
= (λz .z ) TRUE (β)
= TRUE (β)
19/60
Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
=
(λn.n (λx .FALSE ) TRUE ) ONE (def. ISZERO)
=
ONE (λx .FALSE ) TRUE (β)
=
(λfz .fz ) (λx .FALSE ) TRUE (def .ONE )
=
(λz .(λx .FALSE )z ) TRUE (β)
=
(λx .FALSE )TRUE (β)
=
FALSE (β)
20/60
Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx .FALSE ) TRUE ) ONE (def. ISZERO)
=
ONE (λx .FALSE ) TRUE (β)
=
(λfz .fz ) (λx .FALSE ) TRUE (def .ONE )
=
(λz .(λx .FALSE )z ) TRUE (β)
=
(λx .FALSE )TRUE (β)
=
FALSE (β)
20/60
Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx .FALSE ) TRUE ) ONE (def. ISZERO)
= ONE (λx .FALSE ) TRUE (β)
=
(λfz .fz ) (λx .FALSE ) TRUE (def .ONE )
=
(λz .(λx .FALSE )z ) TRUE (β)
=
(λx .FALSE )TRUE (β)
=
FALSE (β)
20/60
Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx .FALSE ) TRUE ) ONE (def. ISZERO)
= ONE (λx .FALSE ) TRUE (β)
= (λfz .fz ) (λx .FALSE ) TRUE (def .ONE )
=
(λz .(λx .FALSE )z ) TRUE (β)
=
(λx .FALSE )TRUE (β)
=
FALSE (β)
20/60
Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx .FALSE ) TRUE ) ONE (def. ISZERO)
= ONE (λx .FALSE ) TRUE (β)
= (λfz .fz ) (λx .FALSE ) TRUE (def .ONE )
= (λz .(λx .FALSE )z ) TRUE (β)
=
(λx .FALSE )TRUE (β)
=
FALSE (β)
20/60
Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx .FALSE ) TRUE ) ONE (def. ISZERO)
= ONE (λx .FALSE ) TRUE (β)
= (λfz .fz ) (λx .FALSE ) TRUE (def .ONE )
= (λz .(λx .FALSE )z ) TRUE (β)
= (λx .FALSE )TRUE (β)
=
FALSE (β)
20/60
Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx .FALSE ) TRUE ) ONE (def. ISZERO)
= ONE (λx .FALSE ) TRUE (β)
= (λfz .fz ) (λx .FALSE ) TRUE (def .ONE )
= (λz .(λx .FALSE )z ) TRUE (β)
= (λx .FALSE )TRUE (β)
= FALSE (β)
20/60
Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f (n) = if (n == 0) then 1 else n ∗ f (n − 1)
We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n(x )
▶ ISZERO := λn.n (λx .FALSE ) TRUE
▶ MULT := λxyz .x (yz ) (seen previously)
▶ PRED := λnfx .n(λgh.h(gf ))(λy .x )(λu.u)
▶ This gives the predecessor of a number
▶ PRED 1 = 0, PRED 2 = 1, …, PRED n = (n-1)
▶ The derivation of this is much longer than for the operations
which increase numbers
▶ Subtraction and division are also difficult!
21/60
Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f (n) = if (n == 0) then 1 else n ∗ f (n − 1)
We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n(x )
▶ ISZERO := λn.n (λx .FALSE ) TRUE
▶ MULT := λxyz .x (yz ) (seen previously)
▶ PRED := λnfx .n(λgh.h(gf ))(λy .x )(λu.u)
▶ This gives the predecessor of a number
▶ PRED 1 = 0, PRED 2 = 1, …, PRED n = (n-1)
▶ The derivation of this is much longer than for the operations
which increase numbers
▶ Subtraction and division are also difficult!
21/60
Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f (n) = if (n == 0) then 1 else n ∗ f (n − 1)
We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n(x )
▶ ISZERO := λn.n (λx .FALSE ) TRUE
▶ MULT := λxyz .x (yz ) (seen previously)
▶ PRED := λnfx .n(λgh.h(gf ))(λy .x )(λu.u)
▶ This gives the predecessor of a number
▶ PRED 1 = 0, PRED 2 = 1, …, PRED n = (n-1)
▶ The derivation of this is much longer than for the operations
which increase numbers
▶ Subtraction and division are also difficult!
21/60
Revision Combinators Encodings Functional programming Review
PRED TWO… is a monster
PRED TWO = λnfx .n(λgh.h(gf ))(λy .x )(λu.u) TWO
= λfx .TWO (λgh.h(gf ))(λy .x )(λu.u)
= λfx .(λab.a(ab))(λgh.h(gf ))(λy .x )(λu.u)
= λfx .
(
λb.
(
λgh.h(gf )
)(
(λgh.h(gf ))b
))
(λy .x )(λu.u)
= λfx .
(
λgh.h(gf )
)((
λgh.h(gf )
)
(λy .x )
)
(λu.u)
= λfx .
(
λgh.h(gf )
)((
λh.h((λy .x )f )
))
(λu.u)
= λfx .
(
λgh.h(gf )
)
(λh.hx )(λu.u)
= λfx .
(
λgh.h(gf )
)
(λi .ix )(λu.u)
= λfx .
(
λh.h((λi .ix )f )
)
(λu.u)
= λfx .(λh.h(fx ))(λu.u)
= λfx .(λu.u)(fx )) = λfx .fx = ONE
22/60
Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f (n) = if (n == 0) then 1 else n ∗ f (n − 1)
We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n(x )
▶ ISZERO := λn.n (λx .FALSE ) TRUE
▶ MULT := λxyz .x (yz )
▶ PRED := λnfx .n(λgh.h(gf ))(λy .x )(λu.u)
23/60
Revision Combinators Encodings Functional programming Review
Recursion example
We want to write something like:
“FACT n = (ISZERO n) 1 (MULT n (FACT (PRED n)))”
We can’t directly define functions self referentially, so we use the Y
Combinator:
▶ H = λfn.(ISZERO n) 1
(
MULT n (f (PRED n))
)
▶ H takes a function and a number. If the number is zero, it
returns 1, otherwise it returns the product of n and f(n-1)
▶ FACTORIAL = Y H
▶ Because YH = H (YH ), the Y Combinator helps us to apply
the H function to itself
24/60
Revision Combinators Encodings Functional programming Review
Recursion example
We want to write something like:
“FACT n = (ISZERO n) 1 (MULT n (FACT (PRED n)))”
We can’t directly define functions self referentially, so we use the Y
Combinator:
▶ H = λfn.(ISZERO n) 1
(
MULT n (f (PRED n))
)
▶ H takes a function and a number. If the number is zero, it
returns 1, otherwise it returns the product of n and f(n-1)
▶ FACTORIAL = Y H
▶ Because YH = H (YH ), the Y Combinator helps us to apply
the H function to itself
24/60
Revision Combinators Encodings Functional programming Review
Recursion example
We want to write something like:
“FACT n = (ISZERO n) 1 (MULT n (FACT (PRED n)))”
We can’t directly define functions self referentially, so we use the Y
Combinator:
▶ H = λfn.(ISZERO n) 1
(
MULT n (f (PRED n))
)
▶ H takes a function and a number. If the number is zero, it
returns 1, otherwise it returns the product of n and f(n-1)
▶ FACTORIAL = Y H
▶ Because YH = H (YH ), the Y Combinator helps us to apply
the H function to itself
24/60
Revision Combinators Encodings Functional programming Review
Factorial 5(overview)
▶ H = λfn.(ISZERO n) 1
(
MULT n (f (PRED n))
)
▶ FACTORIAL = Y H
H takes a function f and a number n. It returns 1 if the number is
0, otherwise the product of n and f (n − 1)
FACTORIAL 5
= (Y H ) 5
= H (Y H ) 5 (Y Combinator!)
= 5 ∗ ((Y H ) 4) (because 5 ̸= 0)
= …
= 120 ∗ ((Y H ) 0)
= 120 ∗ 1 = 120
25/60
Revision Combinators Encodings Functional programming Review
Factorial 5(overview)
▶ H = λfn.(ISZERO n) 1
(
MULT n (f (PRED n))
)
▶ FACTORIAL = Y H
H takes a function f and a number n. It returns 1 if the number is
0, otherwise the product of n and f (n − 1)
FACTORIAL 5 = (Y H ) 5
= H (Y H ) 5 (Y Combinator!)
= 5 ∗ ((Y H ) 4) (because 5 ̸= 0)
= …
= 120 ∗ ((Y H ) 0)
= 120 ∗ 1 = 120
25/60
Revision Combinators Encodings Functional programming Review
Factorial 5(overview)
▶ H = λfn.(ISZERO n) 1
(
MULT n (f (PRED n))
)
▶ FACTORIAL = Y H
H takes a function f and a number n. It returns 1 if the number is
0, otherwise the product of n and f (n − 1)
FACTORIAL 5 = (Y H ) 5
= H (Y H ) 5 (Y Combinator!)
= 5 ∗ ((Y H ) 4) (because 5 ̸= 0)
= …
= 120 ∗ ((Y H ) 0)
= 120 ∗ 1 = 120
25/60
Revision Combinators Encodings Functional programming Review
Factorial 5(overview)
▶ H = λfn.(ISZERO n) 1
(
MULT n (f (PRED n))
)
▶ FACTORIAL = Y H
H takes a function f and a number n. It returns 1 if the number is
0, otherwise the product of n and f (n − 1)
FACTORIAL 5 = (Y H ) 5
= H (Y H ) 5 (Y Combinator!)
= 5 ∗ ((Y H ) 4) (because 5 ̸= 0)
= …
= 120 ∗ ((Y H ) 0)
= 120 ∗ 1 = 120
25/60
Revision Combinators Encodings Functional programming Review
Factorial 5(overview)
▶ H = λfn.(ISZERO n) 1
(
MULT n (f (PRED n))
)
▶ FACTORIAL = Y H
H takes a function f and a number n. It returns 1 if the number is
0, otherwise the product of n and f (n − 1)
FACTORIAL 5 = (Y H ) 5
= H (Y H ) 5 (Y Combinator!)
= 5 ∗ ((Y H ) 4) (because 5 ̸= 0)
= …
= 120 ∗ ((Y H ) 0)
= 120 ∗ 1 = 120
25/60
Revision Combinators Encodings Functional programming Review
Factorial 5(overview)
▶ H = λfn.(ISZERO n) 1
(
MULT n (f (PRED n))
)
▶ FACTORIAL = Y H
H takes a function f and a number n. It returns 1 if the number is
0, otherwise the product of n and f (n − 1)
FACTORIAL 5 = (Y H ) 5
= H (Y H ) 5 (Y Combinator!)
= 5 ∗ ((Y H ) 4) (because 5 ̸= 0)
= …
= 120 ∗ ((Y H ) 0)
= 120 ∗ 1 = 120
25/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3
=
Y H 3
=
H (Y H ) 3 (Y Combinator)
=
(
λfn.(ISZERO n)1
(
MULT n
(
f (PRED n)
)))
(YH )3 (H)
=
(
λn.(ISZERO n) 1
(
MULT n
(
YH (PRED n)
)))
3 (β)
=
(ISZERO 3) 1
(
MULT 3
(
Y H (PRED 3)
))
(β)
=
… = FALSE 1
(
MULT 3
(
Y H (PRED 3)
))
(3 ̸= 0)
=
… = MULT 3
(
Y H (PRED 3)
)
(def. FALSE )
=
… = MULT 3 (Y H 2) (PRED 3 = 2)
26/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3
= Y H 3
=
H (Y H ) 3 (Y Combinator)
=
(
λfn.(ISZERO n)1
(
MULT n
(
f (PRED n)
)))
(YH )3 (H)
=
(
λn.(ISZERO n) 1
(
MULT n
(
YH (PRED n)
)))
3 (β)
=
(ISZERO 3) 1
(
MULT 3
(
Y H (PRED 3)
))
(β)
=
… = FALSE 1
(
MULT 3
(
Y H (PRED 3)
))
(3 ̸= 0)
=
… = MULT 3
(
Y H (PRED 3)
)
(def. FALSE )
=
… = MULT 3 (Y H 2) (PRED 3 = 2)
26/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3
= Y H 3
= H (Y H ) 3 (Y Combinator)
=
(
λfn.(ISZERO n)1
(
MULT n
(
f (PRED n)
)))
(YH )3 (H)
=
(
λn.(ISZERO n) 1
(
MULT n
(
YH (PRED n)
)))
3 (β)
=
(ISZERO 3) 1
(
MULT 3
(
Y H (PRED 3)
))
(β)
=
… = FALSE 1
(
MULT 3
(
Y H (PRED 3)
))
(3 ̸= 0)
=
… = MULT 3
(
Y H (PRED 3)
)
(def. FALSE )
=
… = MULT 3 (Y H 2) (PRED 3 = 2)
26/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3
= Y H 3
= H (Y H ) 3 (Y Combinator)
=
(
λfn.(ISZERO n)1
(
MULT n
(
f (PRED n)
)))
(YH )3 (H)
=
(
λn.(ISZERO n) 1
(
MULT n
(
YH (PRED n)
)))
3 (β)
=
(ISZERO 3) 1
(
MULT 3
(
Y H (PRED 3)
))
(β)
=
… = FALSE 1
(
MULT 3
(
Y H (PRED 3)
))
(3 ̸= 0)
=
… = MULT 3
(
Y H (PRED 3)
)
(def. FALSE )
=
… = MULT 3 (Y H 2) (PRED 3 = 2)
26/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3
= Y H 3
= H (Y H ) 3 (Y Combinator)
=
(
λfn.(ISZERO n)1
(
MULT n
(
f (PRED n)
)))
(YH )3 (H)
=
(
λn.(ISZERO n) 1
(
MULT n
(
YH (PRED n)
)))
3 (β)
=
(ISZERO 3) 1
(
MULT 3
(
Y H (PRED 3)
))
(β)
=
… = FALSE 1
(
MULT 3
(
Y H (PRED 3)
))
(3 ̸= 0)
=
… = MULT 3
(
Y H (PRED 3)
)
(def. FALSE )
=
… = MULT 3 (Y H 2) (PRED 3 = 2)
26/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3
= Y H 3
= H (Y H ) 3 (Y Combinator)
=
(
λfn.(ISZERO n)1
(
MULT n
(
f (PRED n)
)))
(YH )3 (H)
=
(
λn.(ISZERO n) 1
(
MULT n
(
YH (PRED n)
)))
3 (β)
= (ISZERO 3) 1
(
MULT 3
(
Y H (PRED 3)
))
(β)
=
… = FALSE 1
(
MULT 3
(
Y H (PRED 3)
))
(3 ̸= 0)
=
… = MULT 3
(
Y H (PRED 3)
)
(def. FALSE )
=
… = MULT 3 (Y H 2) (PRED 3 = 2)
26/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3
= Y H 3
= H (Y H ) 3 (Y Combinator)
=
(
λfn.(ISZERO n)1
(
MULT n
(
f (PRED n)
)))
(YH )3 (H)
=
(
λn.(ISZERO n) 1
(
MULT n
(
YH (PRED n)
)))
3 (β)
= (ISZERO 3) 1
(
MULT 3
(
Y H (PRED 3)
))
(β)
= … = FALSE 1
(
MULT 3
(
Y H (PRED 3)
))
(3 ̸= 0)
=
… = MULT 3
(
Y H (PRED 3)
)
(def. FALSE )
=
… = MULT 3 (Y H 2) (PRED 3 = 2)
26/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3
= Y H 3
= H (Y H ) 3 (Y Combinator)
=
(
λfn.(ISZERO n)1
(
MULT n
(
f (PRED n)
)))
(YH )3 (H)
=
(
λn.(ISZERO n) 1
(
MULT n
(
YH (PRED n)
)))
3 (β)
= (ISZERO 3) 1
(
MULT 3
(
Y H (PRED 3)
))
(β)
= … = FALSE 1
(
MULT 3
(
Y H (PRED 3)
))
(3 ̸= 0)
= … = MULT 3
(
Y H (PRED 3)
)
(def. FALSE )
=
… = MULT 3 (Y H 2) (PRED 3 = 2)
26/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3
= Y H 3
= H (Y H ) 3 (Y Combinator)
=
(
λfn.(ISZERO n)1
(
MULT n
(
f (PRED n)
)))
(YH )3 (H)
=
(
λn.(ISZERO n) 1
(
MULT n
(
YH (PRED n)
)))
3 (β)
= (ISZERO 3) 1
(
MULT 3
(
Y H (PRED 3)
))
(β)
= … = FALSE 1
(
MULT 3
(
Y H (PRED 3)
))
(3 ̸= 0)
= … = MULT 3
(
Y H (PRED 3)
)
(def. FALSE )
= … = MULT 3 (Y H 2) (PRED 3 = 2)
26/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 2)
FACTORIAL 3
= … = MULT 3 (Y H 2)
=
… = MULT 3 (MULT 2 (Y H 1))
=
… = MULT 3 (MULT 2 (MULT 1 (Y H 0)))
=
… = …(ISZERO 0) 1…
=
… = MULT 3 (MULT 2 (MULT 1 1))
=
… = MULT 3 (MULT 2 1)
=
… = MULT 3 2
=
… = 6
27/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 2)
FACTORIAL 3
= … = MULT 3 (Y H 2)
= … = MULT 3 (MULT 2 (Y H 1))
=
… = MULT 3 (MULT 2 (MULT 1 (Y H 0)))
=
… = …(ISZERO 0) 1…
=
… = MULT 3 (MULT 2 (MULT 1 1))
=
… = MULT 3 (MULT 2 1)
=
… = MULT 3 2
=
… = 6
27/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 2)
FACTORIAL 3
= … = MULT 3 (Y H 2)
= … = MULT 3 (MULT 2 (Y H 1))
= … = MULT 3 (MULT 2 (MULT 1 (Y H 0)))
=
… = …(ISZERO 0) 1…
=
… = MULT 3 (MULT 2 (MULT 1 1))
=
… = MULT 3 (MULT 2 1)
=
… = MULT 3 2
=
… = 6
27/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 2)
FACTORIAL 3
= … = MULT 3 (Y H 2)
= … = MULT 3 (MULT 2 (Y H 1))
= … = MULT 3 (MULT 2 (MULT 1 (Y H 0)))
= … = …(ISZERO 0) 1…
=
… = MULT 3 (MULT 2 (MULT 1 1))
=
… = MULT 3 (MULT 2 1)
=
… = MULT 3 2
=
… = 6
27/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 2)
FACTORIAL 3
= … = MULT 3 (Y H 2)
= … = MULT 3 (MULT 2 (Y H 1))
= … = MULT 3 (MULT 2 (MULT 1 (Y H 0)))
= … = …(ISZERO 0) 1…
= … = MULT 3 (MULT 2 (MULT 1 1))
=
… = MULT 3 (MULT 2 1)
=
… = MULT 3 2
=
… = 6
27/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 2)
FACTORIAL 3
= … = MULT 3 (Y H 2)
= … = MULT 3 (MULT 2 (Y H 1))
= … = MULT 3 (MULT 2 (MULT 1 (Y H 0)))
= … = …(ISZERO 0) 1…
= … = MULT 3 (MULT 2 (MULT 1 1))
= … = MULT 3 (MULT 2 1)
=
… = MULT 3 2
=
… = 6
27/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 2)
FACTORIAL 3
= … = MULT 3 (Y H 2)
= … = MULT 3 (MULT 2 (Y H 1))
= … = MULT 3 (MULT 2 (MULT 1 (Y H 0)))
= … = …(ISZERO 0) 1…
= … = MULT 3 (MULT 2 (MULT 1 1))
= … = MULT 3 (MULT 2 1)
= … = MULT 3 2
=
… = 6
27/60
Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 2)
FACTORIAL 3
= … = MULT 3 (Y H 2)
= … = MULT 3 (MULT 2 (Y H 1))
= … = MULT 3 (MULT 2 (MULT 1 (Y H 0)))
= … = …(ISZERO 0) 1…
= … = MULT 3 (MULT 2 (MULT 1 1))
= … = MULT 3 (MULT 2 1)
= … = MULT 3 2
= … = 6
27/60
Revision Combinators Encodings Functional programming Review
Y Combinator reminder
This worked because the Y Combinator
Y = λf .
(
λx .f (xx )
)(
λx .f (xx )
)
Has the property that F (YF ) = YF for all F .
Important:
▶ When performing the reductions, use that property
▶ Don’t β-reduce the Y Combinator directly.
28/60
Revision Combinators Encodings Functional programming Review
outline
▶ Revision – Lambda Calculus
▶ Y Combinator
▶ Encodings
▶ numbers (a different way)
▶ pairs
▶ lists
▶ Functional Programming
29/60
Revision Combinators Encodings Functional programming Review
Booleans
Reminder: our definition of Church Booleans lets us write:
if B then P else Q
simply as:
B P Q
where B is some boolean. i.e. anything which reduces to
▶ TRUE = λxy .x , or
▶ FALSE = λxy .y
30/60
Revision Combinators Encodings Functional programming Review
Pairs (Barendregt style)
Let P ,Q be expressions in the lambda calculus.
If we write:
[M ,N ] = λz .(if z then M else N )
= λz .zMN
Then:
▶ [M ,N ] TRUE = M
▶ [M ,N ] FALSE = N
We can use [M ,N ] to denote an ordered pair.
31/60
Revision Combinators Encodings Functional programming Review
Pairs (Barendregt)
[M ,N ] TRUE = (λz .z M N ) TRUE
= TRUE M N
= (λxy .x ) M N
= (λy .M ) N
= M
[M ,N ] FALSE = (λz .z M N ) FALSE
= FALSE M N
= (λxy .y) M N
= (λy .y) N
= N
32/60
Revision Combinators Encodings Functional programming Review
Pairs (Barendregt)
[M ,N ] TRUE = (λz .z M N ) TRUE
= TRUE M N
= (λxy .x ) M N
= (λy .M ) N
= M
[M ,N ] FALSE = (λz .z M N ) FALSE
= FALSE M N
= (λxy .y) M N
= (λy .y) N
= N
32/60
Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Recall that predecessor, subtraction, division were difficult in the
Church encoding.
We can use pairs to make another encoding for numbers:
▶ 0 = I = λx .x
▶ n + 1 = [FALSE ,n]
For example:
▶ 1 = [FALSE , 0] = [FALSE , I ] = λz .z (λxy .y)(λx .x )
▶ 2 = [FALSE , 1] = [FALSE , [FALSE , I ]]
▶ 3 = [FALSE , 2] = [FALSE , [FALSE , [FALSE , I ]]]
33/60
Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Recall that predecessor, subtraction, division were difficult in the
Church encoding.
We can use pairs to make another encoding for numbers:
▶ 0 = I = λx .x
▶ n + 1 = [FALSE ,n]
For example:
▶ 1 = [FALSE , 0] = [FALSE , I ] = λz .z (λxy .y)(λx .x )
▶ 2 = [FALSE , 1] = [FALSE , [FALSE , I ]]
▶ 3 = [FALSE , 2] = [FALSE , [FALSE , [FALSE , I ]]]
33/60
Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Recall that predecessor, subtraction, division were difficult in the
Church encoding.
We can use pairs to make another encoding for numbers:
▶ 0 = I = λx .x
▶ n + 1 = [FALSE ,n]
For example:
▶ 1 = [FALSE , 0] = [FALSE , I ] = λz .z (λxy .y)(λx .x )
▶ 2 = [FALSE , 1] = [FALSE , [FALSE , I ]]
▶ 3 = [FALSE , 2] = [FALSE , [FALSE , [FALSE , I ]]]
33/60
Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Recall that predecessor, subtraction, division were difficult in the
Church encoding.
We can use pairs to make another encoding for numbers:
▶ 0 = I = λx .x
▶ n + 1 = [FALSE ,n]
For example:
▶ 1 = [FALSE , 0] = [FALSE , I ] = λz .z (λxy .y)(λx .x )
▶ 2 = [FALSE , 1] = [FALSE , [FALSE , I ]]
▶ 3 = [FALSE , 2] = [FALSE , [FALSE , [FALSE , I ]]]
33/60
Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Recall that predecessor, subtraction, division were difficult in the
Church encoding.
We can use pairs to make another encoding for numbers:
▶ 0 = I = λx .x
▶ n + 1 = [FALSE ,n]
For example:
▶ 1 = [FALSE , 0] = [FALSE , I ] = λz .z (λxy .y)(λx .x )
▶ 2 = [FALSE , 1] = [FALSE , [FALSE , I ]]
▶ 3 = [FALSE , 2] = [FALSE , [FALSE , [FALSE , I ]]]
33/60
Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Some of the operators are a lot simpler:
▶ SUCC = λx .[FALSE , x ] (the next number)
▶ This simply puts another FALSE in front.
▶ SUCC ONE = (λx .[FALSE , x ])ONE = [FALSE ,ONE ] =
[FALSE , [FALSE , I ]]
▶ PRED = λx .x FALSE (the previous number)
▶ PRED ONE = (λx .x FALSE )ONE = ONEFALSE =
[FALSE , I ]FALSE = I
▶ ISZERO = λx .x TRUE
… recall that PRED for the Church numerals was
λnfx .n(λgh.h(gf ))(λy .x )(λu.u)
34/60
Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Some of the operators are a lot simpler:
▶ SUCC = λx .[FALSE , x ] (the next number)
▶ This simply puts another FALSE in front.
▶ SUCC ONE = (λx .[FALSE , x ])ONE = [FALSE ,ONE ] =
[FALSE , [FALSE , I ]]
▶ PRED = λx .x FALSE (the previous number)
▶ PRED ONE = (λx .x FALSE )ONE = ONEFALSE =
[FALSE , I ]FALSE = I
▶ ISZERO = λx .x TRUE
… recall that PRED for the Church numerals was
λnfx .n(λgh.h(gf ))(λy .x )(λu.u)
34/60
Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Addition is more complex, but quite intuitive
▶ base case: ADD(0, y) = y
▶ recursive case: ADD(x , y) = 1 +ADD(x − 1, y)
To implement the recursion we can use the Y Combinator again:
ADD = Y
(
λfxy .(ISZERO x ) y
(
SUCC (f (PRED x ) y)
))
▶ i.e. Y “if x is 0 then y else (1 + f (x − 1, y))”
35/60
Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Addition is more complex, but quite intuitive
▶ base case: ADD(0, y) = y
▶ recursive case: ADD(x , y) = 1 +ADD(x − 1, y)
To implement the recursion we can use the Y Combinator again:
ADD = Y
(
λfxy .(ISZERO x ) y
(
SUCC (f (PRED x ) y)
))
▶ i.e. Y “if x is 0 then y else (1 + f (x − 1, y))”
35/60
Revision Combinators Encodings Functional programming Review
Generalised recursion
We can generalise this idea of recursion to support an arbitrary
number of variables, base and recursive cases.
See section 3.11 in the reference text (Barendregt) if you’re
interested in the fine details of this.
36/60
Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz .zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) =
(λp.p TRUE ) (PAIR a b)
=
PAIR a b TRUE
=
(λxyz .zxy) a b TRUE
=
(λyz .zay) b TRUE
=
(λz .zab) TRUE
=
TRUE a b
=
(λxy .x )ab
=
(λy .a)b
=
a
37/60
Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz .zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) = (λp.p TRUE ) (PAIR a b)
=
PAIR a b TRUE
=
(λxyz .zxy) a b TRUE
=
(λyz .zay) b TRUE
=
(λz .zab) TRUE
=
TRUE a b
=
(λxy .x )ab
=
(λy .a)b
=
a
37/60
Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz .zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) = (λp.p TRUE ) (PAIR a b)
= PAIR a b TRUE
=
(λxyz .zxy) a b TRUE
=
(λyz .zay) b TRUE
=
(λz .zab) TRUE
=
TRUE a b
=
(λxy .x )ab
=
(λy .a)b
=
a
37/60
Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz .zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) = (λp.p TRUE ) (PAIR a b)
= PAIR a b TRUE
= (λxyz .zxy) a b TRUE
=
(λyz .zay) b TRUE
=
(λz .zab) TRUE
=
TRUE a b
=
(λxy .x )ab
=
(λy .a)b
=
a
37/60
Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz .zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) = (λp.p TRUE ) (PAIR a b)
= PAIR a b TRUE
= (λxyz .zxy) a b TRUE
= (λyz .zay) b TRUE
=
(λz .zab) TRUE
=
TRUE a b
=
(λxy .x )ab
=
(λy .a)b
=
a
37/60
Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz .zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) = (λp.p TRUE ) (PAIR a b)
= PAIR a b TRUE
= (λxyz .zxy) a b TRUE
= (λyz .zay) b TRUE
= (λz .zab) TRUE
=
TRUE a b
=
(λxy .x )ab
=
(λy .a)b
=
a
37/60
Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz .zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) = (λp.p TRUE ) (PAIR a b)
= PAIR a b TRUE
= (λxyz .zxy) a b TRUE
= (λyz .zay) b TRUE
= (λz .zab) TRUE
= TRUE a b
=
(λxy .x )ab
=
(λy .a)b
=
a
37/60
Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz .zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) = (λp.p TRUE ) (PAIR a b)
= PAIR a b TRUE
= (λxyz .zxy) a b TRUE
= (λyz .zay) b TRUE
= (λz .zab) TRUE
= TRUE a b
= (λxy .x )ab
=
(λy .a)b
=
a
37/60
Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz .zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) = (λp.p TRUE ) (PAIR a b)
= PAIR a b TRUE
= (λxyz .zxy) a b TRUE
= (λyz .zay) b TRUE
= (λz .zab) TRUE
= TRUE a b
= (λxy .x )ab
= (λy .a)b
= a
37/60
Revision Combinators Encodings Functional programming Review
List (Church)
Idea: lists are pairs of (head, tail)
▶ head is the first list entry
▶ tail is everything else in the list.
I will denote lists as {a, b, c, d , …}
38/60
Revision Combinators Encodings Functional programming Review
List (Church)
We need a way to signal if the list is empty.
Idea: each list entry is a nested pair (isempty, (head, tail))
▶ Empty list = NIL = PAIR TRUE TRUE
▶ Non-empty list = PAIR FALSE (PAIR head tail)
▶ i.e. each list entry has a boolean acting as a sentinel,
signaling if this sublist is empty
A list containing {a, b, c, d} would look like:
(PAIR FALSE (PAIR a
(PAIR FALSE (PAIR b
(PAIR FALSE (PAIR c
(PAIR FALSE (PAIR d NIL))))))))
39/60
Revision Combinators Encodings Functional programming Review
List (Church)
We need a way to signal if the list is empty.
Idea: each list entry is a nested pair (isempty, (head, tail))
▶ Empty list = NIL = PAIR TRUE TRUE
▶ Non-empty list = PAIR FALSE (PAIR head tail)
▶ i.e. each list entry has a boolean acting as a sentinel,
signaling if this sublist is empty
A list containing {a, b, c, d} would look like:
(PAIR FALSE (PAIR a
(PAIR FALSE (PAIR b
(PAIR FALSE (PAIR c
(PAIR FALSE (PAIR d NIL))))))))
39/60
Revision Combinators Encodings Functional programming Review
List (Church)
We need a way to signal if the list is empty.
Idea: each list entry is a nested pair (isempty, (head, tail))
▶ Empty list = NIL = PAIR TRUE TRUE
▶ Non-empty list = PAIR FALSE (PAIR head tail)
▶ i.e. each list entry has a boolean acting as a sentinel,
signaling if this sublist is empty
A list containing {a, b, c, d} would look like:
(PAIR FALSE (PAIR a
(PAIR FALSE (PAIR b
(PAIR FALSE (PAIR c
(PAIR FALSE (PAIR d NIL))))))))
39/60
Revision Combinators Encodings Functional programming Review
List (Church)
We need a way to signal if the list is empty.
Idea: each list entry is a nested pair (isempty, (head, tail))
▶ Empty list = NIL = PAIR TRUE TRUE
▶ Non-empty list = PAIR FALSE (PAIR head tail)
▶ i.e. each list entry has a boolean acting as a sentinel,
signaling if this sublist is empty
A list containing {a, b, c, d} would look like:
(PAIR FALSE (PAIR a
(PAIR FALSE (PAIR b
(PAIR FALSE (PAIR c
(PAIR FALSE (PAIR d NIL))))))))
39/60
Revision Combinators Encodings Functional programming Review
List (Church)
To make our lists useful, we want the following functions:
▶ NIL is an empty list
▶ ISNIL checks if the list is empty
▶ HEAD gets the first element
▶ TAIL gets the rest
▶ CONS prepends a given value to the head of a given list
40/60
Revision Combinators Encodings Functional programming Review
List (Church)
Encoding:
▶ NIL =
PAIR TRUE TRUE (an empty list)
▶ ISNIL =
FIRST (is the list empty)
▶ HEAD =
λz .FIRST (SECONDz )
▶ TAIL =
λz .SECOND (SECONDz )
▶ CONS =
λht .PAIR FALSE (PAIR h t)
41/60
Revision Combinators Encodings Functional programming Review
List (Church)
Encoding:
▶ NIL = PAIR TRUE TRUE (an empty list)
▶ ISNIL =
FIRST (is the list empty)
▶ HEAD =
λz .FIRST (SECONDz )
▶ TAIL =
λz .SECOND (SECONDz )
▶ CONS =
λht .PAIR FALSE (PAIR h t)
41/60
Revision Combinators Encodings Functional programming Review
List (Church)
Encoding:
▶ NIL = PAIR TRUE TRUE (an empty list)
▶ ISNIL = FIRST (is the list empty)
▶ HEAD =
λz .FIRST (SECONDz )
▶ TAIL =
λz .SECOND (SECONDz )
▶ CONS =
λht .PAIR FALSE (PAIR h t)
41/60
Revision Combinators Encodings Functional programming Review
List (Church)
Encoding:
▶ NIL = PAIR TRUE TRUE (an empty list)
▶ ISNIL = FIRST (is the list empty)
▶ HEAD = λz .FIRST (SECONDz )
▶ TAIL =
λz .SECOND (SECONDz )
▶ CONS =
λht .PAIR FALSE (PAIR h t)
41/60
Revision Combinators Encodings Functional programming Review
List (Church)
Encoding:
▶ NIL = PAIR TRUE TRUE (an empty list)
▶ ISNIL = FIRST (is the list empty)
▶ HEAD = λz .FIRST (SECONDz )
▶ TAIL = λz .SECOND (SECONDz )
▶ CONS =
λht .PAIR FALSE (PAIR h t)
41/60
Revision Combinators Encodings Functional programming Review
List (Church)
Encoding:
▶ NIL = PAIR TRUE TRUE (an empty list)
▶ ISNIL = FIRST (is the list empty)
▶ HEAD = λz .FIRST (SECONDz )
▶ TAIL = λz .SECOND (SECONDz )
▶ CONS = λht .PAIR FALSE (PAIR h t)
41/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
=
FIRST NIL
=
(λp.p TRUE ) NIL
=
NIL TRUE
=
PAIR TRUE TRUE TRUE
=
(λxyz .zxy) TRUE TRUE TRUE
=
… = TRUE TRUE TRUE
=
… = TRUE
42/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= FIRST NIL
=
(λp.p TRUE ) NIL
=
NIL TRUE
=
PAIR TRUE TRUE TRUE
=
(λxyz .zxy) TRUE TRUE TRUE
=
… = TRUE TRUE TRUE
=
… = TRUE
42/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= FIRST NIL
= (λp.p TRUE ) NIL
=
NIL TRUE
=
PAIR TRUE TRUE TRUE
=
(λxyz .zxy) TRUE TRUE TRUE
=
… = TRUE TRUE TRUE
=
… = TRUE
42/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= FIRST NIL
= (λp.p TRUE ) NIL
= NIL TRUE
=
PAIR TRUE TRUE TRUE
=
(λxyz .zxy) TRUE TRUE TRUE
=
… = TRUE TRUE TRUE
=
… = TRUE
42/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= FIRST NIL
= (λp.p TRUE ) NIL
= NIL TRUE
= PAIR TRUE TRUE TRUE
=
(λxyz .zxy) TRUE TRUE TRUE
=
… = TRUE TRUE TRUE
=
… = TRUE
42/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= FIRST NIL
= (λp.p TRUE ) NIL
= NIL TRUE
= PAIR TRUE TRUE TRUE
= (λxyz .zxy) TRUE TRUE TRUE
=
… = TRUE TRUE TRUE
=
… = TRUE
42/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= FIRST NIL
= (λp.p TRUE ) NIL
= NIL TRUE
= PAIR TRUE TRUE TRUE
= (λxyz .zxy) TRUE TRUE TRUE
= … = TRUE TRUE TRUE
=
… = TRUE
42/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= FIRST NIL
= (λp.p TRUE ) NIL
= NIL TRUE
= PAIR TRUE TRUE TRUE
= (λxyz .zxy) TRUE TRUE TRUE
= … = TRUE TRUE TRUE
= … = TRUE
42/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d}
=
FIRST {a, b, c, d}
=
(λp.p TRUE ) {a, b, c, d}
=
{a, b, c, d} TRUE
=
PAIR FALSE (PAIR a {b, c, d}) TRUE
=
(λxyz .zxy) FALSE (PAIR a {b, c, d}) TRUE
=
… = TRUE FALSE (PAIR a {b, c, d})
=
… = FALSE
43/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d}
= FIRST {a, b, c, d}
=
(λp.p TRUE ) {a, b, c, d}
=
{a, b, c, d} TRUE
=
PAIR FALSE (PAIR a {b, c, d}) TRUE
=
(λxyz .zxy) FALSE (PAIR a {b, c, d}) TRUE
=
… = TRUE FALSE (PAIR a {b, c, d})
=
… = FALSE
43/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d}
= FIRST {a, b, c, d}
= (λp.p TRUE ) {a, b, c, d}
=
{a, b, c, d} TRUE
=
PAIR FALSE (PAIR a {b, c, d}) TRUE
=
(λxyz .zxy) FALSE (PAIR a {b, c, d}) TRUE
=
… = TRUE FALSE (PAIR a {b, c, d})
=
… = FALSE
43/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d}
= FIRST {a, b, c, d}
= (λp.p TRUE ) {a, b, c, d}
= {a, b, c, d} TRUE
=
PAIR FALSE (PAIR a {b, c, d}) TRUE
=
(λxyz .zxy) FALSE (PAIR a {b, c, d}) TRUE
=
… = TRUE FALSE (PAIR a {b, c, d})
=
… = FALSE
43/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d}
= FIRST {a, b, c, d}
= (λp.p TRUE ) {a, b, c, d}
= {a, b, c, d} TRUE
= PAIR FALSE (PAIR a {b, c, d}) TRUE
=
(λxyz .zxy) FALSE (PAIR a {b, c, d}) TRUE
=
… = TRUE FALSE (PAIR a {b, c, d})
=
… = FALSE
43/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d}
= FIRST {a, b, c, d}
= (λp.p TRUE ) {a, b, c, d}
= {a, b, c, d} TRUE
= PAIR FALSE (PAIR a {b, c, d}) TRUE
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) TRUE
=
… = TRUE FALSE (PAIR a {b, c, d})
=
… = FALSE
43/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d}
= FIRST {a, b, c, d}
= (λp.p TRUE ) {a, b, c, d}
= {a, b, c, d} TRUE
= PAIR FALSE (PAIR a {b, c, d}) TRUE
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) TRUE
= … = TRUE FALSE (PAIR a {b, c, d})
=
… = FALSE
43/60
Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d}
= FIRST {a, b, c, d}
= (λp.p TRUE ) {a, b, c, d}
= {a, b, c, d} TRUE
= PAIR FALSE (PAIR a {b, c, d}) TRUE
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) TRUE
= … = TRUE FALSE (PAIR a {b, c, d})
= … = FALSE
43/60
Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a, b, c, d}
=
(λz .FIRST (SECOND z )) {a, b, c, d}
=
FIRST (SECOND {a, b, c, d})
=
(λp.p TRUE ) (SECOND {a, b, c, d})
=
SECOND {a, b, c, d} TRUE
=
(λp.p FALSE ) {a, b, c, d} TRUE
=
{a, b, c, d} FALSE TRUE
=
PAIR FALSE (PAIR a {b, c, d}) FALSE TRUE
= …
44/60
Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a, b, c, d}
= (λz .FIRST (SECOND z )) {a, b, c, d}
=
FIRST (SECOND {a, b, c, d})
=
(λp.p TRUE ) (SECOND {a, b, c, d})
=
SECOND {a, b, c, d} TRUE
=
(λp.p FALSE ) {a, b, c, d} TRUE
=
{a, b, c, d} FALSE TRUE
=
PAIR FALSE (PAIR a {b, c, d}) FALSE TRUE
= …
44/60
Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a, b, c, d}
= (λz .FIRST (SECOND z )) {a, b, c, d}
= FIRST (SECOND {a, b, c, d})
=
(λp.p TRUE ) (SECOND {a, b, c, d})
=
SECOND {a, b, c, d} TRUE
=
(λp.p FALSE ) {a, b, c, d} TRUE
=
{a, b, c, d} FALSE TRUE
=
PAIR FALSE (PAIR a {b, c, d}) FALSE TRUE
= …
44/60
Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a, b, c, d}
= (λz .FIRST (SECOND z )) {a, b, c, d}
= FIRST (SECOND {a, b, c, d})
= (λp.p TRUE ) (SECOND {a, b, c, d})
=
SECOND {a, b, c, d} TRUE
=
(λp.p FALSE ) {a, b, c, d} TRUE
=
{a, b, c, d} FALSE TRUE
=
PAIR FALSE (PAIR a {b, c, d}) FALSE TRUE
= …
44/60
Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a, b, c, d}
= (λz .FIRST (SECOND z )) {a, b, c, d}
= FIRST (SECOND {a, b, c, d})
= (λp.p TRUE ) (SECOND {a, b, c, d})
= SECOND {a, b, c, d} TRUE
=
(λp.p FALSE ) {a, b, c, d} TRUE
=
{a, b, c, d} FALSE TRUE
=
PAIR FALSE (PAIR a {b, c, d}) FALSE TRUE
= …
44/60
Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a, b, c, d}
= (λz .FIRST (SECOND z )) {a, b, c, d}
= FIRST (SECOND {a, b, c, d})
= (λp.p TRUE ) (SECOND {a, b, c, d})
= SECOND {a, b, c, d} TRUE
= (λp.p FALSE ) {a, b, c, d} TRUE
=
{a, b, c, d} FALSE TRUE
=
PAIR FALSE (PAIR a {b, c, d}) FALSE TRUE
= …
44/60
Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a, b, c, d}
= (λz .FIRST (SECOND z )) {a, b, c, d}
= FIRST (SECOND {a, b, c, d})
= (λp.p TRUE ) (SECOND {a, b, c, d})
= SECOND {a, b, c, d} TRUE
= (λp.p FALSE ) {a, b, c, d} TRUE
= {a, b, c, d} FALSE TRUE
=
PAIR FALSE (PAIR a {b, c, d}) FALSE TRUE
= …
44/60
Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a, b, c, d}
= (λz .FIRST (SECOND z )) {a, b, c, d}
= FIRST (SECOND {a, b, c, d})
= (λp.p TRUE ) (SECOND {a, b, c, d})
= SECOND {a, b, c, d} TRUE
= (λp.p FALSE ) {a, b, c, d} TRUE
= {a, b, c, d} FALSE TRUE
= PAIR FALSE (PAIR a {b, c, d}) FALSE TRUE
= …
44/60
Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a, b, c, d}
= …
=
(λxyz .zxy) FALSE (PAIR a {b, c, d}) FALSE TRUE
=
(λyz .z FALSE y) (PAIR a {b, c, d}) FALSE TRUE
=
(λz .z FALSE (PAIR a {b, c, d})) FALSE TRUE
=
FALSE FALSE (PAIR a {b, c, d}) TRUE
=
… = PAIR a {b, c, d} TRUE (FALSE a b = b)
=
(λxyz .zxy) a {b, c, d} TRUE
=
… = TRUE a {b, c, d}) (3 β-reductions)
=
… = a (TRUE a b = a)
45/60
Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a, b, c, d}
= …
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) FALSE TRUE
=
(λyz .z FALSE y) (PAIR a {b, c, d}) FALSE TRUE
=
(λz .z FALSE (PAIR a {b, c, d})) FALSE TRUE
=
FALSE FALSE (PAIR a {b, c, d}) TRUE
=
… = PAIR a {b, c, d} TRUE (FALSE a b = b)
=
(λxyz .zxy) a {b, c, d} TRUE
=
… = TRUE a {b, c, d}) (3 β-reductions)
=
… = a (TRUE a b = a)
45/60
Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a, b, c, d}
= …
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) FALSE TRUE
= (λyz .z FALSE y) (PAIR a {b, c, d}) FALSE TRUE
=
(λz .z FALSE (PAIR a {b, c, d})) FALSE TRUE
=
FALSE FALSE (PAIR a {b, c, d}) TRUE
=
… = PAIR a {b, c, d} TRUE (FALSE a b = b)
=
(λxyz .zxy) a {b, c, d} TRUE
=
… = TRUE a {b, c, d}) (3 β-reductions)
=
… = a (TRUE a b = a)
45/60
Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a, b, c, d}
= …
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) FALSE TRUE
= (λyz .z FALSE y) (PAIR a {b, c, d}) FALSE TRUE
= (λz .z FALSE (PAIR a {b, c, d})) FALSE TRUE
=
FALSE FALSE (PAIR a {b, c, d}) TRUE
=
… = PAIR a {b, c, d} TRUE (FALSE a b = b)
=
(λxyz .zxy) a {b, c, d} TRUE
=
… = TRUE a {b, c, d}) (3 β-reductions)
=
… = a (TRUE a b = a)
45/60
Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a, b, c, d}
= …
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) FALSE TRUE
= (λyz .z FALSE y) (PAIR a {b, c, d}) FALSE TRUE
= (λz .z FALSE (PAIR a {b, c, d})) FALSE TRUE
= FALSE FALSE (PAIR a {b, c, d}) TRUE
=
… = PAIR a {b, c, d} TRUE (FALSE a b = b)
=
(λxyz .zxy) a {b, c, d} TRUE
=
… = TRUE a {b, c, d}) (3 β-reductions)
=
… = a (TRUE a b = a)
45/60
Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a, b, c, d}
= …
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) FALSE TRUE
= (λyz .z FALSE y) (PAIR a {b, c, d}) FALSE TRUE
= (λz .z FALSE (PAIR a {b, c, d})) FALSE TRUE
= FALSE FALSE (PAIR a {b, c, d}) TRUE
= … = PAIR a {b, c, d} TRUE (FALSE a b = b)
=
(λxyz .zxy) a {b, c, d} TRUE
=
… = TRUE a {b, c, d}) (3 β-reductions)
=
… = a (TRUE a b = a)
45/60
Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a, b, c, d}
= …
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) FALSE TRUE
= (λyz .z FALSE y) (PAIR a {b, c, d}) FALSE TRUE
= (λz .z FALSE (PAIR a {b, c, d})) FALSE TRUE
= FALSE FALSE (PAIR a {b, c, d}) TRUE
= … = PAIR a {b, c, d} TRUE (FALSE a b = b)
= (λxyz .zxy) a {b, c, d} TRUE
=
… = TRUE a {b, c, d}) (3 β-reductions)
=
… = a (TRUE a b = a)
45/60
Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a, b, c, d}
= …
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) FALSE TRUE
= (λyz .z FALSE y) (PAIR a {b, c, d}) FALSE TRUE
= (λz .z FALSE (PAIR a {b, c, d})) FALSE TRUE
= FALSE FALSE (PAIR a {b, c, d}) TRUE
= … = PAIR a {b, c, d} TRUE (FALSE a b = b)
= (λxyz .zxy) a {b, c, d} TRUE
= … = TRUE a {b, c, d}) (3 β-reductions)
=
… = a (TRUE a b = a)
45/60
Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a, b, c, d}
= …
= (λxyz .zxy) FALSE (PAIR a {b, c, d}) FALSE TRUE
= (λyz .z FALSE y) (PAIR a {b, c, d}) FALSE TRUE
= (λz .z FALSE (PAIR a {b, c, d})) FALSE TRUE
= FALSE FALSE (PAIR a {b, c, d}) TRUE
= … = PAIR a {b, c, d} TRUE (FALSE a b = b)
= (λxyz .zxy) a {b, c, d} TRUE
= … = TRUE a {b, c, d}) (3 β-reductions)
= … = a (TRUE a b = a)
45/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS a NIL
=
(λht .PAIR FALSE (PAIR h t)) a NIL
=
(λt .PAIR FALSE (PAIR a t)) NIL
=
PAIR FALSE (PAIR a NIL)
=
{a}
46/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS a NIL
= (λht .PAIR FALSE (PAIR h t)) a NIL
=
(λt .PAIR FALSE (PAIR a t)) NIL
=
PAIR FALSE (PAIR a NIL)
=
{a}
46/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS a NIL
= (λht .PAIR FALSE (PAIR h t)) a NIL
= (λt .PAIR FALSE (PAIR a t)) NIL
=
PAIR FALSE (PAIR a NIL)
=
{a}
46/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS a NIL
= (λht .PAIR FALSE (PAIR h t)) a NIL
= (λt .PAIR FALSE (PAIR a t)) NIL
= PAIR FALSE (PAIR a NIL)
=
{a}
46/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS a NIL
= (λht .PAIR FALSE (PAIR h t)) a NIL
= (λt .PAIR FALSE (PAIR a t)) NIL
= PAIR FALSE (PAIR a NIL)
= {a}
46/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS b (CONS a NIL)
=
(λht .PAIR FALSE (PAIR h t)) b (CONS a NIL)
=
(λt .PAIR FALSE (PAIR b t)) (CONS a NIL)
=
PAIR FALSE (PAIR b (CONS a NIL))
=
PAIR FALSE (PAIR b (CONS a NIL))
=
PAIR FALSE (PAIR b (PAIR FALSE (PAIR a NIL)))
=
{b, a}
47/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS b (CONS a NIL)
= (λht .PAIR FALSE (PAIR h t)) b (CONS a NIL)
=
(λt .PAIR FALSE (PAIR b t)) (CONS a NIL)
=
PAIR FALSE (PAIR b (CONS a NIL))
=
PAIR FALSE (PAIR b (CONS a NIL))
=
PAIR FALSE (PAIR b (PAIR FALSE (PAIR a NIL)))
=
{b, a}
47/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS b (CONS a NIL)
= (λht .PAIR FALSE (PAIR h t)) b (CONS a NIL)
= (λt .PAIR FALSE (PAIR b t)) (CONS a NIL)
=
PAIR FALSE (PAIR b (CONS a NIL))
=
PAIR FALSE (PAIR b (CONS a NIL))
=
PAIR FALSE (PAIR b (PAIR FALSE (PAIR a NIL)))
=
{b, a}
47/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS b (CONS a NIL)
= (λht .PAIR FALSE (PAIR h t)) b (CONS a NIL)
= (λt .PAIR FALSE (PAIR b t)) (CONS a NIL)
= PAIR FALSE (PAIR b (CONS a NIL))
=
PAIR FALSE (PAIR b (CONS a NIL))
=
PAIR FALSE (PAIR b (PAIR FALSE (PAIR a NIL)))
=
{b, a}
47/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS b (CONS a NIL)
= (λht .PAIR FALSE (PAIR h t)) b (CONS a NIL)
= (λt .PAIR FALSE (PAIR b t)) (CONS a NIL)
= PAIR FALSE (PAIR b (CONS a NIL))
= PAIR FALSE (PAIR b (CONS a NIL))
=
PAIR FALSE (PAIR b (PAIR FALSE (PAIR a NIL)))
=
{b, a}
47/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS b (CONS a NIL)
= (λht .PAIR FALSE (PAIR h t)) b (CONS a NIL)
= (λt .PAIR FALSE (PAIR b t)) (CONS a NIL)
= PAIR FALSE (PAIR b (CONS a NIL))
= PAIR FALSE (PAIR b (CONS a NIL))
= PAIR FALSE (PAIR b (PAIR FALSE (PAIR a NIL)))
=
{b, a}
47/60
Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht .PAIR FALSE (PAIR h t)
CONS b (CONS a NIL)
= (λht .PAIR FALSE (PAIR h t)) b (CONS a NIL)
= (λt .PAIR FALSE (PAIR b t)) (CONS a NIL)
= PAIR FALSE (PAIR b (CONS a NIL))
= PAIR FALSE (PAIR b (CONS a NIL))
= PAIR FALSE (PAIR b (PAIR FALSE (PAIR a NIL)))
= {b, a}
47/60
Revision Combinators Encodings Functional programming Review
List encodings
We now have structured data and recursion!
Don’t forget, just as there are many ways to represent a List ADT
in imperative programming, there are many possible encodings for
lists and other structures in lambda calculus.
48/60
Revision Combinators Encodings Functional programming Review
List encodings
We now have structured data and recursion!
Don’t forget, just as there are many ways to represent a List ADT
in imperative programming, there are many possible encodings for
lists and other structures in lambda calculus.
48/60
Revision Combinators Encodings Functional programming Review
outline
▶ Revision – Lambda Calculus
▶ Y Combinator
▶ Encodings
▶ numbers (a different way)
▶ pairs
▶ lists
▶ Functional Programming
49/60
Revision Combinators Encodings Functional programming Review
Fibonacci
In the last tutorial, you probably implemented Fibonacci like this:
( defun f i b ( x )
( i f (< x 2)
1
(+ ( f i b (− x 1) ) ( f i b (− x 2 ) ) )
)
)
This works, but is not very efficient (exponential time complexity!)
In imperative programming you would use variables to store the
sequence (linear time complexity).
A comparable approach in FP is to compute the sequence, e.g. as
a list.
50/60
Revision Combinators Encodings Functional programming Review
Fibonacci
In the last tutorial, you probably implemented Fibonacci like this:
( defun f i b ( x )
( i f (< x 2)
1
(+ ( f i b (− x 1) ) ( f i b (− x 2 ) ) )
)
)
This works, but is not very efficient (exponential time complexity!)
In imperative programming you would use variables to store the
sequence (linear time complexity).
A comparable approach in FP is to compute the sequence, e.g. as
a list.
50/60
Revision Combinators Encodings Functional programming Review
Fibonacci
In the last tutorial, you probably implemented Fibonacci like this:
( defun f i b ( x )
( i f (< x 2)
1
(+ ( f i b (− x 1) ) ( f i b (− x 2 ) ) )
)
)
This works, but is not very efficient (exponential time complexity!)
In imperative programming you would use variables to store the
sequence (linear time complexity).
A comparable approach in FP is to compute the sequence, e.g. as
a list.
50/60
Revision Combinators Encodings Functional programming Review
Fibonacci
In the last tutorial, you probably implemented Fibonacci like this:
( defun f i b ( x )
( i f (< x 2)
1
(+ ( f i b (− x 1) ) ( f i b (− x 2 ) ) )
)
)
This works, but is not very efficient (exponential time complexity!)
In imperative programming you would use variables to store the
sequence (linear time complexity).
A comparable approach in FP is to compute the sequence, e.g. as
a list.
50/60
Revision Combinators Encodings Functional programming Review
Lists in LISP
n i l ; an empty l i s t
( cons e l ) ; p repend e to l i s t l
( l i s t a b c . . . ) ; new l i s t ( a b c . . . )
( ca r l ) ; the head e lement o f l
( cd r l ) ; the t a i l l i s t o f l
( l a s t l ) ; the l a s t e l ement l
(append a b ) ; combine two l i s t s
(member e l ) ; f i r s t s u b l i s t s t a r t i n g e i n l
( reverse l ) ; a m i r r o r o f the l i s t
51/60
Revision Combinators Encodings Functional programming Review
Lists in LISP (examples)
? ( l i s t 1 2 3)
(1 2 3)
? ( cons 1 ( cons 2 ( cons 3 n i l ) ) )
(1 2 3)
? (member 2 ( l i s t 1 3 5) )
NIL
? (member 3 ( l i s t 1 3 5) )
(3 5)
? ( cd r ( l i s t 1 2 3 4 5) )
(2 3 4 5)
? ( cd r ( cd r ( l i s t 1 2 3 4 5 ) ) )
(3 4 5)
? ( ca r ( cd r ( l i s t 1 2 3 4 5 ) ) )
2
52/60
Revision Combinators Encodings Functional programming Review
Fibonacci
Idea: given part of the Fibonacci sequence and a number, add that
many more elements of the sequence.
( defun f i b ( n a )
( i f ( zerop n )
a
( f i b (− n 1)
( cons
(+ ( ca r a ) ( ca r ( cd r a ) ) )
a
) ) ) )
( f i b 100 ( l i s t 1 0) )
53/60
Revision Combinators Encodings Functional programming Review
Fibonacci
Making it a bit nicer:
▶ We can make optional (default) arguments
▶ (car (cdr x)) = (cadr x)
▶ You can repeat the a, d as many times as required
▶ e.g. (cadddr x) is the 4th element
( defun f i b ( n &op t i o n a l ( a ( l i s t 1 0 ) ) )
( i f ( zerop n )
a
( f i b (− n 1)
( cons
(+ ( ca r a ) ( cadr a ) )
a
) ) ) )
( f i b 100)
54/60
Revision Combinators Encodings Functional programming Review
A note on loops in LISP
I avoided using loops to keep the first example closer to lamda
calculus.
There are several ways to use loops in LISP, here’s one:
( defun f i b ( n )
( loop f o r f 1 = 0 then f2
and f 2 = 1 then (+ f1 f2 )
r e p e a t n f i n a l l y ( return f 1 ) ) )
( f i b 100)
1
1source: https://www.cliki.net/Fibonacci
55/60
https://www.cliki.net/Fibonacci
Revision Combinators Encodings Functional programming Review
Java
pub l i c boolean i sP r ime ( long number ) {
return number > 1 &&
LongStream
. r angeC lo s ed (2 , ( long ) Math . s q r t ( number ) )
. noneMatch ( i ndex −> number % index == 0 ) ;
}
i sP r ime (9220000000000000039L) // Output : t r u e
2
▶ “.rangeClosed” gives a stream of values within the range
▶ “.noneMatch” checks the stream against a predicate
▶ “variable -> expression” is a lambda abstraction!
▶ It takes a value (index) from the range, and tests if it divides
the number we’re checking.
2source: https://www.voxxed.com/2015/12/
functional-vs-imperative-programming-fibonacci-prime-and-factorial-in-java-8/
56/60
https://www.voxxed.com/2015/12/functional-vs-imperative-programming-fibonacci-prime-and-factorial-in-java-8/
https://www.voxxed.com/2015/12/functional-vs-imperative-programming-fibonacci-prime-and-factorial-in-java-8/
Revision Combinators Encodings Functional programming Review
Java
pub l i c boolean i sP r ime ( long number ) {
return number > 1 &&
LongStream
. r angeC lo s ed (2 , ( long ) Math . s q r t ( number ) )
. p a r a l l e l ( )
. noneMatch ( i ndex −> number % index == 0 ) ;
}
i sP r ime (9220000000000000039L) // Output : t r u e
3
Adding “.parallel()” is enough magic sauce to get an embarassingly
good speedup.
3source: https://www.voxxed.com/2015/12/
functional-vs-imperative-programming-fibonacci-prime-and-factorial-in-java-8/
57/60
https://www.voxxed.com/2015/12/functional-vs-imperative-programming-fibonacci-prime-and-factorial-in-java-8/
https://www.voxxed.com/2015/12/functional-vs-imperative-programming-fibonacci-prime-and-factorial-in-java-8/
Revision Combinators Encodings Functional programming Review
Python
If you write much Python, you probably write more functional
programming code than you thought.
>>> grade s = [43 , 68 , 35 , 89 , 67 , 65 , 70 ]
>>> l en ( l i s t ( f i l t e r ( lambda x : x>=50, g r ade s ) ) )
5
>>> sum(map( lambda x : x>=50, g r ade s ) )
5
>>> [ x + 5 f o r x i n g rade s ]
[ 4 8 , 73 , 40 , 94 , 72 , 70 , 75 ]
>>> max ( [ x + 5 f o r x i n g rade s ] )
94
58/60
Revision Combinators Encodings Functional programming Review
Python
>>> from f u n c t o o l s import reduce
>>> p r i c e s = [43 , 68 , 35 , 89 , 67 , 65 , 70 ]
>>> s a l e s = [ 3 , 5 , 0 , 3 , 2 , 10 , 30 ]
>>> reduce ( lambda x , y : x+y ,
map( lambda x : x [ 0 ] ∗ x [ 1 ] ,
z ip ( p r i c e s , s a l e s ) ) )
3620
▶ zip combines elements from two iterables into pairs
▶ e.g. [(43, 3), (68, 5), … ]
▶ map applies a function to every element of an iterable
▶ e.g. [43*3, 68*5, … ]
▶ reduce combines the elements using a two parameter function
▶ (((0+129) + 340) + 0) + …
59/60
Revision Combinators Encodings Functional programming Review
Python
>>> from f u n c t o o l s import reduce
>>> p r i c e s = [43 , 68 , 35 , 89 , 67 , 65 , 70 ]
>>> s a l e s = [ 3 , 5 , 0 , 3 , 2 , 10 , 30 ]
>>> reduce ( lambda x , y : x+y ,
map( lambda x : x [ 0 ] ∗ x [ 1 ] ,
z ip ( p r i c e s , s a l e s ) ) )
3620
▶ zip combines elements from two iterables into pairs
▶ e.g. [(43, 3), (68, 5), … ]
▶ map applies a function to every element of an iterable
▶ e.g. [43*3, 68*5, … ]
▶ reduce combines the elements using a two parameter function
▶ (((0+129) + 340) + 0) + …
59/60
Revision Combinators Encodings Functional programming Review
Python
>>> from f u n c t o o l s import reduce
>>> p r i c e s = [43 , 68 , 35 , 89 , 67 , 65 , 70 ]
>>> s a l e s = [ 3 , 5 , 0 , 3 , 2 , 10 , 30 ]
>>> reduce ( lambda x , y : x+y ,
map( lambda x : x [ 0 ] ∗ x [ 1 ] ,
z ip ( p r i c e s , s a l e s ) ) )
3620
▶ zip combines elements from two iterables into pairs
▶ e.g. [(43, 3), (68, 5), … ]
▶ map applies a function to every element of an iterable
▶ e.g. [43*3, 68*5, … ]
▶ reduce combines the elements using a two parameter function
▶ (((0+129) + 340) + 0) + …
59/60
Revision Combinators Encodings Functional programming Review
Review
▶ Revision – Lambda Calculus
▶ When α-reductions are required
▶ η-reductions
▶ Y Combinator
▶ Combinators
▶ Fixed-Point Theorem
▶ Y Combinator
▶ Implementing recursion
▶ Encodings
▶ numbers (a different way)
▶ pairs
▶ lists
▶ Functional Programming
▶ Using lists in LISP
▶ Stream processing in Java
▶ Some ubiquitous Python
60/60
Revision
Lambda Calculus
Combinators
Combinators
Encodings
Pairing
Functional programming
Lists
Review
review