[SOLVED] CS Lambda Calculus PowerPoint Presentation

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.by.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.(ztrue)((x.y.f.((fx)y)one)two))

(z.(ztrue)(y.f.((f one)y)two))

(z.(ztrue)f.((f one) two))

(f.((f one) two))true)

((true one) two))

((x.y.x one) two))

one

Lazy / Non-strict / Normal

(z.(ztrue)((x.y.f.((fx)y)one)two))

(((x.y.f.((fx)y)one)two)true)

((y.f.((fone)y)two)true)

(f.((fone)two)true)

((trueone)two)

((x.y.xone)two)

one

(z.(ztrue)((x.y.f.((fx)y)one)two))

Will the outputs always be the same?
Eager / Strict / Applicative

((f.x.(x(ff))s.(ss))false)

(x.(x(s.(ss)s.(ss)))false)

(false(s.(ss)s.(ss)))

(false(s.(ss)s.(ss)))

Doesnt terminate!
Lazy / Non-strict / Normal

((f.x.(x(ff))s.(ss))false)

(x.(x(s.(ss)s.(ss)))false)

(false(s.(ss)s.(ss)))

(x.y.y(s.(ss)s.(ss)))

y.y
((f.x.(x(ff))s.(ss))false)

Lets practice repetition some more:
sum-from-one

/docProps/thumbnail.jpeg