Merge branch 'master' into working
authorJim <>
Thu, 19 Mar 2015 03:36:16 +0000 (23:36 -0400)
committerJim <>
Thu, 19 Mar 2015 03:36:16 +0000 (23:36 -0400)
* master:
  rename topics/week7__95__combinatory__95__evaluator.mdwn to topics/week7_combinatory_evaluator.mdwn
  light editing, rename functions for clarity
  rename topics/week7_eval_combinatory.mdwn to topics/week7__95__combinatory__95__evaluator.mdwn
  rename eval_combinatory
  post combinatory evaluator
  post eval_combinatory
  rename topics/week7_eval_cl.mdwn to topics/week7_eval_combinatory.mdwn
  add Plexy and some stubs/reorganization
  link to Plexy
  rename topics/_week6_plexy.mdwn to topics/week6_plexy.mdwn

topics/week6_plexy.mdwn [moved from topics/_week6_plexy.mdwn with 83% similarity]
topics/week7_combinatory_evaluator.mdwn [moved from topics/week7_eval_cl.mdwn with 66% similarity]

index b5ecf20..61ac961 100644 (file)
@@ -7,6 +7,8 @@ week in which they were introduced.
 *   [[What is computation?|topics/week3_what_is_computation]]
+*   [[Kaplan on Plexy|topics/week6_plexy]]
 *   Functional Programming
     *   [[Introduction|topics/week1 kapulet intro]]
@@ -18,12 +20,16 @@ week in which they were introduced.
     *   More tips on using Scheme
     *   Types in OCaml and Haskell (will be posted soon)
     *   Practical advice for working with OCaml and/or Haskell (will be posted soon)
+    *   [[Kaplan on Plexy|topics/week6_plexy]] and the Maybe type
+    *   Interpreter for Lambda terms
+    *   Starting with Monads
 *   Order, "static versus dynamic"
     *   [[Order in programming languages and natural language|topics/week1 order]]
     *   [[Reduction Strategies and Normal Forms in the Lambda Calculus|topics/week3_evaluation_order]]
     *   [[Unit and its usefulness|topics/week3 unit]]
+    *   [[Combinatory evaluator|topics/week7_combinatory_evaluator]]
 *   The Untyped Lambda Calculus
@@ -40,14 +46,19 @@ week in which they were introduced.
     *   [[Reduction Strategies and Normal Forms|topics/week3_evaluation_order]]
     *   [[Fixed point combinators|topics/week4_fixed_point_combinators]]
     *   [[More about fixed point combinators|topics/week4_more_about_fixed_point_combinators]]
+    *   Interpreter for Lambda terms
-*   [[Combinatory Logic|topics/week3 combinatory logic]]
+*   Combinatory logic
+    *   [[Introduction|topics/week3 combinatory logic]]
+    *   [[Combinatory evaluator|topics/week7_combinatory_evaluator]]
 *   Typed Lambda Calculi
     *   [[Simply-typed lambda calculus|topics/week5 simply typed]] (will be updated)
     *   [[System F|topics/week5 system F]] (will be updated)
     *   Types in OCaml and Haskell (will be posted soon)
+    *   Starting with Monads
 ## Topics by week ##
@@ -99,10 +110,17 @@ Week 5:
 *   Practical advice for working with OCaml and/or Haskell (will be posted soon)
 *   [[Homework for weeks 5 and 6|exercises/assignment5]]
-Outside readings for week 6:
+Week 6:
-*   [[footnote about "Plexy"|readings/kaplan-plexy.pdf]] from Kaplan's *Demonstratives*
+*   [[footnote about "Plexy"|readings/kaplan-plexy.pdf]] from Kaplan's *Demonstratives* about Plexy; [[our notes|topics/week6_plexy]] comparing to the Maybe type
 *   (Recommended) [[King's discussion of Schiffer|readings/king-on-schiffer.pdf]] in Chapter 4 of *The Nature and Structure of Content* (2007)
-*   Michael Rieppel, "[[Being Something: Properties and Predicative Quantification|readings/rieppel-beingsthg.pdf]]"
 *   (Recommended) [[King's discussion of clausal complements and proposition-designators|readings/king-on-logicism.pdf]] from Chapter 5 of *The Nature and Structure of Content* (2007) <!-- reviews and elaborates his paper "[Designating propositions](" -->
+*   Michael Rieppel, "[[Being Something: Properties and Predicative Quantification|readings/rieppel-beingsthg.pdf]]"
+Week 7:
+*   [[Combinatory evaluator|topics/week7_combinatory_evaluator]]
+*   Interpreter for Lambda terms
+*   Starting with Monads
index a764795..9b6c09c 100644 (file)
@@ -155,6 +155,12 @@ Practical advice for working with OCaml and/or Haskell (all will be posted soon)
 > We will be discussing the readings posted above.
+> Topics: [[Kaplan on Plexy|topics/week6_plexy]]; King on that-clauses and "the proposition that P"; Rieppel on Frege and the concept HORSE
+(**Week 7**) Thursday March 12
+> Topics: [[Combinatory evaluator|topics/week7_combinatory_evaluator]]; Interpreter for Lambda terms; Starting with Monads
 We've added a [[Monad Library]] for OCaml.
similarity index 83%
rename from topics/_week6_plexy.mdwn
rename to topics/week6_plexy.mdwn
index 79d081e..864d84e 100644 (file)
@@ -20,10 +20,10 @@ of *the solar system*, an object representing the relational concept
 denoted by *center*, and so on.  It doesn't matter precisely what that
 structure is, as long as it has distinct internal parts.
-Kaplan names this complex object "Plexy".  On Kaplan's assumptions,
+Kaplan names this complex object "Plexy".  Simplifying Kaplan's presentation, let's suppose
 the name *Plexy* is directly referential, and refers to the complex
 object that represents the meaning of *the center of mass of the solar
+system*. Now consider:
     2. Plexy is a point.
@@ -64,18 +64,20 @@ the meaning of (2) can be `<{P}, point>`: radically different, as desired.
 In terms of the type systems we'll be developing over the next few
 weeks, the type of a DP will be a *sum type*: the disjoint union of the
 class of objects that a directly referential term can refer to, and
-the class of objects that can serve as the complex structure
-corresponding to a DP that is not directly referential.
+the class of objects that can serve as complex meaning structures
+corresponding to DPs as in (1) that are not directly referential.
 ## Motivating Maybe
-Kaplan goes on to use this solution to attack a different problem, the
+At the end of his footnote, Kaplan suggests using his proposal to help with a different problem, the
 problem of non-referring names.  Russell supposed that if a name had
 no referent (e.g., *Santa*), a sentence containing that name would
 have no meaning, since there would be no object to insert into the
 structure representing the meaning of that sentence.  But on Kaplan's
 scheme, there is no problem: *Santa is hungry* would denote `<{},
+hungry>`. This can't be confused with a sentence saying that the empty set is
+hungry, since (supposing we directly refer to the empty set), that would
+denote `<{{}},hungry>`.
 This second idea has some obvious flaws.  For instance, it predicts
 that sentences that differ only in the choice of a non-referring name
@@ -87,12 +89,11 @@ Setting aside such objections, we will see over and over again the
 utility of the general strategy instantiated in Kaplan's strategy for representing the meaning of
 directly-referential expressions:
-    Kaplan's rule for directly-referential expressions:
-    a directly referential expression E contributes either
-    {}   if there is no object that E refers to, or else
-    {P}  if E refers to P
+> Kaplan's rule for directly-referential expressions: a directly referential expression E contributes either:  
+> {}   if there is no object that E refers to, or else  
+> {P}  if E refers to P
-In later weeks, we will call the general form of this technique the Maybe type, and the general strategy for deploying this type the Maybe monad.
+In later weeks, we will call the general form of this technique the "option" or "Maybe" type, and the general strategy for deploying this type "the Maybe monad." (In OCaml one has types like `int option`; in Haskell they are `Maybe Int`.)
 Kaplan, D. 1989. "Demonstratives. In J. Almog, J. Perry, & H. Wettstein
similarity index 66%
rename from topics/week7_eval_cl.mdwn
rename to topics/week7_combinatory_evaluator.mdwn
index 8349a40..9c3ac87 100644 (file)
@@ -2,15 +2,17 @@
 [[!toc levels=2]]
-# Reasoning about evaluation order in Combinatory Logic
+## Reasoning about evaluation order in Combinatory Logic
 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,
-recall that 
+recall that:
-    Ω == ωω == (\x.xx)(\x.xx), so
+    Ω == ωω == (\x.xx)(\x.xx)
     ((\x.I)Ω) == ((\x.I)((\x.xx)(\x.xx)))
                    *      *
@@ -18,12 +20,11 @@ recall that
 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 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're starting off on an infinite loop.
 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 writing a program that allows us to reasoning explicitly about evaluation.
+order by writing a program that allows us to reason 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
@@ -37,7 +38,7 @@ progress.
 The first evaluator we will develop will evaluate terms in Combinatory
 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
+extend our evaluator in homework and other lectures, we'll switch to lambdas, but for
 now, working with the simplicity of Combinatory Logic will make it
 easier to highlight evaluation order issues.
@@ -69,11 +70,11 @@ contain more than one redex:
     KIΩ == KI(SII(SII))
            *  *
-we can choose to reduce the leftmost redex by applying 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 applying the
 reduction rule `S`, in which case we do not get a normal form, and
-we're headed towards an infinite loop.
+we're headed into an infinite loop.
 With sum types, we can define CL terms in OCaml as follows:
@@ -82,28 +83,31 @@ With sum types, we can define CL terms in OCaml as follows:
     let skomega = App (App (App (S, I), I), App (App (S, I), I))
 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
+atomic 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
-reduction behavior we want to try to control.
+reduction behavior we want to try to control. We can *control* it because
+the `App` variant of our datatype merely *encodes* the application of the
+head to the argument, and doesn't actually *perform* that application.
+We have to explicitly model the application ourself.
 Using pattern matching, it is easy to code the one-step reduction
 rules for CL:
-    let reduce_one_step (t:term):term = match t with
-        App(I,a) -> a
+    let reduce_if_redex (t:term) : term = match t with
+      | App(I,a) -> a
       | App(App(K,a),b) -> a
       | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
       | _ -> t
-    # reduce_one_step (App(App(K,S),I));;
+    # reduce_if_redex (App(App(K,S),I));;
     - : term = S
-    # reduce_one_step skomega;;
+    # reduce_if_redex skomega;;
     - : term = App (App (I, App (App (S, I), I)), App (I, App (App (S, I), I)))
-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 the function delivers as a result will also be of
+The definition of `reduce_if_redex` explicitly says that it expects
+its input argument `t` to have type `term`, and the second `: term`
+says that the result the function delivers will also be of
 type `term`.
 The type constructor `App` obscures things a bit, but it's still
@@ -112,9 +116,12 @@ reduction rules for CL.  The OCaml interpreter responses given above show us tha
 function faithfully recognizes that `KSI ~~> S`, and that `Skomega ~~>
-We can now say precisely what it means to be a redex in CL.
+As you would expect, a term in CL is in normal form when it contains
+no redexes (analogously for head normal form, weak head normal form, etc.)
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
+How can we tell whether a term is a redex? Here's one way:
+    let is_redex (t:term):bool = not (t = reduce_if_redex t)
     # is_redex K;;
     - : bool = false
@@ -125,23 +132,23 @@ We can now say precisely what it means to be a redex in CL.
     # is_redex skomega;;
     - : book = true
-Warning: this definition relies on the accidental fact that the
-one-step reduction of a CL term is never identical to the original
-term.  This would not work for the untyped lambda calculus, since
-`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.
-Note that in order to decide whether two terms are equal, OCaml has to
+In order to decide whether two terms are equal, OCaml has to
 recursively compare the elements of complex CL terms.  It is able to
 figure out how to do this because we provided an explicit definition
 of the datatype `term`.
-As you would expect, a term in CL is in normal form when it contains
-no redexes (analogously for head normal form, weak head normal form, etc.)
-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.
-Because we need to process subparts, and because the result after
-processing a subpart may require further processing, the recursive
+Warning: this method for telling whether a term is a redex relies on the accidental fact that the
+one-step reduction of a CL term is never identical to the original
+term.  This would not work for the untyped lambda calculus, since
+`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step. Neither would it work if
+we had chosen some other combinators as primitives (`W W1 W2` reduces to
+`W1 W2 W2`, so if they are all `W`s we'd be in trouble.) We will discuss
+some alternative strategies in other notes.
+So far, we've only asked whether a term _is_ a redex, not whether it _contains_ other redexes as subterms. But
+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. Because we need to process subterms, and because the result after
+processing a subterm may require further processing, the recursive
 structure of our evaluation function has to be somewhat subtle.  To
 truly understand, we will need to do some sophisticated thinking
 about how recursion works.  
@@ -149,13 +156,14 @@ about how recursion works.
 We'll develop our full reduction function in two stages.  Once we have
 it working, we'll then consider a variant.  
-    let rec reduce_stage1 (t:term):term = 
-      if (is_redex t) then reduce_stage1 (reduce_one_step t)
+    let rec reduce_try1 (t:term) : term = 
+      if (is_redex t) then let t' = reduce_if_redex t
+                           in reduce_try1 t'
                       else t
-If the input is a redex, we ship it off to `reduce_one_step` for
+If the input is a redex, we ship it off to `reduce_if_redex` for
 processing.  But just in case the result of the one-step reduction is
-itself a redex, we recursively call `reduce_stage1`.  The recursion
+itself a redex, we recursively apply `reduce_try1` to the result.  The recursion
 will continue until the result is no longer a redex.  We're aiming at
 allowing the evaluator to recognize that
@@ -165,24 +173,27 @@ When trying to understand how recursive functions work, it can be
 extremely helpful to examine an execution trace of inputs and
-    # #trace reduce_stage1;;
-    reduce_stage1 is now traced.
-    # reduce_stage1 (App (I, App (I, K)));;
-    reduce_stage1 <-- App (I, App (I, K))
-      reduce_stage1 <-- App (I, K)
-        reduce_stage1 <-- K
-        reduce_stage1 --> K
-      reduce_stage1 --> K
-    reduce_stage1 --> K
+    # #trace reduce_try1;;
+    reduce_try1 is now traced.
+The first `#` there is OCaml's prompt. The text beginning `#trace ...` is what we typed. Now OCaml will report on all the input to, and results from, the `reduce_try1` function. Watch:
+    # reduce_try1 (App (I, App (I, K)));;
+    reduce_try1 <-- App (I, App (I, K))
+      reduce_try1 <-- App (I, K)
+        reduce_try1 <-- K
+        reduce_try1 --> K
+      reduce_try1 --> K
+    reduce_try1 --> K
     - : term = K
 In the trace, "`<--`" shows the input argument to a call to
-`reduce_stage1`, and "`-->`" shows the output result.
+`reduce_try1`, and "`-->`" shows the output result.
 Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce_stage1` on
+one-step reduction is `IK`.  We recursively call `reduce_try1` on
 this input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce_stage1` on this input.  Since
+reduction is `K`.  We recursively call `reduce_try1` on this input.  Since
 `K` is not a redex, the recursion bottoms out, and we return the
@@ -193,24 +204,24 @@ the following reduction path:
 But the reduction function as written above does not deliver this result:
-    # reduce_stage1 (App (App (I, I), K));;
+    # reduce_try1 (App (App (I, I), K));;
     - : term = App (App (I, I), K)
 The reason is that the top-level term is not a redex to start with,
-so `reduce_stage1` returns it without any evaluation.  
+so `reduce_try1` 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.
+What we want is to evaluate the subterms of a complex term.  We'll do this by pattern matching our
+top-level term to see when it _has_ subterms:
-    let rec reduce (t:term):term = match t with
-        I -> I
+    let rec reduce_try2 (t : term) : term = match t with
+      | I -> I
       | K -> K
       | S -> S
       | App (a, b) -> 
-          let t' = App (reduce a, reduce b) in
-            if (is_redex t') then reduce 2 (reduce_one_step t')
-                             else t'
+          let t' = App (reduce_try2 a, reduce_try2 b) in
+          if (is_redex t') then let t'' = reduce_if_redex t'
+                                in reduce_try2 t''
+                           else t'
 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
@@ -221,24 +232,24 @@ at the top level.
 To understand how this works, follow the trace
-    # reduce (App(App(I,I),K));;
-    reduce <-- App (App (I, I), K)
+    # reduce_try2 (App(App(I,I),K));;
+    reduce_try2 <-- App (App (I, I), K)
-      reduce <-- K          ; first main recursive call
-      reduce --> K
+      reduce_try2 <-- K          ; first main recursive call
+      reduce_try2 --> K
-      reduce <-- App (I, I)  ; second main recursive call
-        reduce <-- I
-        reduce --> I
-        reduce <-- I
-        reduce --> I
-        reduce <-- I
-        reduce --> I
-      reduce --> I
+      reduce_try2 <-- App (I, I)  ; second main recursive call
+        reduce_try2 <-- I
+        reduce_try2 --> I
+        reduce_try2 <-- I
+        reduce_try2 --> I
+        reduce_try2 <-- I
+        reduce_try2 --> I
+      reduce_try2 --> I
-      reduce <-- K           ; third 
-      reduce --> K
-    reduce --> K
+      reduce_try2 <-- K           ; third 
+      reduce_try2 --> K
+    reduce_try2 --> K
     - : term = K
 Ok, there's a lot going on here.  Since the input is complex, the
@@ -259,12 +270,12 @@ In any case, in the second main recursive call, we evaluate `II`.  The
 result is `I`.  
 At this point, we have constructed `t' == App(I,K)`.  Since that's a
-redex, we ship it off to reduce_one_step, getting the term `K` as a
+redex, we ship it off to reduce_if_redex, getting the term `K` as a
 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 reduce
-and reduce_one_step, but that makes for some long traces.
+and reduce_if_redex, but that makes for some long traces.
 So we've solved our first problem: `reduce` now recognizes that `IIK ~~>
 K`, as desired.
@@ -273,7 +284,7 @@ Because the OCaml interpreter evaluates each subexpression in the
 course of building `t'`, however, it will always evaluate the right
 hand subexpression, whether it needs to or not.  And sure enough,
-    # reduce (App(App(K,I),skomega));;
+    # reduce_try2 (App(App(K,I),skomega));;
       C-c C-cInterrupted.
 Running the evaluator with this input leads to an infinite loop, and
@@ -297,25 +308,26 @@ type term = I | S | K | App of (term * term)                   data Term = I | S
 let skomega = App (App (App (S,I), I), App (App (S,I), I))     skomega = (App (App (App S I) I) (App (App S I) I))                      
-                                                               reduce_one_step :: Term -> Term                                      
-let reduce_one_step (t:term):term = match t with               reduce_one_step t = case t of                                      
-    App(I,a) -> a                                                App I a -> a                                                      
+                                                               reduce_if_redex :: Term -> Term                                      
+let reduce_if_redex (t:term):term = match t with               reduce_if_redex t = case t of                                      
+  | App(I,a) -> a                                                App I a -> a                                                      
   | App(App(K,a),b) -> a                                         App (App K a) b -> a                                              
   | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))             App (App (App S a) b) c -> App (App a c) (App b c)                      
   | _ -> t                                                       _ -> t                                                      
                                                                is_redex :: Term -> Bool                                      
-let is_redex (t:term):bool = not (t = reduce_one_step t)       is_redex t = not (t == reduce_one_step t)                      
+let is_redex (t:term):bool = not (t = reduce_if_redex t)       is_redex t = not (t == reduce_if_redex t)                      
-                                                               reduce :: Term -> Term                                              
-let rec reduce (t:term):term = match t with                    reduce t = case t of                                              
-    I -> I                                                       I -> I                                                      
+                                                               reduce_try2 :: Term -> Term                                              
+let rec reduce_try2 (t : term) : term = match t with           reduce_try2 t = case t of                                              
+  | I -> I                                                       I -> I                                                      
   | K -> K                                                       K -> K                                                      
   | S -> S                                                       S -> S                                                      
-  | App (a, b) ->                                                 App a b ->                                                       
-      let t' = App (reduce a, reduce b) in                          let t' = App (reduce a) (reduce b) in                      
-        if (is_redex t') then reduce (reduce_one_step t')             if (is_redex t') then reduce (reduce_one_step t')      
-                         else t'                                                       else t'                                
+  | App (a, b) ->                                                App a b ->                                                       
+      let t' = App (reduce_try2 a, reduce_try2 b) in                 let t' = App (reduce_try2 a) (reduce_try2 b) in                      
+      if (is_redex t') then let t'' = reduce_if_redex t'             if (is_redex t') then reduce_try2 (reduce_if_redex t')      
+                            in reduce_try2 t''                                        else t'                                
+                       else t'
 There are some differences in the way types are made explicit, and in
@@ -324,16 +336,16 @@ Haskell).  But the two programs are essentially identical.
 Yet the Haskell program finds the normal form for `KIΩ`:
-    *Main> reduce (App (App K I) skomega)
+    *Main> reduce_try2 (App (App K I) skomega)
 Woa!  First of all, this is wierd.  Haskell's evaluation strategy is
 called "lazy".  Apparently, Haskell is so lazy that even after we've
-asked it to construct t' by evaluating `reduce a` and `reduce b`, it
-doesn't bother computing `reduce b`.  Instead, it waits to see if we
+asked it to construct `t'` by evaluating `reduce_try2 a` and `reduce_try2 b`, it
+doesn't bother computing `reduce_try2 b`.  Instead, it waits to see if we
 ever really need to use the result.
-So the program as written does NOT fully determine evaluation order
+So the program as written does _not_ fully determine evaluation order
 behavior.  At this stage, we have defined an evaluation order that
 still depends on the evaluation order of the underlying interpreter.
@@ -353,20 +365,19 @@ wait until we have Continuation Passing Style transforms.
 The answer to the first question (Can we adjust the OCaml evaluator to
 exhibit lazy behavior?) is quite simple:
-let rec reduce_lazy (t:term):term = match t with
-    I -> I
-  | K -> K
-  | S -> S
-  | App (a, b) -> 
-      let t' = App (reduce_lazy a, b) in
-        if (is_redex t') then reduce_lazy (reduce_one_step t')
-                         else t'
-There is only one small difference: instead of setting `t'` to `App
-(reduce a, reduce b)`, we omit one of the recursive calls, and have
-`App (reduce a, b)`.  That is, we don't evaluate the right-hand
+    let rec reduce_lazy (t : term) : term = match t with
+      | I -> I
+      | K -> K
+      | S -> S
+      | App (a, b) -> 
+          let t' = App (reduce_lazy a, b) in
+          if (is_redex t') then let t'' = reduce_if_redex t'
+                                in reduce_lazy t''
+                           else t'
+There is only one small difference from `reduce_try2`: instead of setting `t'` to `App
+(reduce_try3 a, reduce_try3 b)`, we omit one of the recursive calls, and have
+`App (reduce_try3 a, b)`.  That is, we don't evaluate the right-hand
 subexpression at all.  Ever!  The only way to get evaluated is to
 somehow get into functor position.