Re: [isabelle] Simplifier and term order



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

On 08/06/2016 08:38, Manuel Eberl wrote:
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







Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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