Applications of compactness in the Smyth powerdomain of streams
type: Item
instance of: scholarly article
title: Applications of compactness in the Smyth powerdomain of streams
zbMATH Open document ID: 0652.68027
DOI: 10.1016/0304-3975(88)90042-4
author: Erik de Vink
author: John-Jules Meyer
published in: Theoretical Computer Science
publication date: 1988-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 68Q99
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 54D30
zbMATH DE Number: 4064458
zbMATH Keywords: compactness
zbMATH Keywords: powerdomains of streams
zbMATH Keywords: Smyth ordering
zbMATH Keywords: denotational semantics
zbMATH Keywords: concurrency
zbMATH Keywords: continuity
zbMATH Keywords: logic programming
reviewed by: Wiktor Bartol
MaRDI profile type: Publication
full work available at URL: 0304-3975(88)90042-4
OpenAlex ID: W2080849782
cites work: A continuous semantics for unbounded nondeterminism
cites work: Q3899466
cites work: Linear time and branching time semantics for recursion with merge
cites work: Q3681901
cites work: Q3745260
cites work: Infinite streams and finite observations in the semantics of uniform concurrency
cites work: Q3347277
cites work: Process algebra for synchronous communication
cites work: Q3657421
cites work: Q3681910
cites work: Stream Processing Functions
cites work: Q5520521
cites work: Q4150804
cites work: Q3339245
cites work: Merging regular processes by means of fixed-point theory
cites work: Hiding in stream semantics of uniform concurrency
cites work: A calculus of communicating systems
cites work: Q3221399
cites work: Q3857704
cites work: Specification-oriented semantics for communicating processes
cites work: A Powerdomain Construction
cites work: Q3290875
cites work: Power domains
cites work: Recursion Equations as a Programming Language
description: scientific article; zbMATH DE number 4064458