程序代写代做代考 scheme data structure Lambda Calculus algorithm Haskell lec16

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: