Email Gateway (Aug 18 2022 at 13:13): Email Gateway (Aug 18 2022 at 13:13):From: Christoph Feller <c_feller@informatik.uni-kl.de>
Hallo!
I have a loop in my simplifier rules and I try to get to the cause of
it. I set Isabelle to give me a simplifier trace and set the
simplifier depth to 5. Then I get a trace that leaves me confused
because I don't get what's going on. I give a reduced version of my
trace to keep it simple. C1 and C2 are constructors, f is a function.
[1] Applying instance of rewrite rule R1
(C1 ?s ?v) : X ==> f ?s ?v == f (C1 ?s ?v) ?v
[1] Trying to rewrite
(C1 (C2 s) v) : X ==> f (C2 s) v == f (C1 (C2 s) v) v
[2] SIMPLIFIER INVOKED ON THE FOLLOWING TERM
(C1 (C2 s) v) : X
[2] Applying instance of rewrite rule R2
(C1 ?s ?v) : X == False
[2] Rewriting
(C1 (C2 s) v) : X == False
[1] Succeeded
f (C2 s) v == f (C1 (C2 s) v) v
What I don't get is: Why does the rule R1 succeed even if it's premise
was simplified to False. Or is there something else going on? Did I
read it wrong?
Thanks in advance,
Christoph Feller
Email Gateway (Aug 18 2022 at 13:13):From: Tobias Nipkow <nipkow@in.tum.de>
I cannot reproduce this behaviour. I get the following:
[0]Adding rewrite rule "Scratch.R1":
C1 ?s1 ?v1 : X ==> f ?s1 ?v1 == f (C1 ?s1 ?v1) ?v1
[0]Adding rewrite rule "Scratch.R2":
C1 ?s1 ?v1 : X == False
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
P (f (C2 s) v)
[1]Applying instance of rewrite rule "Scratch.R1":
C1 ?s1 ?v1 : X ==> f ?s1 ?v1 == f (C1 ?s1 ?v1) ?v1
[1]Trying to rewrite:
C1 (C2 s) v : X ==> f (C2 s) v == f (C1 (C2 s) v) v
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
C1 (C2 s) v : X
[2]Applying instance of rewrite rule "Scratch.R2":
C1 ?s1 ?v1 : X == False
[2]Rewriting:
C1 (C2 s) v : X == False
[1]FAILED
C1 (C2 s) v : X ==> f (C2 s) v == f (C1 (C2 s) v) v
I suspect your subset of the trace does not show the correctly matching
Trying and Succeeded.
Tobias
Christoph Feller schrieb:
Email Gateway (Aug 18 2022 at 13:14):From: Christoph Feller <c_feller@informatik.uni-kl.de>
Hallo,
On Wed, Mar 25, 2009 at 13:23, Tobias Nipkow <nipkow@in.tum.de> wrote:
I cannot reproduce this behaviour. I get the following:
[...]
My concrete case is more complicate than the example so that isn't too
surprising.
I suspect your subset of the trace does not show the correctly matching
Trying and Succeeded.
I can't deny that but before my subset/-sequence I had an failed
attempt at a similiar rule like R1 (where the assumption wasn't
reducible to False) and I didn't leave anything out. Perhaps there is
some output from Isabelle missing here?
I solved the problem as I noticed that I really want a more general form of R1:
(C1 ?s ?v) : X ==> f ?s ?w == f (C1 ?s ?v) ?w
(So the parameter of the function doesn't have to be the same as the
parameter of the constructor.)
Now it's nice that it works but I have no idea why. And while it isn't
really urgent an explanation of that trace would be appreciated as it
could give some insight into the simplifier and what can lead to loops
there.
Tobias
[...]
Christoph Feller
Last updated: May 03 2024 at 08:18 UTC