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

lec17

CS 314 Principles of Programming Languages

Prof. Zheng Zhang
Rutgers University

Lecture 17: Lambda Calculus

October 31, 2018

Class Information

• 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

• 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

• 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

• 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

The context-free grammar for λ-terms:

name (as parameter)

expr (another λ-term)

λ y . y x
Example 1:

Review: λ-terms

The context-free grammar for λ-terms:

y z

func arg

Example 2:

Review: Lambda Calculus

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

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

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

• 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

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

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

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

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

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

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

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

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

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

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

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

YES. x = YF, and Y is called the fixed point combinator.  