Abstract

We define notions of ordered concrete data structure and nondeterministic sequential algorithm, and use them to give an intensional representation of sequential functionals with bounded and unbounded non-determinism.

Sequential algorithms on concrete data structures have been shown to correspond to a particular notion of ``observably sequential functional''. In this work, we extend these results to a setting with bounded and unbounded nondeterminism, defining concrete data structures in which the sets of cells, values and events are ordered, and in which proofs of events may be infinite. The nondeterministic states over an ordered CDS form a \emph{biorder} in the sense of Berry, and we show that stable and monotone functions, costable and continuous functions, and stable and continuous functions on these biorders each correspond to states on a function-space data structure (non-deterministic sequential algorithms), proving Cartesian closure for the corresponding categories.

We then describe ``partial correctness'' and ``total correctness'' interpretations of a functional language with unbounded choice over ordinal types, and prove \emph{universality} results for both models. This is the first ``intensional'' model characterizing the behaviour (with respect to total correctness) of higher-order functionals with unbounded nondeterminism.