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

Regards,
Tjark






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.