author Chris Mon, 9 Mar 2015 01:20:12 +0000 (21:20 -0400) committer Chris Mon, 9 Mar 2015 01:20:12 +0000 (21:20 -0400)
 exercises/_assignment7.mdwn [new file with mode: 0644] patch | blob topics/_week7_eval_cl.mdwn patch | blob | history

diff --git a/exercises/_assignment7.mdwn b/exercises/_assignment7.mdwn
new file mode 100644 (file)
index 0000000..cd798ab
--- /dev/null
@@ -0,0 +1,25 @@
+# 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 -->
index 8a5e9c3..12ac7cf 100644 (file)
@@ -4,16 +4,16 @@

# Reasoning about evaluation order in Combinatory Logic

-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term contains more than one
-redex, we have to choose which one to reduce, and this choice can make
-a difference.  For instance, in the term `((\x.I)(ωω))`, if we reduce
-the leftmost redex first, the term reduces to the normal form `I` in
-one step.  But if we reduce the left most redex instead (namely,
-`(ωω)`), we do not arrive at a normal form, and are in danger of
-entering an infinite loop.
-
-Thanks to the introduction of sum types (disjoint union), we are now
+We've discussed [[evaluation order|topics/week3_evaluation_order]]
+before, primarily in connection with the untyped lambda calculus.
+Whenever a term contains more than one redex, we have to choose which
+one to reduce, and this choice can make a difference.  For instance,
+in the term `((\x.I)(ωω))`, if we reduce the leftmost redex first, the
+term reduces to the normal form `I` in one step.  But if we reduce the
+left most redex instead (namely, `(ωω)`), we do not arrive at a normal
+form, and are in danger of entering an infinite loop.
+
+Thanks to the recent introduction of sum types (disjoint union), we are now
in a position to gain a deeper understanding of evaluation order by
writing a program that experiments with different evaluation order
strategies.
@@ -28,7 +28,7 @@ will not fully succeed in this first attempt, but we will make good
progress.

The first evaluator we will develop will evaluate terms in Combinatory
-Logic.  This significantly simplifies the program, since we won't need
+Logic.  This significantly simplifies the discussion, since we won't need
to worry about variables or substitution.  As we develop and extend
our evaluator in future weeks, we'll switch to lambdas, but for now,
working with the simplicity of Combinatory Logic will make the
@@ -44,26 +44,25 @@ rules:

where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
how to embed the untyped lambda calculus in CL, so it's no
-surprise that the evaluation order issues arise in CL.  To illustrate,
+surprise that evaluation order issues arise in CL.  To illustrate,
we'll use the following definition:

skomega = SII(SII)
~~> I(SII)(I(SII))
~~> SII(SII)

-Instead of the lambda term `Ω`, we'll use the CL term skomega.  We'll
-use the same symbol, `Ω`, though: in a lambda term, `Ω` refers to
-omega, but in a CL term, `Ω` refers to skomega as defined here.
+We'll use the same symbol, `Ω`, though: in a lambda term, `Ω` refers
+to omega, but in a CL term, `Ω` refers to skomega as defined here.

If we consider the term

KIΩ == KI(SII(SII))

-we can choose to reduce the leftmost redex by firing the reduction
+we can choose to reduce the leftmost redex by applying the reduction
rule for `K`, in which case the term reduces to the normal form `I` in
-one step; or we can choose to reduce the skomega part, by firing the
-reduction rule for the leftmost `S`, in which case we do not get a
-normal form, and we're headed towards an infinite loop.
+one step; or we can choose to reduce the skomega part, by applying the
+reduction rule `S`, in which case we do not get a normal form, and
+we're headed towards an infinite loop.

With sum types, we can define terms in CL in OCaml as follows:

@@ -178,7 +177,8 @@ But this function doesn't do enough reduction.

Because the top-level term is not a redex, `reduce1` returns it
without any evaluation.  What we want is to evaluate the subparts of a
-complex term.
+complex term.  We'll do this by mapping the reduction function onto
+the parts of a complex term.

let rec reduce2 (t:term):term = match t with
I -> I
@@ -189,11 +189,12 @@ complex term.
if (is_redex t') then reduce2 (reduce_one_step t')
else t'

-Since we need access to the subterms, we do pattern matching on the
-input term.  If the input is simple, we return it (the first three
-match cases).  If the input is complex, we first process the
-subexpressions, and only then see if we have a redex.  To understand
-how this works, follow the trace carefully:
+Since what we need is access to the subterms, we do pattern matching
+on the input term.  If the input is simple (the first three `match`
+cases), we return it without further processing.  But if the input is
+complex, we first process the subexpressions, and only then see if we
+have a redex at the top level.  To understand how this works, follow
+the trace carefully:

# reduce2 (FA(FA(I,I),K));;
reduce2 <-- FA (FA (I, I), K)
@@ -206,31 +207,35 @@ how this works, follow the trace carefully:
reduce2 --> I
reduce2 <-- I
reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
+        reduce2 <-- I
+        reduce2 --> I
reduce2 --> I

-      reduce2 <-- K           ; fourth
+      reduce2 <-- K           ; third
reduce2 --> K
reduce2 --> K
- : term = K

Ok, there's a lot going on here.  Since the input is complex, the
first thing the function does is construct `t'`.  In order to do this,
-it must reduce the two main subexpressions, `II` and `K`.  But we see
-from the trace that it begins with the right-hand expression, `K`.  We
-didn't explicitly tell it to begin with the right-hand subexpression,
-so control over evaluation order is starting to spin out of our
-control.  (We'll get it back later, don't worry.)
+it must reduce the two main subexpressions, `II` and `K`.
+
+There are three recursive calls to the reduce2 function, each of
+which gets triggered during the processing of this example.  They have
+been marked in the trace.
+
+The don't quite go in the order in which they appear in the code,
+however!  We see from the trace that it begins with the right-hand
+expression, `K`.  We didn't explicitly tell it to begin with the
+right-hand subexpression, so control over evaluation order is starting
+to spin out of our control.  (We'll get it back later, don't worry.)

In any case, in the second main recursive call, we evaluate `II`.  The
-result is `I`.  The third main recursive call tests whether this
-result needs any further processing; it doesn't.
+result is `I`.

At this point, we have constructed `t' == FA(I,K)`.  Since that's a
redex, we ship it off to reduce_one_step, getting the term `K` as a
-result.  The fourth recursive call checks that there is no more
+result.  The third recursive call checks that there is no more
reduction work to be done (there isn't), and that's our final result.

You can see in more detail what is going on by tracing both reduce2
@@ -352,7 +357,6 @@ this discussion:
system in a way that is completely insensitive to the evaluation order
of the specification language?*

-
[By the way, the evaluators given here are absurdly inefficient computationally.
Some computer scientists have trouble even looking at code this inefficient, but
the emphasis here is on getting the concepts across as simply as possible.]