The initial lower and upper power domain constructions PL and PU commute under composition for all cpos. The common result PL (PU X) and PU (PL 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 PL and PU commute on all cpos X, and moreover, that the common result PL (PU X) = PU (PL 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)]
Reinhold Heckmann /