Embedding-projection pair

An embedding-projection pair (or e-p pair for short) is a structure that occurs in domain theory.

It is used in constructing solutions to recursive domain equations, and in the semantics of gradual types.

Definition

Let (D, \sqsubseteq_D) and (E, \sqsubseteq_E) be partial orders. An embedding-projection pair from D to E consists of a pair of monotone maps

\begin{aligned}
  e : D \to E
  &\quad&
  p : E \to D
\end{aligned}

such that

p \circ e = \textsf{id}_D
e \circ p \sqsubseteq \textsf{id}_E

References

The earliest reference that I've been able to trace is in Definition 3.6 of the classic D_\infty paper (which has also appeared as Oxford report PRG07):

Scott, Dana. 1972. ‘Continuous Lattices’. In Toposes, Algebraic Geometry and Logic, edited by F. W. Lawvere, 274:97–136. Lecture Notes in Mathematics. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/BFb0073967.

@inproceedings{scott_1972,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Mathematics}},
	title = {Continuous lattices},
	volume = {274},
	doi = {10.1007/BFb0073967},
	booktitle = {Toposes, {Algebraic} {Geometry} and {Logic}},
	publisher = {Springer Berlin Heidelberg},
	author = {Scott, Dana},
	editor = {Lawvere, F. W.},
	year = {1972},
	pages = {97--136}
}

E-p pairs are used to describe the semantics of gradual types in

New, Max S., and Amal Ahmed. 2018. ‘Graduality from Embedding-Projection Pairs’. Proceedings of the ACM on Programming Languages 2 (ICFP): 1–30. https://doi.org/10.1145/3236768.

@article{new_graduality_2018,
	title = {Graduality from embedding-projection pairs},
	volume = {2},
	doi = {10.1145/3236768},
	number = {ICFP},
	journal = {Proceedings of the ACM on Programming Languages},
	author = {New, Max S. and Ahmed, Amal},
	year = {2018},
	pages = {1--30},
	file = {Full Text:C\:\\Users\\tz20861\\Zotero\\storage\\THPRTHKS\\New and Ahmed - 2018 - Graduality from embedding-projection pairs.pdf:application/pdf},
}