# Cycle Rewriting

## 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 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 ∼ v) iff there exist strings w1,w2 such that u = w1w2 and v = w2w1.

A cycle is an equivalence class w.r.t. ∼.

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‍→R is: [u] o‍→R [v] iff ∃w∈Σ*: u ∼ lw, (l → r) ∈ R, and v ∼ rw

### Cycle Termination

A cycle rewrite relation o‍→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‍→R [ui+1] for all i.

A cycle rewrite relation o‍→R is terminating iff it is not non-terminating.

## Input Format for Cycle Termination Provers

Every termination problem for 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 TPDB).

## Implementations

An approach to prove cycle termination using trace-decreasing matrix interpretations is implemented in the tool 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 torpacyc are included in the tool cycsrs which can also be used online.