The undecidability of self-embedding for term rewriting systems

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...

Full description

Saved in:
Bibliographic Details
Published in:Information processing letters 1985-02, Vol.20 (2), p.61-64
Main Author: Plaisted, David A.
Format: Article
Language:English
Subjects:
Applied sciences
Computer programming
Computer science
Computer science
control theory
systems
Exact sciences and technology
Mathematical analysis
self-embedding
Software
Software engineering
Systems analysis
Techniques
Term rewriting system
termination
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0020-0190
1872-6119
DOI:10.1016/0020-0190(85)90063-8