Effective Transformations on Infinite Trees, with Applications to High Undecidability, Dominoes, and Fairness

Abstract

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. © 1986, ACM. All rights reserved.