*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Simplifier and term order*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 9 Jun 2016 08:11:41 +0200*In-reply-to*: <9d9ecdcf-a2a5-8af5-fe5f-e8a5bb3d6507@in.tum.de>*References*: <9d9ecdcf-a2a5-8af5-fe5f-e8a5bb3d6507@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.1.1

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**

**References**:**[isabelle] Simplifier and term order***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Fwd: Executing 2 Isabelle-2016 or even 2 Jedit processes on Windows
- Next by Date: [isabelle] New AFP entry: Word_Lib
- Previous by Thread: [isabelle] Simplifier and term order
- Next by Thread: [isabelle] New AFP entry: Word_Lib
- Cl-isabelle-users June 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list