diff --git a/Automata.hs b/Automata.hs index 35dacd3..e684a58 100644 --- a/Automata.hs +++ b/Automata.hs @@ -10,15 +10,6 @@ type F a = (,) Bool `O` ((->) a) -- Fixpoint, ie languages type Language a = Mu (F a) --- basic constructor -ctor :: Bool -> (a -> Language a) -> Language a -ctor b t = phi (O (b, t)) - --- For every (F a)-coalgebra x, there is a arrow x -> Language a --- and it is unique, so `Language a` is the final (F a)-coalgebra! -sem :: (Coalgebra (F a) x) => x -> Language a -sem s = ctor b (\w -> sem $ trans w) where O (b, trans) = psi s - -- auciliry function is_member :: [a] -> Language a -> Bool is_member [] l = b where O (b, _) = psi l @@ -49,7 +40,7 @@ instance Coalgebra (F A) X where -- Test a word against it -show_member word = putStrLn $ show (word, is_member word (sem One :: Language A)) +show_member word = putStrLn $ show (word, is_member word (semantics One :: Language A)) main = do let words = [[A], [A,B], [A,B,B], [A,B,B,A], [A,B,A,B,A]] diff --git a/Coalgebra.hs b/Coalgebra.hs index 9459d78..baee4da 100644 --- a/Coalgebra.hs +++ b/Coalgebra.hs @@ -21,3 +21,6 @@ instance Functor f => Algebra f (Mu f) where instance Functor f => Coalgebra f (Mu f) where psi (In x) = x + +semantics :: (Functor f, Coalgebra f x) => x -> (Mu f) +semantics x = phi (fmap semantics (psi x)) diff --git a/Streams.hs b/Streams.hs index 6833144..1ff3cf2 100644 --- a/Streams.hs +++ b/Streams.hs @@ -9,15 +9,6 @@ type F a = (,) a -- This will give the fixpoint, ie a coalgebra, because F is a functor type Stream a = Mu (F a) --- basic constructor -(+:+) :: a -> Stream a -> Stream a -(+:+) a s = phi (a, s) - --- For every (F a)-coalgebra x, there is a arrow x -> Stream a --- and it is unique, so `Stream a` is the final (F a)-coalgebra! -sem :: (Coalgebra (F a) x) => x -> Stream a -sem x = x0 +:+ sem x' where (x0, x') = psi x - -- auxilary functions toList :: Stream a -> [a] toList s = a0 : toList a' where (a0, a') = psi s @@ -32,4 +23,4 @@ instance Coalgebra (F Int) X where main :: IO () main = do - putStrLn $ show $ take 20 $ toList $ (sem One :: Stream Int) \ No newline at end of file + putStrLn $ show $ take 20 $ toList $ (semantics One :: Stream Int) \ No newline at end of file