```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'
```
```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'
```
There is only one small difference: instead of setting `t'` to `FA (reduce a, reduce b)`, we omit one of the recursive calls, and 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?* [By the way, 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.]