Re: [isabelle] Non-terminating function domain qualifier
On Thu, 2009-05-14 at 17:36 -0500, Chris Capel wrote:
> I'm trying to model a context-free grammar in Isabelle. AFAIK, a
> generic function that parses input according to a CFG cannot be proved
> to terminate.
I may be stating the obvious and/or missing your point, but the
membership problem for context-free languages is of course decidable
(see, e.g., http://en.wikipedia.org/wiki/CYK_algorithm).
This archive was generated by a fusion of
Pipermail (Mailman edition) and