~/Dropbox/Lambda/wiki/exercises/# Assignment 6 (week 7)
## Evaluation order in Combinatory Logic
1. Give a term that the lazy evaluators (either [[the Haskell
evaluator|code/ski_evaluator.hs]], or the lazy version of [[the OCaml
evaluator|code/ski_evaluator.ml]]) 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 at least some "functional" CL
expressions. Then provide a modified evaluator that does not perform
reductions in those positions. (Just give the modified version of your
recursive reduction function.)
## Evaluation in the untyped lambda calculus