Termination-Portal.org - User contributions [en]

Cycle Rewriting

2015-07-01T09:21:58Z

Sabel: /* Cycle termination */

== Introduction ==
A cycle can be seen as a string of which the left end is connected to the right end,
by which the string has no left end or right end any more.
For instance, all of the strings abcd, bcda, cdab, dabc represent the same cycle.

Cycle rewriting applies [http://www.termination-portal.org/wiki/String_Rewriting string rewrite rules] to cycles.

For instance, the string rewrite rule bc → cac can be applied to the cycle represented
by the string cdab resulting in dacac.

Termination of a cycle rewrite relation means that there does not exist a cycle which
has an infinite derivation using cycle rewrite steps. Cycle termination is different from
termination of string rewrite systems, since e.g. the system R={ab → ba} is terminating
as a string rewrite system, but it is not cycle-terminating, since ab and ba represent the same cycle.
An example for a cycle-terminating system is {aa → aba}.

== Formal Definition of Cycles and Cycle Rewriting ==
=== Cycles ===
Let Σ be an alphabet.
Two strings u,v ∈ Σ* represent the same cycle (u &sim; v) iff there exist strings w1,w2 such that u = w1w2 and v = w2w1.

A cycle is an equivalence class w.r.t. &sim;.

We write [u] for such an equivalence class with representative u.

=== Cycle Rewriting ===
Let R = {l1 → r1,...,ln → rn} be a string rewrite system.
The cycle rewrite relation of R o&zwj;→R is:
[u] o&zwj;→R [v] iff ∃w∈Σ*: u &sim; lw, (l → r) ∈ R, and v &sim; rw

=== Cycle Termination ===
A cycle rewrite relation o&zwj;→R is non-terminating iff there exists an infinite sequence of
cycle rewrite steps, i.e. there exist strings u1,u2,... ∈Σ*
s.t. [ui] o&zwj;→R [ui+1] for all i.

A cycle rewrite relation o&zwj;→R is terminating iff it is not non-terminating.

== Input Format for Cycle Termination Provers ==
Every termination problem for [http://www.termination-portal.org/wiki/String_Rewriting string rewrite systems] is also a termination problem for
cycle rewrite systems. The input format for provers is the same as for string rewrite systems
(problems can be found in the [http://termination-portal.org/wiki/TPDB TPDB]).

== Implementations ==
An approach to prove cycle termination using trace-decreasing matrix interpretations is implemented in the tool
[http://www.win.tue.nl/~hzantema/torpa.html torpacyc]. Another approach is to reduce cycle termination to string termination by a sound and complete
transformation and then applying a termination prover for termination of string rewrite systems. Several of those transformations
and combinations of these techniques and [http://www.win.tue.nl/~hzantema/torpa.html torpacyc] are included in the tool [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/ cycsrs] which
can also be used [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/cgi/prove online].

== Further Reading ==
Cycle rewriting was introduced in [[#ZBK14|[1]]] where its complexity was analyzed and termination techniques
using arctic and tropical matrix interpretations based on type graphs were developed.

In [[#SZ|[2]]] further termination techniques for cycle termination were introduced: trace-decreasing matrix interpretations as well as
sound and complete transformations from cycle to string termination.

=== References ===
:# H. Zantema, H.J.S. Bruggink and B. Koenig, [http://dx.doi.org/10.1007/978-3-319-08918-8_33 Termination of cycle rewriting], Proceedings of Joint International Conference, RTA-TLCA 2014, Vienna, Austria, July 14-17, 2014 Springer Lecture Notes in Computer Science 8560, pages 476-490
:# David Sabel and Hans Zantema. [http://drops.dagstuhl.de/opus/volltexte/2015/5203 Transforming Cycle Rewriting into String Rewriting.] In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications (RTA 2015), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 285-300, Dagstuhl, Germany, June 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[[Category:Categories]]

Cycle Rewriting

2015-07-01T09:09:17Z

Sabel: /* Further Reading */

== Introduction ==
A cycle can be seen as a string of which the left end is connected to the right end,
by which the string has no left end or right end any more.
For instance, all of the strings abcd, bcda, cdab, dabc represent the same cycle.

Cycle rewriting applies [http://www.termination-portal.org/wiki/String_Rewriting string rewrite rules] to cycles.

For instance, the string rewrite rule bc → cac can be applied to the cycle represented
by the string cdab resulting in dacac.

Termination of a cycle rewrite relation means that there does not exist a cycle which
has an infinite derivation using cycle rewrite steps. Cycle termination is different from
termination of string rewrite systems, since e.g. the system R={ab → ba} is terminating
as a string rewrite system, but it is not cycle-terminating, since ab and ba represent the same cycle.
An example for a cycle-terminating system is {aa → aba}.

== Formal Definition of Cycles and Cycle Rewriting ==
=== Cycles ===
Let Σ be an alphabet.
Two strings u,v ∈ Σ* represent the same cycle (u &sim; v) iff there exist strings w1,w2 such that u = w1w2 and v = w2w1.

A cycle is an equivalence class w.r.t. &sim;.

We write [u] for such an equivalence class with representative u.

=== Cycle Rewriting ===
Let R = {l1 → r1,...,ln → rn} be a string rewrite system.
The cycle rewrite relation of R o&zwj;→R is:
[u] o&zwj;→R [v] iff ∃w∈Σ*: u &sim; lw, (l → r) ∈ R, and v &sim; rw

=== Cycle termination ===
A cycle rewrite relation o&zwj;→R is non-terminating iff there exists an infinite sequence of
cycle rewrite steps, i.e. there exist strings u1,u2,... ∈Σ*
s.t. [ui] o&zwj;→R [ui+1] for all i.

A cycle rewrite relation o&zwj;→R is terminating iff it is not non-terminating.

== Input Format for Cycle Termination Provers ==
Every termination problem for [http://www.termination-portal.org/wiki/String_Rewriting string rewrite systems] is also a termination problem for
cycle rewrite systems. The input format for provers is the same as for string rewrite systems
(problems can be found in the [http://termination-portal.org/wiki/TPDB TPDB]).

== Implementations ==
An approach to prove cycle termination using trace-decreasing matrix interpretations is implemented in the tool
[http://www.win.tue.nl/~hzantema/torpa.html torpacyc]. Another approach is to reduce cycle termination to string termination by a sound and complete
transformation and then applying a termination prover for termination of string rewrite systems. Several of those transformations
and combinations of these techniques and [http://www.win.tue.nl/~hzantema/torpa.html torpacyc] are included in the tool [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/ cycsrs] which
can also be used [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/cgi/prove online].

== Further Reading ==
Cycle rewriting was introduced in [[#ZBK14|[1]]] where its complexity was analyzed and termination techniques
using arctic and tropical matrix interpretations based on type graphs were developed.

In [[#SZ|[2]]] further termination techniques for cycle termination were introduced: trace-decreasing matrix interpretations as well as
sound and complete transformations from cycle to string termination.

=== References ===
:# H. Zantema, H.J.S. Bruggink and B. Koenig, [http://dx.doi.org/10.1007/978-3-319-08918-8_33 Termination of cycle rewriting], Proceedings of Joint International Conference, RTA-TLCA 2014, Vienna, Austria, July 14-17, 2014 Springer Lecture Notes in Computer Science 8560, pages 476-490
:# David Sabel and Hans Zantema. [http://drops.dagstuhl.de/opus/volltexte/2015/5203 Transforming Cycle Rewriting into String Rewriting.] In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications (RTA 2015), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 285-300, Dagstuhl, Germany, June 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[[Category:Categories]]

Cycle Rewriting

2015-07-01T09:01:10Z

Sabel: /* References */

== Introduction ==
A cycle can be seen as a string of which the left end is connected to the right end,
by which the string has no left end or right end any more.
For instance, all of the strings abcd, bcda, cdab, dabc represent the same cycle.

Cycle rewriting applies [http://www.termination-portal.org/wiki/String_Rewriting string rewrite rules] to cycles.

For instance, the string rewrite rule bc → cac can be applied to the cycle represented
by the string cdab resulting in dacac.

Termination of a cycle rewrite relation means that there does not exist a cycle which
has an infinite derivation using cycle rewrite steps. Cycle termination is different from
termination of string rewrite systems, since e.g. the system R={ab → ba} is terminating
as a string rewrite system, but it is not cycle-terminating, since ab and ba represent the same cycle.
An example for a cycle-terminating system is {aa → aba}.

== Formal Definition of Cycles and Cycle Rewriting ==
=== Cycles ===
Let Σ be an alphabet.
Two strings u,v ∈ Σ* represent the same cycle (u &sim; v) iff there exist strings w1,w2 such that u = w1w2 and v = w2w1.

A cycle is an equivalence class w.r.t. &sim;.

We write [u] for such an equivalence class with representative u.

=== Cycle Rewriting ===
Let R = {l1 → r1,...,ln → rn} be a string rewrite system.
The cycle rewrite relation of R o&zwj;→R is:
[u] o&zwj;→R [v] iff ∃w∈Σ*: u &sim; lw, (l → r) ∈ R, and v &sim; rw

=== Cycle termination ===
A cycle rewrite relation o&zwj;→R is non-terminating iff there exists an infinite sequence of
cycle rewrite steps, i.e. there exist strings u1,u2,... ∈Σ*
s.t. [ui] o&zwj;→R [ui+1] for all i.

A cycle rewrite relation o&zwj;→R is terminating iff it is not non-terminating.

== Input Format for Cycle Termination Provers ==
Every termination problem for [http://www.termination-portal.org/wiki/String_Rewriting string rewrite systems] is also a termination problem for
cycle rewrite systems. The input format for provers is the same as for string rewrite systems
(problems can be found in the [http://termination-portal.org/wiki/TPDB TPDB]).

== Implementations ==
An approach to prove cycle termination using trace-decreasing matrix interpretations is implemented in the tool
[http://www.win.tue.nl/~hzantema/torpa.html torpacyc]. Another approach is to reduce cycle termination to string termination by a sound and complete
transformation and then applying a termination prover for termination of string rewrite systems. Several of those transformations
and combinations of these techniques and [http://www.win.tue.nl/~hzantema/torpa.html torpacyc] are included in the tool [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/ cycsrs] which
can also be used [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/cgi/prove online].

== Further Reading ==
Cycle rewriting was introduced in [[#ZBK14|[1]]] where its complexity was analyzed and termination techniques
using arctic and tropical matrix interpretations based on type graphs were developed.

In [[#SZ|[2]]] more termination techniques for cycle termination were introduced: trace-decreasing matrix interpretations as well as
sound and complete transformations from cycle to string termination.

=== References ===
:# H. Zantema, H.J.S. Bruggink and B. Koenig, [http://dx.doi.org/10.1007/978-3-319-08918-8_33 Termination of cycle rewriting], Proceedings of Joint International Conference, RTA-TLCA 2014, Vienna, Austria, July 14-17, 2014 Springer Lecture Notes in Computer Science 8560, pages 476-490
:# David Sabel and Hans Zantema. [http://drops.dagstuhl.de/opus/volltexte/2015/5203 Transforming Cycle Rewriting into String Rewriting.] In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications (RTA 2015), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 285-300, Dagstuhl, Germany, June 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[[Category:Categories]]

Cycle Rewriting

2015-07-01T09:00:04Z

Sabel: /* Further Reading */

== Introduction ==
A cycle can be seen as a string of which the left end is connected to the right end,
by which the string has no left end or right end any more.
For instance, all of the strings abcd, bcda, cdab, dabc represent the same cycle.

Cycle rewriting applies [http://www.termination-portal.org/wiki/String_Rewriting string rewrite rules] to cycles.

For instance, the string rewrite rule bc → cac can be applied to the cycle represented
by the string cdab resulting in dacac.

Termination of a cycle rewrite relation means that there does not exist a cycle which
has an infinite derivation using cycle rewrite steps. Cycle termination is different from
termination of string rewrite systems, since e.g. the system R={ab → ba} is terminating
as a string rewrite system, but it is not cycle-terminating, since ab and ba represent the same cycle.
An example for a cycle-terminating system is {aa → aba}.

== Formal Definition of Cycles and Cycle Rewriting ==
=== Cycles ===
Let Σ be an alphabet.
Two strings u,v ∈ Σ* represent the same cycle (u &sim; v) iff there exist strings w1,w2 such that u = w1w2 and v = w2w1.

A cycle is an equivalence class w.r.t. &sim;.

We write [u] for such an equivalence class with representative u.

=== Cycle Rewriting ===
Let R = {l1 → r1,...,ln → rn} be a string rewrite system.
The cycle rewrite relation of R o&zwj;→R is:
[u] o&zwj;→R [v] iff ∃w∈Σ*: u &sim; lw, (l → r) ∈ R, and v &sim; rw

=== Cycle termination ===
A cycle rewrite relation o&zwj;→R is non-terminating iff there exists an infinite sequence of
cycle rewrite steps, i.e. there exist strings u1,u2,... ∈Σ*
s.t. [ui] o&zwj;→R [ui+1] for all i.

A cycle rewrite relation o&zwj;→R is terminating iff it is not non-terminating.

== Input Format for Cycle Termination Provers ==
Every termination problem for [http://www.termination-portal.org/wiki/String_Rewriting string rewrite systems] is also a termination problem for
cycle rewrite systems. The input format for provers is the same as for string rewrite systems
(problems can be found in the [http://termination-portal.org/wiki/TPDB TPDB]).

== Implementations ==
An approach to prove cycle termination using trace-decreasing matrix interpretations is implemented in the tool
[http://www.win.tue.nl/~hzantema/torpa.html torpacyc]. Another approach is to reduce cycle termination to string termination by a sound and complete
transformation and then applying a termination prover for termination of string rewrite systems. Several of those transformations
and combinations of these techniques and [http://www.win.tue.nl/~hzantema/torpa.html torpacyc] are included in the tool [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/ cycsrs] which
can also be used [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/cgi/prove online].

== Further Reading ==
Cycle rewriting was introduced in [[#ZBK14|[1]]] where its complexity was analyzed and termination techniques
using arctic and tropical matrix interpretations based on type graphs were developed.

In [[#SZ|[2]]] more termination techniques for cycle termination were introduced: trace-decreasing matrix interpretations as well as
sound and complete transformations from cycle to string termination.

=== References ===
:# H. Zantema, H.J.S. Bruggink and B. Koenig, Termination of cycle rewriting, Proceedings of Joint International Conference, RTA-TLCA 2014, Vienna, Austria, July 14-17, 2014 Springer Lecture Notes in Computer Science 8560, pages 476-490
:# David Sabel and Hans Zantema. [http://drops.dagstuhl.de/opus/volltexte/2015/5203 Transforming Cycle Rewriting into String Rewriting.] In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications (RTA 2015), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 285-300, Dagstuhl, Germany, June 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[[Category:Categories]]

Cycle Rewriting

2015-07-01T08:59:20Z

Sabel: /* Implementations */

== Introduction ==
A cycle can be seen as a string of which the left end is connected to the right end,
by which the string has no left end or right end any more.
For instance, all of the strings abcd, bcda, cdab, dabc represent the same cycle.

Cycle rewriting applies [http://www.termination-portal.org/wiki/String_Rewriting string rewrite rules] to cycles.

For instance, the string rewrite rule bc → cac can be applied to the cycle represented
by the string cdab resulting in dacac.

Termination of a cycle rewrite relation means that there does not exist a cycle which
has an infinite derivation using cycle rewrite steps. Cycle termination is different from
termination of string rewrite systems, since e.g. the system R={ab → ba} is terminating
as a string rewrite system, but it is not cycle-terminating, since ab and ba represent the same cycle.
An example for a cycle-terminating system is {aa → aba}.

== Formal Definition of Cycles and Cycle Rewriting ==
=== Cycles ===
Let Σ be an alphabet.
Two strings u,v ∈ Σ* represent the same cycle (u &sim; v) iff there exist strings w1,w2 such that u = w1w2 and v = w2w1.

A cycle is an equivalence class w.r.t. &sim;.

We write [u] for such an equivalence class with representative u.

=== Cycle Rewriting ===
Let R = {l1 → r1,...,ln → rn} be a string rewrite system.
The cycle rewrite relation of R o&zwj;→R is:
[u] o&zwj;→R [v] iff ∃w∈Σ*: u &sim; lw, (l → r) ∈ R, and v &sim; rw

=== Cycle termination ===
A cycle rewrite relation o&zwj;→R is non-terminating iff there exists an infinite sequence of
cycle rewrite steps, i.e. there exist strings u1,u2,... ∈Σ*
s.t. [ui] o&zwj;→R [ui+1] for all i.

A cycle rewrite relation o&zwj;→R is terminating iff it is not non-terminating.

== Input Format for Cycle Termination Provers ==
Every termination problem for [http://www.termination-portal.org/wiki/String_Rewriting string rewrite systems] is also a termination problem for
cycle rewrite systems. The input format for provers is the same as for string rewrite systems
(problems can be found in the [http://termination-portal.org/wiki/TPDB TPDB]).

== Implementations ==
An approach to prove cycle termination using trace-decreasing matrix interpretations is implemented in the tool
[http://www.win.tue.nl/~hzantema/torpa.html torpacyc]. Another approach is to reduce cycle termination to string termination by a sound and complete
transformation and then applying a termination prover for termination of string rewrite systems. Several of those transformations
and combinations of these techniques and [http://www.win.tue.nl/~hzantema/torpa.html torpacyc] are included in the tool [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/ cycsrs] which
can also be used [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/cgi/prove online].

== Further Reading ==
Cycle rewriting was introduced in [[#ZBK14|[1]]] where its complexity was analyzed and termination techniques
using arctic and tropical matrix interpretations based on type graphs were developed.
In [[#SZ|[2]]] more termination techniques for cycle termination were introduced: trace-decreasing matrix interpretations as well as
sound and complete transformations from cycle to string termination.

=== References ===
:# H. Zantema, H.J.S. Bruggink and B. Koenig, Termination of cycle rewriting, Proceedings of Joint International Conference, RTA-TLCA 2014, Vienna, Austria, July 14-17, 2014 Springer Lecture Notes in Computer Science 8560, pages 476-490
:# David Sabel and Hans Zantema. [http://drops.dagstuhl.de/opus/volltexte/2015/5203 Transforming Cycle Rewriting into String Rewriting.] In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications (RTA 2015), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 285-300, Dagstuhl, Germany, June 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[[Category:Categories]]

Cycle Rewriting

2015-07-01T08:58:42Z

Sabel: /* Implementations */

== Introduction ==
A cycle can be seen as a string of which the left end is connected to the right end,
by which the string has no left end or right end any more.
For instance, all of the strings abcd, bcda, cdab, dabc represent the same cycle.

Cycle rewriting applies [http://www.termination-portal.org/wiki/String_Rewriting string rewrite rules] to cycles.

For instance, the string rewrite rule bc → cac can be applied to the cycle represented
by the string cdab resulting in dacac.

Termination of a cycle rewrite relation means that there does not exist a cycle which
has an infinite derivation using cycle rewrite steps. Cycle termination is different from
termination of string rewrite systems, since e.g. the system R={ab → ba} is terminating
as a string rewrite system, but it is not cycle-terminating, since ab and ba represent the same cycle.
An example for a cycle-terminating system is {aa → aba}.

== Formal Definition of Cycles and Cycle Rewriting ==
=== Cycles ===
Let Σ be an alphabet.
Two strings u,v ∈ Σ* represent the same cycle (u &sim; v) iff there exist strings w1,w2 such that u = w1w2 and v = w2w1.

A cycle is an equivalence class w.r.t. &sim;.

We write [u] for such an equivalence class with representative u.

=== Cycle Rewriting ===
Let R = {l1 → r1,...,ln → rn} be a string rewrite system.
The cycle rewrite relation of R o&zwj;→R is:
[u] o&zwj;→R [v] iff ∃w∈Σ*: u &sim; lw, (l → r) ∈ R, and v &sim; rw

=== Cycle termination ===
A cycle rewrite relation o&zwj;→R is non-terminating iff there exists an infinite sequence of
cycle rewrite steps, i.e. there exist strings u1,u2,... ∈Σ*
s.t. [ui] o&zwj;→R [ui+1] for all i.

A cycle rewrite relation o&zwj;→R is terminating iff it is not non-terminating.

== Input Format for Cycle Termination Provers ==
Every termination problem for [http://www.termination-portal.org/wiki/String_Rewriting string rewrite systems] is also a termination problem for
cycle rewrite systems. The input format for provers is the same as for string rewrite systems
(problems can be found in the [http://termination-portal.org/wiki/TPDB TPDB]).

== Implementations ==
An approach to prove cycle termination using trace-decreasing matrix interpretations is implemented in the tool
[http://www.win.tue.nl/~hzantema/torpa.html torpacyc]. Another approach is to reduce cycle termination to string termination by a sound and complete
transformation and then applying a termination prover for termination of string rewrite systems. Several of those transformations
and combinations of these techniques are included in the tool [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/ cycsrs] which
can also be used [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/cgi/prove online].

== Further Reading ==
Cycle rewriting was introduced in [[#ZBK14|[1]]] where its complexity was analyzed and termination techniques
using arctic and tropical matrix interpretations based on type graphs were developed.
In [[#SZ|[2]]] more termination techniques for cycle termination were introduced: trace-decreasing matrix interpretations as well as
sound and complete transformations from cycle to string termination.

=== References ===
:# H. Zantema, H.J.S. Bruggink and B. Koenig, Termination of cycle rewriting, Proceedings of Joint International Conference, RTA-TLCA 2014, Vienna, Austria, July 14-17, 2014 Springer Lecture Notes in Computer Science 8560, pages 476-490
:# David Sabel and Hans Zantema. [http://drops.dagstuhl.de/opus/volltexte/2015/5203 Transforming Cycle Rewriting into String Rewriting.] In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications (RTA 2015), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 285-300, Dagstuhl, Germany, June 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[[Category:Categories]]

Cycle Rewriting

2015-07-01T08:55:25Z

Sabel: /* References */

== Introduction ==
A cycle can be seen as a string of which the left end is connected to the right end,
by which the string has no left end or right end any more.
For instance, all of the strings abcd, bcda, cdab, dabc represent the same cycle.

Cycle rewriting applies [http://www.termination-portal.org/wiki/String_Rewriting string rewrite rules] to cycles.

For instance, the string rewrite rule bc → cac can be applied to the cycle represented
by the string cdab resulting in dacac.

Termination of a cycle rewrite relation means that there does not exist a cycle which
has an infinite derivation using cycle rewrite steps. Cycle termination is different from
termination of string rewrite systems, since e.g. the system R={ab → ba} is terminating
as a string rewrite system, but it is not cycle-terminating, since ab and ba represent the same cycle.
An example for a cycle-terminating system is {aa → aba}.

== Formal Definition of Cycles and Cycle Rewriting ==
=== Cycles ===
Let Σ be an alphabet.
Two strings u,v ∈ Σ* represent the same cycle (u &sim; v) iff there exist strings w1,w2 such that u = w1w2 and v = w2w1.

A cycle is an equivalence class w.r.t. &sim;.

We write [u] for such an equivalence class with representative u.

=== Cycle Rewriting ===
Let R = {l1 → r1,...,ln → rn} be a string rewrite system.
The cycle rewrite relation of R o&zwj;→R is:
[u] o&zwj;→R [v] iff ∃w∈Σ*: u &sim; lw, (l → r) ∈ R, and v &sim; rw

=== Cycle termination ===
A cycle rewrite relation o&zwj;→R is non-terminating iff there exists an infinite sequence of
cycle rewrite steps, i.e. there exist strings u1,u2,... ∈Σ*
s.t. [ui] o&zwj;→R [ui+1] for all i.

A cycle rewrite relation o&zwj;→R is terminating iff it is not non-terminating.

== Input Format for Cycle Termination Provers ==
Every termination problem for [http://www.termination-portal.org/wiki/String_Rewriting string rewrite systems] is also a termination problem for
cycle rewrite systems. The input format for provers is the same as for string rewrite systems
(problems can be found in the [http://termination-portal.org/wiki/TPDB TPDB]).

== Implementations ==
An approach to prove cycle termination using trace-decreasing matrix interpretations is implemented in the tool
[http://www.win.tue.nl/~hzantema/torpa.html torpacyc]. Another approach is to reduce cycle termination to string termination by a sound and complete
transformation and then applying a termination prover for termination of string rewrite systems. Several of those transformations
and combinations of the technique are included in the tool [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/ cycsrs] which
can also be used [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/cgi/prove online].

== Further Reading ==
Cycle rewriting was introduced in [[#ZBK14|[1]]] where its complexity was analyzed and termination techniques
using arctic and tropical matrix interpretations based on type graphs were developed.
In [[#SZ|[2]]] more termination techniques for cycle termination were introduced: trace-decreasing matrix interpretations as well as
sound and complete transformations from cycle to string termination.

=== References ===
:# H. Zantema, H.J.S. Bruggink and B. Koenig, Termination of cycle rewriting, Proceedings of Joint International Conference, RTA-TLCA 2014, Vienna, Austria, July 14-17, 2014 Springer Lecture Notes in Computer Science 8560, pages 476-490
:# David Sabel and Hans Zantema. [http://drops.dagstuhl.de/opus/volltexte/2015/5203 Transforming Cycle Rewriting into String Rewriting.] In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications (RTA 2015), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 285-300, Dagstuhl, Germany, June 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[[Category:Categories]]

Cycle Rewriting

2015-07-01T08:55:01Z

Sabel: Created page with "== Introduction == A cycle can be seen as a string of which the left end is connected to the right end, by which the string has no left end or right end any more. For instanc..."

== Introduction ==
A cycle can be seen as a string of which the left end is connected to the right end,
by which the string has no left end or right end any more.
For instance, all of the strings abcd, bcda, cdab, dabc represent the same cycle.

Cycle rewriting applies [http://www.termination-portal.org/wiki/String_Rewriting string rewrite rules] to cycles.

For instance, the string rewrite rule bc → cac can be applied to the cycle represented
by the string cdab resulting in dacac.

Termination of a cycle rewrite relation means that there does not exist a cycle which
has an infinite derivation using cycle rewrite steps. Cycle termination is different from
termination of string rewrite systems, since e.g. the system R={ab → ba} is terminating
as a string rewrite system, but it is not cycle-terminating, since ab and ba represent the same cycle.
An example for a cycle-terminating system is {aa → aba}.

== Formal Definition of Cycles and Cycle Rewriting ==
=== Cycles ===
Let Σ be an alphabet.
Two strings u,v ∈ Σ* represent the same cycle (u &sim; v) iff there exist strings w1,w2 such that u = w1w2 and v = w2w1.

A cycle is an equivalence class w.r.t. &sim;.

We write [u] for such an equivalence class with representative u.

=== Cycle Rewriting ===
Let R = {l1 → r1,...,ln → rn} be a string rewrite system.
The cycle rewrite relation of R o&zwj;→R is:
[u] o&zwj;→R [v] iff ∃w∈Σ*: u &sim; lw, (l → r) ∈ R, and v &sim; rw

=== Cycle termination ===
A cycle rewrite relation o&zwj;→R is non-terminating iff there exists an infinite sequence of
cycle rewrite steps, i.e. there exist strings u1,u2,... ∈Σ*
s.t. [ui] o&zwj;→R [ui+1] for all i.

A cycle rewrite relation o&zwj;→R is terminating iff it is not non-terminating.

== Input Format for Cycle Termination Provers ==
Every termination problem for [http://www.termination-portal.org/wiki/String_Rewriting string rewrite systems] is also a termination problem for
cycle rewrite systems. The input format for provers is the same as for string rewrite systems
(problems can be found in the [http://termination-portal.org/wiki/TPDB TPDB]).

== Implementations ==
An approach to prove cycle termination using trace-decreasing matrix interpretations is implemented in the tool
[http://www.win.tue.nl/~hzantema/torpa.html torpacyc]. Another approach is to reduce cycle termination to string termination by a sound and complete
transformation and then applying a termination prover for termination of string rewrite systems. Several of those transformations
and combinations of the technique are included in the tool [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/ cycsrs] which
can also be used [http://www.ki.informatik.uni-frankfurt.de/research/cycsrs/cgi/prove online].

== Further Reading ==
Cycle rewriting was introduced in [[#ZBK14|[1]]] where its complexity was analyzed and termination techniques
using arctic and tropical matrix interpretations based on type graphs were developed.
In [[#SZ|[2]]] more termination techniques for cycle termination were introduced: trace-decreasing matrix interpretations as well as
sound and complete transformations from cycle to string termination.

=== References ===
:# H. Zantema, H.J.S. Bruggink and B. Koenig, Termination of cycle rewriting, Proceedings of Joint International Conference, RTA-TLCA 2014, Vienna, Austria, July 14-17, 2014 Springer Lecture Notes in Computer Science 8560, pages 476-490
:# David Sabel and Hans Zantema. [http://drops.dagstuhl.de/opus/volltexte/2015/5203 Transforming Cycle Rewriting into String Rewriting.] In Maribel Fernández, editor, 26th International Conference on Rewriting Techniques and Applications (RTA 2015), volume 36 of Leibniz International Proceedings in Informatics (LIPIcs), pages 285-300, Dagstuhl, Germany, June 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.