From d3b4c1156ba908e5b58c3d8579f944e4f68a697f Mon Sep 17 00:00:00 2001
From: Chris <chris.barker@nyu.edu>
Date: Sun, 8 Mar 2015 14:04:33 -0400
Subject: [PATCH] eval order CL

---
 topics/_week7_eval_cl.mdwn | 4887 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 4887 insertions(+)
 create mode 100644 topics/_week7_eval_cl.mdwn

diff --git a/topics/_week7_eval_cl.mdwn b/topics/_week7_eval_cl.mdwn
new file mode 100644
index 00000000..251f62f4
--- /dev/null
+++ b/topics/_week7_eval_cl.mdwn
@@ -0,0 +1,4887 @@
+<!-- λ Λ ∀ ≡ α β ω Ω -->
+
+[[!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 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
+
+Woa!  First of all, this is wierd.  Haskell's evaluation strategy is
+called "lazy".  Apparently, Haskell is so lazy that even after we've
+asked it to construct t' by evaluating `reduce2 a` and `reduce2 b`, it
+doesn't bother computing `reduce2 b`.  Instead, it waits to see if we
+ever really need to use the result.
+
+So despite intuitions, the program as written does NOT determine
+evaluation order behavior.  At this stage, we have defined an
+evaluation order that still depends on the evaluation order of the
+underlying interpreter.
+
+There are two questions we could ask: Can we adjust the OCaml
+evaluator to exhibit lazy behavior?  and Can we adjust the Haskell
+evaluator to exhibit eager behavior?  The answer to the first question
+is easy and interesting, and we'll give it right away.  The answer to
+the second question is also interesting, but not easy.  There are
+various tricks available in Haskell we could use (such as the `seq`
+operator), but a fully general, satisifying resolution will have to
+wait until we have Continuation Passing Transforms. 
+
+The answer to the first question (Can we adjust the OCaml evaluator to
+exhibit lazy behavior?) is quite simple:
+
+<pre>
+let rec reduce3 (t:term):term = match t with
+    I -> I
+  | K -> K
+  | S -> S
+  | FA (a, b) -> 
+      let t' = FA (reduce3 a, b) in
+        if (is_redex t') then reduce3 (reduce_one_step t')
+                         else t'
+</pre>
+
+There is only one small difference: instead of setting `t'` to
+`FA (reduce a, reduce b)`, we have `FA (reduce a, b)`.  That is, we
+don't evaluate the right-hand subexpression at all.  Ever!  The only
+way to get evaluated is to somehow get into functor position.  
+
+    # reduce3 (FA(FA(K,I),skomega));;
+    - : term = I
+    # reduce3 skomega;;
+    C-c C-cInterrupted.
+
+The evaluator now has no trouble finding the normal form for `KIΩ`,
+but evaluating skomega still gives an infinite loop.
+
+As a final note, we can clarify the larger question at the heart of
+this discussion: 
+
+*How can we can we specify the evaluation order of a computational
+system in a way that is completely insensitive to the evaluation order
+of the specification language?*
-- 
2.11.0