TY - GEN
T1 - Bidomains and full abstraction for countable nondeterminism
AU - Laird, James
PY - 2006
Y1 - 2006
N2 - We describe a denotational semantics for a sequential functional language with random number generation over a countably infinite set (the natural numbers), and prove that it is fully abstract with respect to may-and-must testing. Our model is based on biordered sets similar to Berry's bidomains, and stable, monotone functions. However, (as in prior models of unbounded non-determinism) these functions may not be continuous. Working in a biordered setting allows us to exploit the different properties of both extensional and stable orders to construct a Cartesian closed category of sequential, discontinuous functions, with least and greatest fixpoints having strong enough properties to prove computational adequacy. We establish full abstraction of the semantics by showing that it contains a simple, first-order "universal type-object" within which all types may be embedded using functions defined by (countable) ordinal induction.
AB - We describe a denotational semantics for a sequential functional language with random number generation over a countably infinite set (the natural numbers), and prove that it is fully abstract with respect to may-and-must testing. Our model is based on biordered sets similar to Berry's bidomains, and stable, monotone functions. However, (as in prior models of unbounded non-determinism) these functions may not be continuous. Working in a biordered setting allows us to exploit the different properties of both extensional and stable orders to construct a Cartesian closed category of sequential, discontinuous functions, with least and greatest fixpoints having strong enough properties to prove computational adequacy. We establish full abstraction of the semantics by showing that it contains a simple, first-order "universal type-object" within which all types may be embedded using functions defined by (countable) ordinal induction.
UR - http://www.scopus.com/inward/record.url?scp=33745768576&partnerID=8YFLogxK
UR - http://dx.doi.org/10.1007/11690634_24
U2 - 10.1007/11690634_24
DO - 10.1007/11690634_24
M3 - Chapter in a published conference proceeding
AN - SCOPUS:33745768576
SN - 9783540330455
T3 - Lecture Notes in Computer Science
SP - 352
EP - 366
BT - Foundations of Software Science and Computation Structures
A2 - Aceto, L.
A2 - Ingolfsdottir, A.
PB - Springer Verlag
CY - Berlin, Germany
T2 - 9th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006
Y2 - 25 March 2006 through 31 March 2006
ER -