Cycle Rewriting - Revision history

Sabel: /* Cycle termination */

2015-07-01T09:21:58Z

Cycle termination

Sabel: /* Further Reading */

2015-07-01T09:09:17Z

Sabel: /* References */

2015-07-01T09:01:10Z

References

Sabel: /* Further Reading */

2015-07-01T09:00:04Z

Sabel: /* Implementations */

2015-07-01T08:59:20Z

Implementations

Sabel: /* Implementations */

2015-07-01T08:58:42Z

Implementations

Sabel: /* References */

2015-07-01T08:55:25Z

References

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..."

2015-07-01T08:55:01Z

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..."

New page

== 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.

@@ Line 29: / Line 29: @@
 [u] o&zwj;&rarr;<sub>R</sub> [v] iff &exist;w&isin;&Sigma;<sup>*</sup>: u &sim; lw, (l &rarr; r) &isin; R, and v &sim; rw
-=== Cycle termination ===
+=== Cycle Termination ===
 A cycle rewrite relation o&zwj;&rarr;<sub>R</sub> is non-terminating iff there exists an infinite sequence of
 cycle rewrite steps, i.e. there exist strings u<sub>1</sub>,u<sub>2</sub>,... &isin;&Sigma;<sup>*</sup>

@@ Line 56: / Line 56: @@
 === References ===
-:#<span id="ZBK14"></span>  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
+:#<span id="ZBK14"></span>  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
 :#<span id="SZ15"></span> 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.

← Older revision		Revision as of 08:55, 1 July 2015
Line 58:		Line 58:
	:#<span id="ZBK14"></span> 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		:#<span id="ZBK14"></span> 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
	:#<span id="SZ15"></span> 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.		:#<span id="SZ15"></span> 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]]

@@ Line 52: / Line 52: @@
 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
+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.

@@ Line 45: / Line 45: @@
 [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
+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].