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'