代写 Java lisp math python parallel Lambda Calculus COMP2022: Formal Languages and Logic

COMP2022: Formal Languages and Logic
2018, Semester 2, Week 3
Joseph Godbehere 16th August, 2018

COMMONWEALTH OF AUSTRALIA Copyright Regulations 1969 WARNING
This material has been reproduced and communicated to you by or on behalf of the University of Sydney pursuant to part VB of the Copyright Act 1968 (the Act).
The material in this communication may be subject to copyright under the Act. Any further copying or communication of this material by you may be subject of copyright protect under the Act.
Do not remove this notice.

Revision Combinators Encodings Functional programming Review
outline
▶ Revision – Lambda Calculus
▶ Y Combinator
▶ Encodings
▶ numbers (a different way) ▶ pairs
▶ lists
▶ Functional Programming
3/60

Revision Combinators Encodings Functional programming Review
When are α-reductions required?
If they never change the meaning, why bother?
▶ Readability
▶ β-reduction assumes all variables have different labels
▶ Usually it doesn’t matter… ▶ … except when it does!
▶ … even worse – it’s not enough to only look at the subformula being reduced
4/60

Revision Combinators Encodings Functional programming Review
WRONG
▶ Where is the error?
λx .(λyx .y )x = λx.(λx.x) = λx.(λy.y) = λxy.y
= FALSE
5/60

Revision Combinators Encodings Functional programming Review
WRONG
▶ Where is the error? ▶ Why is it a mistake?
λx .(λyx .y )x = λx.(λx.x) = λx.(λy.y) = λxy.y
= FALSE
(mistake!)
5/60

Revision Combinators Encodings Functional programming Review
WRONG
▶ Where is the error?
▶ Why is it a mistake?
λx .(λyx .y )x = λx.(λx.x) = λx.(λy.y) = λxy.y
= FALSE
(mistake!)
▶ x was bound to the first λ, but on line 2 it is not! Free variables in N should not become bound in M [x := N ]
5/60

Revision Combinators Encodings Functional programming Review
CORRECT
λx .(λyx .y )x
= λx.(λyz.y)x (α) = λx.(λz.x) (β) = λxz.x
= TRUE
Rule of thumb: always perform α reductions before β reductions. ▶ sometimes it’s necessary
▶ usually makes the formula easier to read too
6/60

Revision Combinators Encodings Functional programming Review
η-reduction (Eta)
If x is not free in M, then we can write:
λx.Mx = M
Idea: any input applied to this will simply be applied to M
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
Necessary Logical Notation: Quantifiers
▶ “for all possible values of X …” denoted ∀X
▶ “there exists a value of X such that …” denoted ∃X
Examples (for all positive rational numbers)
▶ “∀x (x ∗ 1 = x )” is true
▶ “∃x (x + 1 = 4)” is true (choose x = 3)
▶ “∀x (x + 1 = 4)” is false (e.g. false on x = 1)
▶ “∃x∀y (xy = 0)” is true (choose x = 0)
▶ “∃x∀y (xy = 1)” is false (whatever we choose for x, we’ll be able to find a y that doesn’t work)
▶ “∀x ∃y (xy = 1)” is true (for any x , we can choose y = 1 ) x
9/60

Revision Combinators Encodings Functional programming Review
Combinators
A combinator is any expression M which contains no free variables.
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)
10/60

Revision Combinators Encodings Functional programming Review
Combinators
A combinator is any expression M which contains no free variables.
Example:
▶ λxy.xyz is not a combinator (z is free)
▶ λxy.xyy is a combinator (all variables bound)
Combinators combine values into expressions without relying on quantifiers or explicitly defining variables.
10/60

Revision Combinators Encodings Functional programming Review
Combinator examples
Standard combinators:
▶ I = λx.x (identity)
▶ K = λxy.x (true)
▶ K∗ = λxy.y (false)
▶ S = λxyz.xz(yz) (generalisation of application)
We can easily deduce (by using β reduction): ▶ IM = M
▶ KMN = M
▶ K∗MN = N
▶ SMNL = ML(NL)
Interestingly, these λ-free combinators are sufficient to make expressions equal to any λ term. We will not talk about that further today though.
11/60

Revision Combinators Encodings Functional programming Review
Solving simple equations
∃G ∀X GX =XXX
(Where X , F are expressions in the lambda calculus)
12/60

Revision Combinators Encodings Functional programming Review
Solving simple equations
∃G ∀X GX =XXX
(Where X , F are expressions in the lambda calculus)
“There exists some G such that for all X it’s true that GC = XXX ”
Proof:
▶ Let G = λx.xxx
12/60

Revision Combinators Encodings Functional programming Review
Fixed Point Combinators
A fixed point combinator is a combinator which has a fixed point.
WesayF hasafixedpointif∃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
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
14/60

Revision Combinators Encodings Functional programming Review
Fixed point theorem (i)
Theorem:
“For all F, there exists some X such that FX = X”
∀F ∃X FX = X ▶ i.e. all functions have a fixed point
Proof:
Let W = λx.F(xx) and X = WW. Then:
X=
14/60

Revision Combinators Encodings Functional programming Review
Fixed point theorem (ii)
There is a fixed point combinator (the “Y Combinator”)
such that
Proof:
YF =
( )( )
Y = λf . λx.f (xx) λx.f (xx) ∀F F(YF)=YF
15/60

Revision Combinators Encodings Functional programming Review
Fixed point theorem (ii)
There is a fixed point combinator (the “Y Combinator”)
such that Proof:
( )( )
Y = λf . λx.f (xx) λx.f (xx) ∀F F(YF)=YF
(( )( ))
YF = λf.λx.f(xx) λx.f(xx) F = (λx.F(xx))(λx.F(xx))
=
(defn.ofY) (β−reduction)
15/60

Revision Combinators Encodings Functional programming Review
Fixed point theorem (ii)
There is a fixed point combinator (the “Y Combinator”)
such that Proof:
( )( )
Y = λf . λx.f (xx) λx.f (xx) ∀F F(YF)=YF
(( )( ))
(defn.ofY) (β−reduction) (by pf. of theorem (i))
YF = λf.λx.f(xx) λx.f(xx) F = (λx.F(xx))(λx.F(xx))
(( )( ))
= F λx.F(xx) λx.F(xx) =
15/60

Revision Combinators Encodings Functional programming Review
Fixed point theorem (ii)
There is a fixed point combinator (the “Y Combinator”)
such that Proof:
( )( )
Y = λf . λx.f (xx) λx.f (xx) ∀F F(YF)=YF
(( )( ))
(defn.ofY) (β−reduction) (by pf. of theorem (i)) (by equality above)
YF = λf.λx.f(xx) λx.f(xx) F = (λx.F(xx))(λx.F(xx))
(( )( ))
= F λx.F(xx) λx.F(xx) = F(YF)
15/60

Revision Combinators Encodings Functional programming Review
Y Combinator
So, uh… Why is this interesting?
16/60

Revision Combinators Encodings Functional programming Review
Y Combinator
So, uh… Why is this interesting?
1. Good news: it allows us to write self recursive functions
▶ it effectively lets us define variables
2. Bad news: it leads to Curry’s Paradox, and the incompleteness of lamdba calculus
▶ not all valid expressions can be proved / computed
16/60

Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f(n)=if (n==0)then1elsen∗f(n−1)
17/60

Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f(n)=if (n==0)then1elsen∗f(n−1) We’ll need some helper functions / encodings:
▶ Church numerals: cn = λfx .f n (x )
▶ This notation, indicating n repetitions of f (…) is a little dangerous (but convenient)
▶ Be aware that Church numerals have the form: λfz .f (f (f (f (fz )))) ̸= λfz .fffffz
17/60

Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= = = = =
19/60

Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= (λn.n (λx.FALSE) TRUE) ZERO =
=
=
=
(def. ISZERO)
19/60

Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= (λn.n (λx.FALSE) TRUE) ZERO
= ZERO (λx.FALSE) TRUE =
=
=
(def. ISZERO) (β)
19/60

Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= (λn.n (λx.FALSE) TRUE) ZERO
= ZERO (λx.FALSE) TRUE
= (λfz.z) (λx.FALSE) TRUE =
=
(def. ISZERO) (β) (def.ZERO)
19/60

Revision Combinators Encodings Functional programming Review
ISZERO ZERO
ISZERO ZERO
= (λn.n (λx.FALSE) TRUE) ZERO
= ZERO (λx.FALSE) TRUE
= (λfz.z) (λx.FALSE) TRUE
= (λz.z) TRUE =
(def. ISZERO) (β) (def.ZERO) (β)
19/60

Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= = = = = =
20/60

Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx.FALSE) TRUE) ONE =
=
=
=
=
(def. ISZERO)
20/60

Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx.FALSE) TRUE) ONE
= ONE (λx.FALSE) TRUE =
=
=
=
(def. ISZERO) (β)
20/60

Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx.FALSE) TRUE) ONE
= ONE (λx.FALSE) TRUE
= (λfz.fz) (λx.FALSE) TRUE =
=
=
(def. ISZERO) (β) (def.ONE)
20/60

Revision Combinators Encodings Functional programming Review
ISZERO ONE
ISZERO ONE
= (λn.n (λx.FALSE) TRUE) ONE
= ONE (λx.FALSE) TRUE
= (λfz.fz) (λx.FALSE) TRUE
= (λz .(λx .FALSE )z ) TRUE =
=
(def. ISZERO) (β) (def.ONE) (β )
20/60

Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f(n)=if (n==0)then1elsen∗f(n−1)
We’ll need some helper functions / encodings: ▶ Church numerals: cn = λfx .f n (x )
▶ ISZERO := λn.n (λx.FALSE) TRUE
▶ MULT := λxyz.x(yz) (seen previously)
▶ PRED := λnfx.n(λgh.h(gf ))(λy.x)(λu.u) ▶ This gives the predecessor of a number
▶ PRED1=0,PRED2=1,…,PREDn=(n-1)
▶ The derivation of this is much longer than for the operations
which increase numbers
21/60

Revision Combinators Encodings Functional programming Review
Recursion example
Suppose we want to compute factorials:
f(n)=if (n==0)then1elsen∗f(n−1)
We’ll need some helper functions / encodings: ▶ Church numerals: cn = λfx .f n (x )
▶ ISZERO := λn.n (λx.FALSE) TRUE
▶ MULT := λxyz.x(yz) (seen previously)
▶ PRED := λnfx.n(λgh.h(gf ))(λy.x)(λu.u) ▶ This gives the predecessor of a number
▶ PRED1=0,PRED2=1,…,PREDn=(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
We want to write something like:
“FACT n = (ISZERO n) 1 (MULT n (FACT (PRED n)))”
We can’t directly define functions self referentially, so we use the Y Combinator:
▶ H = λfn.(ISZERO n) 1 (MULT n (f (PRED n)))
▶ H takes a function and a number. If the number is zero, it returns 1, otherwise it returns the product of n and f(n-1)
24/60

Revision Combinators Encodings Functional programming Review
Recursion example
We want to write something like:
“FACT n = (ISZERO n) 1 (MULT n (FACT (PRED n)))”
We can’t directly define functions self referentially, so we use the Y Combinator:
▶ H = λfn.(ISZERO n) 1 (MULT n (f (PRED n)))
▶ H takes a function and a number. If the number is zero, it
returns 1, otherwise it returns the product of n and f(n-1)
▶ FACTORIAL = Y H
▶ Because YH = H (YH ), the Y Combinator helps us to apply the H function to itself
24/60

Revision Combinators Encodings Functional programming Review
Factorial 5(overview)
▶ H = λfn.(ISZERO n) 1 (MULT n (f (PRED n))) ▶ FACTORIAL = Y H
H takes a function f and a number n. It returns 1 if the number is 0, otherwise the product of n and f (n − 1)
FACTORIAL 5
25/60

Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3 =
= =
= =
=
= =
26/60

Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3 =YH3
= =
= =
=
= =
26/60

Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3 =YH3
= H (Y H ) 3 =
= =
=
= =
(Y Combinator)
26/60

Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3 =YH3
= H (Y H ) 3 (Y Combinator)
( ( ( )))
(YH )3 (H)
= λfn.(ISZERO n)1 MULT n =
=
=
= =
f (PRED n)
26/60

Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 1)
FACTORIAL 3 =YH3
= 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) ( ( ))
=(ISZERO 3)1 MULT 3 Y H (PRED 3) =
= =
3 (β) (β)
26/60

Revision Combinators Encodings Functional programming Review
Factorial 3 (detailed 2)
FACTORIAL 3
= … = MULT 3 (Y H 2) =
=
=
=
=
=
=
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)) =
=
=
=
=
=
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))) =
=
=
=
=
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…
=
=
=
=
27/60

Revision Combinators Encodings Functional programming Review
Y Combinator reminder
This worked because the Y Combinator
( )( )
Y = λf . λx.f (xx) λx.f (xx) Has the property that F(YF) = YF for all F.
Important:
▶ When performing the reductions, use that property ▶ Don’t β-reduce the Y Combinator directly.
28/60

Revision Combinators Encodings Functional programming Review
Booleans
Reminder: our definition of Church Booleans lets us write:
simply as:
if BthenPelseQ BPQ
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
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.
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)
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
34/60

Revision Combinators Encodings Functional programming Review
Numbers (Barendregt style)
Addition is more complex, but quite intuitive
▶ base case: ADD(0, y) = y
▶ recursivecase: 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 “ifx is0theny else(1+f(x−1, y))”
35/60

Revision Combinators Encodings Functional programming Review
Generalised recursion
We can generalise this idea of recursion to support an arbitrary number of variables, base and recursive cases.
See section 3.11 in the reference text (Barendregt) if you’re interested in the fine details of this.
36/60

Revision Combinators Encodings Functional programming Review
Pairs (Church)
Similar idea, but not identical to the encoding Barendregt uses.
▶ PAIR = λxyz.zxy
▶ FIRST = λp.p TRUE
▶ SECOND = λp.p FALSE
e.g.
FIRST (PAIR a b) = (λp.p TRUE) (PAIR a b) =
= = = = = = =
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.
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))
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
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 =
▶ ISNIL = ▶ HEAD = ▶ TAIL = ▶ CONS =
41/60

Revision Combinators Encodings Functional programming Review
List (Church)
Encoding:
▶ NIL = PAIR TRUE TRUE (an empty list) ▶ ISNIL =
▶ HEAD =
▶ TAIL =
▶ CONS =
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 =
▶ TAIL =
▶ CONS =
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 =
▶ CONS =
41/60

Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= = = = = = =
42/60

Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL = FIRST NIL =
=
=
=
=
=
42/60

Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= FIRST NIL
= (λp.p TRUE) NIL =
=
=
=
=
42/60

Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL NIL
= FIRST NIL
= (λp.p TRUE) NIL
= NIL 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 =
=
=
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 =
=
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 =
42/60

Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d} =
= = = = = =
43/60

Revision Combinators Encodings Functional programming Review
List (Church)
Example:
ISNIL {a, b, c, d} = FIRST {a,b,c,d} =
=
=
=
=
=
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} =
=
=
=
=
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 =
=
=
=
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 =
=
=
43/60

Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a,b,c,d} =
= = = = = =
44/60

Revision Combinators Encodings Functional programming Review
List (Church) example
HEAD {a,b,c,d}
= (λz.FIRST (SECOND z)) {a,b,c,d} =
=
=
=
=
=
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}) =
=
=
=
=
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 =
=
=
44/60

Revision Combinators Encodings Functional programming Review
List (Church) example (continued)
HEAD {a,b,c,d} = …
= = = = = = = =
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 =
=
=
= = = =
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) =
=
=
45/60

Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht.PAIR FALSE (PAIR h t) CONS a NIL
= = = =
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 =
=
=
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
=
=
46/60

Revision Combinators Encodings Functional programming Review
List (Church) cons
CONS = λht.PAIR FALSE (PAIR h t) CONS b (CONS a NIL)
= = = = = =
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) =
=
=
=
=
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)) =
=
=
47/60

Revision Combinators Encodings Functional programming Review
List encodings
We now have structured data and recursion!
48/60

Revision Combinators Encodings Functional programming Review
List encodings
We now have structured data and recursion!
Don’t forget, just as there are many ways to represent a List ADT in imperative programming, there are many possible encodings for lists and other structures in lambda calculus.
48/60

Revision Combinators Encodings Functional programming Review
Fibonacci
In the last tutorial, you probably implemented Fibonacci like this:
(defun fib (x) (if (< x 2) 1 (+ (fib (− x 1)) (fib (− x 2))) ) ) 50/60 Revision Combinators Encodings Functional programming Review Fibonacci In the last tutorial, you probably implemented Fibonacci like this: (defun fib (x) (if (< x 2) 1 (+ (fib (− x 1)) (fib (− x 2))) ) ) This works, but is not very efficient (exponential time complexity!) 50/60 Revision Combinators Encodings Functional programming Review Fibonacci In the last tutorial, you probably implemented Fibonacci like this: (defun fib (x) (if (< x 2) 1 (+ (fib (− x 1)) (fib (− x 2))) ) ) This works, but is not very efficient (exponential time complexity!) In imperative programming you would use variables to store the sequence (linear time complexity). 50/60 Revision Combinators Encodings Functional programming Review Fibonacci In the last tutorial, you probably implemented Fibonacci like this: (defun fib (x) (if (< x 2) 1 (+ (fib (− x 1)) (fib (− x 2))) ) ) This works, but is not very efficient (exponential time complexity!) In imperative programming you would use variables to store the sequence (linear time complexity). A comparable approach in FP is to compute the sequence, e.g. as a list. 50/60 Revision Combinators Encodings Functional programming Review Lists in LISP nil (cons e l) (list a b c ...) (car l) (cdr l) (last l) (append a b) (member e l) (reverse l) ; an empty list ; prepend e to list l ; new list (a b c ...) ; the head element of l ; the tail list of l ; the last element l ; combine two lists ; first sublist starting e in l ; a mirror of the list 51/60 Revision Combinators Encodings Functional programming Review Lists in LISP (examples) ? (list 1 2 3) (1 2 3) ? (cons 1 (cons 2 (cons 3 nil))) (1 2 3) ? (member 2 (list 1 3 5)) NIL ? (member 3 (list 1 3 5)) (3 5) ? (cdr (list 1 2 3 4 5)) (2 3 4 5) ? (cdr (cdr (list 1 2 3 4 5))) (3 4 5) ? (car (cdr (list 1 2 3 4 5))) 2 52/60 Revision Combinators Encodings Functional programming Review Fibonacci Idea: given part of the Fibonacci sequence and a number, add that many more elements of the sequence. (defun fib (n a) (if (zerop n) a (fib (− n 1) ( cons (+ (car a) (car (cdr a))) a )))) (fib 100 (list 1 0)) 53/60 Revision Combinators Encodings Functional programming Review Fibonacci Making it a bit nicer: ▶ We can make optional (default) arguments ▶ (car (cdr x)) = (cadr x) ▶ You can repeat the a, d as many times as required ▶ e.g. (cadddr x) is the 4th element (defun fib (n &optional (a ( list 1 0))) (if (zerop n) a (fib (− n 1) ( cons (+ (car a) (cadr a)) a )))) (fib 100) 54/60 Revision Combinators Encodings Functional programming Review A note on loops in LISP I avoided using loops to keep the first example closer to lamda calculus. There are several ways to use loops in LISP, here’s one: (defun fib (n) (loop for f1 = 0 then f2 and f2 = 1 then (+ f1 f2) repeat n finally (return f1))) (fib 100) 1 1source: https://www.cliki.net/Fibonacci 55/60 Revision Combinators Encodings Functional programming Review Java public boolean isPrime(long number) { return number > 1 &&
LongStream
.rangeClosed(2, (long) Math.sqrt(number)) . noneMatch( index −> number % index == 0);
}
isPrime (9220000000000000039L) // Output : true
2
▶ “.rangeClosed” gives a stream of values within the range ▶ “.noneMatch” checks the stream against a predicate
▶ “variable -> expression” is a lambda abstraction!
▶ It takes a value (index) from the range, and tests if it divides the number we’re checking.
2source: https://www.voxxed.com/2015/12/
functional-vs-imperative-programming-fibonacci-prime-and-factorial-in-j
56/60

Revision Combinators Encodings Functional programming Review
Java
public boolean isPrime(long number) { return number > 1 &&
LongStream
.rangeClosed(2, (long) Math.sqrt(number)) .parallel()
. noneMatch( index −> number % index == 0);
}
isPrime (9220000000000000039L) // Output : true
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-j
57/60

Revision Combinators Encodings Functional programming Review
Python
If you write much Python, you probably write more functional programming code than you thought.
>>> grades = [43, 68, 35, 89, 67, 65, 70]
>>> len( list ( filter (lambda x: x>=50, grades )))
5
>>> sum(map(lambda x: x>=50, grades))
5
>>> [ x + 5 f o r x i n g r a d e s ]
[48, 73, 40, 94, 72, 70, 75] >>>max([x+5 for x in grades])
94
58/60

Revision Combinators Encodings Functional programming Review
Python
>>> >>> >>> >>>
3620
from functools import reduce
prices = [43, 68, 35, 89, 67, 65, 70] sales = [3, 5, 0, 3, 2, 10, 30] reduce(lambda x,y: x+y,
map(lambda x: x[0]∗x[1], zip(prices , sales )))
▶ 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, … ]
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

Related Posts