# 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: substitution Once you grok reduction and evaluation order in Combinatory Logic, we're going to begin to construct an evaluator for a simple language that includes lambda abstraction. We're going to work through the issues twice: once with a function that does substitution in the obvious way. You'll see it's somewhat complicated. The complications come from the need to worry about variable capture. (Seeing these complications should give you an inkling of why we presented the evaluation order discussion using Combinatory Logic, since we don't need to worry about variables in CL.) We're not going to ask you to write the entire program yourself. Instead, we're going to give you [[the complete program, minus a few little bits of glue|code/reduction_with_substitution.ml]]. What you need to do is understand how it all fits together. When you do, you'll understand how to add the last little bits to make functioning program. 1. In the previous homework, you built a function that took an identifier and a lambda term and returned a boolean representing whether that identifier occured free inside of the term. Your first task is to complete the `free_in` function, which has been crippled in the code base (look for lines that say `COMPLETE THIS LINE`). Once you have your function working, you should be able to run queries such as this: # free_in "x" (App (Abstract ("x", Var "x"), Var "x"));; - : bool = true 2. Once you get the `free_in` function working, you'll need to complete the `substitute` function. You'll see a new wrinkle on OCaml's pattern-matching construction: `| PATTERN when x = 2 -> RESULT`. This means that a match with PATTERN is only triggered if the boolean condition in the `when` clause evaluates to true. Sample target: # substitute (App (Abstract ("x", ((App (Abstract ("x", Var "x"), Var "y")))), Constant (Num 3))) "y" (Constant (Num 4));; - : lambdaTerm = App (Abstract ("x", App (Abstract ("x", Var "x"), Constant (Num 4))), Constant (Num 3)) 3. Once you have completed the previous two problems, you'll have a complete evaluation program. Here's a simple sanity check for when you get it working: # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));; - : lambdaTerm = Constant (Num 3) 4. What kind of evaluation strategy does this evaluator use? In particular, what are the answers to the three questions about evaluation strategy as given in the discussion of [[evaluation strategies|topics/week3_evaluation_order]] as Q1, Q2, and Q3? ## Evaluation in the untyped calculus: environments Ok, the previous strategy sucked: tracking free and bound variables, computing fresh variables, it's all super complicated. Here's a better strategy. Instead of keeping all of the information about which variables have been bound or are still free implicitly inside of the terms, we'll keep score. This will require us to carry around a scorecard, which we will call an "environment". This is a familiar strategy, since it amounts to evaluating expressions relative to an assignment function. The difference between the assignment function approach above, and this approach, is one huge step towards monads. 5. First, you need to get [[the evaluation code|code/reduction_with_environments.ml]] working. Look in the code for places where you see "not yet implemented", and get enough of those places working that you can use the code to evaluate terms. 6. A snag: what happens when we want to replace a variable with a term that itself contains a free variable? term environment ------------- ------------- (\w.(\y.y)w)2 [] (\y.y)w [w->2] y [w->2, y->w] In the first step, we bind `w` to the argument `2`. In the second step, we bind `y` to the argument `w`. In the third step, we would like to replace `y` with whatever its current value is according to our scorecard. On the simple-minded view, we would replace it with `w`. But that's not the right result, because `w` itself has been mapped onto 2.