-type term = I | S | K | FA of (term * term) data Term = I | S | K | FA Term Term deriving (Eq, Show)
-
-let skomega = FA (FA (FA (S,I), I), FA (FA (S,I), I)) skomega = (FA (FA (FA S I) I) (FA (FA S I) I))
-
- reduce_one_step :: Term -> Term
-let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
- FA(I,a) -> a FA I a -> a
- | FA(FA(K,a),b) -> a FA (FA K a) b -> a
- | FA(FA(FA(S,a),b),c) -> FA(FA(a,c),FA(b,c)) FA (FA (FA S a) b) c -> FA (FA a c) (FA b c)
- | _ -> t _ -> t
-
- is_redex :: Term -> Bool
-let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
-
- reduce2 :: Term -> Term
-let rec reduce2 (t:term):term = match t with reduce2 t = case t of
- I -> I I -> I
- | K -> K K -> K
- | S -> S S -> S
- | FA (a, b) -> FA a b ->
- let t' = FA (reduce2 a, reduce2 b) in let t' = FA (reduce2 a) (reduce2 b) in
- if (is_redex t') then reduce2 (reduce_one_step t') if (is_redex t') then reduce2 (reduce_one_step t')
- else t' else t'
+type term = I | S | K | App of (term * term) data Term = I | S | K | App Term Term deriving (Eq, Show)
+
+let skomega = App (App (App (S,I), I), App (App (S,I), I)) skomega = (App (App (App S I) I) (App (App S I) I))
+
+ reduce_one_step :: Term -> Term
+let reduce_one_step (t:term):term = match t with reduce_one_step t = case t of
+ App(I,a) -> a App I a -> a
+ | App(App(K,a),b) -> a App (App K a) b -> a
+ | App(App(App(S,a),b),c) -> App(App(a,c),App(b,c)) App (App (App S a) b) c -> App (App a c) (App b c)
+ | _ -> t _ -> t
+
+ is_redex :: Term -> Bool
+let is_redex (t:term):bool = not (t = reduce_one_step t) is_redex t = not (t == reduce_one_step t)
+
+ reduce :: Term -> Term
+let rec reduce (t:term):term = match t with reduce t = case t of
+ I -> I I -> I
+ | K -> K K -> K
+ | S -> S S -> S
+ | App (a, b) -> App a b ->
+ let t' = App (reduce a, reduce b) in let t' = App (reduce a) (reduce b) in
+ if (is_redex t') then reduce (reduce_one_step t') if (is_redex t') then reduce (reduce_one_step t')
+ else t' else t'