Parsing with Proof
Hi everyone on haskell-cafe, I am wondering about how to give a correctness prove of a simple parsing algorithm. I tried to think of a simple example but even in this case I don't know how. I have an abstract syntax:
data Parens = Empty | Wrap Parens | Append Parens Parens
assumption (A), in Append x y, x and y are never Empty assumption (B), Strings only contain '(' and ')' characters and a printing function
print :: Parens -> String print Empty = "" print (Wrap m) = "(" ++ print m ++ ")" print (Append x y) = print x ++ print y
So the idea is that I would like to write parse :: String -> Maybe Parens, such that if it gives Nothing then the String was malformed, if it gives Just x then the string should be equal to print x. I think I can write such a function in a few different ways, but I don't know how to prove this code works, could anybody show me how? Thank you for any replies. -- View this message in context: http://www.nabble.com/Parsing-with-Proof-tp22814576p22814576.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
Hi muad, muad wrote:
I think I can write such a function in a few different ways, but I don't know how to prove this code works, could anybody show me how?
Why don't you pick a specific implementation first and share it with us? The proof heavily depends on the precise implementation. Kind regards, Martijn.
I am wondering about how to give a correctness prove of a simple parsing algorithm. I tried to think of a simple example but even in this case I don't know how.
I'm not sure I understand your question, but I'm guessing you're looking for general techniques for the formal verification of combinator-based parsers. Here's a quick brain dump of related work that might help you get started. Nils Anders Danielsson wrote a verified regexp matcher in Agda a while ago. http://www.cs.chalmers.se/~ulfn/darcs/Agda2/examples/AIM6/RegExp/ Although this isn't quite parsing, the ideas are relatively simple so it's a good place to start. (Bob Harper has a theoretical pearl on the topic, which might be worth checking out to get some inspiration). More recently, Nils Anders has extended this to parser combinators together with Ulf Norell: http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-parser-combinat... Alternatively, you could explore how to implement similar ideas in Coq. I'm a big Program fan and recently used it to verify some simple programs in the state monad. I've just submitted a paper about this: http://www.cse.chalmers.se/~wouter/Publications/HoareStateMonad.pdf I'd imagine you might be able to take a similar approach to applicative (or monadic) parser combinators. Doaitse Swierstra recently wrote a good overview tutorial about parser combinators in general that is certainly worth checking out: http://www.cs.uu.nl/research/techreps/repo/CS-2008/2008-044.pdf Hope this helps, Wouter
Hi Martijn and Wouter, Based on the parser combinators paper, I put a monad together,
data Parser s t = Parser ([s] -> [(t, [s])])
pFail = Parser (const []) pReturn a = Parser (\inp -> [(a, inp)]) pSymbol s = Parser (\inp -> case inp of x:xs | x == s -> [(s,xs)] ; _ -> []) pChoice (Parser m) (Parser n) = Parser (\inp -> m inp ++ n inp) pBind :: Parser s a -> (a -> Parser s b) -> Parser s b pBind (Parser m) f = Parser (x m f) where x :: ([s] -> [(a, [s])]) -> (a -> Parser s b) -> [s] -> [(b, [s])] x m f inp = concatMap (y f) (m inp) y f (a,s) = case f a of Parser g -> g s
instance Monad (Parser s) where return = pReturn ; (>>=) = pBind instance MonadPlus (Parser s) where mzero = pFail ; mplus = pChoice
runParser (Parser f) inp = f inp
and wrote the parser using that:
left = pSymbol '(' right = pSymbol ')'
parens = wrappend `mplus` empty where empty = return Empty wrappend = do left ; p <- parens ; right ; q <- parens ; return (Wrap p & q) where m & Empty = m m & n = Append m n
I really like the approach Wouter used for the State monad and I hope to follow that idea for this, I am not sure how to do it yet but I will scribble and see where it goes. Thanks very much for the advice! -- View this message in context: http://www.nabble.com/Parsing-with-Proof-tp22814576p22835016.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.
participants (3)
-
Martijn van Steenbergen -
muad -
Wouter Swierstra