zbMATH — the first resource for mathematics

Lower and upper power domain constructions commute on all cpos. (English) Zbl 0748.68038
Summary: The initial lower and upper power domain constructions \({\mathcal P}_ \vee\) and \({\mathcal P}_ \wedge\) commute under composition for all cpos (K. E. Flannery and J. J. Martin [J. Comput. Syst. Sci. 40(2), 125-135 (1990; Zbl 0699.06008)]). The common result \({\mathcal P}_ \vee({\mathcal P}_ \wedge X)\) and \({\mathcal P}_ \wedge({\mathcal P}_ \vee X)\) is the free frame over the cpo \(X\).
Our proof differs completely from the proof of K. E. Flannery and J. J. Martin [loc. cit.]. It uses algebraic methods and does not rely on any explicit representations of the power domains.

68Q55 Semantics in the theory of computing
06B35 Continuous lattices and posets, applications
Full Text: DOI
[1] Flannery, K.E.; Martin, J.J., The Hoare and smyth power domain constructors commute under composition, J. comput. system sci., 40, 125-135, (1990) · Zbl 0699.06008
[2] Heckmann, R., Power domain constructions, () · Zbl 0769.08005
[3] Heckmann, R., Power dornain constructions, Sci. comput. programming, (1991), to appear
[4] R. Heckmann, An upper power domain construction in terms of strongly compact sets, accepted by MFPS ’91.
[5] Hennessy, M.C.B.; Plotkin, G.D., Full abstraction for a simple parallel programming language, (), 108-120 · Zbl 0457.68006
[6] Hoofman, R., Powerdomains, ()
[7] Vickers, S., Topology via logic, () · Zbl 0668.54001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.