Question: Easy Beta

  1. (λx.xyzx) w

    Answer: (λx.xyzx) w →β wyzw

  2. (λx.xxx) (yz)

    Answer: (λx.xxx) (yz) →β yzyzyz

  3. (λy.xyz)

    Answer: (λy.xyz) cannot be beta reduced as there is no application.

  4. (λx.x) (λz.zw) y

    Answer: (λx.x) (λz.zw) y →β (λz.zw) y →β yw

  5. (λx.x u) (λz.wzwz) yv

    Answer: (λx.x u) (λz.wzwz) yv →β (λz.wzwz) u yv →β wuwu yv

  6. (λy.(λw.ywy)) x u

    Answer: (λy.(λw.ywy)) x u →β (λw.xwx) u →β xux

  7. (λx.(λy.xyxy)) y z

    Answer: (λx.(λy.xyxy)) y =α (λx.(λw.xwxw)) y z →β (λw.ywyw) z →β yzyz

Question: Converting

In each of the following, use alpha conversion to make all sets of bound variables have unique names.

Note: We have explicitly done the alpha conversion in two steps, to re-iterate the principle. See page 13 of the lambda slides to understand this explicit form.

  1. (λx.zx) x

    Answer: (λx.zx) x =α (λa.zx[x\a]) x →β (λa.za) x

  2. (λy.yxy) yy

    Answer: (λy.yxy) yy =α (λa.yxy[y\a]) yy →β (λa.axa) yy

  3. ((λx.xy) z) ((λy.xy) z)

    Answer: ((λx.xy) z) ((λy.xy) z) =α ((λa.xy[x\a]) z) ((λb.xy[y\b]) z) →β ((λa.ay) z) ((λb.xb) z)

  4. (λx.yx) (λx.xyx) z

    Answer: (λx.yx) (λx.xyx) z =α (λa.yx[x\a]) (λb.xyx[x\b]) z →β (λa.ya) (λb.byb) z

  5. (λx.(λy.xx)) ((λy.uyw) v)

    Answer: (λx.(λy.xx)) ((λy.uyw) v) =α (λx.(λz.xx[y\z])) ((λy.ayc) b) →β (λx.(λw.xx)) ((λy.ayc) b)

Question: Alpha and Beta Together

Now that we can do alpha conversion and beta reduction, we can tackle many interesting and challenging lambda expressions. See if you can reduce the following:

  1. (λx.xx) (λz.z) y

    Answer: (λx.xx) (λz.z) y →β (λz.z) (λz.z) y =α (λw.w) (λz.z) y →β (λz.z) y →β y

  2. (λx.(λy.xy)) y z

    Answer: (λx.(λy.xy)) y z =α (λx.(λw.xw)) y z →β (λw.yw) z →β yz

  3. (λx.(λy.x y)) (λz.z y) v

    Answer: (λx.(λy.x y)) (λz.z y) v =α (λx.(λw.x w)) (λz.z y) v →β (λw.(λz.z y) w) v →β (λz.z y) v →β v w

  4. (λy.x) (λy.((λy.z) y)) yx

    Answer: (λy.x) (λy.((λy.z) y)) yx =α (λu.x)(λv.((λw.z) v)) yx →β x yx We converted all λy in one batch, renaming them and the variables they have bound all.

  5. (λx.xx) (λx.xx)

    Answer: (λx.xx) (λx.xx) =α (λy.yy) (λx.xx) →β (λx.xx) (λx.xx) And we’re back where we started! Continuously evaluating this would result in an infinite series of beta reductions. Not every expression can be finitely beta reduced!