|
|
@ -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]] |
|
|
|