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 is a cpo, there is no good way to equip the powerset with a cpo structure. Instead, a somewhat more involved construction, involving finitely generated subsets of , is required. There are then multiple ways of ordering those.
Each such way gives rise to a powerdomain construction. There are three main ones:
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 over a cpo , we need to be algebraic. Thus, is a functor on the category of algebraic cpos. However, that category is not cartesian closed, which leads to other issues.
The first powerdomain construction was due to Gordon Plotkin, and appeared in a 1976 SICOMP article:
Plotkin, Gordon D. 1976. ‘A Powerdomain Construction’. SIAM Journal on Computing 5 (3): 452–87.
@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}
}
Plotkin, Gordon. 1983. Domains (Pisa Notes). [ps]
@online{plotkin_1983,
title = {Domains ({Pisa} {Notes})},
url = {https://homepages.inf.ed.ac.uk/gdp/publications/Domains_a4.ps},
author = {Plotkin, Gordon},
year = {1983}
}
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}
}