[isabelle] Non-terminating function domain qualifier
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?
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)
This archive was generated by a fusion of
Pipermail (Mailman edition) and