程序代写代做代考 scheme python data structure Lambda Calculus Haskell AI COMP2022: Formal Languages and Logic – 2018, Semester 2, Week 2

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 then else
▶ If is true, return result of , otherwise

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

= (λ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 () body)
▶ Translates to:

(setq ‘(lambda () body))

>> ( 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 as first element,

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
at 0x02F66270>
>>> f (1 )
.< l o c a l s >. at 0x02F66150>
>>> f ( 1 ) ( 3 )
.< l o c a l s >..< l o c a l s >. at 0x02F66198>
>>> 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