Levels of undecidability in rewriting

TY - JOUR

T1 - Levels of undecidability in rewriting

AU - Endrullis, Jörg

AU - Geuvers, Herman

AU - Simonsen, Jakob Grue

AU - Zantema, Hans

PY - 2011/2

Y1 - 2011/2

N2 - Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed. In this paper we give an overview of how the main properties of first order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms. Most uniform properties are Π20-complete. The particular problem of local confluence turns out to be Π20-complete for ground terms, but only Π20-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be Π11-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy. Some of our results are new or have appeared in our earlier publications. Others are based on folklore constructions, and are included for completeness as their precise classifications have hardly been noticed previously.

AB - Undecidability of various properties of first-order term rewriting systems is well-known. An undecidable property can be classified by the complexity of the formula defining it. This classification gives rise to a hierarchy of distinct levels of undecidability, starting from the arithmetical hierarchy classifying properties using first order arithmetical formulas, and continuing into the analytic hierarchy, where quantification over function variables is allowed. In this paper we give an overview of how the main properties of first order term rewriting systems are classified in these hierarchies. We consider properties related to normalization (strong normalization, weak normalization and dependency problems) and properties related to confluence (confluence, local confluence and the unique normal form property). For all of these we distinguish between the single term version and the uniform version. Where appropriate, we also distinguish between ground and open terms. Most uniform properties are Π20-complete. The particular problem of local confluence turns out to be Π20-complete for ground terms, but only Π20-complete (and thereby recursively enumerable) for open terms. The most surprising result concerns dependency pair problems without minimality flag: we prove this problem to be Π11-complete, hence not in the arithmetical hierarchy, but properly in the analytic hierarchy. Some of our results are new or have appeared in our earlier publications. Others are based on folklore constructions, and are included for completeness as their precise classifications have hardly been noticed previously.

U2 - 10.1016/j.ic.2010.09.003

DO - 10.1016/j.ic.2010.09.003

M3 - Journal article

SN - 0890-5401

VL - 209

SP - 227

EP - 245

JO - Information and Computation

JF - Information and Computation

IS - 2

ER -