James Laird - Extensional and Intensional Semantics of Bounded and Unbounded Nondeterminism

lmcs:4043 - Logical Methods in Computer Science, November 24, 2021, Volume 17, Issue 4 - https://doi.org/10.46298/lmcs-17(4:11)2021
Extensional and Intensional Semantics of Bounded and Unbounded NondeterminismArticle

Authors: James Laird

    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.


    Volume: Volume 17, Issue 4
    Published on: November 24, 2021
    Accepted on: August 31, 2021
    Submitted on: November 2, 2017
    Keywords: Computer Science - Logic in Computer Science,F.3.2

    Consultation statistics

    This page has been seen 1432 times.
    This article's PDF has been downloaded 325 times.