X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek7_eval_cl.mdwn;h=8349a40c5356e08d850a6685d57ba331928d0b6b;hp=65b0200b0d0eca2c43f7cafa910bdc8f71b79dcf;hb=4aea3a471f66d67fccff34189186f8cdb561dd68;hpb=ad7fea353514a45be62c56bbc9f8df266db0266b

diff --git a/topics/week7_eval_cl.mdwn b/topics/week7_eval_cl.mdwn
index 65b0200b..8349a40c 100644
--- a/topics/week7_eval_cl.mdwn
+++ b/topics/week7_eval_cl.mdwn
@@ -15,22 +15,21 @@ recall that
     ((\x.I)Ω) == ((\x.I)((\x.xx)(\x.xx)))
                    *      *
 
-There are two redexes in this term; we've marked the operative lambda
+There are two redexes in this term; we've marked the operative lambdas
 with a star.  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
+to the normal form `I` in one step.  But if we reduce the rightmost
 redex instead, the "reduced" form is `(\x.I)Ω` again, and we are in
 danger of entering an infinite loop.
 
-Thanks to the recent introduction of sum types (disjoint union), we
+Thanks to the introduction of sum types (disjoint union) in the last lecture, we
 are now in a position to gain a deeper understanding of evaluation
-order by reasoning explicitly about evaluation by writing a program
-that evaluates terms.
+order by writing a program that allows us to reasoning explicitly about evaluation.
 
 One thing we'll see is that it is all too easy for the evaluation
 order properties of an evaluator to depend on the evaluation order
 properties of the programming language in which the evaluator is
 written.  We would like to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
+evaluation is insensitive to the evaluator language.  That is, the goal is to
 find an order-insensitive way to reason about evaluation order.  We
 will not fully succeed in this first attempt, but we will make good
 progress.
@@ -85,7 +84,7 @@ With sum types, we can define CL terms in OCaml as follows:
 This type definition says that a term in CL is either one of the three
 simple expressions (`I`, `K`, or `S`), or else a pair of CL
 expressions.  `App` stands for Functional Application.  With this type
-definition, we can encode skomega, as well as other terms whose
+definition, we can encode Skomega, as well as other terms whose
 reduction behavior we want to try to control.
 
 Using pattern matching, it is easy to code the one-step reduction
@@ -104,13 +103,13 @@ rules for CL:
 
 The definition of `reduce_one_step` explicitly says that it expects
 its input argument `t` to have type `term`, and the second `:term`
-says that the type of the output it delivers as a result will be of
+says that the type of the output the function delivers as a result will also be of
 type `term`.
 
 The type constructor `App` obscures things a bit, but it's still
 possible to see how the one-step reduction function is just the
-reduction rules for CL.  The OCaml interpreter shows us that the
-function faithfully recognizes that `KSI ~~> S`, and `skomega ~~>
+reduction rules for CL.  The OCaml interpreter responses given above show us that the
+function faithfully recognizes that `KSI ~~> S`, and that `Skomega ~~>
 I(SII)(I(SII))`.
 
 We can now say precisely what it means to be a redex in CL.
@@ -144,7 +143,7 @@ that are not at the top level of the term.
 Because we need to process subparts, and because the result after
 processing a subpart may require further processing, the recursive
 structure of our evaluation function has to be somewhat subtle.  To
-truly understand, you will need to do some sophisticated thinking
+truly understand, we will need to do some sophisticated thinking
 about how recursion works.  
 
 We'll develop our full reduction function in two stages.  Once we have
@@ -163,7 +162,7 @@ allowing the evaluator to recognize that
     I (I K) ~~> I K ~~> K
 
 When trying to understand how recursive functions work, it can be
-extremely helpful to examining an execution trace of inputs and
+extremely helpful to examine an execution trace of inputs and
 outputs.
 
     # #trace reduce_stage1;;
@@ -197,8 +196,10 @@ But the reduction function as written above does not deliver this result:
     # reduce_stage1 (App (App (I, I), K));;
     - : term = App (App (I, I), K)
 
-Because the top-level term is not a redex to start with,
-`reduce_stage1` returns it without any evaluation.  What we want is to
+The reason is that the top-level term is not a redex to start with,
+so `reduce_stage1` returns it without any evaluation.  
+
+What we want is to
 evaluate the subparts of a complex term.  We'll do this by evaluating
 the subparts of the top-level expression.
 
@@ -215,7 +216,9 @@ Since we need access to the subterms, we do pattern matching on the
 input.  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
+at the top level.  
+
+To understand how this works, follow the trace
 carefully:
 
     # reduce (App(App(I,I),K));;
@@ -263,7 +266,7 @@ 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 reduce
 and reduce_one_step, but that makes for some long traces.
 
-So we've solved our first problem: reduce recognizes that `IIK ~~>
+So we've solved our first problem: `reduce` now recognizes that `IIK ~~>
 K`, as desired.
 
 Because the OCaml interpreter evaluates each subexpression in the
@@ -278,7 +281,7 @@ the only way to get out is to kill the interpreter with control-c.
 
 Instead of performing the leftmost reduction first, and recognizing 
 that this term reduces to the normal form `I`, we get lost endlessly
-trying to reduce skomega.
+trying to reduce Skomega.
 
 ## Laziness is hard to overcome