代写 data structure Scheme Haskell lisp python AI Lambda Calculus COMP2022: Formal Languages and Logic

COMP2022: Formal Languages and Logic
2018, Semester 2, Week 2
Joseph Godbehere 9th 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 Currying Encodings LISP Lambdas in Languages Review
outline
▶ Revision – Lambda Calculus ▶ Currying
▶ Encodings
▶ Functional Programming: LISP
3/60

Revision Currying Encodings LISP Lambdas in Languages Review
Operations
▶ Application
▶ Notation: A · B
▶ Expression B is applied to expression A
4/60

Revision Currying Encodings LISP Lambdas in Languages Review
Operations
▶ Application
▶ Notation: A · B
▶ Expression B is applied to expression A
▶ Abstraction
▶ λx.M
▶ Variable x is abstracted in expression M
4/60

Revision Currying Encodings LISP Lambdas in Languages Review
Rewriting
▶ M [x := N ]
▶ Expression M , but all free occurrences of x are replaced with
N
▶ e.g.
▶ (xyzλx.(zxz))[x := A] = ▶ (xyzλx.(zxz))[y := B] = ▶ (xyzλx.(zxz))[z := C] =
5/60

Revision Currying Encodings LISP Lambdas in Languages Review
Rewriting
▶ M [x := N ]
▶ Expression M , but all free occurrences of x are replaced with
N
▶ e.g.
▶ (xyzλx.(zxz))[x := A] = (Ayzλx.(zxz)) ▶ (xyzλx.(zxz))[y := B] =
▶ (xyzλx.(zxz))[z := C] =
5/60

Revision Currying Encodings LISP Lambdas in Languages Review
Rewriting
▶ M [x := N ]
▶ Expression M , but all free occurrences of x are replaced with
N
▶ e.g.
▶ (xyzλx.(zxz))[x := A] = (Ayzλx.(zxz))
▶ (xyzλx.(zxz))[y := B] = (xBzλx.(zxz)) ▶ (xyzλx.(zxz))[z := C] =
5/60

Revision Currying Encodings LISP Lambdas in Languages Review
Rewriting
▶ M [x := N ]
▶ Expression M , but all free occurrences of x are replaced with
N
▶ e.g.
▶ (xyzλx.(zxz))[x := A] = (Ayzλx.(zxz))
▶ (xyzλx.(zxz))[y := B] = (xBzλx.(zxz)) ▶ (xyzλx.(zxz))[z := C] = (xyCλx.(CxC))
5/60

Revision Currying Encodings LISP Lambdas in Languages Review
α-reduction
▶ Rename a λ to remove a name conflict
▶ λx.M =λy.(M[x :=y])
▶ y must be a new variable
▶ You must not choose a symbol that is already in use
6/60

Revision Currying Encodings LISP Lambdas in Languages Review
β -reduction
▶ Solve an abstraction
▶ (λx.M)·N =M[x :=N]
▶ Note: the free occurrences of x in M is exactly the set of occurrences which bound to the λx. in (λx.M)
7/60

Revision Currying Encodings LISP Lambdas in Languages Review
outline
▶ Revision – Lambda Calculus ▶ Currying
▶ Encodings
▶ Functional Programming
8/60

Revision Currying Encodings LISP Lambdas in Languages Review
Two arguments
▶ Suppose we have a function f(x,y) which requires two arguments.
9/60

Revision Currying Encodings LISP Lambdas in Languages Review
Two arguments
▶ Suppose we have a function f(x,y) which requires two arguments.
▶ LetFx =λy.f(x,y)andF=λx.Fx
9/60

Revision Currying Encodings LISP Lambdas in Languages Review
Two arguments
▶ Suppose we have a function f(x,y) which requires two arguments.
▶ LetFx =λy.f(x,y)andF=λx.Fx
▶ F is a function which takes one input, and returns a function Fx , which will take the next input.
9/60

Revision Currying Encodings LISP Lambdas in Languages Review
Example
Normalarithmetic: f(x,y)=(x+y)/2 Lambda calculus: (λx.(λy.(x + y)/2))
((λx.(λy.(x + y)/2)) · 5) · 7
10/60

Revision Currying Encodings LISP Lambdas in Languages Review
Example
Normalarithmetic: f(x,y)=(x+y)/2 Lambda calculus: (λx.(λy.(x + y)/2))
((λx.(λy.(x + y)/2)) · 5) · 7 = (λy.(5 + y)/2) · 7
10/60

Revision Currying Encodings LISP Lambdas in Languages Review
Currying
▶ A n-ary parameter function can be represented in the lambda calculus through Currying
11/60

Revision Currying Encodings LISP Lambdas in Languages Review
Currying
▶ A n-ary parameter function can be represented in the lambda calculus through Currying
▶ An n argument function returns an (n − 1) argument function, which returns an (n − 2) argument function, …
11/60

Revision Currying Encodings LISP Lambdas in Languages Review
Evaluation
Recall the example from earlier:
((λx.(λy.(x + y)/2)) · 5) · 7 = (λy.(5 + y)/2) · 7
= (5 + 7)/2
=6
The function is partially evaluated at each step ▶ The first function returns (λy.(5 + y)/2)
12/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Too many parentheses! Let’s make it simpler:
13/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Too many parentheses! Let’s make it simpler: ▶ Wecanwrite(A·B)asAB
13/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Too many parentheses! Let’s make it simpler:
▶ Wecanwrite(A·B)asAB
▶ For function application we use association to the left: ABCDEF ≡ (((((AB)C)D)E)F)
13/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ For function abstraction we use association to the right λx1x2x3…xk .M
14/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ For function abstraction we use association to the right
λx1x2x3…xk .M
= λx1.λx2.λx3….λxk .M
14/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ For function abstraction we use association to the right
λx1x2x3…xk .M
= λx1.λx2.λx3….λxk .M
= (λx1.(λx2.(λx3.(…(λxk .M )…))))
14/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Abstraction is right associative
▶ Application is left associative
▶ The abstractions and applications match up nicely:
(λxyz.((z −x)×y)) 4 2 3
15/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Abstraction is right associative ▶ Application is left associative ▶ If we wrote it out in full…
(λxyz.((z −x)×y)) 4 2 3
(( ))
= λx.λy.(λz.((z−x)×y)) 423
16/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Abstraction is right associative ▶ Application is left associative ▶ If we wrote it out in full…
= =
=
(λxyz.((z −x)×y)) 4 2 3 (( ))
λx.λy.(λz.((z−x)×y)) 423
((( ( )) ) )
λx. λy.(λz.((z −x)×y)) (( ))
λy.(λz.((z −4)×y)) ·2 ·3
·4 ·2 ·3
(λz.((z −4)×2))·3 (3−4)×2
=
= =−2
16/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Question:
1. Is λx.xy = (λx.(xy)), or 2. is λx.xy = (λx.x)y ?
17/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Question:
1. Is λx.xy = (λx.(xy)), or 2. is λx.xy = (λx.x)y ?
▶ Answer: (1), it’s (λx.(xy))
17/60

Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Question:
1. Is λx.xy = (λx.(xy)), or 2. is λx.xy = (λx.x)y ?
▶ Answer: (1), it’s (λx.(xy))
▶ Use parentheses to limit the scope of the λ if needed
17/60

Revision Currying Encodings LISP Lambdas in Languages Review
Currying
▶ Suppose we wanted to abstract a function with k arguments: (λx1x2x3…xk .N )
18/60

Revision Currying Encodings LISP Lambdas in Languages Review
Currying
▶ Suppose we wanted to abstract a function with k arguments: (λx1x2x3…xk .N )
▶ If we apply k arguments, v1…vk, we get this: (λx1x2x3…xk .N )v1v2v3…vk
▶ Each β-reduction partially evaluates the function:
▶ v1 replaces x1. The resulting function takes k − 1 arguments:
(λx2x3…xk .N [x1 : v1])v2v3…vk ▶ … then v2 would replace x2, etc.
18/60

Revision Currying Encodings LISP Lambdas in Languages Review
outline
▶ Revision – Lambda Calculus
▶ Currying
▶ Encodings
▶ Functional Programming: LISP
19/60

Revision Currying Encodings LISP Lambdas in Languages Review
But… How do we actually do anything?
20/60

Revision Currying Encodings LISP Lambdas in Languages Review
Untyped Lambda Calculus
▶ Lambda calculus does not have primitives ▶ No numbers
▶ No arithmetic operators
▶ No aggregated data types (classes etc.) ▶ No control flow (only recursion!)
▶ However, I’m claiming that it is computationally equivalent to a Turing Machine!
21/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
▶ Boolean constants:
▶ TRUE := λxy.x ▶ FALSE := λxy.y
22/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
▶ Boolean constants: ▶ TRUE := λxy.x
▶ FALSE := λxy.y
▶ Now we can do conditional logic:
▶ IFELSE := λfxy.fxy has semantics similar to:
▶ if then else
▶ If is true, return result of , otherwise
22/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE TRUE A B
23/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE TRUE A B
= (λfxy.fxy) (λxy.x) A B (macro substitution)
23/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE TRUE A B
= (λfxy.fxy) (λxy.x) A B (macro substitution) = (λfay.fay) (λxy.x) A B (α-reduction)
23/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE TRUE A B = (λfxy.fxy) (λxy.x) A B = (λfay.fay) (λxy.x) A B = (λfab.fab) (λxy.x) A B
(macro substitution) (α-reduction) (α-reduction)
23/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE TRUE A B
= (λfxy.fxy) (λxy.x) A B
= (λfay.fay) (λxy.x) A B
= (λfab.fab) (λxy.x) A B
= (λab .(λxy .x )ab ) A B
(macro substitution) (α-reduction) (α-reduction) (β -reduction)
23/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE TRUE A B
= (λfxy.fxy) (λxy.x) A B
= (λfay.fay) (λxy.x) A B
= (λfab.fab) (λxy.x) A B
= (λab .(λxy .x )ab ) A B
= (λb.(λxy.x)Ab) B
(macro substitution) (α-reduction) (α-reduction) (β -reduction) (β-reduction)
23/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE TRUE A B
= (λfxy.fxy) (λxy.x) A B
= (λfay .fay ) (λxy .x ) A B
= (λfab .fab ) (λxy .x ) A B
= (λab .(λxy .x )ab ) A B
= (λb .(λxy .x )Ab ) B
= (λxy .x )AB )
(macro substitution) (α-reduction) (α-reduction) (β -reduction) (β -reduction) (β -reduction)
23/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE TRUE A B
= (λfxy.fxy) (λxy.x) A B
= (λfay .fay ) (λxy .x ) A B
= (λfab .fab ) (λxy .x ) A B
= (λab .(λxy .x )ab ) A B
= (λb .(λxy .x )Ab ) B
= (λxy .x )AB )
= (λy .A)B )
(macro substitution) (α-reduction) (α-reduction) (β -reduction) (β -reduction) (β -reduction) (β -reduction)
23/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE TRUE A B = (λfxy.fxy) (λxy.x) A
B B B
(macro substitution) (α-reduction) (α-reduction) (β -reduction) (β -reduction) (β -reduction) (β -reduction) (β -reduction)
= (λfay .fay ) (λxy .x )
= (λfab .fab ) (λxy .x )
= (λab .(λxy .x )ab ) A
= (λb .(λxy .x )Ab ) B
= (λxy .x )AB )
= (λy .A)B )
= A
A A B
23/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE FALSE A B
24/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE FALSE A B
= (λfxy.fxy) (λxy.y) A B (macro substitution)
24/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE FALSE A B
= (λfxy.fxy) (λxy.y) A B (macro substitution) = (λfay.fay) (λxy.y) A B (α-reduction)
24/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE FALSE A B
= (λfxy.fxy) (λxy.y) A B
= (λfay.fay) (λxy.y) A B
= (λfab.fab) (λxy.y) A B
= (λab.(λxy.y)ab) A B
(macro substitution) (α-reduction) (α-reduction) (β-reduction)
24/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE FALSE A B
= (λfxy.fxy) (λxy.y) A B
= (λfay.fay) (λxy.y) A B
= (λfab.fab) (λxy.y) A B
= (λab.(λxy.y)ab) A B
= (λb.(λxy.y)Ab) B
(macro substitution) (α-reduction) (α-reduction) (β-reduction) (β-reduction)
24/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE FALSE A B
= (λfxy.fxy) (λxy.y) A B
= (λfay.fay) (λxy.y) A B
= (λfab.fab) (λxy.y) A B
= (λab .(λxy .y )ab ) A B
= (λb .(λxy .y )Ab ) B
= (λxy .y )AB )
(macro substitution) (α-reduction) (α-reduction) (β -reduction) (β -reduction) (β -reduction)
24/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE FALSE A B
= (λfxy.fxy) (λxy.y) A B
= (λfay.fay) (λxy.y) A B
= (λfab.fab) (λxy.y) A B
= (λab .(λxy .y )ab ) A B
= (λb .(λxy .y )Ab ) B
= (λxy .y )AB )
= (λy.y)B)
(macro substitution) (α-reduction) (α-reduction) (β -reduction) (β -reduction) (β -reduction) (β -reduction)
24/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
IFELSE FALSE A B
= (λfxy.fxy) (λxy.y) A B
= (λfay.fay) (λxy.y) A B
= (λfab.fab) (λxy.y) A B
(macro substitution) (α-reduction) (α-reduction) (β -reduction) (β -reduction) (β -reduction) (β -reduction) (β -reduction)
= (λab .(λxy .y )ab ) A
= (λb .(λxy .y )Ab ) B
= (λxy .y )AB )
= (λy.y)B)
= B
B
24/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
▶ Boolean constants: ▶ TRUE := λxy.x
▶ FALSE := λxy.y ▶ IFELSE := λfxy.fxy
▶ Boolean operators: ▶ NOT := λfxy.fyx
▶ OR := λxy.xxy ▶ AND := λxy.xyx
25/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: NOT
▶ NOT := λfxy.fyx
▶ NOT is a function which takes 3 arguments
▶ Suppose f was a function which takes 2 arguments ▶ x, y would be those arguments
26/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
NOT TRUE
27/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
NOT TRUE
= (λfxy.fyx)(λxy.x) (macro substitution)
27/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
NOT TRUE
= (λfxy.fyx)(λxy.x) (macro substitution) = (λfxy.fyx)(λay.a) (α-reduction)
27/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
NOT TRUE
= (λfxy.fyx)(λxy.x) = (λfxy.fyx)(λay.a) = (λfxy.fyx)(λab.a)
(macro substitution) (α-reduction) (α-reduction)
27/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
NOT TRUE
= (λfxy.fyx)(λxy.x) = (λfxy.fyx)(λay.a) = (λfxy.fyx)(λab.a) = λxy.(λab.a)yx
(macro substitution) (α-reduction) (α-reduction) (β-reduction)
27/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
NOT TRUE
= (λfxy.fyx)(λxy.x)
= (λfxy.fyx)(λay.a)
= (λfxy.fyx)(λab.a)
= λxy.(λab.a)yx
= λxy.(λb.y)x
(macro substitution) (α-reduction) (α-reduction) (β-reduction) (β-reduction)
27/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
NOT TRUE
= (λfxy.fyx)(λxy.x)
= (λfxy .fyx )(λay .a )
= (λfxy .fyx )(λab .a )
= λxy .(λab .a )yx
= λxy .(λb .y )x
= λxy .y
(macro substitution) (α-reduction) (α-reduction) (β -reduction) (β -reduction) (β -reduction)
27/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
NOT TRUE
= (λfxy.fyx)(λxy.x)
= (λfxy .fyx )(λay .a )
= (λfxy .fyx )(λab .a )
= λxy .(λab .a )yx
= λxy .(λb .y )x
= λxy .y
= FALSE
(macro substitution) (α-reduction) (α-reduction) (β -reduction) (β -reduction) (β -reduction) (macro substitution)
27/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: numbers
▶ The natural numbers can be thought of as a sequence, starting from 0, and successively increasing by one.
28/60

Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: numbers
▶ The natural numbers can be thought of as a sequence, starting from 0, and successively increasing by one.
▶ More formally, we can define them inductively: ▶ Basic clause: 0 is a number and is in the set
▶ Inductive clause: for any element x in the natural numbers, x + 1 is an element of the natural numbers
28/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
▶ Natural numbers in lambda calculus have two constructors:
▶ ZERO := λxy.y
▶ This represents 0
▶ It is the same formula we used to encode FALSE
▶ SUCCESSOR := λxyz.y(xyz)
▶ Returns the next number in the sequence
29/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
▶ Natural numbers in lambda calculus have two constructors:
▶ ZERO := λxy.y
▶ This represents 0
▶ It is the same formula we used to encode FALSE ▶ SUCCESSOR := λxyz.y(xyz)
▶ Returns the next number in the sequence
▶ We’re now ready to start constructing the natural numbers!
29/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
ONE
= SUCCESSOR ZERO
30/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
ONE
= SUCCESSOR ZERO
= (λxyz.y(xyz))(λxy.y) (macro)
30/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
ONE
= SUCCESSOR ZERO
= (λxyz.y(xyz))(λxy.y) (macro) = (λxyz.y(xyz))(λab.b) (α)
30/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
ONE
= SUCCESSOR ZERO
= (λxyz.y(xyz))(λxy.y) (macro)
= (λxyz.y(xyz))(λab.b) (α)
= λyz.y((λab.b)yz) (β)
30/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
ONE
= SUCCESSOR ZERO
= (λxyz.y(xyz))(λxy.y) (macro)
= (λxyz.y(xyz))(λab.b) (α)
= λyz.y((λab.b)yz) (β)
= λyz.y((λb.b)z) (β)
30/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
TWO
= SUCCESSOR ONE
= (λxyz.y(xyz))(λyz.yz) (macro)
31/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
TWO
= SUCCESSOR ONE
= (λxyz.y(xyz))(λyz.yz) (macro) = (λxyz.y(xyz))(λab.ab) (α)
31/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
TWO
= SUCCESSOR ONE
= (λxyz.y(xyz))(λyz.yz) (macro) = (λxyz.y(xyz))(λab.ab) (α) = λyz.y((λab.ab)yz) (β)
31/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
TWO
= SUCCESSOR ONE
= (λxyz.y(xyz))(λyz.yz) (macro)
= (λxyz.y(xyz))(λab.ab) (α)
= λyz.y((λab.ab)yz) (β)
= λyz.y((λb.yb)z) (β)
31/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
THREE
= SUCCESSOR TWO = …
= λyz.y(y(yz))
32/60

Revision Currying Encodings LISP Lambdas in Languages Review
Church numerals
THREE
= SUCCESSOR TWO = …
= λyz.y(y(yz))
FOUR
= SUCCESSOR THREE = …
= λyz.y(y(y(yz)))
32/60

Revision Currying Encodings LISP Lambdas in Languages Review
Arithmetic?
▶ We have numbers. Do they work?
33/60

Revision Currying Encodings LISP Lambdas in Languages Review
Arithmetic?
▶ We have numbers. Do they work?
▶ Arithmetic:
▶ ADD := λxypq.xp(ypq)
▶ MULT := λxyz.x(yz) ▶ EXP := λxy.yx
33/60

Revision Currying Encodings LISP Lambdas in Languages Review
Addition example
ADD TWO THREE
34/60

Revision Currying Encodings LISP Lambdas in Languages Review
Addition example
ADD TWO THREE
()
= λxypq.xp(ypq) (λyz.y(yz)) (λyz.y(y(yz)))
34/60

Revision Currying Encodings LISP Lambdas in Languages Review
Addition example
ADD TWO THREE
()
= (λxypq.xp(ypq)) (λyz.y(yz)) (λyz.y(y(yz)))
= λxypq.xp(ypq) (λab.a(ab)) (λcd.c(c(cd))) (α)
34/60

Revision Currying Encodings LISP Lambdas in Languages Review
Addition example
ADD TWO THREE
()
= (λxypq.xp(ypq)) (λyz.y(yz)) (λyz.y(y(yz)))
= λxypq.xp(ypq) (λab.a(ab)) (λcd.c(c(cd))) (α)
= (λypq.(λab.a(ab))p(ypq)) (λcd.c(c(cd))) (β)
= (λypq.(λb.p(pb))(ypq)) (λcd.c(c(cd))) (β)
= (λypq.p(p(ypq))) (λcd.c(c(cd))) (β)
34/60

Revision Currying Encodings LISP Lambdas in Languages Review
Multiplication example
MULT EIGHT THIRTEEN
35/60

Revision Currying Encodings LISP Lambdas in Languages Review
Multiplication example
MULT EIGHT THIRTEEN
= (λxyz .x (yz ))(λfx .f (f (f (f (f (f (f (fx ))))))))
(λfx .f (f (f (f (f (f (f (f (f (f (f (f (fx )))))))))))))
35/60

Revision Currying Encodings LISP Lambdas in Languages Review
Multiplication example
Just kidding
MULT EIGHT THIRTEEN
= (λxyz .x (yz ))(λfx .f (f (f (f (f (f (f (fx ))))))))
(λfx .f (f (f (f (f (f (f (f (f (f (f (f (fx ))))))))))))) = …
35/60

Revision Currying Encodings LISP Lambdas in Languages Review
Multiplication example
MULT TWO THREE
36/60

Revision Currying Encodings LISP Lambdas in Languages Review
Multiplication example
MULT TWO THREE
= (λxyz.x(yz)) TWO THREE
36/60

Revision Currying Encodings LISP Lambdas in Languages Review
Multiplication example
MULT TWO THREE
= (λxyz.x(yz)) TWO THREE = (λyz.TWO (yz)) THREE
36/60

Revision Currying Encodings LISP Lambdas in Languages Review
Multiplication example
MULT TWO THREE
= (λxyz.x(yz)) TWO THREE = (λyz.TWO (yz)) THREE
= λz.TWO (THREE z)
36/60

Revision Currying Encodings LISP Lambdas in Languages Review
Multiplication example
MULT TWO THREE
= (λxyz.x(yz)) TWO THREE
= (λyz.TWO (yz)) THREE
= λz.TWO (THREE z) ()
= λz. λfx.f (fx) (THREE z)
( ( ))
= λz. λx.(THREE z) (THREE z)x
()
= λzx.(THREE z) (THREE z)x
( )( )
= λzx. (λfx.f (f (fx))) z ((λfx.f (f (fx))) z)x
36/60

Revision Currying Encodings LISP Lambdas in Languages Review
Recursion
In imperative languages, we can easily write recursive code:
def factorial(x): if x == 1:
return 1
return x∗factorial(x−1)
… by referencing the method itself by name.
So far, we haven’t directly seen iteration or recursion in the lambda calculus.
37/60

Revision Currying Encodings LISP Lambdas in Languages Review
Recursion
In the last tutorial you tried to reduce:
(λx .xx )(λx .xx )
38/60

Revision Currying Encodings LISP Lambdas in Languages Review
Recursion
In the last tutorial you tried to reduce:
(λx .xx )(λx .xx ) … and discovered that it looped forever.
38/60

Revision Currying Encodings LISP Lambdas in Languages Review
Recursion
In the last tutorial you tried to reduce:
(λx .xx )(λx .xx ) … and discovered that it looped forever.
This is related to a slightly more useful construct called the Y Combinator:
Y ≡ λf .(λx.f (xx))(λx.f (xx))
38/60

Revision Currying Encodings LISP Lambdas in Languages Review
outline
▶ Revision – Lambda Calculus
▶ Currying
▶ Encodings
▶ Functional Programming: LISP
39/60

Revision Currying Encodings LISP Lambdas in Languages Review
LISP
▶ LISP is the second oldest programming language in common use
▶ Invented in 1958 by John McCarthy
▶ Was very popular in the AI boom
▶ Is a functional programming language
▶ Is a practical implementation of the Lambda Calculus
▶ Has many dialects (e.g. Clojure, Common Lisp, Racket, Scheme, etc.)
40/60

Revision Currying Encodings LISP Lambdas in Languages Review
LISP = LISt Processing
▶ LISP has atoms
▶ Numbers, e.g. 10
▶ Identifiers, e.g. Foo
▶ Strings, e.g. “filename”
▶ LISP has lists
▶ can contain other lists
▶ can contain atoms
▶ can contain nothing (empty)
▶ very small syntax:

Related Posts