On the development of a denotational model

Utworzono: poniedziałek, 29 kwiecień 2019 15:18

Poprawiono: poniedziałek, 30 wrzesień 2019 10:15

Odsłony: 8893

An experiment with denotational semantics, a published version, SN Computer Science (2020) 1:15 Download

DOI: 10.1007/s42979-019-0013-0

The published version constitutes a minor abbreviation of the following preprint. The latter also has a more reader-friendly layout.

An experiment with denotational semantics, a preprint 2019 Download

DOI: 10.13140/RG.2.2.31272.42249

Keywords:  set-theoretic denotational semantics, many-sorted algebras, three-valued predicate calculus, a denotational model of types, abstract syntax, concrete syntax.

This is a short-cut of this aspect of The book which concerns designing programming languages along with their denotational models.

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-Strachey 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.

The langue is equipped with a strong typing mechanism which covers basic types (numbers, Booleans and texts), lists, arrays, record and their arbitrary combinations plus SQL oriented types — rows, tables and databases. The model of types includes SQL integrity constraints.