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.
Let and be partial orders. An embedding-projection pair from to consists of a pair of monotone maps
such that
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}
}
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},
}