lec16
CS 314 Principles of Programming Languages
Prof. Zheng Zhang
Rutgers University
Lecture 16: Lambda Calculus
October 26, 2018
Lambda Calculus: Historical Origin
2
• The imperative and functional models grew out of work undertaken
by Alan Turing, Alonzo Church, Stephen Kleene, Emil Post, and etc
in 1930s.
– Different formalizations of the notion of an algorithm, or “effective
procedure”, based on automata, symbolic manipulation, recursive
function definitions, and combinatorics.
Lambda Calculus: Historical Origin
3
• Turing’s model of computing was the Turing machine a sort of
pushdown automaton using an unbounded storage “tape”
The Turing machine computes in an imperative way, by changing the
values in cells of its tape – like variables just as a high level
imperative program computes by changing the values of variables.
Lambda Calculus: Historical Origin
4
• Church’s model of computing is called the lambda calculus
It is based on the notion of parameterized expressions (with each
parameter introduced by an occurrence of the letter λ — hence the
notation’s name). Lambda calculus was the inspiration for
functional programming: one uses it to compute by substituting
parameters into expressions, just as one computes in a high level
functional program by passing arguments to functions.
Functional Programming
5
• Functional languages such as Lisp, Scheme, FP, ML, Miranda,
and Haskell are an attempt to realize Church’s lambda calculus in
practical form as a programming language
• The key idea: do everything by composing functions
– No mutable state
– No side effects
– Function as first-class values
Lambda Calculus
6
• a variable x
• (λx. M) ⇒ where x is a variable and λ is a λ-term (abstraction)
• (M N) ⇒ where M and N are both λ-terms (application)
λ-terms are inductively defined.
A λ-term is:
λ-terms
7
The context-free grammar for λ-terms:
λ-term → expr
expr → name | number | λ name . expr | func arg
func → name | ( λ name . expr ) | func arg
arg → name | number | ( λ name . expr ) | ( func arg )
name (as parameter)
expr (another λ-term)
λ y . y x
Example 1:
λ-terms
8
The context-free grammar for λ-terms:
λ-term → expr
expr → name | number | λ name . expr | func arg
func → name | ( λ name . expr ) | func arg
arg → name | number | ( λ name . expr ) | ( func arg )
y z
func arg
Example 2:
Lambda Calculus
9
Associativity and Precedence
• Function application is left associative: (f g z) is ((f g) z)
• Function application has precedence over function abstraction.
“function body” extends as far to the right as possible:
(λx.yz) is (λx.(yz))
• Multiple arguments: (λxy.z) is (λx(λy.z))
Free and Bound Variables
10
Abstraction (λx. M) “binds” variable x in “body” M. You can
think of this as a declaration of variable x with scope M.
(λ y . y z) y
binding
occurrence
bound
occurrence
free
occurrence
Free and Bound Variables
11
Note:
A variable can occur free and bound in a λ-term.
Example:
λx.λy. (λz. xyz) y
“free” is relative to a λ-sub-term.
y is free y is bound
Free and Bound Variables
12
• free(x) = {x}
• free(M N) = free(M) ∪ free(N)
• free (λx.M) = free(M) – free(x)
Let M, N be λ-terms and x is a variable. The set of free variable
of M, free(M), is defined inductively as follows:
Function Application
13
Computation in lambda calculus is based on the concept or reduction.
Simplify an expression until it can no longer be simplified.
(λx.E)y →β E[y/x]
1. Return function body E
2. Replace every free occurrence of x in E with y
β–reduction:
Function Application
14
Computation in lambda calculus is based on the concept or reduction.
Simplify an expression until it can no longer be simplified.
(λx.E)y →β E[y/x]
1. Return function body E
2. Replace every free occurrence of x in E with y
β–reduction:
(λa.λb.a+b) 2 x →β (λb.2+b) x
→β 2+x
Example:
Function Application
15
Computation in lambda calculus is based on the concept or reduction.
Simplify an expression until it can no longer be simplified.
α–reduction:
(λx.E) → α λy.E[y/x]
Function Application
16
Computation in lambda calculus is based on the concept or reduction.
Simplify an expression until it can no longer be simplified.
α–reduction:
(λx.E) → α λy.E[y/x]
(λa.λb.a+b) b 2 →β (λb.b+b) 2
→β 2+2
Example: This is incorrect.
Function Application
17
Computation in lambda calculus is based on the concept or reduction.
Simplify an expression until it can no longer be simplified.
α–reduction:
(λx.E) → α λy.E[y/x]
λa.λb.a+b b 2 →α λa.λx.a+x b 2
→β λx.b+x 2
Example:
→β b+2
Perform α–reduction first
Function Application
18
• An equivalence relation can be defined based on ≅-convertible λ-
terms. “Reduction” rules really work both ways, but we are
interested in reducing the complexity of λ-term (forward direction)
• α–reduction does not reduce the complexity of λ-term
• β–reduction: corresponds to application, models computation
Computation in the lambda calculus is based on the concept or
reduction (rewriting rules). The goal is to “simplify” an expression
until it can no longer be further simplified.
(λx.M)N ⇒β [N/x]M (β–reduction)
(λx.M) ⇒α λy.[y/x]M (α–reduction), if y ∉ free(M)
Note:
Reduction
19
• A subterm of the form (λx.M)N is called a redex (reduction expression)
• A reduction is any sequence of α–reductions and β–reductions
• A term that cannot be β–reduced are said to be in β normal form
• A subterm that is an abstraction or a variable is said to be in
head normal form .
Question: Does a β normal form always exist?
Example:
((λx.xx)) (λx.xx)))
if ≡ λp. λm. λn.(p m n)
Programming in Lambda Calculus
20
Remember: Computation in the lambda calculus is a sequence of
applications of reduction rules (mostly β–reductions).
Logical constants and operations (incomplete list):
true ≡ λa. λb. a select-first
false ≡ λa. λb. b select-second
if true 3 4if T 3 4
When T is true,
return 3
≡ λp.λm.λn.(p m n) true 3 4
≡ λp.λm.λn.(p m n) λa.λb.a 3 4
→β λa.λb.a 3 4
→β 3
≡ abbreviated as
cond ≡ λx. λy. λz.(x y z)
Programming in Lambda Calculus
21
Remember: Computation in the lambda calculus is a sequence of
applications of reduction rules (mostly β–reductions).
Logical constants and operations (incomplete list):
true ≡ λa. λb. a select-first
false ≡ λa. λb. b select-second
cond p m n
≅ p m n
≅ λa.λb.a m n
≅ m
if p is true
return m
if p is false
return n
cond p m n
≅ p m n
≅ λa.λb.b m n
≅ n
not ≡ λx. (x false true)
Programming in Lambda Calculus
22
Remember: Computation in the lambda calculus is a sequence of
applications of reduction rules (mostly β–reductions).
Logical constants and operations (incomplete list):
true ≡ λa. λb. a select-first
false ≡ λa. λb. b select-second
not y
≅ λx. (x false true) y
≅ y false true
≅ λa.λb.a false true
≅ false
if y is true
return false
if y is false
return true
not y
≅ λx. (x false true) y
≅ y false true
≅ λa.λb.b false true
≅ true
and ≡ λx. λy. (x y false)
Programming in Lambda Calculus
23
Remember: Computation in the lambda calculus is a sequence of
applications of reduction rules (mostly β–reductions).
Logical constants and operations (incomplete list):
true ≡ λa. λb. a select-first
false ≡ λa. λb. b select-second
and m n
≅ m n false
≅ λa.λb.a n false
≅ n
if m is true
return n
if m is false
return false
and m n
≅ m n false
≅ λa.λb.b n false
≅ false
cond ≡ λp. λm. λn.(p m n)
not ≡ λx. (x false true)
and ≡ λx. λy. (x y false)
or ≡ homework
Programming in Lambda Calculus
24
Remember: Computation in the lambda calculus is a sequence of
applications of reduction rules (mostly β–reductions).
Logical constants and operations (incomplete list):
true ≡ λa. λb. a select-first
false ≡ λa. λb. b select-second
Programming in Lambda Calculus
25
What about data structures?
Data structures:
pairs can be represented as:
[M.N] ≡ λz. (z M N)
Programming in Lambda Calculus
26
What about data structures?
Data structures:
pairs can be represented as:
[M.N] ≡ λz. (z M N)
first ≡ λx. (x true) (car)
first [M.N] ≡ λx.(x true) λz.(z M N)
→β λz.(z M N) true
→β true M N
→β M
Programming in Lambda Calculus
27
What about data structures?
Data structures:
pairs can be represented as:
[M.N] ≡ λz. (z M N)
second ≡ λx. (x false) (cdr)
second [M.N]≡ λx.(x false) λz.(z M N)
→β λz.(z M N) fase
→β false M N
→β N
Programming in Lambda Calculus
28
What about data structures?
Data structures:
pairs can be represented as:
[M.N] ≡ λz. (z M N)
first ≡ λx. (x true) (car)
second ≡ λx. (x false) (cdr)
build ≡ λx.λy.λz. (z x y) (cons)
Programming in Lambda Calculus
29
What about the encoding of arithmetic constants?
Church Numerals:
0 ≡ λfx. x
1 ≡ λfx. (f x)
2 ≡ λfx. (f (f x))
…
n ≡ λfx.( f ( f (… ( f x) … )) ≡ λfx. (f nx)
The natural number n is represented as a function that applies a function f
n-times to x.
succ ≡ λm. (λfx.(f (m f x)))
add ≡ λmn. (λfx.((m f) (n f x)))
mult ≡ λmn. (λfx.((m (n f)) x))
isZero? ≡ λm. (m λx.false true)
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
Programming in Lambda Calculus
30
m = 2
n = 3
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
31
m = 2
n = 3
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
32
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
33
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
34
2 ≡ λfx. (f (f x))
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
35
f in 2 ≡ λfx.(f (f x))
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
36
f in 2 ≡ λfx.(f (f x))
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
37
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
38
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
39
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
40
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
41
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
42
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
43
Programming in Lambda Calculus
44
Example:
(mult 2 3)
((λmn.( λfx.((m (n f)) x) )) 2 3)
λf0x0.((2 (3 f0) ) x0)
λf0x0.((2 (λfx.(f3x) f0) ) x0)
λf0x0.((2 (λx.(f03x)) ) x0)
λf0x0.( (2 (λx1.(f03 x1)) ) x0)
λf0x0.((λx.( (λx1.(f0
3 x1)) ( (λx1.(f03 x1) ) x) )) x0) =
λf0x0.((λx. ((λx1.(f03 x1)) (f03 x) ) ) x0)
λf0x0. (( λx.( f03 (f03 x) ) ) x0)
λf0x0.(f0
3 (f0
3 x0))
λfx.(f6 x) = 6
≡
→β,
≡
→β
→α
→β
→β
→β
→β
→α
Programming in Lambda Calculus
45
Examples:
(isZero? 0)
= ( ((λfx.x) (λy.false)) true) =
= ( (λx.x) true) = true
(isZero? n) when n >0 ?
false ≡ λa. λb. b
not ≡ λx. (x false true)
isZero? ≡ λm. (m λy.false true)
Next Lecture
46
• Scott, Chapter 11.1 – 11.3
• Scott, Chapter 11.7
Reading: