## Combinator Exercise page 48 and 49:

• 1) `ππ₯.π₯π₯π₯` - yes this is a combinator
• 2) `ππ₯π¦.π§π₯` - NOT a combinator since `z` is a free variable
• 3) Yes this is a combinator:
``````πxyz.xy(zx)
πx.πy.πz.xy(zx)
[x := zx]πy.πz.xy
πy.πz.zxxy
``````
• 4) Yes this is a combinator:
``````πxyz.xy(zxy)
πx.πy.πz.xy(zxy)
[x := zxy]πy.πz.xy
πy.πz.zxyxy
``````
• 5) NOT a a combinator (lesson learned: you have to look at whatβs passed in to see if itβs a combinator):
``````πxy.xy(zxy)
πx.πy.xy(zxy)
[x := zxy]πy.xy
πy.zxyy
``````

## Normal form or diverge? page 49

• 1) `πX.XXX` - normal form because it stabilizes at the value of whatever input value is passed in repeated 3 times e.g. `3` becomes `333` and stays `333`
• 2) Diverges!
``````[Z := (πY.YY)]ZZ
(πY.YY)(πY.YY)
``````
• 3) `(πx.xxx)z` -normal form because this evaluates to `zzz`

## Beta Reduce page 49

• 1) final value: `z`
``````(πabc.cba)zz(πwv.w)
(πa.πb.πc.cba)(z)z(πw.πv.w) # first z becomes argument
[a := z] (πb.πc.cba) z (πw.πv.w)
(πb.πc.cbz) (z) (πw.πv.w)
[b := z] (πc.cbz) (πw.πv.w)
(πc.czz) (πw.πv.w)
[c := (πw.πv.w)]czz
(πw.πv.w)(z)z
[w :=z ](πv.w) (z)
(πv.z)(z)
[v := z] z
z
``````
• 2) final value: `bb`
``````(πx.πy.xyy)(πa.a)b
[x := (πa.a)]πy.xyyb
πy.(πa.a)yy(b)
[y := b](πa.a)yy
(πa.a)(b)b
[a := b] ab
bb
``````
• 3) final value:`qq`
``````(πy.y)(πx.xx)(πz.zq)
[y := (πx.xx)]y(πz.zq)
(πx.xx)(πz.zq)
[x := (πz.zq)]xx
(πz.zq)(πz.zq)
[z := (πz.zq)]zq
(πz.zq)(q)
[z := q]zq
qq
``````
• 4) `(πz.z)(πz.zz)(πz.zy)` Hint: alpha equivalence. If i follow the hint letβs try: `(πz.z)(πa.aa)(πb.bc)` This reduces to final value: `cc` Here is the reduction:
``````(πz.z)(πa.aa)(πb.bc)
[z := (πa.aa)]z(πb.bc)
(πa.aa)(πb.bc)
[a := (πb.bc)]aa
(πb.bc)(πb.bc)
[b := (πb.bc)]bc
(πb.bc)(c)
[b := c]bc
cc
``````
• 5) final value: `yy` detailed reduction:
``````(πx.πy.xyy)(πy.y)y
[x := (πy.y)]πy.xyy(y)
(πy.(πy.y)yy)(y)
[y := y](πy.y)y(y)
(πy.y)(y)y)
[y := y] (y)(y)
yy
``````
• 6) final value: `b(πa.ba)c` detailed reduction:
``````(πa.aa)(πb.ba)c
[a := (πb.ba)]aac
(πb.ba)(πb.ba)c
[b := (πb.ba)]bac
(πb.ba)a(c)
[b := a]bac
aac
``````
• 7) final value: `(πz1.za)` detailed reduction:
``````(πxyz.xz(yz))(πx.z)(πx.a)
(πx.πy.πz.xz(yz))(πx.z)(πx.a) # rename z to z1 before substituting in next step for less confusion
[x := (πx.z)]πy.πz1.xz(yz1)(πx.a)
(πy.πz1.(πx.z)z1(yz1)(πx.a)
[y := (πx.a)]πz1.(πx.z)z1(yz1)
(πz1.(πx.z)z1((πx.a)z1) # d)
comment: "Canβt apply z1 to anything, evaluation strategy is normal order so leftmost outermost is the order of the day. Our leftmost, outermost lambda has no remaining arguments to be applied so we now examine the terms nested within to see if they are in normal form. (π₯.π§) gets applied to π§1, tosses the π§1 away and returns π§. π§ is now being applied to ((π₯.π)(π§1))" - didn't understand this explanation
(πz1.z((πx.a)z1)) # e)
comment: "Cannot reduce π§ further, itβs free and we know nothing, so we go inside yet another nesting and reduce ((π₯.π)(π§1)). π₯.π gets applied to π§1, but tosses it away and returns the free variable π. The π is now part of the body of that expression. All of our terms are in normal order now" - I understand [x := z1] but need to revisit the rest
(πz1.za)
``````