zbMATH — the first resource for mathematics

The Hoare and Symth power domain constructors commute under composition. (English) Zbl 0699.06008
Summary: This paper examines the composition of the Smyth and Hoare power domains \((P_ S\) and \(P_ H)\) applied over the class of consistently complete algebraic partial orders represented by Scott’s category of information systems. It is proposed that both orders of applications yield equivalent domains. This is motivated by interpreting data elements in the Smyth as disjunction of propositions and those in the Hoare as conjunctions (as suggested by Scott), giving the two conjunctive-disjunctive forms for each of the double power domains. Then, using elementary category theory, it is shown that the images of any object under \(P_ S\circ P_ H\) and under \(P_ H\circ P_ S\) are isomorphic, and hence that both constructors are equivalent as functors.

06B35 Continuous lattices and posets, applications
68P05 Data structures
68Q55 Semantics in the theory of computing
Full Text: DOI
[1] MacLane, S., Categories for the working Mathematician, (), 7-19
[2] Martin, J.J., FAD—A functional programming language that supports abstract data types, (), 247-262
[3] Okie, E., An implementation of a typed functional programming language, ()
[4] Plotkin, G., A powerdomain construction, SIAM J. comput., 5, 452-487, (1976) · Zbl 0355.68015
[5] Scott, D., Domains for denotational semantics, (), (corrected and expanded version of a paper prepared for ICALP ’82) · Zbl 0495.68025
[6] Shamir, A.; Wadge, W., Data types as objects, () · Zbl 0353.68050
[7] Smyth, M., Power domains, J. comput. system sci., 16, No. 1, 23-36, (1978) · Zbl 0391.68011
[8] Winskel, G., A note on powerdomains and modality, (), 505-514
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.