Question: Reducing to Normal Form

State whether each of the following lambda expressions are in normal form and if not, reduce it until it is.

  1. λx.xxx

Answer:

This expression is in normal form.

  1. (λx.xxx) (λx.x)

Answer:

This expression is not in normal form. It can be further reduced like so: (λx.xxx) (λx.x)β (λx.x)(λx.x)(λx.x)β (λx.x)(λx.x)β (λx.x)

  1. λx.yz

Answer:

This expression is in normal form.

  1. (λx.(λy.yx) (xz)) y z

Answer:

This expression is not in normal form. It can be further reduced like so: (λx.(λy.yx) (xz)) y zβ (λx.xzx) y zβ yzy z

  1. (λx.x w)((λy.y)(λz.(λu.u)z))

Answer:

This expression is not in normal form. It can be further reduced like so: (λx.x w)((λy.y)(λz.(λu.u)z))β (λy.y)(λz.(λu.u)z) wβ (λz.(λu.u)z) wβ (λz.z) wβ w

Question: Lazily and Eagerly Evaluating Lambda Expressions

For each of the following expressions, try to evaluate them using the lazy method of evaluation and the eager method of evaluation. Do they both produce a result? If so, do they come up with the same result? Which was easier?

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

Answer:

Eager Evaluation: (λx.λy.(y x)) ((λz.z) w)β (λx.λy.(y x)) wβ λy.(y w)

Lazy Evaluation: (λx.λy.(y x)) ((λz.z) w)β λy.(y ((λz.z) w))β λy.(y w)

  1. (λx.xy)(λy.zy)

Answer:

Eager Evaluation: (λx.xy)(λy.zy)β (λy.zy)yβ zy

Lazy Evaluation: (λx.xy)(λy.zy)β (λy.zy)yβ zy

Notice that both the eager and lazy evaluation are the same

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

Answer:

Eager Evaluation: (λx.y)((λx.xx)(λx.xx))β ((λx.y)((λx.xx)(λx.xx)) which is the exact same, so it repeats forever.

Lazy Evaluation: (λx.y)((λx.xx)(λx.xx))β y

Notice that the eager evaluation does not reach the normal form.

  1. (λx.x w)((λy.y)(λz.(λu.u)z))

Answer:

Eager Evaluation: (λx.x w)((λy.y)(λz.(λu.u)z))β (λx.x w)((λy.y)(λz.z))β (λx.x w)(λz.z)β (λx.x w)(λz.z)β (λz.z) wβ w

Lazy Evaluation: (λx.x w)((λy.y)(λz.(λu.u)z))β ((λy.y)(λz.(λu.u)z)) wβ (λz.(λu.u)z) wβ (λu.u) wβ w

  1. ((λf.(λx.fffx)) ((λy.yy) z)) z

Answer:

Eager Evaluation: ((λf.(λx.fffx)) ((λy.yy) z)) zβ ((λf.(λx.fffx)) zz) zβ (λx.zzzzzzx) zβ zzzzzzz

Lazy Evaluation: ((λf.(λx.fffx)) ((λy.yy) z)) zβ (λx.((λy.yy) z)((λy.yy) z)((λy.yy) z)x) zβ ((λy.yy) z)((λy.yy) z)((λy.yy) z)zβ zz((λy.yy) z)((λy.yy) z)zβ zzzz((λy.yy) z)zβ zzzzzzz