X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2F_assignment6.mdwn;h=9a3d04c049c4733d854cfd51ea829b13d4e7f24c;hp=587a1e0fb877326f01605281abaa4363ed029de6;hb=57dee2bbf8450a3ee982f8bdc868a6258b38da0e;hpb=238ead02860158d6b1292cbf911b0ca3b3a4c456 diff --git a/exercises/_assignment6.mdwn b/exercises/_assignment6.mdwn index 587a1e0f..9a3d04c0 100644 --- a/exercises/_assignment6.mdwn +++ b/exercises/_assignment6.mdwn @@ -2,31 +2,113 @@ ## Evaluation order in Combinatory Logic -1. Give a term that the lazy evaluators (either the Haskell evaluator, -or the lazy version of the OCaml evaluator) 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. +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 -"functional" CL expressions. Then provide a modified evaluator that -does not perform reductions in those positions. +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.) -3. Converting to lambdas. Using the type definitions you developed in -homework 5, rebuild the evaluator in OCaml to handle the untyped -lambda calculus. Making use of the occurs_free function you built, -we'll provide a function that performs safe substitution. +## 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.