PLS Lab

Recursive domain equations

Please expand.

Solving recursive domain equations

The 'standard' way of solving recursive domain equations is through domain theory.

Broadly speaking, there are three methods for solving them:

  1. The colimit method. This is the original method developed by Scott in the 1960s, and it involves taking a colimit of embedding-projection pairs. It is explained in detail in the classic paper by Smyth and Plotkin 1982. It yields a domain D and an isomorphism D \cong F(D).
  2. The information system method. This method is based on Scott's alternative presentation of domains as information systems. It has the advantage of giving a solution D that satisfies D = F(D) on the nose (!). It is described in Larsen and Winskel 1991.
  3. Through universal domains. This uses least fixed points of continuous operations on universal domains. It is described in Gunter and Scott 1990.

References

Smyth, M. B., and G. D. Plotkin. 1982. ‘The Category-Theoretic Solution of Recursive Domain Equations’. SIAM Journal on Computing 11 (4): 761–83. https://doi.org/10.1137/0211062.
@article{smyth_1982,
	title = {The {Category}-{Theoretic} {Solution} of {Recursive} {Domain} {Equations}},
	volume = {11},
	doi = {10.1137/0211062},
	number = {4},
	journal = {SIAM Journal on Computing},
	author = {Smyth, M. B. and Plotkin, G. D.},
	year = {1982},
	pages = {761--783}
}
Larsen, Kim Guldstrand, and Glynn Winskel. 1991. ‘Using Information Systems to Solve Recursive Domain Equations’. Information and Computation 91 (2): 232–58. https://doi.org/10.1016/0890-5401(91)90068-D.
@article{larsen1991,
	title = {Using information systems to solve recursive domain equations},
	volume = {91},
	doi = {10.1016/0890-5401(91)90068-D},
	pages = {232--258},
	number = {2},
	journaltitle = {Information and Computation},
	author = {Larsen, Kim Guldstrand and Winskel, Glynn},
	date = {1991},
}
Gunter, D., and D. S. Scott. 1990. ‘Semantic Domains’. In Handbook of Theoretical Comptuer Science, edited by J. van Leeuwen, B:633–74. Elsevier. https://doi.org/10.1016/B978-0-444-88074-1.50017-2. pdf
@incollection{gunter_1990,
	title = {Semantic Domains},
	volume = {B},
	pages = {633--674},
	booktitle = {Handbook of Theoretical Comptuer Science},
	publisher = {Elsevier},
	author = {Gunter, D. and Scott, D. S.},
	editor = {van Leeuwen, J.},
	date = {1990},
	doi = {10.1016/B978-0-444-88074-1.50017-2}
}