Added Automata :D
This commit is contained in:
parent
b26e5d4b5b
commit
b5e9aca237
3 changed files with 67 additions and 10 deletions
56
Automata.hs
Normal file
56
Automata.hs
Normal file
|
@ -0,0 +1,56 @@
|
|||
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeOperators, ScopedTypeVariables, OverlappingInstances #-}
|
||||
|
||||
import Control.Monad.Instances
|
||||
import Control.Compose
|
||||
import Coalgebra
|
||||
|
||||
-- F X = 2 x X^A, for some fixed alphabet A
|
||||
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
|
||||
is_member (a:r) l = is_member r (trans a) where O (_, trans) = psi l
|
||||
|
||||
|
||||
|
||||
-- Our alphabet
|
||||
data A = A | B
|
||||
deriving Show
|
||||
|
||||
-- Our example automaton, we will look at its language given by sem
|
||||
data X = One | Two | Three
|
||||
trans :: X -> A -> X
|
||||
trans One A = Two
|
||||
trans One B = Three
|
||||
trans Two A = Three
|
||||
trans Two B = One
|
||||
trans Three _ = Three
|
||||
|
||||
fin :: X -> Bool
|
||||
fin One = True;
|
||||
fin Two = True;
|
||||
fin _ = False;
|
||||
|
||||
instance Coalgebra (F A) X where
|
||||
psi x = O (fin x, trans x)
|
||||
|
||||
|
||||
-- Test a word against it
|
||||
show_member word = putStrLn $ show (word, is_member word (sem One :: Language A))
|
||||
|
||||
main = do
|
||||
let words = [[A], [A,B], [A,B,B], [A,B,B,A], [A,B,A,B,A]]
|
||||
sequence $ map show_member words
|
10
Coalgebra.hs
10
Coalgebra.hs
|
@ -1,13 +1,13 @@
|
|||
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
|
||||
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}
|
||||
module Coalgebra where
|
||||
|
||||
import Control.Monad
|
||||
import Control.Monad.Instances
|
||||
|
||||
-- Definitions for (co)algebras
|
||||
class Functor f => Algebra f m where
|
||||
-- Definitions for (co)algebras, adding fundeps helped in the Automata case...
|
||||
class Functor f => Algebra f m | m -> f where
|
||||
phi :: f m -> m
|
||||
|
||||
class Functor f => Coalgebra f m where
|
||||
class Functor f => Coalgebra f m | m -> f where
|
||||
psi :: m -> f m
|
||||
|
||||
-- Fixpoint, ie f (Mu f) = Mu f
|
||||
|
|
11
Streams.hs
11
Streams.hs
|
@ -3,16 +3,17 @@
|
|||
import Control.Monad.Instances
|
||||
import Coalgebra
|
||||
|
||||
-- F X = A x X, for a fixed A, The prelude already provides the functor instance :)
|
||||
-- F X = A x X, for a fixed A, this has a functor instance
|
||||
type F a = (,) a
|
||||
|
||||
-- This will give the fixpoint, ie a coalgebra.
|
||||
-- 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 = In (a, s)
|
||||
(+:+) a s = phi (a, s)
|
||||
|
||||
-- For every other (F a)-coalgebra x, there is a arrow x -> Stream a
|
||||
-- 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
|
||||
|
@ -22,7 +23,7 @@ toList :: Stream a -> [a]
|
|||
toList s = a0 : toList a' where (a0, a') = psi s
|
||||
|
||||
|
||||
-- example, with a very simple (F Int)-coalgebra, 1 -> 2, 2 -> 3, 3 -> 2
|
||||
-- example with a very simple (F Int)-coalgebra, 1 -> 2, 2 -> 3, 3 -> 2
|
||||
data X = One | Two | Three
|
||||
instance Coalgebra (F Int) X where
|
||||
psi One = (1, Two)
|
||||
|
|
Reference in a new issue