The initial lower and upper power domain constructions P_L and P_U commute under composition for all cpos. The common result P_L (P_U X) and P_U (P_L X) is the free frame over the cpo X.

In [FM90], the lower and upper power domain constructions were shown to commute on bounded complete algebraic cpos. For the proof, these cpos were represented by information systems. In this paper, we show that the two constructions P_L and P_U commute on all cpos X, and moreover, that the common result P_L (P_U X) = P_U (P_L X) is the free frame over X. Our proof differs completely from the proof of [FM90]. It uses algebraic methods and does not rely on any explicit representations of the power domains.

Key words: Formal semantics, domain theory, power domains, algebraic theories, cpo's, free frame over a cpo

[Paper.ps.gz (7p, 36k, reformatted)]