SN Computer Science - An Experiment with Denotational Semantics
From the journal, SN Computer Science, comes a paper on An Experiment with Denotational Semantics. This paper is free to read (link) through open access.
Abstract
The paper is devoted to showing how to systematically design a programming language in “reverse order”, i.e., from denotations to syntax. This construction is developed in an algebraic framework consisting of three many-sorted algebras: of denotations, of an abstract syntax and of a concrete syntax. These algebras are constructed in such a way that there is a unique homomorphism from concrete syntax to denotations, which constitutes the denotational semantics of the language. Besides its algebraic framework, the model is set-theoretic, i.e., the denotational domains are just sets, rather than Scott’s reflexive domains. The method is illustrated by a layer-by-layer development of a virtual language Lingua: an applicative layer, an imperative layer (with recursive procedures) and an SQL layer where Lingua is regarded as an API (Application Programming Interface) for an SQL engine. The latter is given a denotational semantics as well. Mathematically, the model is based on so-called naive denotational semantics (Blikle and Tarlecki in Information processing 83. Elsevier Science Publishers B.V., North-Holland, 1983), Many-sorted algebras (Goguen et al. in J ACM 24:68–95, 1977), equational grammars (Blikle in Inform Control 21:134–147, 1972), and a three-valued predicate calculus based on a three-valued proposition calculus of McCarthy (A basis for a mathematical theory of computation, North Holland, 1967). Three-valued predicates provide an adequate framework for error-handling mechanisms and also for the development of a Hoare-like logic with clean termination (Blikle in Acta Inform 16:199–217, 1981) for Lingua. That logic is used in Blikle and Chrząstowski-Wachtel (Complete Unambiguous, https://doi.org/10.13140/rg.2.2.27499.39201/3, 2019) for the development of correctness-preserving programs’ constructors. This issue is, however, not covered by the paper. The langue is equipped with a strong typing mechanism which covers basic types (numbers, Booleans, etc.), lists, arrays, record and their arbitrary combinations plus SQL-like types: rows, tables, and databases. The model of types includes SQL-integrity constraints.
