Email Gateway (Aug 22 2022 at 13:34): Email Gateway (Aug 22 2022 at 13:34):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I've been playing around with normalisation of monad expressions and
have run into a few problems.
First of all, one thing I noticed is that the simplifier sometimes fails
to apply permutative rules when I thought it should, e.g. minimal example:
typedecl a
typedecl b
typedecl c
typedecl d
axiomatization
a :: "(a ⇒ a ⇒ c) ⇒ d" and
b :: "b ⇒ b ⇒ c" and
c :: "a ⇒ a ⇒ b"
where
a_commute: "a (λx y. b (f x y) (g x y)) ≡ a (λx y. b (g x y) (f x y))"
ML_val ‹
let
val ctxt = @{context} addsimps @{thms a_commute}
val ct = @{cterm "a (λx y. b (c x y) (c y x))"}
val ct' = @{cterm "a (λy x. b (c x y) (c y x))"}
in
(ct,ct') |> apply2 (Raw_Simplifier.rewrite_cterm
(false,false,false) (K (K NONE)) ctxt)
end
›
I would have expected the simplifier to rewrite one of these terms to
the other – but it doesn't do anything for either of them. After adding
some tracing code, I believe that the reason is that the simplifier does
not β-normalise terms before comparing them. Is this the intended behaviour?
In any case, for monad normalisation, the simplifier's idea of what
constitutes a permutative rule is too restrictive in any case, so I set
up a "TERM_ORD" dummy constant similar to the "NO_MATCH" and
"ASSUMPTION" constants. "TERM_ORD a b" gets rewritten to "True" by a
simproc iff the first argument is strictly smaller than the second.
(cong rules ensure that TERM_ORD's arguments do not get simplified
themselves) For the reasons outlined above, it also performs
β-η-reduction before comparing the terms.
This works very well in most cases, but I found one pathological example
of the form
t := bind A (λx. bind A (λy. bind (B x y) (λ_. bind (B y x) (λ_. e))))
The commutativity rule for bind, which is
bind A (λx. bind B (λy. C x y)) = bind B (λy. bind A (λx. C x y)) ,
can be applied either to the whole of t (flipping the first two binds)
or to the third bind (flipping the 3rd and 4th bind). In both cases, we
get the term
t' := bind A (λx. bind A (λy. bind (B y x) (λ_. bind (B x y) (λ_. e))))
The problem is now that when flipping the first two binds, the arguments
of B are "Bound 1" and "Bound 0". However, when flipping the last two
binds, they are "Free ":001"" and "Free ":002"" because the simplifier
instantiates bound variables to free variables like this when passing an
abstraction. This exactly reverses the term order, since the Bounds are
counted inside-out and the Frees are counted outside-in. This means that
"TERM_ORD" will be rewritten to "True" in both cases and we get an
infinite rewriting cycle.
What is the best way to solve this problem? Can the simplifier ever run
into a problem like this or is that prevented by the fact that it
doesn't do β normalisation?
The most robust way would probably be to replace the Free variables with
(dangling) bound variables before performing the term order comparison,
but I don't think the necessary information is publicly available in the
context.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 13:34):From: Tobias Nipkow <nipkow@in.tum.de>
The fact that the simplifier does not β-normalise terms before comparing them is
possibly a combination of the fact that I never expected it to be used in such
situations and the potential cost of the normalisation. I suspect it would break
too many proofs if we changed that behaviour, although I would of course make
sense from a logical point of view.
Tobias
smime.p7s
Last updated: Apr 20 2024 at 12:26 UTC