added Wordsworth
[lambda.git] / topics / _week7_eval_cl.mdwn
index 09a480b..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:
 
@@ -125,7 +124,7 @@ no redexes.
 In order to fully reduce a term, we need to be able to reduce redexes
 that are not at the top level of the term.
 
-    (II)I ~~> IK ~~> K
+    (II)K ~~> IK ~~> K
 
 That is, we want to be able to first evaluate the redex `II` that is
 a proper subpart of the larger term, to produce a new intermediate term
@@ -153,7 +152,7 @@ processing.  But just in case the result of the one-step reduction is
 itself a redex, we recursively call `reduce1`.  The recursion will
 continue until the result is no longer a redex.
 
-    #trace reduce1;;
+    # #trace reduce1;;
     reduce1 is now traced.
     # reduce1 (FA (I, FA (I, K)));;
     reduce1 <-- FA (I, FA (I, K))
@@ -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
@@ -351,3 +356,7 @@ this discussion:
 *How can we can we specify the evaluation order of a computational
 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.]