ON TERMINATION OF ONE RULE REWRITE SYSTEMS

The undecidability of the termination of rewrite systems is usually pr oved by reduction to the halting of Turing machines, In particular, Da uchet proves the undecidability of the termination of one rule rewrite systems by coding Turing machines into one rule rewrite systems. Rewr ite systems are a very simple model of computation and one may expect proofs in this model to be more straightforward than those referring t o the more complex model of Turing machines. In this paper we deduce t he problem of termination of one rule rewrite systems to problems some what more related to rewrite systems namely to Post correspondence pro blems and to termination of semi-Thue systems. Proofs we obtain this w ay are shorter and we expect other interesting applications from these codings. In particular, the second part proposes a simulation of semi -Thue systems by one rule systems.