[isabelle] [Fwd: Re: Non-terminating function domain qualifier]



forgot to cc my answer to the list

-------- Original Message --------
Subject: Re: [isabelle] Non-terminating function domain qualifier
Date: Fri, 15 May 2009 09:49:46 +0200
From: Alexander Krauss <krauss at in.tum.de>
To: Chris Capel <pdf23ds at gmail.com>

Hi Chris,

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?

You can prove termination for some subset by showing that some property
of the input implies parse_len_dom. Note that f_dom is currently just an
abbreviation for "accp parse_len_rel" which is itself defined
inductively as the call relation of your function.

Alex






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