Applications of compactness in the Smyth powerdomain of streams (Q1107301)

The paper shows the crucial role of compactness in the theory of powerdomains of streams with the Smyth ordering, used in denotational semantics of concurrency. Compactness is characterized here by two properties of powerdomains: closedness and boundedness. The latter notion, introduced in the paper, concerns a certain finiteness condition on the set of truncations of streams and is analogous to the finite- branching condition on trees. It is shown that boundedness (instead of the finiteness of the set of atomic actions) is sufficient to prove the continuity of operators on streams. This generalization also leads to a relaxation of the compacity requirements for continuity: only stream-sets that are to act as denotations need be compact. Further, the authors consider functions on sets of streams that are lifted from continuous functions on streams and prove their continuity. These results can be applied in several areas of denotational semantics of programming languages, as it is illustrated by examples concerning uniform imperative concurrency, stream programming and logic programming.