--- /dev/null
+<!-- λ Λ ∀ ≡ α β ω Ω -->
+
+[[!toc levels=2]]
+
+# Reasoning about evaluation order in Combinatory Logic
+
+We've discussed [[evaluation order|topics/week3_evaluation_order]]
+before, primarily in connection with the untyped lambda calculus.
+Whenever a term contains more than one redex, we have to choose which
+one to reduce, and this choice can make a difference. For instance,
+recall that
+
+ Ω == ωω == (\x.xx)(\x.xx), so
+
+ ((\x.I)Ω) == ((\x.I)((\x.xx)(\x.xx)))
+ * *
+
+There are two redexes in this term; we've marked the operative lambda
+with a star. If we reduce the leftmost redex first, the term reduces
+to the normal form `I` in one step. But if we reduce the left most
+redex instead, the "reduced" form is `(\x.I)Ω` again, and we are in
+danger of entering an infinite loop.
+
+Thanks to the recent introduction of sum types (disjoint union), we
+are now in a position to gain a deeper understanding of evaluation
+order by reasoning explicitly about evaluation by writing a program
+that evaluates terms.
+
+One thing we'll see is that it is all too easy for the evaluation
+order properties of an evaluator to depend on the evaluation order
+properties of the programming language in which the evaluator is
+written. We would like to write an evaluator in which the order of
+evaluation is insensitive to the evaluator language. The goal is to
+find an order-insensitive way to reason about evaluation order. We
+will not fully succeed in this first attempt, but we will make good
+progress.
+
+The first evaluator we will develop will evaluate terms in Combinatory
+Logic. This significantly simplifies the discussion, since we won't
+need to worry about variables or substitution. As we develop and
+extend our evaluator in future weeks, we'll switch to lambdas, but for
+now, working with the simplicity of Combinatory Logic will make it
+easier to highlight evaluation order issues.
+
+A brief review of Combinatory Logic: a term in CL is the combination
+of three basic expressions, `S`, `K`, and `I`, governed by the
+following reduction rules:
+
+ Ia ~~> a
+ Kab ~~> a
+ Sabc ~~> ac(bc)
+
+where `a`, `b`, and `c` stand for an arbitrary term of CL. We've seen
+how to embed the untyped lambda calculus in CL, so it's no surprise
+that evaluation order issues arise in CL. To illustrate, we'll use
+the following definition:
+
+ skomega = SII
+ Skomega = skomega skomega == SII(SII)
+ ~~> I(SII)(I(SII))
+ ~~> SII(SII)
+
+We'll use the same symbol, `Ω`, for Omega and Skomega: in a lambda
+term, `Ω` refers to Omega, but in a CL term, `Ω` refers to Skomega as
+defined here.
+
+Just as in the corresponding term in the lambda calculus, CL terms can
+contain more than one redex:
+
+ KIΩ == KI(SII(SII))
+ * *
+
+we can choose to reduce the leftmost redex by applying the reduction
+rule for `K`, in which case the term reduces to the normal form `I` in
+one step; or we can choose to reduce the Skomega part, by applying the
+reduction rule `S`, in which case we do not get a normal form, and
+we're headed towards an infinite loop.
+
+With sum types, we can define CL terms in OCaml as follows:
+
+ type term = I | K | S | App of (term * term)
+
+ let skomega = App (App (App (S, I), I), App (App (S, I), I))
+
+This type definition says that a term in CL is either one of the three
+simple expressions (`I`, `K`, or `S`), or else a pair of CL
+expressions. `App` stands for Functional Application. With this type
+definition, we can encode skomega, as well as other terms whose
+reduction behavior we want to try to control.
+
+Using pattern matching, it is easy to code the one-step reduction
+rules for CL:
+
+ let reduce_one_step (t:term):term = match t with
+ App(I,a) -> a
+ | App(App(K,a),b) -> a
+ | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
+ | _ -> t
+
+ # reduce_one_step (App(App(K,S),I));;
+ - : term = S
+ # reduce_one_step skomega;;
+ - : term = App (App (I, App (App (S, I), I)), App (I, App (App (S, I), I)))
+
+The definition of `reduce_one_step` explicitly says that it expects
+its input argument `t` to have type `term`, and the second `:term`
+says that the type of the output it delivers as a result will be of
+type `term`.
+
+The type constructor `App` obscures things a bit, but it's still
+possible to see how the one-step reduction function is just the
+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 (App(K,I));;
+ - : bool = false
+ # is_redex (App(App(K,I),S));;
+ - : bool = true
+ # is_redex skomega;;
+ - : book = true
+
+Warning: this definition relies on the accidental fact that the
+one-step reduction of a CL term is never identical to the original
+term. This would not work for the untyped lambda calculus, since
+`((\x.xx)(\x.xx)) ~~> ((\x.xx)(\x.xx))` in one step.
+
+Note that in order to decide whether two terms are equal, OCaml has to
+recursively compare the elements of complex CL terms. It is able to
+figure out how to do this because we provided an explicit definition
+of the datatype `term`.
+
+As you would expect, a term in CL is in normal form when it contains
+no redexes (analogously for head normal form, weak head normal form, etc.)
+
+In order to fully reduce a term, we need to be able to reduce redexes
+that are not at the top level of the term.
+Because we need to process subparts, and because the result after
+processing a subpart may require further processing, the recursive
+structure of our evaluation function has to be somewhat subtle. To
+truly understand, you will need to do some sophisticated thinking
+about how recursion works.
+
+We'll develop our full reduction function in two stages. Once we have
+it working, we'll then consider a variant.
+
+ let rec reduce_stage1 (t:term):term =
+ if (is_redex t) then reduce_stage1 (reduce_one_step t)
+ 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 `reduce_stage1`. The recursion
+will continue until the result is no longer a redex. We're aiming at
+allowing the evaluator to recognize that
+
+ I (I K) ~~> I K ~~> K
+
+When trying to understand how recursive functions work, it can be
+extremely helpful to examining an execution trace of inputs and
+outputs.
+
+ # #trace reduce_stage1;;
+ reduce_stage1 is now traced.
+ # reduce_stage1 (App (I, App (I, K)));;
+ reduce_stage1 <-- App (I, App (I, K))
+ reduce_stage1 <-- App (I, K)
+ reduce_stage1 <-- K
+ reduce_stage1 --> K
+ reduce_stage1 --> K
+ reduce_stage1 --> K
+ - : term = K
+
+In the trace, "`<--`" shows the input argument to a call to
+`reduce_stage1`, and "`-->`" shows the output result.
+
+Since the initial input (`I(IK)`) is a redex, the result after the
+one-step reduction is `IK`. We recursively call `reduce_stage1` on
+this input. Since `IK` is itself a redex, the result after one-step
+reduction is `K`. We recursively call `reduce_stage1` on this input. Since
+`K` is not a redex, the recursion bottoms out, and we return the
+result.
+
+But this function doesn't do enough reduction. We want to recognize
+the following reduction path:
+
+ I I K ~~> I K ~~> K
+
+But the reduction function as written above does not deliver this result:
+
+ # reduce_stage1 (App (App (I, I), K));;
+ - : term = App (App (I, I), K)
+
+Because the top-level term is not a redex to start with,
+`reduce_stage1` returns it without any evaluation. What we want is to
+evaluate the subparts of a complex term. We'll do this by evaluating
+the subparts of the top-level expression.
+
+ let rec reduce (t:term):term = match t with
+ I -> I
+ | K -> K
+ | S -> S
+ | App (a, b) ->
+ let t' = App (reduce a, reduce b) in
+ if (is_redex t') then reduce 2 (reduce_one_step t')
+ else t'
+
+Since we need access to the subterms, we do pattern matching on the
+input. If the input is simple (the first three `match` cases), we
+return it without further processing. But if the input is complex, we
+first process the subexpressions, and only then see if we have a redex
+at the top level. To understand how this works, follow the trace
+carefully:
+
+ # reduce (App(App(I,I),K));;
+ reduce <-- App (App (I, I), K)
+
+ reduce <-- K ; first main recursive call
+ reduce --> K
+
+ reduce <-- App (I, I) ; second main recursive call
+ reduce <-- I
+ reduce --> I
+ reduce <-- I
+ reduce --> I
+ reduce <-- I
+ reduce --> I
+ reduce --> I
+
+ reduce <-- K ; third
+ reduce --> K
+ reduce --> 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`.
+
+There are three recursive calls to the `reduce` function, each of
+which gets triggered during the processing of this example. They have
+been marked in the trace.
+
+The don't quite go in the order in which they appear in the code,
+however! 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`.
+
+At this point, we have constructed `t' == App(I,K)`. Since that's a
+redex, we ship it off to reduce_one_step, getting the term `K` as a
+result. The third recursive call checks that there is no more
+reduction work to be done (there isn't), and that's our final result.
+
+You can see in more detail what is going on by tracing both reduce
+and reduce_one_step, but that makes for some long traces.
+
+So we've solved our first problem: reduce recognizes that `IIK ~~>
+K`, as desired.
+
+Because the OCaml interpreter evaluates each subexpression in the
+course of building `t'`, however, it will always evaluate the right
+hand subexpression, whether it needs to or not. And sure enough,
+
+ # reduce (App(App(K,I),skomega));;
+ C-c C-cInterrupted.
+
+Running the evaluator with this input leads to an infinite loop, and
+the only way to get out is to kill the interpreter with control-c.
+
+Instead of performing the leftmost reduction first, and recognizing
+that this term reduces to the normal form `I`, we get lost endlessly
+trying to reduce skomega.
+
+## Laziness is hard to overcome
+
+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 | App of (term * term) data Term = I | S | K | App Term Term deriving (Eq, Show)
+
+let skomega = App (App (App (S,I), I), App (App (S,I), I)) skomega = (App (App (App S I) I) (App (App S I) I))
+
+ reduce_one_step :: Term -> Term
+let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
+ App(I,a) -> a App I a -> a
+ | App(App(K,a),b) -> a App (App K a) b -> a
+ | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c)) App (App (App S a) b) c -> App (App a c) (App b c)
+ | _ -> t _ -> t
+
+ is_redex :: Term -> Bool
+let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
+
+ reduce :: Term -> Term
+let rec reduce (t:term):term = match t with reduce t = case t of
+ I -> I I -> I
+ | K -> K K -> K
+ | S -> S S -> S
+ | App (a, b) -> App a b ->
+ let t' = App (reduce a, reduce b) in let t' = App (reduce a) (reduce b) in
+ if (is_redex t') then reduce (reduce_one_step t') if (is_redex t') then reduce (reduce_one_step t')
+ else t' else t'
+</pre>
+
+There are some differences in the way types are made explicit, and in
+the way terms are specified (`App(a,b)` for Ocaml versus `App a b` for
+Haskell). But the two programs are essentially identical.
+
+Yet the Haskell program finds the normal form for `KIΩ`:
+
+ *Main> reduce (App (App K I) skomega)
+ 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 `reduce a` and `reduce b`, it
+doesn't bother computing `reduce b`. Instead, it waits to see if we
+ever really need to use the result.
+
+So the program as written does NOT fully determine evaluation order
+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?
+
+* 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, or the `deepseq`
+operator), but a fully general, satisifying resolution will have to
+wait until we have Continuation Passing Style transforms.
+
+The answer to the first question (Can we adjust the OCaml evaluator to
+exhibit lazy behavior?) is quite simple:
+
+<pre>
+let rec reduce_lazy (t:term):term = match t with
+ I -> I
+ | K -> K
+ | S -> S
+ | App (a, b) ->
+ let t' = App (reduce_lazy a, b) in
+ if (is_redex t') then reduce_lazy (reduce_one_step t')
+ else t'
+</pre>
+
+There is only one small difference: instead of setting `t'` to `App
+(reduce a, reduce b)`, we omit one of the recursive calls, and have
+`App (reduce a, b)`. That is, we don't evaluate the right-hand
+subexpression at all. Ever! The only way to get evaluated is to
+somehow get into functor position.
+
+ # reduce3 (App(App(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.
+
+We can now 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?*
+
+As a final note, we should mention that the evaluators given here are
+absurdly inefficient computationally. Some computer scientists have
+trouble even looking at code this inefficient, but the emphasis here
+is on getting the concepts across as simply as possible.