1 type term = I | S | K | App of (term * term)
3 let skomega = App (App (App (S,I), I), App (App (S,I), I))
4 let test = App (App (K,I), skomega)
6 let reduce_one_step (t:term):term = match t with
9 | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c))
12 let is_redex (t:term):bool = not (t = reduce_one_step t)
14 let rec reduce (t:term):term = match t with
19 let t' = App (reduce a, reduce b) in
20 if (is_redex t') then reduce (reduce_one_step t')
23 let rec reduce_lazy (t:term):term = match t with
28 let t' = App (reduce_lazy a, b) in
29 if (is_redex t') then reduce_lazy (reduce_one_step t')