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.