I'm trying to implement Pushdown Automata (as described in Sipser's Introduction to the Theory of Computation) in Haskell. I have a working definition:
import Data.List
import Data.Maybe(fromMaybe)
-- A Pushdown Automaton with states of type q,
-- inputs of type s, and a stack of type g
data PDA q s g = P { state :: [q]
, start :: q
, delta :: [Rule q s g]
-- the transition function is list of relations
, final :: [q] -- list of accept states
}
-- rules are mappings from a (state, Maybe input, Maybe stack) to
-- a list of (state, Maybe stack)
-- Nothing represents the empty element ε
type Rule q s g = ((q, Maybe s, Maybe g), [(q, Maybe g)])
push :: Maybe a -> [a] -> [a]
push (Just x) xs = x:xs
push Nothing xs = xs
-- returns the popped element and the stack without that element
pop :: [a] -> (Maybe a, [a])
pop (x:xs) = (Just x, xs)
pop [] = (Nothing, [])
lookup' :: Eq a => a -> [(a, [b])] -> [b]
lookup' a xs = fromMaybe [] (lookup a xs)
-- calls deltaStar with the start state and an empty stack,
-- and checks if any of the resulting states are accept states
accepts :: (Eq q, Eq s, Eq g) => PDA g s q -> [s] -> Bool
accepts p xs = any ((`elem` final p). fst) $ deltaStar (start p) (delta p) xs []
deltaStar :: (Eq q, Eq s, Eq g)
=> q -- the current state
-> [Rule q s g] -- delta
-> [s] -- inputs
-> [g] -- the stack
-> [(q, Maybe g)]
deltaStar q rs (x:xs) st = nub . concat $
map (\(a, b) -> deltaStar a rs xs $ push b stack)
(lookup' (q, Just x, fst $ pop st) rs) ++
map (\(a, b) -> deltaStar a rs (x:xs) $ push b stack)
(lookup' (q, Nothing, fst $ pop st) rs) ++
map (\(a, b) -> deltaStar a rs xs $ push b st)
(lookup' (q, Just x, Nothing) rs) ++
map (\(a, b) -> deltaStar a rs (x:xs) $ push b st)
(lookup' (q, Nothing, Nothing) rs)
where stack = snd $ pop st
deltaStar q rs [] st = nub $ (q, Nothing)
: lookup' (q, Nothing, fst $ pop st) rs
++ lookup' (q, Nothing, Nothing) rs
Which gives me the expected results. However, looking at my deltaStar function, I can't help but feel there must be a more elegant way to write it. I manually check for Transitions that have ε in the input or stack, which I don't think I can get around, but this kind of Non-Determinism using concat and map looks like the List Monad to me. I would love to be able to write something like
deltaStar q rs (x:xs) st = do
(a, b) <- lookup' (q, Just x, fst $ pop st) rs
(c, d) <- lookup' (q, Nothing, fst $ pop st) rs
(e, f) <- lookup' (q, Just x, Nothing) rs
(g, h) <- lookup' (q, Nothing, Nothing) rs
concat [ deltaStar a rs xs $ push b stack
, deltaStar c rs (x:xs) $ push d stack
, deltaStar e rs xs $ push f st
, deltaStar g rs (x:xs) $ push h st]
where stack = snd $ pop st
deltaStar q rs [] st = nub $ (q, Nothing)
: lookup' (q, Nothing, fst $ pop st) rs
++ lookup' (q, Nothing, Nothing) rs
But that deltaStar will almost always return [], as when any of the pattern binds fail, the whole computation will return []. Is there a solution to this or should I stick to my definition?
I tested my original function with the language True^n False^n, defined as such:
langA :: PDA Int Bool Char
langA = P [1,2,3,4]
1
delta
[1,4]
where delta = [ ((1, Nothing, Nothing), [(2, Just '$')])
, ((2, Just False, Nothing),[(2, Just '0')])
, ((2, Just True, Just '0'), [(3, Nothing)])
, ((3, Just True, Just '0'), [(3, Nothing)])
, ((3, Nothing, Just '$'), [(4, Nothing)])]
Li-yao Xia's answer shows how to use more typeclass-polymorphic operations, but doesn't address the code duplication. In this answer I show how to address that. The main idea is this: there are just two things that vary, and they vary independently, namely whether we consume a letter and whether we consume from the stack. So let's nondeterministically choose for each!
(Warning: untested code follows.)
deltaStar q rs (x:xs) st = do
(stackSymbol, st') <- [pop st, (Nothing, st)]
(stringSymbol, xs') <- [(Just x, xs), (Nothing, x:xs)]
(a, b) <- lookup' (q, stringSymbol, stackSymbol) rs
deltaStar a rs xs' (push b st')