×

The undecidability of self-embedding for term rewriting systems. (English) Zbl 0571.68025

The self-embedding property of term rewriting systems is closely related to the uniform termination property, since a nonself-embedding term rewriting system is uniform terminating. The self-embedding property is shown to be undecidable and partially decidable. It follows that the nonself-embedding property is not partially decidable. This is true even for globally finite term rewriting systems. The same construction gives an easy alternate proof that uniform termination is undecidable in general and also for globally finite term rewriting systems. Also, the looping property is shown to be undecidable in the same way.

MSC:

68Q65 Abstract data types; algebraic specification
Full Text: DOI

References:

[1] Dershowitz, N., Orderings for term-rewriting systems, Theoret. Comput. Sci., 17, 279-301 (1982) · Zbl 0525.68054
[2] Hopcroft, J.; Ullman, J. D., Introduction to Automata Theory, Languages, and Computation (1979), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0426.68001
[3] Huet, G.; Lankford, D., On the uniform halting problem for term rewriting systems, INRIA Tech. Rept. 283 (1978)
[4] Plaisted, D., A recursively defined ordering for proving termination of term-rewriting systems, (Rept. No. 943 (1978), Department of Computer Science, University of Illinois at Urbana-Champaign)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.