data Term = I | S | K | App Term Term deriving (Eq, Show) skomega = (App (App (App S I) I) (App (App S I) I)) test = (App (App K I) skomega) reduce_if_redex :: Term -> Term reduce_if_redex t = case t of 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 is_redex :: Term -> Bool is_redex t = not (t == reduce_if_redex t) reduce_try2 :: Term -> Term reduce_try2 t = case t of I -> I K -> K S -> S App a b -> let t' = App (reduce_try2 a) (reduce_try2 b) in if (is_redex t') then reduce_try2 (reduce_if_redex t') else t'