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.


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


fn:Stephan Merz
org:INRIA Nancy & LORIA
adr;quoted-printable:;;615 rue du Jardin Botanique;Villers-l=C3=A8s-Nancy;;54602;France
email;internet:Stephan.Merz at
tel;work:(+33) 354 95 84 78
tel;fax:(+33) 383 41 30 79

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