[SOLVED] python Java Lambda Calculus COMP2022: Formal Languages and Logic 2018, Semester 2, Week 3

$25

File Name: python_Java_Lambda_Calculus_COMP2022:_Formal_Languages_and_Logic__2018,_Semester_2,_Week_3.zip
File Size: 847.8 KB

5/5 - (1 vote)

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 doesnt matter
except when it does!

even worse its 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 its 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)
xy (xy = 0) is true (choose x = 0)
xy (xy = 1) is false (whatever we choose for x , well be

able to find a y that doesnt work)
xy (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
KMN = 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
KMN = 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
KMN = 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 its 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 its 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 its 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 its 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 its 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 Currys 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 Currys 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 Currys 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)

Well 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)

Well 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)

Well 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)

Well 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 its
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)

Well 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 its

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)

Well 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)

Well 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)

Well 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)

Well 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 cant 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 cant 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 cant 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
Dont -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 youre
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!

Dont 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!

Dont 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 thesequence (linear time complexity).A comparable approach in FP is to compute the sequence, e.g. asa list.50/60Revision Combinators Encodings Functional programming ReviewFibonacciIn 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 thesequence (linear time complexity).A comparable approach in FP is to compute the sequence, e.g. asa list.50/60Revision Combinators Encodings Functional programming ReviewFibonacciIn 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 thesequence (linear time complexity).A comparable approach in FP is to compute the sequence, e.g. asa list.50/60Revision Combinators Encodings Functional programming ReviewFibonacciIn 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 thesequence (linear time complexity).A comparable approach in FP is to compute the sequence, e.g. asa list.50/60Revision Combinators Encodings Functional programming ReviewLists in LISPn 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 t51/60Revision Combinators Encodings Functional programming ReviewLists 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 ) ) )252/60Revision Combinators Encodings Functional programming ReviewFibonacciIdea: given part of the Fibonacci sequence and a number, add thatmany 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/60Revision Combinators Encodings Functional programming ReviewFibonacciMaking 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/60Revision Combinators Encodings Functional programming ReviewA note on loops in LISPI avoided using loops to keep the first example closer to lamdacalculus.There are several ways to use loops in LISP, heres one:( defun f i b ( n )( loop f o r f 1 = 0 then f2and 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)11source: https://www.cliki.net/Fibonacci55/60https://www.cliki.net/FibonacciRevision Combinators Encodings Functional programming ReviewJavapub 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 were 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

Reviews

There are no reviews yet.

Only logged in customers who have purchased this product may leave a review.

Shopping Cart
[SOLVED] python Java Lambda Calculus COMP2022: Formal Languages and Logic 2018, Semester 2, Week 3
$25