+<!-- λ Λ ∀ ≡ α β ω Ω -->
+
+[[!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?*