程序代写代做代考 python Java Lambda Calculus COMP2022: Formal Languages and Logic – 2018, Semester 2, Week 3

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