Non-Looping String Rewriting
Alfons Geser, Symbolisches Rechnen,
Wilhelm-Schickard-Institut für Informatik,
Universität Tübingen, Sand 13, 72076 Tübingen, Germany
2 Department of Computer Science, Universiteit Utrecht, P.O. Box 80.089, 3508 TB Utrecht, The Netherlands
Accepted: June 1999
String rewriting reductions of the form , called loops, are the most frequent cause of infinite reductions (non- termination). Regarded as a model of computation, infinite reductions are unwanted whence their static detection is important. There are string rewriting systems which admit infinite reductions although they admit no loops. Their non-termination is particularly difficult to uncover. We present a few necessary conditions for the existence of loops, and thus establish a means to recognize the difficult case. We show in detail four relevant criteria: (i) the existence of loops is characterized by the existence of looping forward closures; (ii) dummy elimination, a non-termination preserving transformation method, also preserves the existence of loops; (iii) dummy introduction, a transformation method that supports subsequent dummy elimination, likewise preserves loops; (iv) bordered systems can be reduced to smaller systems on a larger alphabet, preserving the existence and the non-existence of loops. We illustrate the power of the four methods by giving a two-rule string rewriting system over a two-letter alphabet which admits an infinite reduction but no loop. So far, the least known such system had three rules.
Mathematics Subject Classification: 68Q42 / 20M10
Key words: string rewriting / semi-thue system / termination / loop / term rewriting / transformation ordering / dummy introduction / dummy elimination / overlap closure / forward closure.
© EDP Sciences, 1999