X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=exercises%2F_assignment6.mdwn;h=aabcbe07b2d5bd25a082e06319b9a511d2909380;hp=587a1e0fb877326f01605281abaa4363ed029de6;hb=bd471e735a942a3489670fb2c935c7577624627d;hpb=238ead02860158d6b1292cbf911b0ca3b3a4c456 diff --git a/exercises/_assignment6.mdwn b/exercises/_assignment6.mdwn index 587a1e0f..aabcbe07 100644 --- a/exercises/_assignment6.mdwn +++ b/exercises/_assignment6.mdwn @@ -2,31 +2,27 @@ ## 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. +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 -"functional" CL expressions. Then provide a modified evaluator that -does not perform reductions in those positions. +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.) -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. - +## Evaluation in the untyped lambda calculus