重写中不可判定性的层级
计算机科学中的逻辑
2009-03-02 v1 计算复杂性
摘要
一阶项重写系统各种性质的不可判定性是众所周知的。不可判定性质可以通过定义该性质的公式的复杂性来分类。这产生了一个具有不同不可判定性层级的层次结构，从使用一阶算术公式对性质进行分类的算术层级开始，并延续到允许对函数变量进行量化的解析层级。在本文中，我们考察了一阶项重写系统的性质，并在此层级中对它们进行分类。单项的弱规范化与强规范化被证明是 Sigma-0-1-完全的，而它们的一致版本以及带极小性标志的依赖对问题是 Pi-0-2-完全的。我们发现合流性对于单项和一致情况都是 Pi-0-2-完全的。出乎意料的是，基项的弱合流性比开项的弱合流性更难。前者性质是 Pi-0-2-完全的，而后者是 Sigma-0-1-完全的（从而是递归可枚举的）。最令人惊讶的结果是关于不带极小性标志的依赖对问题：我们证明它是 Pi-1-1-完全的，这意味着该性质超越了算术层级，本质上是解析的。
引用
@article{arxiv.0902.4723,
title = {Degrees of Undecidability in Rewriting},
author = {Joerg Endrullis and Herman Geuvers and Hans Zantema},
journal= {arXiv preprint arXiv:0902.4723},
year = {2009}
}