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



Scott West wrote:
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.

Hello Scott,

when defining the above function with "fun", you also have to supply
a suitable congruence rule for foldr in order to be able to prove
termination. However, it might actually be easier to define all_children
without using foldr, i.e. by turning the first parameter into a list
of objects that still have to be inspected:

  all_children :: obj list => obj set => obj set
  all_children [] seen = seen
  all_children (src # srcs) seen =
    if src \<in> seen
      then all_children srcs seen
      else
        all_children (children src @ srcs) (seen \<union> {src})

This approach is used in the formalization of depth first search
by Nishihara an Minamide, which you can find in the AFP:

  http://afp.sourceforge.net/entries/Depth-First-Search.shtml

I recently generalized this formalization a little (using locales),
allowing the user to freely choose the representation of "obj set",
as well as the implementation of the children, \<union>, and \<in>
operators. You can currently find the generalized version at

  http://www.in.tum.de/~berghofe/papers/automata/DFS.thy

For examples of how to apply this version of DFS, see

  http://www.in.tum.de/~berghofe/papers/automata/Automata.thy

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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