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

The termination of a similar operation (depth-first traversal)
on a graph given by a function is discussed on pages 8-10

It uses a lexicographic combination of measure functions.


On Apr 27, 2009, at 6:51 AM, 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.


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