*To*: Peter Lammich <peter.lammich at uni-muenster.de>*Subject*: Re: [isabelle] Term rewriting systems*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 11 Sep 2008 19:32:32 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <48C92814.3030704@uni-muenster.de>*References*: <48C92814.3030704@uni-muenster.de>*User-agent*: Thunderbird 2.0.0.16 (Macintosh/20080707)

I am not aware of any support for confluence proofs other than abstract relation-algebraic theorems. Have you proved confluence by hand yet? By some standard method, like absence of critical pairs? If not, do that first, by reducing it to some standard variety of rewrite system. As you correctly note, list patterns of the form xs @ [t] @ ys could be a problem. Either you have to do rewriting modulo associativity of @ or add associativity of @ in both dirctions as a rewrite rule, which loses termination but may preserve confluence. Tobias Peter Lammich schrieb: > Hi all, > > I wonder whether there is any tool support (best Isabelle compatible > tool support) to reason about term rewriting systems of the following form: > > I have a term rewriting system defined over terms of the form: > > datatype 'm action = ENTER "'m" | LEAVE "'m" | USE "'m set" > datatype 'm tree = NIL | NODE "'m action" "'m tree list" "'m tree" > > the rules are like this: > > 1) NODE (ENTER m) c1 (NODE (LEAVE m) c2 > t) -> NODE (USE m) (c1 at c2) t > 2) NODE (ENTER m) c1 (NODE (USE m') c2 (NODE (LEAVE m) c3 t)) > -> NODE (USE (m\<union>m')) (c1 at c2@c3) t > 3) NODE (USE u1) c1 (NODE (USE u2) c2 t) > -> NODE (USE (u1\<union>u2)) (c1 at c2) t > 4) NODE (USE u) (c1 at NIL#c2) t > -> NODE (USE u) (c1 at c2) t > 5) NODE (USE u) (c1@(NODE (USE u1) cs1 ts1)@c2@(NODE (USE u2) cs2 > ts2)@c3) t -> NODE (USE u) (c1@(NODE (USE (u1\<union>u2)) cs1 > ts1)#c2 at cs2@ts2#c3) t > 6) NODE (USE u1) (c1@(NODE (USE u2) cs ts)#c2) NIL -> > NODE (USE (u1\<union>u2)) (c1 at cs@ts#c2) > > My rewriting strategy is rewriting of an arbitrary subterm. Currently I > define an inductive predicate step ("->") by the rules 1-6 and > additionally the inductive rules: > 7) t -> t' ==> NODE a c t -> NODE a c t' > 8) t -> t' ==> NODE a (c1 at t#c2) x -> NODE a (c1 at t'#c2) x > > I want to show termination and confluence of this system. Termination is > easy, as the size of the tree decreases in any step, hence I easily get > lemma "wfP (step^--)" > > By Newman's lemma (A version is in HOL/Lambda/Commutation.thy), it > suffices to show local confluence, I even think my system above has the > diamond property. > > Is there any standard approach to term rewriting systems in Isabelle or > are there some other tools out there, to show confluence (and > termination) as automatic as possible? > Are there any suggestions on how to show local confluence of such a > system in Isabelle (as automatic as possible)? > > The main problem seems to be the non-constructor patterns (like c1 at t#c2) > I use in my rewriting rules (4,5,6,8) > > Thanks for any suggestions/comments in advance, best > Peter > > > > >

**References**:**[isabelle] Term rewriting systems***From:*Peter Lammich

- Previous by Date: [isabelle] Term rewriting systems
- Next by Date: [isabelle] Final Call for Participation: VSTTE'08
- Previous by Thread: [isabelle] Term rewriting systems
- Next by Thread: Re: [isabelle] Term rewriting systems
- Cl-isabelle-users September 2008 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