Sequential Algorithms for Unbounded Nondeterminism

We give extensional and intensional characterizations of higher-order functional programs with unbounded nondeterminism: as stable and monotone functions between the biorders of states of ordered concrete data structures, and as sequential algorithms (states of an exponential ocds) which compute them. Our fundamental result establishes that these representations are equivalent, by showing how to construct a unique sequential algorithm which computes a given stable and monotone function.We illustrate by defining a denotational semantics for a functional language with countable nondeterminism (“fair PCF”), with an interpretation of fixpoints which allows this to be proved to be computationally adequate. We observe that our model contains functions which cannot be computed in fair PCF, by identifying a further property of the definable elements, and so show that it is not fully abstract.