Extensional and Intensional Semantics of Bounded and Unbounded Nondeterminism

TL;DR

This paper develops a comprehensive semantic framework for nondeterministic functional programs, establishing equivalences between extensional and intensional models, and analyzing their properties with respect to bounded and unbounded nondeterminism.

Contribution

It introduces a novel dual characterization of nondeterministic programs using biorders and sequential algorithms, and proves full abstraction for bounded nondeterminism models.

Findings

Extensional and intensional semantics are equivalent for nondeterministic programs.

Bounded nondeterminism models are fully abstract for may- and must-testing.

Unbounded nondeterminism models are not fully abstract, with identifiable weak continuity properties.

Abstract

We give extensional and intensional characterizations of functional programs with nondeterminism: as structure preserving functions between biorders, and as nondeterministic sequential algorithms on ordered concrete data structures which compute them. A fundamental result establishes that these extensional and intensional representations are equivalent, by showing how to construct the unique sequential algorithm which computes a given monotone and stable function, and describing the conditions on sequential algorithms which correspond to continuity with respect to each order. We illustrate by defining may-testing and must-testing denotational semantics for sequential functional languages with bounded and unbounded choice operators. We prove that these are computationally adequate, despite the non-continuity of the must-testing semantics of unbounded nondeterminism. In the bounded case, we prove that our continuous models are fully abstract with respect to may-testing and must-testing by identifying a simple universal type, which may also form the basis for models of the untyped {\lambda}-calculus. In the unbounded case we observe that our model contains computable functions which are not denoted by terms, by identifying a further "weak continuity" property of the definable elements, and use this to establish that it is not fully abstract.