hw6

diff --git a/code/ski_evaluator.hs b/code/ski_evaluator.hs
new file mode 100644 (file)
index 0000000..845d6da
--- /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 (file)
index 0000000..10d130e
--- /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 (file)
index 0000000..aabcbe0
--- /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
+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.
+
+<!-- reduce3 (FA (K, FA (I, I))) -->
+
+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 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.)
+
+<!-- just add early no-op cases for Ka and Sab -->
+
+## Evaluation in the untyped lambda calculus
+

diff --git a/exercises/_assignment7.mdwn b/exercises/_assignment7.mdwn
deleted file mode 100644 (file)
index 8cf57f2..0000000
--- 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.
-
-<!-- reduce3 (FA (K, FA (I, I))) -->
-
-
-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.
-
-<!-- just add early no-op cases for Ka and Sab -->
-
-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.
-