[isabelle] Simplifier and term order


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

  a :: "(a â a â c) â d" and
  b :: "b â b â c" and
  c :: "a â a â b"
    a_commute: "a (Îx y. b (f x y) (g x y)) â a (Îx y. b (g x y) (f x y))"

ML_val â
    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))"}
(ct,ct') |> apply2 (Raw_Simplifier.rewrite_cterm (false,false,false) (K (K NONE)) ctxt)

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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.