# [isabelle] Simplifier and term order

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

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