git is a pain

[lambda.git] / topics / week7_eval_cl.mdwn

diff --git a/topics/week7_eval_cl.mdwn b/topics/week7_eval_cl.mdwn
index 65b0200..8349a40 100644 (file)
--- 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)))
                    *      *
 
     ((\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
 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.
 
 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
 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
 
 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.
 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
 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
 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`
 
 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
 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.
 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
 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
 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
     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;;
 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)
 
     # 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.
 
 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
 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));;
 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.
 
 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
 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
 
 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
 
 
 ## Laziness is hard to overcome