exercises/_assignment6.mdwn

   1 # 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: substitution
  28
  29 Once you grok reduction and evaluation order in Combinatory Logic,
  30 we're going to begin to construct an evaluator for a simple language
  31 that includes lambda abstraction.  We're going to work through the
  32 issues twice: once with a function that does substitution in the
  33 obvious way.  You'll see it's somewhat complicated.  The complications
  34 come from the need to worry about variable capture.  (Seeing these
  35 complications should give you an inkling of why we presented the
  36 evaluation order discussion using Combinatory Logic, since we don't
  37 need to worry about variables in CL.)
  38
  39 We're not going to ask you to write the entire program yourself.
  40 Instead, we're going to give you [[the complete program, minus a few
  41 little bits of glue|code/reduction_with_reduction.ml]].  What you need to do is
  42 understand how it all fits together.  When you do, you'll understand
  43 how to add the last little bits to make functioning program.
  44
  45 1. In the previous homework, you built a function that took an
  46 identifier and a lambda term and returned a boolean representing
  47 whether that identifier occured free inside of the term.  Your first
  48 task is to complete the `free_in` function, which has been crippled in
  49 the code base (look for lines that say `COMPLETE THIS LINE`).  Once
  50 you have your function working, you should be able to run queries such
  51 as this:
  52
  53     # free_in "x" (App (Abstract ("x", Var "x"), Var "x"));;
  54     - : bool = true
  55
  56 2. Once you get the `free_in` function working, you'll need to
  57 complete the `substitute` function.  You'll see a new wrinkle on
  58 OCaml's pattern-matching construction: `| PATTERN when x = 2 ->
  59 RESULT`.  This means that a match with PATTERN is only triggered if
  60 the boolean condition in the `when` clause evaluates to true.
  61 Sample target:
  62
  63     # substitute (App (Abstract ("x", ((App (Abstract ("x", Var "x"), Var "y")))), Constant (Num 3))) "y" (Constant (Num 4));;
  64     - : lambdaTerm = App (Abstract ("x", App (Abstract ("x", Var "x"), Constant (Num 4))), Constant (Num 3))
  65
  66 3. Once you have completed the previous two problems, you'll have a
  67 complete evaluation program. Here's a simple sanity check for when you
  68 get it working:
  69
  70     # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
  71     - : lambdaTerm = Constant (Num 3)
  72
  73 What kind of evaluation strategy does this evaluator use?  In
  74 particular, what are the answers to the three questions about
  75 evaluation strategy as given in the discussion of [[evaluation
  76 strategies|topics/week3_evaluation_order]] as Q1, Q2, and Q3?
  77
  78 ## Evaluation in the untyped calculus: environments
  79
  80 Ok, the previous strategy sucked: tracking free and bound variables,
  81 computing fresh variables, it's all super complicated.
  82 Here's a better strategy.
  83
  84