ch01.adoc

1 All you need is lambda

1.6 Multiple arguments

Intermission: Exercises

1. b) λxy.xz equals λmn.mz

2. c) λxy.xxy equals λa(λb).aab although it should be λa(λb.aab) I think

3. b) λxyz.zx equals λtos.st

1.11 Exercises

Combinators

Combinator is lambda term with no free variable

λxyz.xz(yz) → λyz.yz(z) → λz.zz

1. λx.xxx - yes

2. λxy.zx - no, z not in head

3. λxyz.xy(zx) - yes

4. λxyz.xy(zxy) - yes

5. λxy.xy(zxy) - no, z not in head

Normal form or diverge

Diverge - reduction does not end

1. λx.xxx - converge, no reduction

2. (λz.zzz)(λy.yy) - diverge, (λz.zzz)(λy.yy) → (λy.yy)(λy.yy)(λy.yy) → λy.yy)(λy.yy(λy.yy) into more nested expressions

3. (λx.xxx)z - converge, (λx.xxx)z → zzz

Beta reduce

Reduce in normal order, that is leftmost outermost first. Otherwise you get different results.

1. (λabc.cba)zz(λwv.w) → (λc.czz)(λwv.w) → (λwv.w)zz → z

2. (λx.λy.xyy)(λa.a)b → (λy.(λa.a)yy)b → (λa.a)bb → bb

3. (λy.y)(λx.xx)(λz.zq) → (λx.xx)(λz.zq) → (λz.zq)(λz.zq) → (λz.zq)q → qq

4. (λz.z)(λz.zz)(λz.zy) → (λz.zz)(λz.zy) → (λz.zy)(λz.zy) → (λz.zy)y → yy

5. (λx.λy.xyy)(λy.y)y → (λy.(λy.y)yy)y → (λy.y)yy → yy

6. (λa.aa)(λb.ba)c → (λb.ba)(λb.ba)c → ((λb.ba)a)c → aac

7. (λxyz.xz(yz))(λx.z)(λx.a) → (λyz1.(λx.z)z1(yz1))(λx.a) → (λz1.(λx.z)z1λx.a)z1 → (λz1.zλx.a)z1 → λz1.za