Date: Sun, 15 Mar 2015 12:23:52 0400
Subject: [PATCH] exx

..._environments.ml => reduction_with_closures.ml}  2 +
code/ski_evaluator.hs  16 ++
code/ski_evaluator.ml  20 ++
exercises/_assignment6.mdwn  105 ++++++++++++
4 files changed, 80 insertions(+), 63 deletions()
rename code/{_reduction_with_environments.ml => reduction_with_closures.ml} (98%)
diff git a/code/_reduction_with_environments.ml b/code/reduction_with_closures.ml
similarity index 98%
rename from code/_reduction_with_environments.ml
rename to code/reduction_with_closures.ml
index db406c75..dc3d8fa2 100644
 a/code/_reduction_with_environments.ml
+++ b/code/reduction_with_closures.ml
@@ 58,7 +58,7 @@ let rec eval (term:lambdaTerm) (r:env) : value =
 value > eval body (push bound_ident value r))
 App(head, arg) > (match eval head r with
 LiteralV lit > raise (Stuck (App(Constant(LiteralC lit), arg)))
  Closure (Abstract(bound_ident, body), saved_r) > let argval = eval arg r in eval body (push bound_ident argval saved_r)
+  Closure (Abstract(bound_ident, body), saved_r) > eval body (push bound_ident arg saved_r) (* FIX ME *)
 Closure (Constant (FunctC Leq), saved_r) > failwith "not yet implemented"
 Closure (Constant (FunctC (_ as prim)), saved_r) >
(match (prim, eval arg r) with
diff git a/code/ski_evaluator.hs b/code/ski_evaluator.hs
index 845d6dad..26f1c0e6 100644
 a/code/ski_evaluator.hs
+++ b/code/ski_evaluator.hs
@@ 1,13 +1,13 @@
data Term = I  S  K  FA Term Term deriving (Eq, Show)
+data Term = I  S  K  App Term Term deriving (Eq, Show)
skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
test = (FA (FA K I) skomega)
+skomega = (App (App (App S I) I) (App (App S I) I))
+test = (App (App K I) skomega)
reduce_one_step :: Term > Term
reduce_one_step t = case t of
 FA I a > a
 FA (FA K a) b > a
 FA (FA (FA S a) b) c > FA (FA a c) (FA b c)
+ App I a > a
+ App (App K a) b > a
+ App (App (App S a) b) c > App (App a c) (App b c)
_ > t
is_redex :: Term > Bool
@@ 18,7 +18,7 @@ reduce t = case t of
I > I
K > K
S > S
 FA a b >
 let t' = FA (reduce a) (reduce b) in
+ App a b >
+ let t' = App (reduce a) (reduce b) in
if (is_redex t') then reduce (reduce_one_step t')
else t'
diff git a/code/ski_evaluator.ml b/code/ski_evaluator.ml
index 5e23ff9a..4d6f9a12 100644
 a/code/ski_evaluator.ml
+++ b/code/ski_evaluator.ml
@@ 1,12 +1,12 @@
type term = I  S  K  FA of (term * term)
+type term = I  S  K  App of (term * term)
let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
let test = FA (FA (K,I), skomega)
+let skomega = App (App (App (S,I), I), App (App (S,I), I))
+let test = App (App (K,I), skomega)
let reduce_one_step (t:term):term = match t with
 FA(I,a) > a
  FA(FA(K,a),b) > a
  FA(FA(FA(S,a),b),c) > FA(FA(a,c),FA(b,c))
+ App(I,a) > a
+  App(App(K,a),b) > a
+  App(App(App(S,a),b),c) > App(App(a,c),App(b,c))
 _ > t
let is_redex (t:term):bool = not (t = reduce_one_step t)
@@ 15,8 +15,8 @@ let rec reduce (t:term):term = match t with
I > I
 K > K
 S > S
  FA (a, b) >
 let t' = FA (reduce a, reduce b) in
+  App (a, b) >
+ let t' = App (reduce a, reduce b) in
if (is_redex t') then reduce (reduce_one_step t')
else t'
@@ 24,7 +24,7 @@ let rec reduce_lazy (t:term):term = match t with
I > I
 K > K
 S > S
  FA (a, b) >
 let t' = FA (reduce_lazy a, b) in
+  App (a, b) >
+ let t' = App (reduce_lazy a, b) in
if (is_redex t') then reduce_lazy (reduce_one_step t')
else t'
diff git a/exercises/_assignment6.mdwn b/exercises/_assignment6.mdwn
index 2e4f7044..0f654f25 100644
 a/exercises/_assignment6.mdwn
+++ b/exercises/_assignment6.mdwn
@@ 8,39 +8,37 @@ evaluatorcode/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
strategiestopics/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.)
+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
Once you grok reduction and evaluation order in Combinatory Logic,
+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. 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.)
+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 gluecode/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.
+little bits of gluecode/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
@@ 54,15 +52,16 @@ as this:
 : 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 patternmatching 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:
+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 patternmatching
+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:
@@ 75,7 +74,7 @@ particular, what are the answers to the three questions about
evaluation strategy as given in the discussion of [[evaluation
strategiestopics/week3_evaluation_order]] as Q1, Q2, and Q3?
## Evaluation in the untyped calculus: environments
+## 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.
@@ 84,10 +83,10 @@ 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.
+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
codecode/reduction_with_environments.ml]] working. Look in the
@@ 97,20 +96,34 @@ 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]

+ 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 simpleminded view, we would replace it with
`w`. But that's not the right result, because `w` itself has been
mapped onto 2.
+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 closuresexercises/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
@@ 141,9 +154,13 @@ suitable for 1 and >=>:
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). It turns out that 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. Then the
obvious singleton for the Option monad is \p.Just p. What is the
composition operator >=> for the Option monad? Show your answer is
correct by proving that it obeys the monad laws.
+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.11.0