From 3bac08e63835f94a9cc11b6eacda6f5916aed1aa Mon Sep 17 00:00:00 2001
From: Chris <chris.barker@nyu.edu>
Date: Sun, 8 Mar 2015 14:08:26 -0400
Subject: [PATCH] edits

---
 topics/_week7_eval_cl.mdwn | 4545 --------------------------------------------
 1 file changed, 4545 deletions(-)

diff --git a/topics/_week7_eval_cl.mdwn b/topics/_week7_eval_cl.mdwn
index 251f62f4..ec88fda7 100644
--- a/topics/_week7_eval_cl.mdwn
+++ b/topics/_week7_eval_cl.mdwn
@@ -284,4551 +284,6 @@ Haskell).  But the two programs are essentially identical.
 
 Yet the Haskell program finds the normal form for KI -->
 
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI
- -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are made explicit, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KI -->
-
-[[!toc levels=2]]
-
-# Reasoning about evaluation order in Combinatory Logic
-
-We've discussed evaluation order before, primarily in connection with
-the untyped lambda calculus.  Whenever a term has 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
-in a position to gain a deeper understanding by writing a program that
-allows us to experiment with different evaluation order strategies.
-
-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 will seek to write an evaluator in which the order of
-evaluation is insensitive to the evaluator language.  The goal is to
-find an order-insensitive way to reason about evaluation order.
-
-The first evaluator we develop will evaluate terms in Combinatory
-Logic.  That will significantly simplify the program, 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 elegant simplicity of Combinatory Logic will
-make the evaluation order issues easier to grasp.
-
-A brief review: a term in CL is the combination of three basic
-expressions, `S`, `K`, and `I`, governed by the following reduction
-rules:
-
-    Ia ~~> a
-    Kab ~~> b
-    Sabc ~~> ac(bc)
-
-where `a`, `b`, and `c` stand for an arbitrary term of CL.  We've seen
-that how to embed the untyped lambda calculus in CL, so it's no
-surprise that the same evaluation order issues arise in CL.
-
-    skomega = SII(SII)
-            ~~> I(SII)(I(SII))
-            ~~> SII(SII)
-
-Instead of the lambda term `Ω`, we'll use the CL term skomega, defined
-here, though we'll use the same symbol, `Ω`.  If we consider the term
-
-    KIΩ == KI(SII(SII))
-
-we can choose to reduce the leftmost redex by firing 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 fo `S`, in which case we do not get a normal form,
-we're headed towards an infinite loop.
-
-With sum types, we can define terms in CL in OCaml as follows:
-
-    type term = I | S | K | FA of (term * term)
-
-    let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
-    let test1 = FA (FA (K,I), skomega)
-
-This recursive type definition says that a term in CL is either one of
-the three simple expressions, or else a pair of CL expressions.
-Following Heim and Kratzer, `FA` stands for Functional Application.
-With this type definition, we can encode skomega, as well as other
-terms whose reduction behavior we want to control.
-
-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
-        FA(I,a) -> a
-      | FA(FA(K,a),b) -> a
-      | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
-      | _ -> t
-
-    # reduce_one_step (FA(FA(K,S),I));;
-    - : term = S
-    # reduce_one_step skomega;;
-    - : term = FA (FA (I, FA (FA (S, I), I)), FA (I, FA (FA (S, I), I)))
-
-The need to explicitly insert the type constructor `FA` 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 ~~> I(SII)(I(SII))`.
-
-We can now say precisely what it means to be a redex in CL.
-
-    let is_redex (t:term):bool = not (t = reduce_one_step t)
-
-    # is_redex K;;
-    - : bool = false
-    # is_redex (FA(K,I));;
-    - : bool = false
-    # is_redex (FA(FA(K,I),S));;
-    - : bool = true
-    # is_redex skomega;;
-    - : book = true
-
-Warning: this definition relies on the 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 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.
-
-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.
-
-    (KKI)SI ~~> KSI ~~> S
-
-That is, we want to be able to first evaluate the redex `KKI` that is
-a proper subpart of the larger term to produce a new intermediate term
-that we can then evaluate to the final normal form.
-
-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 quite subtle.  To truly
-understand it, you will need to do some sophisticated thinking about
-how recursion works.  We'll show you how to keep track of what is
-going on by constructing an recursive execution trace of inputs and
-outputs.
-
-We'll develop our full reduction function in stages.  Once we have it
-working, we'll then consider some variants.  Just to be precise, we'll
-distinguish each microvariant with its own index number embedded in
-its name.
-
-    let rec reduce1 (t:term):term = 
-      if (is_redex t) then reduce1 (reduce_one_step t)
-                      else t
-
-If the input is a redex, we ship it off to `reduce_one_step` for
-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;;
-    reduce1 is now traced.
-    # reduce1 (FA (I, FA (I, K)));;
-    reduce1 <-- FA (I, FA (I, K))
-      reduce1 <-- FA (I, K)
-        reduce1 <-- K
-        reduce1 --> K
-      reduce1 --> K
-    reduce1 --> K
-    - : term = K
-
-Since the initial input (`I(IK)`) is a redex, the result after the
-one-step reduction is `IK`.  We recursively call `reduce1` on this
-input.  Since `IK` is itself a redex, the result after one-step
-reduction is `K`.  We recursively call `reduce1` on this input.  Since
-`K` is not a redex, the recursion bottoms out, and we simply return
-it.  
-
-But this function doesn't do enough reduction.
-
-    # reduce1 (FA (FA (I, I), K));;
-    - : term = FA (FA (I, I), K)
-
-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.
-
-    let rec reduce2 (t:term):term = match t with
-        I -> I
-      | K -> K
-      | S -> S
-      | FA (a, b) -> 
-          let t' = FA (reduce2 a, reduce2 b) in
-            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.  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:
-
-    # reduce2 (FA(FA(I,I),K));;
-    reduce2 <-- FA (FA (I, I), K)
-
-      reduce2 <-- K          ; first main recursive call
-      reduce2 --> K
-
-      reduce2 <-- FA (I, I)  ; second main recursive call
-        reduce2 <-- I
-        reduce2 --> I
-        reduce2 <-- I
-        reduce2 --> I
-      reduce2 <-- I
-
-      reduce2 --> I           ; third main recursive call
-      reduce2 --> I
-
-      reduce2 <-- K           ; fourth
-      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.)
-
-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.  
-
-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
-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
-and reduce_one_step, but that makes for some long traces.
-
-So we've solved our first problem: reduce2 recognizes that `IIK ~~>
-K`, as desired.
-
-Because the OCaml interpreter evaluates the rightmost expression  
-in the course of building `t'`, however, it will always evaluate the
-right hand subexpression, whether it needs to or not.  And sure
-enough,
-
-    # reduce2 (FA(FA(K,I),skomega));;
-      C-c C-cInterrupted.
-
-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.
-
-To emphasize that our evaluation order here is at the mercy of the
-evaluation order of OCaml, here is the exact same program translated
-into Haskell.  We'll put them side by side to emphasize the exact parallel.
-
-<pre>
-OCaml                                                          Haskell
-==========================================================     =========================================================
-
-type term = I | S | K | FA of (term * term)                    data Term = I | S | K | FA Term Term deriving (Eq, Show)      
-							       							      
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))	       skomega = (FA (FA (FA S I) I) (FA (FA 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				      
-    FA(I,a) -> a					         FA I a -> a						      
-  | FA(FA(K,a),b) -> a					         FA (FA K a) b -> a					      
-  | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))		         FA (FA (FA S a) b) c -> FA (FA a c) (FA 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)		      
-							       							      
-							       reduce2 :: Term -> Term					      
-let rec reduce2 (t:term):term = match t with		       reduce2 t = case t of					      
-    I -> I						         I -> I						      
-  | K -> K						         K -> K						      
-  | S -> S						         S -> S						      
-  | FA (a, b) -> 					         FA a b -> 						      
-      let t' = FA (reduce2 a, reduce2 b) in		           let t' = FA (reduce2 a) (reduce2 b) in		      
-        if (is_redex t') then reduce2 (reduce_one_step t')           if (is_redex t') then reduce2 (reduce_one_step t')      
-                         else t'			                              else t'                                
-</pre>
-
-There are some differences in the way types are specified, and in
-the way terms are specified (`FA(a,b)` for Ocaml versus `FA a b` for
-Haskell).  But the two programs are essentially identical.
-
-Yet the Haskell program finds the normal form for KIΩ.
-
     *Main> reduce2 (FA (FA K I) skomega)
     I
 
-- 
2.11.0