Domain theory is a branch of order theory that can be used to provide semantics for programming languages with recursion.
Domain theory is primarily about two things:
Many open problems in domain-theoretic modelling of programming languages are given in [Jung et al. 1996].
Which of these have been resolved since?
Those two areas are sometimes known by the two slogans domains individually, and domains collectively.
Let be a partial order.
The meaning of is that " is at least as informative as ." We sometimes call the information order.
This intuition has its origins in viewing both and as partial functions. In that case, is more defined than , and agrees with it on input-output pairs where it is defined.
In order to define things by recursion in a partial order, some notion of completeness is required. The most common one is directed completeness.
Definition. is directed-complete (colloquially, a dcpo) if every directed set has a least upper bound.
Let be a nonempty subset of . is directed whenever every pair has an upper bound in , i.e. an element such that and .
Directedness means that every pair of elements of carries compatible information: there is at least one element that is more informative than both (and hence, the information that and carry is not contradictory). Thus, is "going somewhere": its elements can be seen as approximants that can be combined into better approximants. Directed-completeness means that every such "set with a purpose" has a least upper bound, i.e. a least informative element fitting the "specification" given by all the approximants.
Alternatively, we can replace directed-completeness with -completeness.
is -complete if any increasing chain of elements of has a least upper bound .
The 's can be thought of as a sequence of increasingly informative elements of , and the least upper bound can be thought of as the "limit" of this sequence, i.e. the least informative object that contains all the information carried by the approximations .
In the presence of the axiom of choice, and restricting to dcpos with countable bases, directed-completeness and -completeness coincide. Without choice or countable bases, dcpos are the right definition, and -cpos look bizarre: see 2.2.4 in [Abramsky and Jung 1994].
Please expand
Please expand: approximation, compact elements, algebraic cpos, ...
Please expand: solving domain equations
Abramsky, Samson, and Achim Jung. 1994. ‘Domain Theory’. In Handbook of Logic in Computer Science, edited by Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum, 3:1–168. Oxford University Press. pdf
@incollection{abramsky_domain_1994,
title = {Domain {Theory}},
volume = {3},
url = {https://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf},
booktitle = {Handbook of {Logic} in {Computer} {Science}},
publisher = {Oxford University Press},
author = {Abramsky, Samson and Jung, Achim},
editor = {Abramsky, Samson and Gabbay, Dov M. and Maibaum, Thomas S. E.},
year = {1994},
pages = {1--168}
}
Stoltenberg-Hansen, V., I. Lindström, and E. R. Griffor. 1994. Mathematical Theory of Domains. Cambridge: Cambridge University Press. https://doi.org/10.1017/CBO9781139166386.
@book{stoltenberg-hansen_1994,
title = {Mathematical {Theory} of {Domains}},
isbn = {978-1-139-16638-6},
publisher = {Cambridge University Press},
author = {Stoltenberg-Hansen, V. and Lindstr\"{o}m, I. and Griffor, E. R.},
year = {1994},
doi = {10.1017/CBO9781139166386}
}
Stoy, Joseph E. 1977. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press.
Schmidt, David A. 1986. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon. http://people.cs.ksu.edu/~schmidt/text/densem.html.
Winskel, Glynn. 2001. The Formal Semantics of Programming Languages: An Introduction. Foundations of Computing. MIT Press.
Fiore, M. P., A. Jung, E. Moggi, P. O’Hearn, J. Riecke, G. Rosolini, and I. Stark. 1996. ‘Domains and Denotational Semantics: History, Accomplishments and Open Problems’. Bulletin of the European Association for Theoretical Computer Science 59: 227–56. [pdf]
@article{jung_1996,
title = {Domains and {Denotational} {Semantics}: {History}, {Accomplishments} and {Open} {Problems}},
volume = {59},
journal = {Bulletin of the European Association for Theoretical Computer Science},
author = {Jung, A. and Fiore, M. P. and Moggi, E. and O'Hearn, P. and Riecke, J. and Rosolini, G. and Stark, I.},
year = {1996},
pages = {227--256}
}