Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Apt, K.R., Plotkin, G.D.: Countable nondeterminism and random assignment. Journal of the ACM 33(4), 724–767 (1986)
Berry, G.: Stable models of typed λ-calculi. In: Proceedings of the 5th International Colloquium on Automata, Languages and Programming. LNCS, vol. 62, pp. 72–89. Springer, Heidelberg (1978)
Cartwright, R., Felleisen, M.: Observable sequentiality and full abstraction. In: Proceedings of POPL 1992 (1992)
Curien, P.-L., Winskel, G., Plotkin, G.: Bistructures, bidomains and linear logic. In: Milner Festschrift, MIT Press, Cambridge (1997)
Di Gianantonio, P., Honsell, F., Plotkin, G.: Uncountable limits and the lambda calculus. Nordic Journal of Computing 2(2), 126–145 (1995)
Harmer, R., McCusker, G.: A fully abstract games semantics for finite non-determinism. In: Proceedings of the Fourteenth Annual Symposium on Logic in Computer Science, LICS 1999, IEEE Computer Society Press, Los Alamitos (1998)
Laird, J.: Bistability: an extensional characterization of sequentiality. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, Springer, Heidelberg (2003)
Laird, J.: Sequentiality in bounded bidomains. Fundamenta Informaticae 65, 173–191 (2005)
Lassen, S.B., Pitcher, C.: Similarity and bisimilarity for countable non-determinism and higher-order functions. Electronic Notes in Theoretical Computer Science 10 (1997)
Levy, P.B.: Infinite trace equivalence. In: Games for Logic and Programming Languages, pp. 195–209 (2005)
Longley, J.: Universal types and what they are good for. In: Domain Theory, Logic and Computation: Proceedings of the 2nd International Symposium on Domain Theory, Kluwer, Dordrecht (2004)
Plotkin, G.: Lectures on predomains and partial functions, Notes for a course given at the Center for the study of Language and Information, Stanford (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Laird, J. (2006). Bidomains and Full Abstraction for Countable Nondeterminism. In: Aceto, L., Ingólfsdóttir, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11690634_24
Download citation
DOI: https://doi.org/10.1007/11690634_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33045-5
Online ISBN: 978-3-540-33046-2
eBook Packages: Computer ScienceComputer Science (R0)