Automata theory, state reachability in Haskell

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

This is neat, methinks.

A couple of questions/points:

• Is the || any (== s') rs part of canReachExcluding necessary?

• 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.

• 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.

StackExchange Code Review Q#32266, answer score: 2