Email Gateway (Aug 22 2022 at 10:58): Email Gateway (Aug 22 2022 at 10:58):From: Lars Hupel <hupel@in.tum.de>
Dear list,
I have a general question about how to avoid simplifier loops which might
occur in the function package under somewhat non-trivial circumstances.
Here's an example:
fun apply'2 where
"apply'2 thiss'500 index'10 =
(if 0 <= index'10 & index'10 < length thiss'500 then
if index'10 = 0 then hd thiss'500 else apply'2 (tl thiss'500)
(index'10 - 1)
else undefined)"
fun reverseIndex'0 where
"reverseIndex'0 l'5 i'3 =
((case l'5 of x'14 # xs'18 => reverseIndex'0 l'5 i'3) /\
apply'2 (rev l'5) i'3 = apply'2 l'5 (length l'5 - 1 - i'3))"
The simplifier will loop during the proofs for the internal construction
of "reverseIndex'0". While looping, I get the following in the output
panel, repeated many times:
linarith_split_limit exceeded (current value is 9)
I'm pretty sure the culprit is the defining equation of "apply'2", because
marking it with "[simp del]" will lead the function package to complain
about non-termination in "reverseIndex'0" instead.
On the other hand, I've seen similar definitions (recursive specifications
without pattern matching on the left-hand side, let me call them
"potentially loopy") which looked like they could give rise to looping go
through without problems. I'm not exactly sure what the side conditions
are.
Anyway, my question is a bit broader: Do you have any suggestion of how I
can avoid these situations in general? I'm a happy user of "simps_of_case"
which can translate potentially loopy equations into non-loopy ones.
However, this only works when the equations use case expressions on their
right-hand sides, but not for "if" expressions. Any general advice?
(I should add once more that the specifications I process are
automatically generated.)
Cheers
Lars
Email Gateway (Aug 22 2022 at 10:58):From: Lars Noschinski <noschinl@in.tum.de>
These simp-rules lead to non-termination if the simplifier cannot solve
the condition. The reason is that if a term of this form cannot be
simplified any further, the simplifier applies the splitter with
split_if, yielding to subgoals on which this equation can be applied.
-- Lars
Last updated: Apr 25 2024 at 08:20 UTC