{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:02Z","timestamp":1753894382394,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T00:00:00Z","timestamp":1637712000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We give extensional and intensional characterizations of functional programs\nwith nondeterminism: as structure preserving functions between biorders, and as\nnondeterministic sequential algorithms on ordered concrete data structures\nwhich compute them. A fundamental result establishes that these extensional and\nintensional representations are equivalent, by showing how to construct the\nunique sequential algorithm which computes a given monotone and stable\nfunction, and describing the conditions on sequential algorithms which\ncorrespond to continuity with respect to each order. We illustrate by defining\nmay-testing and must-testing denotational semantics for sequential functional\nlanguages with bounded and unbounded choice operators. We prove that these are\ncomputationally adequate, despite the non-continuity of the must-testing\nsemantics of unbounded nondeterminism. In the bounded case, we prove that our\ncontinuous models are fully abstract with respect to may-testing and\nmust-testing by identifying a simple universal type, which may also form the\nbasis for models of the untyped {\\lambda}-calculus. In the unbounded case we\nobserve that our model contains computable functions which are not denoted by\nterms, by identifying a further \"weak continuity\" property of the definable\nelements, and use this to establish that it is not fully abstract.<\/jats:p>","DOI":"10.46298\/lmcs-17(4:11)2021","type":"journal-article","created":{"date-parts":[[2021,11,25]],"date-time":"2021-11-25T21:00:25Z","timestamp":1637874025000},"source":"Crossref","is-referenced-by-count":0,"title":["Extensional and Intensional Semantics of Bounded and Unbounded Nondeterminism"],"prefix":"10.46298","volume":"Volume 17, Issue 4","author":[{"given":"James","family":"Laird","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2021,11,24]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/8749\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/8749\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T20:16:58Z","timestamp":1687292218000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/4043"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,24]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-17(4:11)2021","relation":{"has-preprint":[{"id-type":"arxiv","id":"1710.10203v3","asserted-by":"subject"},{"id-type":"arxiv","id":"1710.10203v2","asserted-by":"subject"},{"id-type":"arxiv","id":"1710.10203v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1710.10203","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1710.10203","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2021,11,24]]},"article-number":"4043"}}