From 6eb94b1b0c2bd030c11a3da469e769faa5ada8d9 Mon Sep 17 00:00:00 2001
From: Chris
Date: Sat, 14 Mar 2015 08:14:10 0400
Subject: [PATCH] hw6

code/ski_evaluator.hs  24 ++++++++++++++++++++++++
code/ski_evaluator.ml  30 ++++++++++++++++++++++++++++++
exercises/_assignment6.mdwn  28 ++++++++++++++++++++++++++++
exercises/_assignment7.mdwn  31 
4 files changed, 82 insertions(+), 31 deletions()
create mode 100644 code/ski_evaluator.hs
create mode 100644 code/ski_evaluator.ml
create mode 100644 exercises/_assignment6.mdwn
delete mode 100644 exercises/_assignment7.mdwn
diff git a/code/ski_evaluator.hs b/code/ski_evaluator.hs
new file mode 100644
index 00000000..845d6dad
 /dev/null
+++ b/code/ski_evaluator.hs
@@ 0,0 +1,24 @@
+data Term = I  S  K  FA Term Term deriving (Eq, Show)
+
+skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
+test = (FA (FA 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)
+ _ > t
+
+is_redex :: Term > Bool
+is_redex t = not (t == reduce_one_step t)
+
+reduce :: Term > Term
+reduce t = case t of
+ I > I
+ K > K
+ S > S
+ FA a b >
+ let t' = FA (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
new file mode 100644
index 00000000..10d130e0
 /dev/null
+++ b/code/ski_evaluator.ml
@@ 0,0 +1,30 @@
+type term = I  S  K  FA of (term * term)
+
+let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
+let test = FA (FA (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))
+  _ > t
+
+let is_redex (t:term):bool = not (t = reduce_one_step t)
+
+let rec reduce_eager (t:term):term = match t with
+ I > I
+  K > K
+  S > S
+  FA (a, b) >
+ let t' = FA (reduce_eager a, reduce_eager b) in
+ if (is_redex t') then reduce_eager (reduce_one_step t')
+ else t'
+
+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
+ if (is_redex t') then reduce_lazy (reduce_one_step t')
+ else t'
diff git a/exercises/_assignment6.mdwn b/exercises/_assignment6.mdwn
new file mode 100644
index 00000000..aabcbe07
 /dev/null
+++ b/exercises/_assignment6.mdwn
@@ 0,0 +1,28 @@
+# Assignment 6 (week 7)
+
+## Evaluation order in Combinatory Logic
+
+1. Give a term that the lazy evaluators (either [[the Haskell
+evaluatorcode/ski_evaluator.hs]], or the lazy version of [[the OCaml
+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.)
+
+
+
+## Evaluation in the untyped lambda calculus
+
diff git a/exercises/_assignment7.mdwn b/exercises/_assignment7.mdwn
deleted file mode 100644
index 8cf57f2c..00000000
 a/exercises/_assignment7.mdwn
+++ /dev/null
@@ 1,31 +0,0 @@
# Assignment 6 (week 7)

## 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.




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.



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.


2.11.0