Bidomains and full abstraction for countable nondeterminism

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publicationProceedings of the 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software , ETAPS 2006 Vienna, Austria, March 2006
EditorsL. Aceto, A. Ingolfsdottir
Place of PublicationBerlin, Germany
PublisherSpringer Verlag
Pages352-366
Number of pages15
ISBN (Print)9783540330455
DOIs
Publication statusPublished - 2006
Event9th 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 - Vienna, Austria
Duration: 25 Mar 200631 Mar 2006

Publication series

NameLecture Notes in Computer Science
Volume3921

Conference

Conference9th 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
CountryAustria
CityVienna
Period25/03/0631/03/06

Fingerprint

Nondeterminism
Semantics
Countable
Cartesian Closed Category
Random number Generation
Denotational Semantics
Discontinuous Functions
Fixpoint
Monotone Function
Natural number
Fruit
Proof by induction
Language
Random number generation
First-order
Testing
Model
Abstraction
Object

ASJC Scopus subject areas

  • Computer Science(all)
  • Biochemistry, Genetics and Molecular Biology(all)
  • Theoretical Computer Science

Cite this

Laird, J. (2006). Bidomains and full abstraction for countable nondeterminism. In L. Aceto, & A. Ingolfsdottir (Eds.), Foundations of Software Science and Computation Structures: Proceedings of the 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software , ETAPS 2006 Vienna, Austria, March 2006 (pp. 352-366). (Lecture Notes in Computer Science ; Vol. 3921 ). Berlin, Germany: Springer Verlag. https://doi.org/10.1007/11690634_24

Bidomains and full abstraction for countable nondeterminism. / Laird, James.

Foundations of Software Science and Computation Structures: Proceedings of the 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software , ETAPS 2006 Vienna, Austria, March 2006. ed. / L. Aceto; A. Ingolfsdottir. Berlin, Germany : Springer Verlag, 2006. p. 352-366 (Lecture Notes in Computer Science ; Vol. 3921 ).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Laird, J 2006, Bidomains and full abstraction for countable nondeterminism. in L Aceto & A Ingolfsdottir (eds), Foundations of Software Science and Computation Structures: Proceedings of the 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software , ETAPS 2006 Vienna, Austria, March 2006. Lecture Notes in Computer Science , vol. 3921 , Springer Verlag, Berlin, Germany, pp. 352-366, 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, Vienna, Austria, 25/03/06. https://doi.org/10.1007/11690634_24
Laird J. Bidomains and full abstraction for countable nondeterminism. In Aceto L, Ingolfsdottir A, editors, Foundations of Software Science and Computation Structures: Proceedings of the 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software , ETAPS 2006 Vienna, Austria, March 2006. Berlin, Germany: Springer Verlag. 2006. p. 352-366. (Lecture Notes in Computer Science ). https://doi.org/10.1007/11690634_24
Laird, James. / Bidomains and full abstraction for countable nondeterminism. Foundations of Software Science and Computation Structures: Proceedings of the 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software , ETAPS 2006 Vienna, Austria, March 2006. editor / L. Aceto ; A. Ingolfsdottir. Berlin, Germany : Springer Verlag, 2006. pp. 352-366 (Lecture Notes in Computer Science ).
@inproceedings{ef6aa7b61dc44149b374d420aad19368,
title = "Bidomains and full abstraction for countable nondeterminism",
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.",
author = "James Laird",
year = "2006",
doi = "10.1007/11690634_24",
language = "English",
isbn = "9783540330455",
series = "Lecture Notes in Computer Science",
publisher = "Springer Verlag",
pages = "352--366",
editor = "L. Aceto and A. Ingolfsdottir",
booktitle = "Foundations of Software Science and Computation Structures",

}

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 - Conference contribution

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

ER -