exercises/_assignment6.mdwn

   1 ~/Dropbox/Lambda/wiki/exercises/# Assignment 6 (week 7)
   2
   3 ## Evaluation order in Combinatory Logic
   4
   5 1. Give a term that the lazy evaluators (either [[the Haskell
   6 evaluator|code/ski_evaluator.hs]], or the lazy version of [[the OCaml
   7 evaluator|code/ski_evaluator.ml]]) do not evaluate all the way to a
   8 normal form, i.e., that contains a redex somewhere inside of it after
   9 it has been reduced.
  10
  11 <!-- reduce3 (FA (K, FA (I, I))) -->
  12
  13 2. One of the [[criteria we established for classifying reduction
  14 strategies|topics/week3_evaluation_order]] strategies is whether they
  15 reduce subexpressions hidden under lambdas.  That is, for a term like
  16 `(\x y. x z) (\x. x)`, do we reduce to `\y.(\x.x) z` and stop, or do
  17 we reduce further to `\y.z`?  Explain what the corresponding question
  18 would be for CL. Using either the OCaml CL evaluator or the Haskell
  19 evaluator developed in the wiki notes, prove that the evaluator does
  20 reduce expressions inside of at least some "functional" CL
  21 expressions.  Then provide a modified evaluator that does not perform
  22 reductions in those positions. (Just give the modified version of your
  23 recursive reduction function.)
  24
  25 <!-- just add early no-op cases for Ka and Sab -->
  26
  27 ## Evaluation in the untyped lambda calculus
  28