COMP2022: Formal Languages and Logic – 2018, Semester 2, Week 2
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
▶ Abstraction
▶ λx .M
▶ Variable x is abstracted in expression M
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] =
(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
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
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
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.
▶ Let Fx = λy .f (x , y) and F = λx .Fx
▶ F is a function which takes one input, and returns a function
Fx , which will take the next input.
▶ The output of the second function will be f (x , y).
9/60
Revision Currying Encodings LISP Lambdas in Languages Review
Two arguments
▶ Suppose we have a function f (x , y) which requires two
arguments.
▶ Let Fx = λy .f (x , y) and F = λx .Fx
▶ F is a function which takes one input, and returns a function
Fx , which will take the next input.
▶ The output of the second function will be f (x , y).
9/60
Revision Currying Encodings LISP Lambdas in Languages Review
Two arguments
▶ Suppose we have a function f (x , y) which requires two
arguments.
▶ Let Fx = λy .f (x , y) and F = λx .Fx
▶ F is a function which takes one input, and returns a function
Fx , which will take the next input.
▶ The output of the second function will be f (x , y).
9/60
Revision Currying Encodings LISP Lambdas in Languages Review
Two arguments
▶ Suppose we have a function f (x , y) which requires two
arguments.
▶ Let Fx = λy .f (x , y) and F = λx .Fx
▶ F is a function which takes one input, and returns a function
Fx , which will take the next input.
▶ The output of the second function will be f (x , y).
9/60
Revision Currying Encodings LISP Lambdas in Languages Review
Example
Normal arithmetic: 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
= (5 + 7)/2
= 6
10/60
Revision Currying Encodings LISP Lambdas in Languages Review
Example
Normal arithmetic: 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
= (5 + 7)/2
= 6
10/60
Revision Currying Encodings LISP Lambdas in Languages Review
Example
Normal arithmetic: 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
= (5 + 7)/2
= 6
10/60
Revision Currying Encodings LISP Lambdas in Languages Review
Example
Normal arithmetic: 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
= (5 + 7)/2
= 6
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
▶ An n argument function returns an (n − 1) argument
function, which returns an (n − 2) argument function, …
▶ e.g. (λx .(λy .(λz .f (x , y , z )))) · 1 = (λy .(λz .f (1, y , z )))
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, …
▶ e.g. (λx .(λy .(λz .f (x , y , z )))) · 1 = (λy .(λz .f (1, y , z )))
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, …
▶ e.g. (λx .(λy .(λz .f (x , y , z )))) · 1 = (λy .(λz .f (1, y , z )))
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)
▶ 7 is then applied to the new function
▶ (5 + 7)/2 is evaluated and returned
12/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)
▶ 7 is then applied to the new function
▶ (5 + 7)/2 is evaluated and returned
12/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)
▶ 7 is then applied to the new function
▶ (5 + 7)/2 is evaluated and returned
12/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)
▶ 7 is then applied to the new function
▶ (5 + 7)/2 is evaluated and returned
12/60
Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Too many parentheses! Let’s make it simpler:
▶ We can write (A · B) as A B
▶ For function application we use association to the left:
ABCDEF ≡ (((((AB)C )D)E )F )
▶ i.e. the leftmost application happens first
13/60
Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Too many parentheses! Let’s make it simpler:
▶ We can write (A · B) as A B
▶ For function application we use association to the left:
ABCDEF ≡ (((((AB)C )D)E )F )
▶ i.e. the leftmost application happens first
13/60
Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Too many parentheses! Let’s make it simpler:
▶ We can write (A · B) as A B
▶ For function application we use association to the left:
ABCDEF ≡ (((((AB)C )D)E )F )
▶ i.e. the leftmost application happens first
13/60
Revision Currying Encodings LISP Lambdas in Languages Review
Notation
▶ Too many parentheses! Let’s make it simpler:
▶ We can write (A · B) as A B
▶ For function application we use association to the left:
ABCDEF ≡ (((((AB)C )D)E )F )
▶ i.e. the leftmost application happens first
13/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 )…))))
▶ This means the leftmost λ will match with the first input
applied to the function
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 )…))))
▶ This means the leftmost λ will match with the first input
applied to the function
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 )…))))
▶ This means the leftmost λ will match with the first input
applied to the function
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 )…))))
▶ This means the leftmost λ will match with the first input
applied to the function
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
=
(
λyz .((z − 4)× y)
)
2 3
=
(
λz .((z − 4)× 2)
)
3
= (3− 4)× 2
= − 2
15/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
=
(
λyz .((z − 4)× y)
)
2 3
=
(
λz .((z − 4)× 2)
)
3
= (3− 4)× 2
= − 2
15/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
=
(
λyz .((z − 4)× y)
)
2 3
=
(
λz .((z − 4)× 2)
)
3
= (3− 4)× 2
= − 2
15/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
=
(
λyz .((z − 4)× y)
)
2 3
=
(
λz .((z − 4)× 2)
)
3
= (3− 4)× 2
= − 2
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))
))
4 2 3
=
(((
λx .
(
λy .(λz .((z − x )× y))
))
· 4
)
· 2
)
· 3
=
((
λy .(λz .((z − 4)× y))
)
· 2
)
· 3
=
(
λz .((z − 4)× 2)
)
· 3
= (3− 4)× 2
= − 2
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))
))
4 2 3
=
(((
λx .
(
λy .(λz .((z − x )× y))
))
· 4
)
· 2
)
· 3
=
((
λy .(λz .((z − 4)× y))
)
· 2
)
· 3
=
(
λz .((z − 4)× 2)
)
· 3
= (3− 4)× 2
= − 2
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))
))
4 2 3
=
(((
λx .
(
λy .(λz .((z − x )× y))
))
· 4
)
· 2
)
· 3
=
((
λy .(λz .((z − 4)× y))
)
· 2
)
· 3
=
(
λz .((z − 4)× 2)
)
· 3
= (3− 4)× 2
= − 2
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))
))
4 2 3
=
(((
λx .
(
λy .(λz .((z − x )× y))
))
· 4
)
· 2
)
· 3
=
((
λy .(λz .((z − 4)× y))
)
· 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 ?
▶ 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
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
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 )
▶ 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
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
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!
▶ So, how can we represent data types?
▶ They must be expressed as functions, known as encodings
21/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!
▶ So, how can we represent data types?
▶ They must be expressed as functions, known as encodings
21/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!
▶ So, how can we represent data types?
▶ They must be expressed as functions, known as encodings
21/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!
▶ So, how can we represent data types?
▶ They must be expressed as functions, known as encodings
21/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
▶ If
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
▶ If
22/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)
= (λfab.fab) (λxy .x ) A B (α-reduction)
= (λab.(λxy .x )ab) A B (β-reduction)
= (λb.(λxy .x )Ab) B (β-reduction)
= (λxy .x )AB) (β-reduction)
= (λy .A)B) (β-reduction)
= A (β-reduction)
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)
= (λfab.fab) (λxy .x ) A B (α-reduction)
= (λab.(λxy .x )ab) A B (β-reduction)
= (λb.(λxy .x )Ab) B (β-reduction)
= (λxy .x )AB) (β-reduction)
= (λy .A)B) (β-reduction)
= A (β-reduction)
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)
= (λfab.fab) (λxy .x ) A B (α-reduction)
= (λab.(λxy .x )ab) A B (β-reduction)
= (λb.(λxy .x )Ab) B (β-reduction)
= (λxy .x )AB) (β-reduction)
= (λy .A)B) (β-reduction)
= A (β-reduction)
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)
= (λfab.fab) (λxy .x ) A B (α-reduction)
= (λab.(λxy .x )ab) A B (β-reduction)
= (λb.(λxy .x )Ab) B (β-reduction)
= (λxy .x )AB) (β-reduction)
= (λy .A)B) (β-reduction)
= A (β-reduction)
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)
= (λfab.fab) (λxy .x ) A B (α-reduction)
= (λab.(λxy .x )ab) A B (β-reduction)
= (λb.(λxy .x )Ab) B (β-reduction)
= (λxy .x )AB) (β-reduction)
= (λy .A)B) (β-reduction)
= A (β-reduction)
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)
= (λfab.fab) (λxy .x ) A B (α-reduction)
= (λab.(λxy .x )ab) A B (β-reduction)
= (λb.(λxy .x )Ab) B (β-reduction)
= (λxy .x )AB) (β-reduction)
= (λy .A)B) (β-reduction)
= A (β-reduction)
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)
= (λfab.fab) (λxy .x ) A B (α-reduction)
= (λab.(λxy .x )ab) A B (β-reduction)
= (λb.(λxy .x )Ab) B (β-reduction)
= (λxy .x )AB) (β-reduction)
= (λy .A)B) (β-reduction)
= A (β-reduction)
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)
= (λfab.fab) (λxy .x ) A B (α-reduction)
= (λab.(λxy .x )ab) A B (β-reduction)
= (λb.(λxy .x )Ab) B (β-reduction)
= (λxy .x )AB) (β-reduction)
= (λy .A)B) (β-reduction)
= A (β-reduction)
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)
= (λfab.fab) (λxy .x ) A B (α-reduction)
= (λab.(λxy .x )ab) A B (β-reduction)
= (λb.(λxy .x )Ab) B (β-reduction)
= (λxy .x )AB) (β-reduction)
= (λy .A)B) (β-reduction)
= A (β-reduction)
23/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)
= (λfab.fab) (λxy .y) A B (α-reduction)
= (λab.(λxy .y)ab) A B (β-reduction)
= (λb.(λxy .y)Ab) B (β-reduction)
= (λxy .y)AB) (β-reduction)
= (λy .y)B) (β-reduction)
= B (β-reduction)
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)
= (λfab.fab) (λxy .y) A B (α-reduction)
= (λab.(λxy .y)ab) A B (β-reduction)
= (λb.(λxy .y)Ab) B (β-reduction)
= (λxy .y)AB) (β-reduction)
= (λy .y)B) (β-reduction)
= B (β-reduction)
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)
= (λfab.fab) (λxy .y) A B (α-reduction)
= (λab.(λxy .y)ab) A B (β-reduction)
= (λb.(λxy .y)Ab) B (β-reduction)
= (λxy .y)AB) (β-reduction)
= (λy .y)B) (β-reduction)
= B (β-reduction)
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)
= (λfab.fab) (λxy .y) A B (α-reduction)
= (λab.(λxy .y)ab) A B (β-reduction)
= (λb.(λxy .y)Ab) B (β-reduction)
= (λxy .y)AB) (β-reduction)
= (λy .y)B) (β-reduction)
= B (β-reduction)
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)
= (λfab.fab) (λxy .y) A B (α-reduction)
= (λab.(λxy .y)ab) A B (β-reduction)
= (λb.(λxy .y)Ab) B (β-reduction)
= (λxy .y)AB) (β-reduction)
= (λy .y)B) (β-reduction)
= B (β-reduction)
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)
= (λfab.fab) (λxy .y) A B (α-reduction)
= (λab.(λxy .y)ab) A B (β-reduction)
= (λb.(λxy .y)Ab) B (β-reduction)
= (λxy .y)AB) (β-reduction)
= (λy .y)B) (β-reduction)
= B (β-reduction)
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)
= (λfab.fab) (λxy .y) A B (α-reduction)
= (λab.(λxy .y)ab) A B (β-reduction)
= (λb.(λxy .y)Ab) B (β-reduction)
= (λxy .y)AB) (β-reduction)
= (λy .y)B) (β-reduction)
= B (β-reduction)
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)
= (λfab.fab) (λxy .y) A B (α-reduction)
= (λab.(λxy .y)ab) A B (β-reduction)
= (λb.(λxy .y)Ab) B (β-reduction)
= (λxy .y)AB) (β-reduction)
= (λy .y)B) (β-reduction)
= B (β-reduction)
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)
= (λfab.fab) (λxy .y) A B (α-reduction)
= (λab.(λxy .y)ab) A B (β-reduction)
= (λb.(λxy .y)Ab) B (β-reduction)
= (λxy .y)AB) (β-reduction)
= (λy .y)B) (β-reduction)
= B (β-reduction)
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
▶ i.e. NOT outputs f , except its arguments have swapped
around!
26/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
▶ i.e. NOT outputs f , except its arguments have swapped
around!
26/60
Revision Currying Encodings LISP Lambdas in Languages Review
Encodings: truth
NOT TRUE
= (λfxy .fyx )(λxy .x ) (macro substitution)
= (λfxy .fyx )(λay .a) (α-reduction)
= (λfxy .fyx )(λab.a) (α-reduction)
= λxy .(λab.a)yx (β-reduction)
= λxy .(λb.y)x (β-reduction)
= λxy .y (β-reduction)
= FALSE (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)
= (λfxy .fyx )(λab.a) (α-reduction)
= λxy .(λab.a)yx (β-reduction)
= λxy .(λb.y)x (β-reduction)
= λxy .y (β-reduction)
= FALSE (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)
= (λfxy .fyx )(λab.a) (α-reduction)
= λxy .(λab.a)yx (β-reduction)
= λxy .(λb.y)x (β-reduction)
= λxy .y (β-reduction)
= FALSE (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)
= (λfxy .fyx )(λab.a) (α-reduction)
= λxy .(λab.a)yx (β-reduction)
= λxy .(λb.y)x (β-reduction)
= λxy .y (β-reduction)
= FALSE (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)
= (λfxy .fyx )(λab.a) (α-reduction)
= λxy .(λab.a)yx (β-reduction)
= λxy .(λb.y)x (β-reduction)
= λxy .y (β-reduction)
= FALSE (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)
= (λfxy .fyx )(λab.a) (α-reduction)
= λxy .(λab.a)yx (β-reduction)
= λxy .(λb.y)x (β-reduction)
= λxy .y (β-reduction)
= FALSE (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)
= (λfxy .fyx )(λab.a) (α-reduction)
= λxy .(λab.a)yx (β-reduction)
= λxy .(λb.y)x (β-reduction)
= λxy .y (β-reduction)
= FALSE (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)
= (λfxy .fyx )(λab.a) (α-reduction)
= λxy .(λab.a)yx (β-reduction)
= λxy .(λb.y)x (β-reduction)
= λxy .y (β-reduction)
= FALSE (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.
▶ 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
▶ Extremal clause: nothing is in the set of natural numbers
unless it is obtained by the inductive clause and basis clause
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
▶ Extremal clause: nothing is in the set of natural numbers
unless it is obtained by the inductive clause and basis clause
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
▶ Extremal clause: nothing is in the set of natural numbers
unless it is obtained by the inductive clause and basis clause
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
▶ Extremal clause: nothing is in the set of natural numbers
unless it is obtained by the inductive clause and basis clause
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
▶ Extremal clause: nothing is in the set of natural numbers
unless it is obtained by the inductive clause and basis clause
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
▶ We’re now ready to start constructing the natural numbers!
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
▶ 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
= (λxyz .y(xyz ))(λxy .y) (macro)
= (λxyz .y(xyz ))(λab.b) (α)
= λyz .y((λab.b)yz ) (β)
= λyz .y((λb.b)z ) (β)
= λyz .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 ) (β)
= λyz .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 ) (β)
= λyz .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 ) (β)
= λyz .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 ) (β)
= λyz .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 ) (β)
= λyz .yz (β)
30/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 ) (β)
= λyz .y(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 ) (β)
= λyz .y(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 ) (β)
= λyz .y(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 ) (β)
= λyz .y(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 ) (β)
= λyz .y(yz ) (β)
31/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
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?
▶ Arithmetic:
▶ ADD := λxypq .xp(ypq)
▶ MULT := λxyz .x (yz )
▶ EXP := λxy .yx
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
=
(
λ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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
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))) (β)
= λpq .p(p((λcd .c(c(cd)))pq)) (β)
= λpq .p(p((λd .p(p(pd)))q)) (β)
= λpq .p(p(p(p(pq)))) (β)
= FIVE
34/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 )))))))))))))
= …
Just kidding
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 )))))))))))))
= …
Just kidding
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 )))))))))))))
= …
Just kidding
35/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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX
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
)
= λzx .
(
λx .z (z (zx ))
)(
(λx .z (z (zx )))x
)
= λzx .
(
λx .z (z (zx ))
)(
z (z (zx ))
)
= λzx .z (z (z (z (z (zx ))))))
= SIX 36/60
Revision Currying Encodings LISP Lambdas in Languages Review
Recursion
In imperative languages, we can easily write recursive code:
def f a c t o r i a l ( x ) :
i f x == 1 :
return 1
return x∗ f a c t o r i a l ( 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 )
… 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 ))
Next week, we’ll use this to compute recursive functions in the
lambda calculus.
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 ))
Next week, we’ll use this to compute recursive functions in the
lambda calculus.
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 ))
Next week, we’ll use this to compute recursive functions in the
lambda calculus.
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 ))
Next week, we’ll use this to compute recursive functions in the
lambda calculus.
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:
41/60
Revision Currying Encodings LISP Lambdas in Languages Review
List Examples in LISP
(1 2 3)
( )
(+ 1 2)
(∗ (+ 1 2) (− 2 3) )
( sq 1 2)
( s e t q a 100)
( defun sq ( n ) (∗ n n ) )
( l e t ( ( a 6 ) ) a )
( i f t 5 6)
( cons 5 6)
( cons ( cons 6 7) )
42/60
Revision Currying Encodings LISP Lambdas in Languages Review
Concepts of LISP
▶ LISP has a data structure model
▶ Lists
▶ Atoms
▶ Even programs are written as lists.
▶ Even LISP is written as a list.
▶ No other data structures
43/60
Revision Currying Encodings LISP Lambdas in Languages Review
Evaluation
▶ Prefix notation of function calls as lists
▶ Operation is first element
▶ Second and following elements are arguments
▶ (
▶ Examples:
(+ 4 2)
(+ 3 (+ 3 2) )
( sq (∗ 4 2) )
44/60
Revision Currying Encodings LISP Lambdas in Languages Review
Numerical Functions
▶ Numerical operations:
▶ Addition: (+ 1 2)
▶ Subtraction: (- 1 2)
▶ Multiplication: (* 1 2)
▶ Division: (/ 1 2)
▶ Square root: (sqrt x)
▶ Base Exponent: (expt x y)
▶ Trigonometric Functions: (sin x)
▶ Absolute Value: (abs x)
▶ Modulo: (mod x y)
▶ Rounding: (round x)
45/60
Revision Currying Encodings LISP Lambdas in Languages Review
Interaction
▶ Interaction with lisp is done in a read-eval-print loop
▶ Loop consists of the following steps:
▶ Parse input and construct LISP object
▶ Evaluate LISP object to produce output
▶ Print output object
▶ Example:
>> (+ 1 2)
3
46/60
Revision Currying Encodings LISP Lambdas in Languages Review
Variables
▶ Variables can be defined by:
( s e t q
▶ Semantics
:=
▶ Occurrence of variable symbol replaces variable symbol by the
value of the variable
▶ Example:
>> ( s e t q a (+ 5 3) )
8
>> a
8
47/60
Revision Currying Encodings LISP Lambdas in Languages Review
Quote
▶ If lists should not be evaluated, use function quote
>> ( s e t q a (+ 1 2) )
3
>> ( s e t q a ( quote (+ 1 2 ) ) )
(+ 1 2)
▶ There is a short-hand form, using a single quotation mark
>> ( s e t q a ’(+ 1 2) )
(+ 1 2)
48/60
Revision Currying Encodings LISP Lambdas in Languages Review
Condition Function
▶ Definition: (if
▶ Boolean values in LISP are given by two symbols
▶ Symbol nil (equal to the empty list) represents false
▶ T represents true
>> ( i f n i l 1 2)
2
>> ( i f (= 10 10) 1 2)
1
>> ( i f ( ) 1 2)
2
49/60
Revision Currying Encodings LISP Lambdas in Languages Review
Predicates
▶ Type checking predicates
▶ (atom x) checks whether x is not a list
▶ (integerp x) checks whether x is an integer
▶ (numberp x) checks whether x is a number
▶ (stringp x) checks whether x is a string
▶ Numerical predicates
▶ (oddp x) checks whether x is integer and odd
▶ (evenp x) checks whether x is integer and even
▶ Equality
▶ (equal x y) checks structural equality
▶ (eql x y) checks atom equality
▶ (eq x y) checks identity
▶ (= x y) checks numerical equality
▶ Logical operators
▶ (or x y) logical OR
▶ (and x y) logical AND
50/60
Revision Currying Encodings LISP Lambdas in Languages Review
Functions
▶ Function declaration:
(defun
▶ Translates to:
(setq
>> ( defun f a c t o r i a l ( x )
( i f (= x 0)
1
(∗ x ( f a c t o r i a l (− x 1 ) ) ) ) )
FACTORIAL
>> ( f a c t o r i a l 4)
24
▶ Next week we’ll do this in lambda calculus directly – without
the impurity of defining variables
51/60
Revision Currying Encodings LISP Lambdas in Languages Review
Bindings
▶ Definition:
(let ((
body)
>> ( l e t
( ( a 3) ( b 4) ( c 5 ) )
(+ (∗ a b ) c ) )
17
>> a
E r r o r : v a r i a b l e A i s unbound
52/60
Revision Currying Encodings LISP Lambdas in Languages Review
Bindings (2)
▶ Let allows local bindings of variables
▶ Bindings might be nested – innermost variable is taken
>> ( l e t
( ( a 3 ) )
( l e t
( ( a 5 ) )
a
) )
5
53/60
Revision Currying Encodings LISP Lambdas in Languages Review
List Construction
▶ Construction with cons: (cons )
▶ Cons returns a new list with
followed by elements in
▶ Construction with list: (list
>> ( cons 1 n i l )
(1 )
>> ( cons ’ a ’ ( b c ) )
( a b c )
>> ( l i s t 1 2 3)
(1 2 3)
54/60
Revision Currying Encodings LISP Lambdas in Languages Review
List Access
▶ Access first element: (first )
▶ Access all but first element: (rest )
>> ( f i r s t ’ ( a b c ) )
a
>> ( r e s t ’ ( a b c ) )
( b c )
55/60
Revision Currying Encodings LISP Lambdas in Languages Review
λ in LISP
>> (( lambda ( x ) (+ x 1) ) 4)
5
>> ( ( lambda ( x y z ) (∗ (+ x x ) z ) ) 1 3 5)
10
56/60
Revision Currying Encodings LISP Lambdas in Languages Review
λ in Haskell
>> (\ x −> x + 1) 4
5
>> (\ x y z −> ( x + x ) ∗ z ) 1 3 5
10
57/60
Revision Currying Encodings LISP Lambdas in Languages Review
λ in Python
>> ( lambda x : x + 1) 4
5
>> ( lambda x : lambda y : lambda z : ( x + x ) ∗ z ) ( 1 ) ( 3 ) ( 5 )
10
>>> f = lambda x : lambda y : lambda z : ( x + x ) ∗ z
>>> f
>>> f (1 )
>>> f ( 1 ) ( 3 )
>>> f ( 1 ) ( 3 ) ( 5 )
10
58/60
Revision Currying Encodings LISP Lambdas in Languages Review
λ in Python
>>> NOT = lambda f : lambda x : lambda y : f ( y ) ( x )
>>> TRUE = lambda x : lambda y : x
>>> FALSE = lambda x : lambda y : y
>>> IF = lambda f : lambda x : lambda y : f ( x ) ( y )
>>> IF (NOT(TRUE) ) (” a ”) (” b ”)
’ a ’
>>> IF (NOT(NOT(TRUE) ) ) (” a ”) (” b ”)
’ b ’
59/60
Revision Currying Encodings LISP Lambdas in Languages Review
Review
▶ Lambda Calculus revision
▶ Application, Abstraction
▶ Rewriting
▶ α and β reductions
▶ Currying
▶ Multiple arguments
▶ Associativity
▶ Encodings
▶ Boolean logic
▶ Church numerals, arithmetic
▶ Functional programming
▶ Introduction to LISP
▶ Brief look λ in other languages
60/60
Revision
Lambda Calculus
Currying
Currying
Encodings
outline
Truth
LISP
outline
LISP
Lambdas in Languages
examples
Review
review