We prove that termination is undecidable for non-length-increasing string rewriting systems, using linear-bounded automata. On the other hand, we prove the undecidability of confluence for terminating rewriting systems when terms begin by a fixed symbol. These two results illustrate that sometimes restriction of problem to recognizable domains modify decidability properties, sometimes it does not. (We only consider finite terms).
This work was supported by PRC
Mathématiques et informatique
and ESPRIT2 Working Group ASMICS.