type term = I | S | K | App of (term * term) let skomega = App (App (App (S,I), I), App (App (S,I), I)) let test = App (App (K,I), skomega) 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'