A general result on infinite trees and its applications
David Harel · 1984
A generic translation between various kinds of recursive trees is 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 “@@@@-abiding” infinite paths of the former. Here @@@@ an be any member of a very wide class of properties of infinite paths. Two of the applications involve the formulation of large classes of π11 variants of classical computational problems, and the existence of a general method for proving termination of nondeterministic or concurrent programs under any reasonable notion of fairness.