2e4f70444aa40105471e83a71efba74b8c380be6
1 # Assignment 6 (week 7)
3 ## Evaluation order in Combinatory Logic
5 1. Give a term that the lazy evaluators (either [[the Haskell
6 evaluator|code/ski_evaluator.hs]], or the lazy version of [[the OCaml
7 evaluator|code/ski_evaluator.ml]]) do not evaluate all the way to a
8 normal form, i.e., that contains a redex somewhere inside of it after
9 it has been reduced.
11 <!-- reduce3 (FA (K, FA (I, I))) -->
13 2. One of the [[criteria we established for classifying reduction
14 strategies|topics/week3_evaluation_order]] strategies is whether they
15 reduce subexpressions hidden under lambdas.  That is, for a term like
16 `(\x y. x z) (\x. x)`, do we reduce to `\y.(\x.x) z` and stop, or do
17 we reduce further to `\y.z`?  Explain what the corresponding question
18 would be for CL. Using either the OCaml CL evaluator or the Haskell
19 evaluator developed in the wiki notes, prove that the evaluator does
20 reduce expressions inside of at least some "functional" CL
21 expressions.  Then provide a modified evaluator that does not perform
22 reductions in those positions. (Just give the modified version of your
23 recursive reduction function.)
25 <!-- just add early no-op cases for Ka and Sab -->
27 ## Evaluation in the untyped lambda calculus: substitution
29 Once you grok reduction and evaluation order in Combinatory Logic,
30 we're going to begin to construct an evaluator for a simple language
31 that includes lambda abstraction.  We're going to work through the
32 issues twice: once with a function that does substitution in the
33 obvious way.  You'll see it's somewhat complicated.  The complications
34 come from the need to worry about variable capture.  (Seeing these
35 complications should give you an inkling of why we presented the
36 evaluation order discussion using Combinatory Logic, since we don't
37 need to worry about variables in CL.)
39 We're not going to ask you to write the entire program yourself.
40 Instead, we're going to give you [[the complete program, minus a few
41 little bits of glue|code/reduction_with_substitution.ml]].  What you need to do is
42 understand how it all fits together.  When you do, you'll understand
43 how to add the last little bits to make functioning program.
45 1. In the previous homework, you built a function that took an
46 identifier and a lambda term and returned a boolean representing
47 whether that identifier occured free inside of the term.  Your first
48 task is to complete the `free_in` function, which has been crippled in
49 the code base (look for lines that say `COMPLETE THIS LINE`).  Once
50 you have your function working, you should be able to run queries such
51 as this:
53     # free_in "x" (App (Abstract ("x", Var "x"), Var "x"));;
54     - : bool = true
56 2. Once you get the `free_in` function working, you'll need to
57 complete the `substitute` function.  You'll see a new wrinkle on
58 OCaml's pattern-matching construction: `| PATTERN when x = 2 ->
59 RESULT`.  This means that a match with PATTERN is only triggered if
60 the boolean condition in the `when` clause evaluates to true.
61 Sample target:
63     # substitute (App (Abstract ("x", ((App (Abstract ("x", Var "x"), Var "y")))), Constant (Num 3))) "y" (Constant (Num 4));;
64     - : lambdaTerm = App (Abstract ("x", App (Abstract ("x", Var "x"), Constant (Num 4))), Constant (Num 3))
66 3. Once you have completed the previous two problems, you'll have a
67 complete evaluation program. Here's a simple sanity check for when you
68 get it working:
70     # reduce (App (Abstract ("x", Var "x"), Constant (Num 3)));;
71     - : lambdaTerm = Constant (Num 3)
73 4. What kind of evaluation strategy does this evaluator use?  In
75 evaluation strategy as given in the discussion of [[evaluation
76 strategies|topics/week3_evaluation_order]] as Q1, Q2, and Q3?
78 ## Evaluation in the untyped calculus: environments
80 Ok, the previous strategy sucked: tracking free and bound variables,
81 computing fresh variables, it's all super complicated.
83 Here's a better strategy. Instead of keeping all of the information
84 about which variables have been bound or are still free implicitly
85 inside of the terms, we'll keep score.  This will require us to carry
86 around a scorecard, which we will call an "environment".  This is a
87 familiar strategy, since it amounts to evaluating expressions relative
88 to an assignment function.  The difference between the assignment
89 function approach above, and this approach, is one huge step towards
92 5. First, you need to get [[the evaluation
93 code|code/reduction_with_environments.ml]]  working.  Look in the
94 code for places where you see "not yet implemented", and get enough of
95 those places working that you can use the code to evaluate terms.
97 6. A snag: what happens when we want to replace a variable with a term
98 that itself contains a free variable?
100 <pre>
101 term          environment
102 ------------- -------------
103 (\w.(\y.y)w)2 []
104 (\y.y)w       [w->2]
105 y             [w->2, y->w]
106 </pre>
108 In the first step, we bind `w` to the argument `2`.  In the second
109 step, we bind `y` to the argument `w`.  In the third step, we would
110 like to replace `y` with whatever its current value is according to
111 our scorecard.  On the simple-minded view, we would replace it with
112 `w`.  But that's not the right result, because `w` itself has been
113 mapped onto 2.
117 Mappables (functors), MapNables (applicatives functors), and Monads
118 (composables) are ways of lifting computations from unboxed types into
119 boxed types.  Here, a "boxed type" is a type function with one missing
120 piece, which we can think of as a function from a type to a type.
121 Call this type function M, and let P, Q, R, and S be variables over types.
123 Recall that a monad requires a singleton function 1:P-> MP, and a
124 composition operator >=>: (P->MQ) -> (Q->MR) -> (R->MS) that obey the
125 following laws:
127     1 >=> k = k
128     k >=> 1 = k
129     j >=> (k >=> l) = (j >=> k) >=> l
131 For instance, the identity monad has the identity function I for 1
132 and ordinary function composition (o) for >=>.  It is easy to prove
133 that the laws hold for any expressions j, k, and l whose types are
134 suitable for 1 and >=>:
136     1 >=> k == I o k == \p. I (kp) ~~> \p.kp ~~> k
137     k >=> 1 == k o I == \p. k (Ip) ~~> \p.kp ~~> k
139     (j >=> k) >=> l == (\p.j(kp)) o l == \q.(\p.j(kp))(lq) ~~> \q.j(k(lq))
140     j >=> (k >=> l) == j o (k o l) == j o \p.k(lp) == \q.j(\p.k(lp)q) ~~> \q.j(k(lq))
142 1. On a number of occasions, we've used the Option type to make our
143 conceptual world neat and tidy (for instance, think of the discussion
144 of Kaplan's Plexy).  It turns out that there is a natural monad for
145 the Option type.  Borrowing the notation of OCaml, let's say that "`'a
146 option`" is the type of a boxed `'a`, whatever type `'a` is.  Then the
147 obvious singleton for the Option monad is \p.Just p.  What is the
148 composition operator >=> for the Option monad?  Show your answer is
149 correct by proving that it obeys the monad laws.