Automata theory, state reachability in Haskell

Question

I wrote a small library to learn Haskell while studying Automata theory. I have some concerns on my algorithm to evaluate state reachability. That is, I think it might be improved if I can avoid checking paths already excluded in other branches of the search for a valid path. This one recursively checks each path separately.

I hope I didn't forget anything. Other suggestions are obviously welcome!

Automaton data type

-- | Represents an automaton in the form
--   /G = (X, E, f, Gamma, x_0, X_m)/
--
--   NB: we're not including Gamma in the definition of Automaton
data Automa st ev = Automa {
    states     :: [st],             -- ^ /X/, set of states
    events     :: [ev],             -- ^ /E/, set of events
    mapTrans   :: M.Map (st,ev) st, -- ^ not /f/, but a map of
                                    --   transitions (see 'trans')
    initial    :: st,               -- ^ /x_0/, initial state
    marked     :: [st]              -- ^ /X_m/, set of marked states
} deriving (Show, Read)

Reachability function

-- | True if a state can reach another for some string of events.
canReach :: (Ord st, Ord ev)
    => st                   -- ^ starting state 's'
    -> st                   -- ^ arrival state 's''
    -> Automa st ev
    -> Bool
canReach s s' au = canReachExcluding s s' au []

-- | True if a state can reach another for some string of events,
--   excluding passing from specified states.
canReachExcluding :: (Ord st, Ord ev)
    => st                   -- ^ starting state 's'
    -> st                   -- ^ arrival state 's''
    -> Automa st ev
    -> [st]                 -- ^ the states to be excluded
    -> Bool
canReachExcluding s s' au ex = s == s' || any (== s') rs
    || any (\x -> canReachExcluding x s' au (s:ex)) rs
        where rs = reach1From s au \\ ex

-- | Returns states reachable from specified state in one step.
reach1From :: (Ord st, Ord ev) => st -> Automa st ev -> [st]
reach1From s au = [ trans' (s,e) au | e <- gammaL s au ]

Accessory functions

-- | Indicator function of active states for an automaton
gamma :: (Ord st, Ord ev)
    => (st,ev)                 -- ^ state-event pair of interest
    -> Automa st ev
    -> Bool                    -- ^ 'True' if 'ev' is active for 'st'
gamma (s,e) au = M.member (s,e) $ mapTrans au

-- | Returns a list of active events for a state of a given 'Automa'
gammaL :: (Ord st, Ord ev) => st -> Automa st ev -> [ev]
gammaL s au = [ e | e <- events au, gamma (s,e) au ]

-- | Transition function: where do I get if 'ev' happens when in 'st'?
trans :: (Ord st, Ord ev) => (st, ev) -> Automa st ev -> Maybe st
trans (s,e) au = M.lookup (s,e) $ mapTrans au

-- | Like 'trans', but to be used if you're sure it's a valid
--   transition (i.e. saves you a 'fromJust').
trans' :: (Ord st, Ord ev) => (st, ev) -> Automa st ev -> st
trans' (s,e) au = fromJust $ M.lookup (s,e) $ mapTrans au

Answer 1

This is neat, methinks.

A couple of questions/points:

1. Is the || any (== s') rs part of canReachExcluding necessary?
2. In the same definition, the part rs = reach1From s au \\ ex takes time linear in the size of ex. Using a set (or hash) instead of a list for ex would probably improve your running time significantly in practice. But of course, that'd likely be at the expense of the clarity of your beautiful program.
3. You are of course right that your program checks "states excluded in other branches". What you are "really" implementing is depth-first search (DFS) on the graph defined by the automaton, and so you might want to look for a more efficient (functional) implementation of DFS. In that case, you could either look at the Haskell Library implementation, or maybe just this quick-and-dirty approach.