-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'
+let reduce_if_redex (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
+
+let is_redex (t:term):bool = not (t = reduce_if_redex t)
+
+let rec reduce_try2 (t:term):term = match t with
+ | I -> I
+ | K -> K
+ | S -> S
+ | App (a, b) ->
+ let t' = App (reduce_try2 a, reduce_try2 b) in
+ if (is_redex t') then let t'' = reduce_if_redex t'
+ in reduce_try2 t''
+ else t'
+
+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'