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