Coherently complete cpo

A cpo (D, \sqsubseteq) is coherently complete just if all of its coherent subsets have a least upper bound.

A subset X \subseteq D is coherent just if any two x, y \in X have an upper bound in D (not necessarily in X!).

Relevance

All domains appearing in the model of PCF are coherently complete Streicher 2006.

Comparison

Coherent complete cpos are similar to that of consistently complete cpos.

However, consistently complete cpos require every subset with an upper bound (or, equivalently, every finite subset with an upper bound) to have a supremum.

In contrast, coherent complete cpos do not ask that the entire subset X \subseteq D has an upper bound, only that any two of its elements have an upper bound. Thus, the coherence here is pairwise rather than collective.

References

@book{streicher_domain-theoretic_2006,
	title = {Domain-theoretic Foundations of Functional Programming},
	publisher = {World Scientific},
	author = {Streicher, Thomas},
	date = {2006},
	file = {Streicher - 2006 - Domain-theoretic Foundations of Functional Program.pdf:/Users/lambdabetaeta/Zotero/storage/CWBJKQDH/Streicher - 2006 - Domain-theoretic Foundations of Functional Program.pdf:application/pdf},
}