Email Gateway (Aug 18 2022 at 13:16): Email Gateway (Aug 18 2022 at 13:16):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Scott West wrote:
This example, and others similar to it, are described in the paper by
Slind and Owens, available from
http://www.cs.utah.edu/~slind/papers/hosc.regexp/
Michael.
Email Gateway (Aug 18 2022 at 13:16):From: Alexander Krauss <krauss@in.tum.de>
Hi Scott,
This is nonterminating in general, unless the obj type is finite. So
there can't be just a simple "measure".
If your application does not require the functional view (like for code
generation), you best define all_children as an inductive set or
predicate, which avoids all termination issues and is usually much simpler.
You can define partial functions in Isabelle (see the function tutorial
for a small example), but this introduces explicit domain predicates and
in particular prevents code generation unless your function is
tail-recursive (this is how it is done in Stefan's formalization...)
But if you really just need all_children defined somehow, then just use
"inductive"
Alex
Email Gateway (Aug 18 2022 at 13:16):From: Stephan Merz <Stephan.Merz@loria.fr>
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:
Stephan_Merz.vcf
Email Gateway (Aug 18 2022 at 13:16):From: Konrad Slind <slind@cs.utah.edu>
The termination of a similar operation (depth-first traversal)
on a graph given by a function is discussed on pages 8-10
of
http://www.cs.utah.edu/~slind/papers/hosc.regexp/paper.pdf
It uses a lexicographic combination of measure functions.
Cheers,
Konrad.
Email Gateway (Aug 18 2022 at 13:28):From: Scott West <scott.west@inf.ethz.ch>
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
Email Gateway (Aug 18 2022 at 13:28):From: Stefan Berghofer <berghofe@in.tum.de>
Scott West wrote:
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
Email Gateway (Aug 18 2022 at 13:30):From: Scott West <scott.west@inf.ethz.ch>
Hello Alex,
Exactly! You will need to define a set "L" which contains all the nodes
that can be "seen". Instead of "measures" I would prefer the use of
"psubset" here.
I'll look at psubset, thanks!
But this is not the only problem you have here. Moreover the use of
"foldr" complicates the proof. When you start your termination proof,
you will notice, that there is no call of "foldr" anymore. Here the
"Higher Order Recursion"
(http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf, chapter 9)
comes into play. "foldr" is eliminated using the congruence rule
'foldr_cong' (from List.thy) I think. But this rule 'abstracts' over the
second argument (of f), so that you are not able state anything about it
(and you will need it to proof termination). Therefore you have probably
first to find the right congruence rule for 'foldr' that somehow
preserves the information, that the second argument of f is always a
subset of "L".
I read the functions.pdf that you pointed me to, however I still dont'
feel as if I know how the congruence mechanism works in practice. How
does it abstract' over the second argument of f' ?
If I do need to reformulate the foldr_cong rule to fit my needs, are
there any good examples of how these rules are applied during the proof,
so I can see what's going wrong?
Maybe it is a better idea to eliminate the use of foldr (if possible)
completely.
I do now have a version that I created without foldr that I can prove
termination. However eventually I will be doing things where foldr
becomes important (modeling imperative code, so the accumulated
parameter will be the state). So I guess I'm going down a more difficult
road ;).
Thanks again for the help!
Regards,
Scott
Email Gateway (Aug 18 2022 at 13:32):From: Alexander Schimpf <info@hitstec.de>
Dear Scott,
Scott West schrieb:
Hello Alex,
Exactly! You will need to define a set "L" which contains all the
nodes that can be "seen". Instead of "measures" I would prefer the
use of "psubset" here.
I'll look at psubset, thanks!
But this is not the only problem you have here. Moreover the use of
"foldr" complicates the proof. When you start your termination proof,
you will notice, that there is no call of "foldr" anymore. Here the
"Higher Order Recursion"
(http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf, chapter
9) comes into play. "foldr" is eliminated using the congruence rule
'foldr_cong' (from List.thy) I think. But this rule 'abstracts' over
the second argument (of f), so that you are not able state anything
about it (and you will need it to proof termination). Therefore you
have probably first to find the right congruence rule for 'foldr'
that somehow preserves the information, that the second argument of f
is always a subset of "L".I read the functions.pdf that you pointed me to, however I still dont'
feel as if I know how the congruence mechanism works in practice. How
does itabstract' over the second argument off' ?If I do need to reformulate the foldr_cong rule to fit my needs, are
there any good examples of how these rules are applied during the
proof, so I can see what's going wrong?
Well, I am not really sure if there are any. But I've created a small
example, that I think addresses your problem. Instead of using foldr
explicitly and to avoid the problems arise with congruence rules, I've
just used mutual recursion
(http://isabelle.in.tum.de/dist/Isabelle/doc/functions.pdf, Chapter 5)
to achieve the same behavior. In my example (see Test.thy) the function
'f' is similar to your 'all_children' function, the (abstract) function
'g' is somewhat similar to your 'children' function.
After the function definition is established and the completeness is
proofed, the termination proof is considered, which relies on the fact,
that there is an function called 'lim' which computes an upper bound for
'f' (and therefore for its second argument). So far, 'lim' is not really
defined in my example (that's up to you), but requires some properties
to be true (for example finiteness, etc.)
After that a special partial termination property (called 'subset_prop')
for the function 'f' and its mutual recursive counterpart 'foldr_f' is
proofed, since it is required in the termination proof. This property is
important and I don't think you can get a similar property when you use
'foldr' directly (but I've not verified that!)
At the end the termination proof is established using a special
termination ordering (called 'my_term_ord'), which is a lexicographical
combination of 'finite_psubset' and the 'less_than' relation. The latter
is needed since in my mutual recursive version the termination of the
foldr replacement have to also to be proofed.
Maybe it is a better idea to eliminate the use of foldr (if possible)
completely.
I do now have a version that I created without foldr that I can prove
termination. However eventually I will be doing things where foldr
becomes important (modeling imperative code, so the accumulated
parameter will be the state). So I guess I'm going down a more
difficult road ;).
Just try using the mutual recursive version that I've suggested in the
example. After finishing the termination it is probably possible to
proof, that the mutual recursive (helphing) funciton 'foldr_f' is in
fact (in some sense) equal to the ordinary 'foldr' function, so that it
can be replaced.
Thanks again for the help!
No problem, so far!
Regards,
Alex
Test.thy
Last updated: May 03 2024 at 08:18 UTC