-data Term = I | S | K | FA Term Term deriving (Eq, Show)
+data Term = I | S | K | App Term Term deriving (Eq, Show)
-skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-test = (FA (FA K I) skomega)
+skomega = (App (App (App S I) I) (App (App S I) I))
+test = (App (App 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)
+ 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
I -> I
K -> K
S -> S
- FA a b ->
- let t' = FA (reduce a) (reduce b) in
+ App a b ->
+ let t' = App (reduce a) (reduce b) in
if (is_redex t') then reduce (reduce_one_step t')
else t'