--- /dev/null
+data Term = I | S | K | FA Term Term deriving (Eq, Show)
+
+skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
+test = (FA (FA K I) skomega)
+
+reduce_one_step :: Term -> Term
+reduce_one_step t = case t of
+ FA I a -> a
+ FA (FA K a) b -> a
+ FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
+ _ -> t
+
+is_redex :: Term -> Bool
+is_redex t = not (t == reduce_one_step t)
+
+reduce :: Term -> Term
+reduce t = case t of
+ I -> I
+ K -> K
+ S -> S
+ FA a b ->
+ let t' = FA (reduce a) (reduce b) in
+ if (is_redex t') then reduce (reduce_one_step t')
+ else t'
--- /dev/null
+type term = I | S | K | FA of (term * term)
+
+let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I))
+let test = FA (FA (K,I), skomega)
+
+let reduce_one_step (t:term):term = match t with
+ FA(I,a) -> a
+ | FA(FA(K,a),b) -> a
+ | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c))
+ | _ -> t
+
+let is_redex (t:term):bool = not (t = reduce_one_step t)
+
+let rec reduce_eager (t:term):term = match t with
+ I -> I
+ | K -> K
+ | S -> S
+ | FA (a, b) ->
+ let t' = FA (reduce_eager a, reduce_eager b) in
+ if (is_redex t') then reduce_eager (reduce_one_step t')
+ else t'
+
+let rec reduce_lazy (t:term):term = match t with
+ I -> I
+ | K -> K
+ | S -> S
+ | FA (a, b) ->
+ let t' = FA (reduce_lazy a, b) in
+ if (is_redex t') then reduce_lazy (reduce_one_step t')
+ else t'