lec17
CS 314 Principles of Programming Languages
Prof. Zheng Zhang
Rutgers University
Lecture 17: Lambda Calculus
October 31, 2018
Class Information
2
• Midterm exam 11/7 Wednesday 10:20am – 11:40am
• Extended hours are Posted
• No classes on 11/2 this Friday
Review: Lambda Calculus – Historical Origin
3
• 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.
Review: Functional Programming
4
• 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
Review: Lambda Calculus
5
• 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:
Review: λ-terms
6
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:
Review: λ-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 )
y z
func arg
Example 2:
Review: Lambda Calculus
8
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))
Review: Free and Bound Variables
9
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
Review: Free and Bound Variables
10
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
Review: Free and Bound Variables
11
• 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:
Review: Function Application
12
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:
Review: 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:
(λa.λb.a+b) 2 x →β (λb.2+b) x
→β 2+x
Example:
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]
β–reduction:
Example:
(λa.λb.a+b) b 2 →β (λb.b+b) 2
→β 2+2
Incorrect
We should not perform β–reduction if y is a bound variable within E
b is a bound variable within λa.λb.a+b This is called capturing
Review: 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]
Review: 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 →α (λa.λx.a+x) b 2
→β λx.b+x 2
Example:
→β b+2
Perform α–reduction first
cond ≡ λp. λm. λn.(p m n)
not ≡ λx. (x false true)
and ≡ λx. λy. (x y false)
or ≡ homework
Review: Programming in Lambda Calculus
17
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
Review: Programming in Lambda Calculus
18
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
19
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)
Recursion in Lambda Calculus
20
Does this make sense?
f ≡ … f …
In lambda calculus, ≡ is “abbreviated as”, but not an assignment.
In lambda calculus, ≡ is “abbreviated as”, not an assignment.
Recursion in Lambda Calculus
21
Does this make sense?
f ≡ … f …
add ≡ λmn. ( if (isZero?n) m (add (m+1) (n-1)) )
Incorrect! “add” is not defined
λf.(λmn.( if (isZero?n) m (f (m+1) (n-1))) ) add
How about
λmn.( if (isZero?n) m (add (m+1) (n-1))) add=
F
add=F add
“add” is a fixed point to function F
Function Fixed Points
22
The fixed point of a function g is the set of values
Examples:
function g fix(g)
λx.6 {6}
λx.(6 – x) {3}
λx.((x * x) + (x – 4)) {-2, 2}
λx.x entire domain of function f
λx.(x + 1) { }
{ x | x = g(x) }
Function Fixed Points
23
YES. x = YF, and Y is called the fixed point combinator.
Y ≡ λf.((λx.f(x x)) (λx.f(x x)))
YF = ((λf.((λx.f( x x)) (λx.f( x x )))) F)
= (λx.F(x x)) (λx.F(x x))
= F( (λx.F(x x)) (λx.F(x x)))
= F(YF)
Is there a way to “compute” the fixed point of any function F
x = F(x)
Function Fixed Points
24
YES. x = YF, and Y is called the fixed point combinator.
Y ≡ λf.((λx.f(x x)) (λx.f(x x)))
YF = ((λf.((λx.f( x x)) (λx.f( x x )))) F)
= (λx.F(x x)) (λx.F(x x))
= F( (λx.F(x x)) (λx.F(x x)))
= F(YF)
Is there a way to “compute” the fixed point of any function F
x = F(x)
Function Fixed Points
25
YES. x = YF, and Y is called the fixed point combinator.
Y ≡ λf.((λx.f(x x)) (λx.f(x x)))
YF = ((λf.((λx.f( x x)) (λx.f( x x )))) F)
= (λx.F(x x)) (λx.F(x x))
= F( (λx.F(x x)) (λx.F(x x)))
= F(YF)
Is there a way to “compute” the fixed point of any function F
x = F(x)
Function Fixed Points
26
YES. x = YF, and Y is called the fixed point combinator.
Y ≡ λf.((λx.f(x x)) (λx.f(x x)))
YF = ((λf.((λx.f( x x)) (λx.f( x x )))) F)
= (λx.F(x x)) (λx.F(x x))
= F( (λx.F(x x)) (λx.F(x x)))
= F(YF)
Is there a way to “compute” the fixed point of any function F
x = F(x)
Function Fixed Points
27
Is there a way to “compute” the fixed point of any function F
x = F(x)
YES. x = YF, and Y is called the fixed point combinator.
Y ≡ λf.((λx.f(x x)) (λx.f(x x)))
YF = ((λf.((λx.f( x x)) (λx.f( x x )))) F)
= (λx.F(x x)) (λx.F(x x))
= F( (λx.F(x x)) (λx.F(x x)))
= F(YF)
Function Fixed Points
28
Is there a way to “compute” the fixed point of any function F
x = F(x)
YES. x = YF, and Y is called the fixed point combinator.
Y ≡ λf.((λx.f(x x)) (λx.f(x x)))
YF = ((λf.((λx.f( x x)) (λx.f( x x )))) F)
YF = (λx.F(x x)) (λx.F(x x))
YF = F( (λx.F(x x)) (λx.F(x x)))
= F(YF)
Function Fixed Points
29
Is there a way to “compute” the fixed point of any function F
x = F(x)
YES. x = YF, and Y is called the fixed point combinator.
Y ≡ λf.((λx.f(x x)) (λx.f(x x)))
YF = ((λf.((λx.f( x x)) (λx.f( x x )))) F)
YF = (λx.F(x x)) (λx.F(x x))
YF = F( (λx.F(x x)) (λx.F(x x)))
YF = F(YF)
The Y – Combinator Example (Cont.)
30
• Informally, the Y-Combinator allows us to get as many copies
of the recursive procedure body as we need. The computation
“unrolls” recursive procedure calls one at a time
Y ≡ λf.((λx.f(x x)) (λx.f(x x)))
The Y – Combinator
31
Example:
F ≡ λf. (λmn. if (isZero? n) then m else (f (succ m) (pred n)))
= (((λf.((λx.f(x x)) (λx.f(x x)))) F) 3 2)
= ( (F (YF) ) 3 2)
= ((λmn.if (isZero? n) then m else YF (succ m) (pred n))) 3 2)
= if (isZero? 2) then 3 else YF (succ 3) (pred 2))
= ( YF 4 1)
= ((F (YF)) 4 1)
= if (isZero? 1) then 4 else YF (succ 4) (pred 1))
= ( YF 5 0 )
= ( F (YF) 5 0 )
= if (isZero? 0) then 5 else ( YF (succ 5) (pred 0))
= 5
(YF 3 2)
Lambda Calculus – Final Remarks
32
• We can express all computable functions in our λ-calculus.
• All computable functions can be expressed by the following two
combinators, referred to as S and K.
– K ≡ λxy.x
– S ≡ λxyz.xz(yz)
Combinatoric logic is as powerful as Turing Machines.
Next Lecture
33
• Scott, Chapter 11.1 – 11.3
• Scott, Chapter 11.7
• ALSU, Chapter 11.1 – 11.3
Reading: