Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Term rewriting systems

view this post on Zulip Email Gateway (Aug 18 2022 at 12:22):

From: Peter Lammich <peter.lammich@uni-muenster.de>
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@c2) t
2) NODE (ENTER m) c1 (NODE (USE m') c2 (NODE (LEAVE m) c3 t))
-> NODE (USE (m\<union>m')) (c1@c2@c3) t
3) NODE (USE u1) c1 (NODE (USE u2) c2 t)
-> NODE (USE (u1\<union>u2)) (c1@c2) t
4) NODE (USE u) (c1@NIL#c2) t
-> NODE (USE u) (c1@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@cs2@ts2#c3) t
6) NODE (USE u1) (c1@(NODE (USE u2) cs ts)#c2) NIL ->
NODE (USE (u1\<union>u2)) (c1@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@t#c2) x -> NODE a (c1@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@t#c2)
I use in my rewriting rules (4,5,6,8)

Thanks for any suggestions/comments in advance, best
Peter

view this post on Zulip Email Gateway (Aug 18 2022 at 12:22):

From: Tobias Nipkow <nipkow@in.tum.de>
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:

view this post on Zulip Email Gateway (Aug 18 2022 at 12:22):

From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Peter Lammich wrote:

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@c2) t
2) NODE (ENTER m) c1 (NODE (USE m') c2 (NODE (LEAVE m) c3 t))
-> NODE (USE (m\<union>m')) (c1@c2@c3) t
3) NODE (USE u1) c1 (NODE (USE u2) c2 t)
-> NODE (USE (u1\<union>u2)) (c1@c2) t
4) NODE (USE u) (c1@NIL#c2)
t
-> NODE (USE u) (c1@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@cs2@ts2#c3) t
6) NODE (USE u1) (c1@(NODE (USE u2) cs ts)#c2) NIL
-> NODE (USE (u1\<union>u2)) (c1@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@t#c2) x -> NODE a (c1@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@t#c2) I use in my rewriting rules (4,5,6,8)

Thanks for any suggestions/comments in advance, best
Peter

Peter,

I have a lot of proofs relating to some theorems for proving rewrite
systems terminating. There are a number of examples of its application
to specific rewrite rule systems.

The model of term which is rewritten is (n-ary function symbol) (list of
n subterms),
so rewriting a subterm naturally is rewriting f (c1@t#c2) to f (c1@t'#c2).

The work is focussed on proving general results rather than applying
them to particular systems, but you may find it useful. At the moment
it runs in Isabelle 2005,
I started trying to update it to Isabelle 2007 but the incompatibilities
are significant.

It's at http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/snabs/
(also uses http://users.rsise.anu.edu.au/~jeremy/isabelle/2005/gen/)

Jeremy

>
>
>

Last updated: May 03 2024 at 04:19 UTC