Sequential algorithms for unbounded nondeterminism

Research output: Contribution to journalArticlepeer-review

3 Citations (SciVal)
83 Downloads (Pure)


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.

Original languageEnglish
Pages (from-to)271-287
Number of pages17
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 21 Dec 2015


  • Biorders
  • Fairness
  • Nondeterminism
  • Sequential Algorithms


Dive into the research topics of 'Sequential algorithms for unbounded nondeterminism'. Together they form a unique fingerprint.

Cite this