Improvements to the termination checker #115
Conversation
(but not timeout)
…mytests/Termination2.scala
but do it in sizeDecreasing, because DRY, and because it provides more flexibility for other potential implementations of sizeDecreasing
1) The termination checker (of which only 1 instance exists per run) 2) The modules which depend on a size function (of which several instances per run might exist, one per size function impl)
counting from 31 down to 0 instead of from 0 up to 31
the TerminationRegression test checks if counterexamples are found
| )) | ||
|
|
||
| if (s1.length > s2.length || (s1.length == s2.length && !strict)) { | ||
| or(andJoin(sameSizeExprs), greaterBecauseGreaterAtFirstDifferentPos) |
There was a problem hiding this comment.
Awesome work!
I'm not sure I understand the argument here about strict decreasing when s1.length > s2.length. I do believe this works for the relation processor because we are guaranteed that greaterBecauseGreaterAtFirstDifferentPos will be proved for some call but if we wanted to use lexicographicDecreasing outside of this processor (eg. in the chain processor) we could run afoul of this assumption. Does this optimization actually help for any the current examples?
Other than this minor gripe, I think we're pretty much good to merge! :)
There was a problem hiding this comment.
The reason I included this s1.length > s2.length is that the strict decreasing order and the weak decreasing order should be compatible in the sense that forall x y, x > y <==> ! y >= x. Or in other words, forall x y, x > y XOR y >= x.
Now for x = (a, b, c, plus, some, stuff) and y = (a, b, c), y >= x does not hold, so x > y should hold, but that's only the case if we have this s1.length > s2.length condition.
Note, though, that having compatible > and >= is not absolutely necessary for the termination checker to work correctly. If we removed the s1.length > s2.length condition, the > relation would become a slightly smaller set, but I think all the examples would still work.
Nevertheless, I'd like to keep the s1.length > s2.length condition, because if you claim to implement a strict and weak lexicographic order, people will expect them to be compatible, and if later this is used somewhere else where it's required that they're compatible but they're not, it might lead to bad surprises.
There was a problem hiding this comment.
Ah, I see. I guess that the fact that we have finite argument list sizes means this actually is a strict decreasing metric. We can merge once you've rebased.
On a completely unrelated subject, I'm surprised that reverse_reverse_equivalence doesn't go through. Shouldn't the automatically generated size invariant on reverse be sufficient for termination without the extra witness parameter?
There was a problem hiding this comment.
Yes, having finite argument list lengths is crucial, because it's needed for the lexicographic order to be well-founded. Otherwise we could have infinite decreasing chains like b > ab > aab > aaab ...
Regarding reverse_reverse_equivalence, I also was a bit surprised that it didn't work, but I don't understand the Strengthener well enough in order to debug it...
|
Rebased version is at https://github.com/samuelgruetter/leon/tree/termination6. |
|
Merged |
Summary of changes:
abs(x)for BigInt instead of zeroRelationComparatorcan use different size functions--verify --terminationoptions are given together, verification and termination checking is performed in one runThe termination checker now succeeds on all regression tests, including those for verification.
regression/verification/purescala/valid/Monads3.scalaassociative_lemma_inductdoes lexicographic induction on its first three argumentsregression/verification/purescala/valid/FlatMap.scalaregression/verification/purescala/valid/ParBalance.scalareverse_reverse_equivalence(s: BigInt, list: List)always decreases on s, but we cannot prove what happens withlist(because it's reversed), so the lexicographic measure helps, because it allows us to ignore the second argumentregression/verification/purescala/valid/MergeSort.scalaParBalance, but withdef weirdSort(s : BigInt, in : List)regression/verification/purescala/valid/Nat.scalaregression/verification/purescala/valid/BitsTricks.scalaregression/termination/valid/CountTowardsZero.scalaregression/termination/looping/OddEven.scalaSelfCallsProcessorregression/termination/looping/WrongFibonacci.scalaNote: The path of the testcases refer to the testcases as they are in this PR, not as they are on master.