On the Herbrand-Kleene universe for nondeterministic computations (Q1060011)

For nondeterministic recursive equations over an arbitrary signature of function symbols including the nondeterministic choice operator ''or'' the interpretation is factorized according to the techniques developed earlier by the author. It is shown that one can either associate an infinite tree with the equations, then interpret the function symbol ''or'' as a nondeterministic choice operator and so mapping the tree onto a set of infinite trees and then interpret these trees. Or one can interpret the recursive equation directly yielding a set-valued function. Both possibilities lead to the same result, i.e., one obtains a communication diagram. However, one has to use more refined techniques than just powerdomains. This explains and solves a problem posed by \textit{M. Nivat} [Information processing, Proc. IFIP Congr., Tokyo and Melbourne 1980, 17- 28 (1980; Zbl 0444.68011)]. Basically, the construction gives a generalization of the powerdomain approach applicable to arbitrary nonflat (nondiscrete) algebraic domains.