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

If you are on mobile, here’s a screenshot:

Untitled

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

If you are on mobile, here’s a screenshot:

Untitled

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)

If you are on mobile, screenshots

1. and 2.

Untitled

3. and 4.

Untitled

5. and 6.

Untitled

7.

Untitled

Leave a comment on github