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


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