X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2F_assignment6.mdwn;h=b6a00dedd31771e23b6cfc49627b9ca4b87d8f28;hp=587a1e0fb877326f01605281abaa4363ed029de6;hb=35de8baadf52a3f6488fbd0463cdc331a4ea02e3;hpb=238ead02860158d6b1292cbf911b0ca3b3a4c456 diff --git a/exercises/_assignment6.mdwn b/exercises/_assignment6.mdwn index 587a1e0f..b6a00ded 100644 --- a/exercises/_assignment6.mdwn +++ b/exercises/_assignment6.mdwn @@ -2,31 +2,187 @@ ## 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 the eager version of the OCaml CL evaluator, +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.) -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. +## Evaluation in the untyped lambda calculus: substitution - +Having sketched the issues with a discussion of Combinatory Logic, +we're going to begin to construct an evaluator for a simple language +that includes lambda abstraction. In this problem set, 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.) -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. +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. 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)) + +By the way, 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. + +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 and closures + +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 for philosophers of language and for linguists, +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. What does your evaluator code do? + +We'll guide you to a solution involving closures. The first step is +to allow values to carry around a specific environment with them: + + type value = LiteralV of literal | Closure of lambdaTerm * env + +This will provide the extra information we need to evaluate an +identifier all the way down to the correct final result. Here is a +[[modified version of the evaluator that provides all the scaffoling for +passing around closures|exercises/reduction_with_closures]]. +The problem is with the following line: + + | Closure (Abstract(bound_ident, body), saved_r) -> eval body (push bound_ident arg saved_r) (* FIX ME *) + +What should it be in order to solve the problem? + + +## Monads + +Mappables (functors), MapNables (applicatives functors), and Monads +(composables) are ways of lifting computations from unboxed types into +boxed types. Here, a "boxed type" is a type function with one missing +piece, which we can think of as a function from a type to a type. +Call this type function M, and let P, Q, R, and S be variables over types. + +Recall that a monad requires a singleton function 1:P-> MP, and a +composition operator >=>: (P->MQ) -> (Q->MR) -> (P->MR) [the type for +the composition operator given here corrects a "type"-o from the class handout] +that obey the following laws: + + 1 >=> k = k + k >=> 1 = k + j >=> (k >=> l) = (j >=> k) >=> l + +For instance, the identity monad has the identity function I for 1 +and ordinary function composition (o) for >=>. It is easy to prove +that the laws hold for any expressions j, k, and l whose types are +suitable for 1 and >=>: + + 1 >=> k == I o k == \p. I (kp) ~~> \p.kp ~~> k + k >=> 1 == k o I == \p. k (Ip) ~~> \p.kp ~~> k + + (j >=> k) >=> l == (\p.j(kp)) o l == \q.(\p.j(kp))(lq) ~~> \q.j(k(lq)) + j >=> (k >=> l) == j o (k o l) == j o \p.k(lp) == \q.j(\p.k(lp)q) ~~> \q.j(k(lq)) + +1. On a number of occasions, we've used the Option type to make our +conceptual world neat and tidy (for instance, think of the discussion +of Kaplan's Plexy). As we learned in class, there is a natural monad +for the Option type. Borrowing the notation of OCaml, let's say that +"`'a option`" is the type of a boxed `'a`, whatever type `'a` is. +More specifically, + + 'a option = Nothing | Just 'a + +Then the obvious singleton for the Option monad is \p.Just p. Give +(or reconstruct) the composition operator >=> we discussed in class. +Show your composition operator obeys the monad laws. + +2. Do the same with crossy lists. That is, given an arbitrary type +'a, let the boxed type be a list of objects of type 'a. The singleton +is `\p.[p]`, and the composition operator is + + >=> (first:P->[Q]) (second:Q->[R]) :(P->[R]) = fun p -> [r | q <- first p, r <- second q] + +Sanity check: + + f p = [x, x+1] + s q = [x*x, x+x] + >=> f s 7 = [49, 14, 64, 16] + +3. Do the same for zippy lists. That is, you need to find a +composition operator such that + + f p = [x, x+1] + s q = [x*x, x+x] + >=> f s 7 = [49, 64] + +and then prove it obeys the monad laws.