PLS Lab

Domain Theory

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?

Basics

Those two areas are sometimes known by the two slogans domains individually, and domains collectively.

Domains individually

Partial orders and information

Let (D, \sqsubseteq) be a partial order. The meaning of x \sqsubseteq y is that "y is at least as informative as x." We sometimes call \sqsubseteq the information order. This intuition has its origins in viewing both x and y as partial functions. In that case, y is more defined than x, and agrees with it on input-output pairs where it is defined.

Completeness

To develop an understanding of recursion, domain theory requires a partial order to be complete. This completeness is used to define elements of "(co)limits" of finite processes.

The most common kind of completeness is directed completeness: a dcpo is a partial order that has suprema of directed subsets.

However, directed completeness is overkill for defining functions by recursion. For that it suffices to have \omega completeness: an \omega-cpo is a partial order that has suprema of \omega chains, i.e. sequences x_0 \sqsubseteq x_1 \sqsubseteq .... This is obviously weaker than directed completeness, but more than enough for many purposes.

Continuity

Please expand

Other topics

Please expand: approximation, compact elements, algebraic cpos, ...

Domains collectively

Please expand: solving domain equations

References

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}
}