# Assignment 6 (week 7) ## Evaluation order in Combinatory Logic 1. Give a term that the lazy evaluators (either the Haskell evaluator, or the lazy version of the OCaml evaluator) do not evaluate all the way to a normal form, i.e., that contains a redex somewhere inside of it after it has been reduced. 2. One of the [[criteria we established for classifying reduction strategies| topics/week3_evaluation_order]] strategies is whether they reduce subexpressions hidden under lambdas. That is, for a term like `(\x y. x z) (\x. x)`, do we reduce to `\y.(\x.x) z` and stop, or do we reduce further to `\y.z`? Explain what the corresponding question would be for CL. Using either the OCaml CL evaluator or the Haskell evaluator developed in the wiki notes, prove that the evaluator does reduce expressions inside of "functional" CL expressions. Then provide a modified evaluator that does not perform reductions in those positions. 3. Converting to lambdas. Using the type definitions you developed in homework 5, rebuild the evaluator in OCaml to handle the untyped lambda calculus. Making use of the occurs_free function you built, we'll provide a function that performs safe substitution.