1 data Term = I | S | K | FA Term Term deriving (Eq, Show)
3 skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
4 test = (FA (FA K I) skomega)
6 reduce_one_step :: Term -> Term
7 reduce_one_step t = case t of
10 FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
13 is_redex :: Term -> Bool
14 is_redex t = not (t == reduce_one_step t)
16 reduce :: Term -> Term
22 let t' = FA (reduce a) (reduce b) in
23 if (is_redex t') then reduce (reduce_one_step t')