Email Gateway (Aug 18 2022 at 13:29): Email Gateway (Aug 18 2022 at 13:29):From: Chris Capel <pdf23ds@gmail.com>
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. So I do not try to prove termination, which leaves me
with a domain qualifier on everything,
parse_len_dom (grammar, input) --> parse_len grammar, input = x
What I'm wondering is if it's possible, for a specific grammar and
input that I know will terminate, to prove "parse_len g, inp = n":
without the qualifier. Or is it required to prove termination in the
general case to ever get rid of that qualifier?
Chris Capel
Email Gateway (Aug 18 2022 at 13:30):From: Alexander Krauss <krauss@in.tum.de>
forgot to cc my answer to the list
Email Gateway (Aug 18 2022 at 13:30):From: Tjark Weber <webertj@in.tum.de>
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
Email Gateway (Aug 18 2022 at 13:30):From: Chris Capel <pdf23ds@gmail.com>
Out of curiosity, how is is accp defined in Wellfounded.thy? It
doesn't seem to be explicit. My best guess is that "inductive_set x"
defines "xp" as a predicate. (This does seem to be the case.) But this
behavior appears not to be documented in the Isar reference manual.
Chris Capel
Last updated: May 03 2024 at 12:27 UTC