X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=exercises%2Fassignment7.mdwn;h=8dfc42d3b33bc7408b7073b4d2fc0919637ab62b;hb=cd5d55412e3ebef73b08b17584fccf36f6f18c44;hp=ebc20e064bc1ad1f7d02756ad8a015913dfaea9d;hpb=a99932db08dadc468764f1dfcc32d19760b52c5a;p=lambda.git diff --git a/exercises/assignment7.mdwn b/exercises/assignment7.mdwn deleted file mode 100644 index ebc20e06..00000000 --- a/exercises/assignment7.mdwn +++ /dev/null @@ -1,180 +0,0 @@ -# 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 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.) - - -## 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.) - -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 lists. That is, given an arbitrary type -'a, let the boxed type be ['a], i.e., 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]) = List.flatten (List.map f (g a)) - -For example: - - f p = [p, p+1] - s q = [q*q, q+q] - >=> f s 7 = [49, 14, 64, 16] -