×

Logic of domains. (English) Zbl 0854.68058

Basel: Birkhäuser. 259 p. (1991).
The advent of high level programming languages has made it necessary to give precise meaning of their syntaxes. It turned out the new features of these languages e.g. recursive procedures were less amenable to the analysis by the means of the conventional operational semantics. Hence, by the end of the 1960’s, Scott and Strachey developed a new type of semantics called denotational. Their approach is based on the idea that the semantics of a programming language should be formally specified by a small number of basic mathematical construction of partial orders of information. The mathematical part of their method is called domain theory and the methodology which uses domain theory to specify the meaning of a programming language is called denotational semantics.
A denotational semantics of a programming language is usually given by assigning to each piece of program an element in a domain. Due to the possible self-applicative nature of some parts of programs e.g. recursive procedures, the domains must sometimes have special properties. Typically, such a domain \(D\) must be isomorphic to its function space \([D \to D]\). This is not possible in a naive set-theoretical setting because exponentiation increases cardinality of sets. Scott has shown that the cardinality problem can be overcome in the framework of complete partial orders by restricting the function space to (in some sense continuous) functions. By this way, Scott described a denotational semantics of the un-typed \(\lambda\)-calculus, a typical system of self-application. Since then, domain theory has advanced to the extent that it is possible to give denotational semantics to most programming languages.
The monograph under review is a revised version of the author’s PhD Thesis submitted to the University of Cambridge in 1989. It presents the author’s work on the logical aspects of SFP domains (i.e. directed limits of Sequence of Finite inductive Partial orders) and stable domains. The author tries to convey to the reader the state of knowledge on logic of domains and to point to some directions of future research.
The monograph is divided in two parts. The first part, Chapters 1 to 5 is concerned with the category of SFP domains. It gives basic facts about these domains, introduces an information-system representation for SFP domains endowed with a Gentzen-style entilment. It gives rise to a category of Strongly Finite Sequent Structures (SFSS category) which is shown to be equivalent to the category of SFP domains. Various constructions e.g. function space, power domains and complete partial order are given for the SFSS category as a step towards the logics of SFP domains. The \(\mu\)-calculus is studied which lays an extra structure upon assertions making the logic corresponding to a domain more expressive.

MSC:

68Q55 Semantics in the theory of computing
68-02 Research exposition (monographs, survey articles) pertaining to computer science
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite