重写中的不可判定度
Degrees of Undecidability in Rewriting
摘要：
一阶项重写系统的各种性质的不可判定性是众所周知的。一个不可判定的属性可以根据定义它的公式的复杂性来分类，这就产生了一个由不同层次的不可判定性组成的层次结构，从使用一阶算术公式对属性进行分类的算术层次结构开始，一直到允许对函数变量进行量化的分析层次结构。在本文中，我们考虑一阶项重写系统的性质，并在这个层次中对它们进行分类。单个项的弱和强规范化是Sigma-0-1-完全的，而它们的统一版本以及带有极小标志的依赖对问题是Pi-0-2-完全的。我们发现，汇合是Pi-0-2-完全的单项和一致。出乎意料地，基项的弱汇合比开项的弱汇合更难。前一个性质是Pi-0-2-完全的，而后者是Sigma-0-1-完全的（因此是递归可递归的）。最令人惊讶的结果是没有极小标志的依赖对问题：我们证明这是Pi-1-1-完全的，这意味着这个属性超过了算术层次，本质上是解析的。
英文摘要：
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 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 also quantification over function variables is allowed. In this paper we consider properties of first order term rewriting systems and classify them in this hierarchy. Weak and strong normalization for single terms turn out to be Sigma-0-1-complete, while their uniform versions as well as dependency pair problems with minimality flag are Pi-0-2-complete. We find that confluence is Pi-0-2-complete both for single terms and uniform. Unexpectedly weak confluence for ground terms turns out to be harder than weak confluence for open terms. The former property is Pi-0-2-complete while the latter is Sigma-0-1-complete (and thereby recursively enumerable). The most surprising result is on dependency pair problems without minimality flag: we prove this to be Pi-1-1-complete, which means that this property exceeds the arithmetical hierarchy and is essentially analytic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
