Powerdomains

A powerdomain construction is a way of giving semantics to programs that combine recursion and nondeterminism.

In order to give denotational semantics to programs with recursion we use domain theory. Likewise, to give denotational semantics to programs with nondeterminism, we usually use a powerset: programs denote elements of a powerset, so that each program can be modelled as producing zero, one, or more outputs.

So, how can we mix recursion with nondeterminism? The problem is that powersets and complete partial orders do not make a good pair. If (D, \sqsubseteq_D) is a cpo, there is no good way to equip the powerset \mathcal{P}(D) with a cpo structure. Instead, a somewhat more involved construction, involving finitely generated subsets of D, is required. There are then multiple ways of ordering those.

Each such way gives rise to a powerdomain construction. There are three main ones:

• the Hoare powerdomain
• the Smyth powerdomain
• the Plotkin powerdomain

Categories closed under powerdomains

Perhaps one of the most unpleasant aspect of powerdomains is that they require additional conditions on the domain that they are based on, over and above just being a cpo.

For example, to constuct the Plotkin powerdomain \mathcal{P}(D) over a cpo D, we need D to be algebraic. Thus, \mathcal{P} is a functor on the category of algebraic cpos. However, that category is not cartesian closed, which leads to other issues.

References

• Cornell CS 6100 (2013) lecture notes on powerdomains

• The first powerdomain construction was due to Gordon Plotkin, and appeared in a 1976 SICOMP article:

@article{plotkin_1976,
	title = {A powerdomain construction},
	volume = {5},
	number = {3},
	journal = {SIAM Journal on Computing},
	author = {Plotkin, Gordon D.},
	year = {1976},
	pages = {452--487}
}

• A 'textbook' exposition of powerdomains can be found in Gordon Plotkin's "Pisa" notes:

@online{plotkin_1983,
	title = {Domains ({Pisa} {Notes})},
	url = {https://homepages.inf.ed.ac.uk/gdp/publications/Domains_a4.ps},
	author = {Plotkin, Gordon},
	year = {1983}
}

• For a modern exposition based on algebraic theories see the survey

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