Consistent Plotkin powerdomains. (Q471476): Difference between revisions

Powerdomains are well known objects in domain theory. The Plotkin powerdomain \(P(L)\) is the free dcpo-semilattice over a continuous domain \(L\). In applications joins and meets sometimes only exist under consistency conditions, i.e., if two elements have an upper bound, then a join is guaranteed to exist, and similarly for meets. Various powerdomain constructions can be adapted to obtain constructions under consistency conditions. In this article the authors locate a subset of the Plotkin powerdomain \(P(L)\) to obtain a consistent version of the Plotkin powerdomain for a Lawson compact continuous domain \(L\), freely adding consistent semilattice operations. The few preliminary concepts (i.e., a construction of the Plotkin powerdomain in terms of lenses) are quickly introduced and then the consistent Plotkin powerdomain is constructed as the set \(P_C(L)\); the consistent lenses in a Lawson compact continuous domain \(L\), which is a Scott closed subset of the Plotkin powerdomain \(P(L)\).