Non-Looping String Rewriting

¹ Alfons Geser, Symbolisches Rechnen, Wilhelm-Schickard-Institut für Informatik, Universität Tübingen, Sand 13, 72076 Tübingen, Germany
² Department of Computer Science, Universiteit Utrecht, P.O. Box 80.089, 3508 TB Utrecht, The Netherlands

Received: October 1998
Accepted: June 1999

Abstract

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.