```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'
```
```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'
```
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.