```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_if_redex :: Term -> Term
let reduce_if_redex (t:term):term = match t with               reduce_if_redex t = case t of
| App(I,a) -> a                                                App I a -> a
| App(App(K,a),b) -> a                                         App (App K a) b -> a
| App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))             App (App (App S a) b) c -> App (App a c) (App b c)
| _ -> t                                                       _ -> t

is_redex :: Term -> Bool
let is_redex (t:term):bool = not (t = reduce_if_redex t)       is_redex t = not (t == reduce_if_redex t)

reduce_try2 :: Term -> Term
let rec reduce_try2 (t : term) : term = match t with           reduce_try2 t = case t of
| I -> I                                                       I -> I
| K -> K                                                       K -> K
| S -> S                                                       S -> S
| App (a, b) ->                                                App a b ->
let t' = App (reduce_try2 a, reduce_try2 b) in                 let t' = App (reduce_try2 a) (reduce_try2 b) in
if (is_redex t') then let t'' = reduce_if_redex t'             if (is_redex t') then reduce_try2 (reduce_if_redex t')
in reduce_try2 t''                                        else t'
else t'
```
There are some differences in the way types are made explicit, and in 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_try2 (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_try2 a` and `reduce_try2 b`, it doesn't bother computing `reduce_try2 b`. Instead, it waits to see if we ever really need to use the result. So the program as written does _not_ fully determine evaluation order 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: let rec reduce_try3 (t : term) : term = match t with | I -> I | K -> K | S -> S | App (a, b) -> let t' = App (reduce_try3 a, b) in if (is_redex t') then let t'' = reduce_if_redex t' in reduce_try3 t'' else t' There is only one small difference from `reduce_try2`: instead of setting `t'` to `App (reduce_try3 a, reduce_try3 b)`, we omit one of the recursive calls, and have `App (reduce_try3 a, b)`. That is, we don't evaluate the right-hand subexpression at all. Ever! The only way to get evaluated is to somehow get into functor position. # reduce_try3 (App(App(K,I),skomega));; - : term = I # reduce_try3 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.