Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness
Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness
复制标题
DOI：
10.1145/4904.4993
复制
发表时间：
1986-01
期刊：
影响因子：
--
通讯作者：
D. Harel
中科院分区：
文献类型：
--
作者：
D. Harel
给出了各种递归树之间的初等平移。证明了有限或可数无限分枝的树可以有效地与无限分枝树一一对应，使得后者的无限路径对应于前者的“P-遵守”无限路径。这里，P可以是无限路径的一类非常广泛的性质中的任何成员。对于许多房产来说，相反的情况也是成立的。其中两个应用涉及(A)经典计算问题的大类高度不可判定的变体的公式，特别是，容易描述的III11-完全的多米诺骨牌问题，以及(B)在任何合理的公平概念下，存在证明不确定或并发程序终止的一般方法。
Elementary translations between various kinds of recursive trees are presented. It is shown that trees of either finite or countably infinite branching can be effectively put into one-one correspondence with infinitely branching trees in such a way that the infinite paths of the latter correspond to the “P-abiding” infinite paths of the former. Here P can be any member of a very wide class of properties of infinite paths. For many properties ??, the converse holds too. Two of the applications involve (a) the formulation of large classes of highly undecidable variants of classical computational problems, and in particular, easily describable domino problems that are III11-complete, and (b) the existence of a general method for proving termination of nondeterministic or concurrent programs under any reasonable notion of fairness.