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.ml]]. What you need to do is
+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. Here's a
-first target for when you get it working:
-
- # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
- - : lambdaTerm = Constant (Num 3)
+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 adapt your previous solution as necessary to work with the
-code base. Once you have your function working, you should be able to
-run queries such as this:
+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.