Re: [isabelle] Termination Proof ``fun'' ;)



Basically you'll have to take the complement of your set "seen" with respect to the set of reachable nodes (i.e., the transitive closure of the children function from the node "src"). And yes, you'll have to prove that transitive closure to be a finite set, otherwise the function wouldn't terminate.

We have recently formalized a very similar function in the context of an automaton construction for model checking, and I could send you the theories and a paper (off-list) if you are interested.

Regards,
Stephan

Scott West wrote:
Hello all,

I have recently been trying to write a function, which Isabelle would like to know terminates. The basic task is to find reachability, but I don't have an explicit graph, I have a function which returns children of the current node.

So I recursively define this function to essentially be something like:

all_children :: obj => obj set => obj set
all_children src seen =
  if src \<in> seen
    then seen
    else
      foldr all_children (children src) (seen \<union> {src})

I can't for the life of me figure out what the measure function should be in this case. Been thinking on it for a few days and I don't know how to state a termination proof in a way that Isabelle will understand. I should preface that by saying I only know of the "measure" method... and even then, not really well.

If anyone could provide some hint on how to go about this, then that would be great.

Regards,
Scott

begin:vcard
fn:Stephan Merz
n:Merz;Stephan
org:INRIA Nancy & LORIA
adr;quoted-printable:;;615 rue du Jardin Botanique;Villers-l=C3=A8s-Nancy;;54602;France
email;internet:Stephan.Merz at loria.fr
tel;work:(+33) 354 95 84 78
tel;fax:(+33) 383 41 30 79
x-mozilla-html:FALSE
url:http://www.loria.fr/~merz/
version:2.1
end:vcard



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