PowerPoint Presentation
CS 345
Lecture 14
Using lab 4 starter file, review numbers, succ and pred, and add.
Take a moment to talk about cn-to-num
1
New Today
Considerations of evaluation order in more complex Lambda Calculus expressions
((λx.λy.x λa.a) λb.b)
Evaluation order?
Eager / Strict / Applicative
(λb.b (λx.λy.x λa.a))
(λb.b λy.λa.a)
λy.λa.a
Lazy / Non-strict / Normal
(λb.b (λx.λy.x λa.a))
(λx.λy.x λa.a)
λy.λa.a
(λb.b (λx.λy.x λa.a))
Evaluation order?
Eager / Strict / Applicative
((λp.λq.(p q) (λx.x λa.λb.a)) λk.k)
((λp.λq.(p q) λa.λb.a) λk.k)
(λq.(λa.λb.a q) λk.k)
(λa.λb.a λk.k)
λb.λk.k
Lazy / Non-strict / Normal
((λp.λq.(p q) (λx.x λa.λb.a)) λk.k)
(λq.((λx.x λa.λb.a) q) λk.k)
((λx.x λa.λb.a) λk.k)
(λa.λb.a λk.k)
λb.λk.k
((λp.λq.(p q) (λx.x λa.λb.a)) λk.k)
Evaluation order?
Eager / Strict / Applicative
(λz.(z true) ((λx.λy.λf.((f x) y) one) two))
(λz.(z true) (λy.λf.((f one) y) two))
(λz.(z true) λf.((f one) two))
(λf.((f one) two)) true)
((true one) two))
((λx.λy.x one) two))
one
Lazy / Non-strict / Normal
(λz.(z true) ((λx.λy.λf.((f x) y) one) two))
(((λx.λy.λf.((f x) y) one) two) true)
((λy.λf.((f one) y) two) true)
(λf.((f one) two) true)
((true one) two)
((λx.λy.x one) two)
one
(λz.(z true) ((λx.λy.λf.((f x) y) one) two))
Will the outputs always be the same?
Eager / Strict / Applicative
((λf.λx.(x (f f)) λs.(s s)) false)
(λx.(x (λs.(s s) λs.(s s))) false)
(false (λs.(s s) λs.(s s)))
(false (λs.(s s) λs.(s s)))
Doesn’t terminate!
Lazy / Non-strict / Normal
((λf.λx.(x (f f)) λs.(s s)) false)
(λx.(x (λs.(s s) λs.(s s))) false)
(false (λs.(s s) λs.(s s)))
(λx.λy.y (λs.(s s) λs.(s s)))
λy.y
((λf.λx.(x (f f)) λs.(s s)) false)
Let’s practice repetition some more:
sum-from-one
/docProps/thumbnail.jpeg