Projects per year
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 maytesting and musttesting denotational semantics for sequential functional languages with bounded and unbounded choice operators. We prove that these are computationally adequate, despite the noncontinuity of the musttesting semantics of unbounded nondeterminism. In the bounded case, we prove that our continuous models are fully abstract with respect to maytesting and musttesting 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.
Original language  English 

Article number  11 
Journal  Logical Methods in Computer Science 
Volume  17 
Issue number  4 
DOIs  
Publication status  Published  24 Nov 2021 
Keywords
 cs.LO
 F.3.2
Fingerprint
Dive into the research topics of 'Extensional and Intensional Semantics of Bounded and Unbounded Nondeterminism'. Together they form a unique fingerprint.Projects
 1 Finished

Semantic Types for Verified Program Behaviour
Engineering and Physical Sciences Research Council
28/02/14 → 31/07/17
Project: Research council