The undecidability of the semi-unification problem
The undecidability of the semi-unification problem
复制标题
半统一问题的不可判定性
DOI：
10.1145/100216.100279
复制
发表时间：
1990
期刊：
影响因子：
--
通讯作者：
P. Urzyczyn
中科院分区：
文献类型：
--
作者：
A. Kfoury;J. Tiuryn;P. Urzyczyn
半统一问题（SUP）是一阶统一和匹配问题的自然推广。这个问题出现在计算机科学和逻辑的各个分支中。虽然已知有几个特殊的SUP案件是可以确定的，但这个问题在总体上已经开放了好几年。通过将图灵机的“有界性问题”简化为“有界性问题”，我们证明了一般情况下图灵机是不可判定的。这种有界性问题的不可判定性是由20世纪60年代中期发展起来的一种技术来证明图灵机的相关结果
Abstract The Semi-Unification Problem (SUP) is a natural generalization of both first-order unification and matching. The problem arises in various branches of computer science and logic. Although several special cases of SUP are known to be decidable, the problem in general has been open for several years. We show that SUP in general is undecidable, by reducing what we call the "boundedness problem" of Turing machines to SUP. The undecidability of this boundedness problem is established by a technique developed in the mid-1960s to prove related results about Turing machines