From: Chris Date: Sat, 14 Mar 2015 12:14:10 +0000 (-0400) Subject: hw6 X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=6eb94b1b0c2bd030c11a3da469e769faa5ada8d9 hw6 --- 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 +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 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. -