Email Gateway (Aug 22 2022 at 18:52): Email Gateway (Aug 22 2022 at 18:52):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I have a set of 6 mutually recursive functions and the attempt to prove
termination with lexicographic order is not returning even after 30
minutes. If I reduce it back to 5 functions then it does (but not
immediately; it takes about 10 minutes).
Is there any tracing available for me to see what is happening or a timeout
that I can set that will result in the matrix (possibly incomplete) being
shown?
I could use the order it finds with the 5-function termination proof and
attempt to extend it to include the sixth one but the order is a product of
four measures built out of <mlex> and case_sum, and it is tricky keeping
track of things and could be brittle when adding additional functions or
recursive calls.
Cheers
Mark
Email Gateway (Aug 22 2022 at 18:52):From: Alexander Krauss <krauss@in.tum.de>
Hi Mark,
I have a set of 6 mutually recursive functions and the attempt to prove
termination with lexicographic order is not returning even after 30
minutes. If I reduce it back to 5 functions then it does (but not
immediately; it takes about 10 minutes).
The lexcographic_order method enumerates a set of possible candidates
for measure functions. Unfortunately, if you have n mutually recursive
functions with k arguments each, then there are ~ k^n candidates, which
will lead to ~ k^2n proof obligations being tried. This probably
explains what you are seeing.
I don't think there is any tracing that would help you here.
Here are some options you might try:
Try the "size_change" method. It deals differently with mutual
recursion, and IIRC it does not have the blowup problem. There may be
other issues, but it is worth a try.
Come up with the termination argument yourself. Often, this is not so
hard even for complicated definitions.
Simplify the definition (possibly deriving the original form afterwards).
I could use the order it finds with the 5-function termination proof and
attempt to extend it to include the sixth one but the order is a product of
four measures built out of <mlex> and case_sum, and it is tricky keeping
track of things and could be brittle when adding additional functions or
recursive calls.
This sounds brittle indeed. Another way of making it more robust (though
quite verbose) would be to define 6 (mutually recursive) measure
functions, and using them for the termination argument. Then at least it
is clear how to extend it later...
Hope this helps (a bit)
Alex
Last updated: Apr 19 2024 at 20:15 UTC