Designing languages with mathematical semantics

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

Poprawiono: wtorek, 20 sierpień 2024 15:34

Odsłony: 6072

By a mathematical semantics of a programming language, we shall mean a function that assigns meanings to programs. Since the 1970s, many researchers have started to believe that such semantics, to be “practical,” must be compositional, i.e., that the meaning of a whole must be a composition of the meanings of its parts. Later, such semantics were called denotational — the meaning of a program is its denotation — and for about two decades, researchers investigated the possibilities of defining denotational semantics for existing programming languages. The two most complete (although not fully formalized) such semantics were written in 1980 for Ada and CHILL in a metalanguage VDM. A little later, in 1987, Andrzej Blikle described a denotational semantics of a subset of Pascal. In the latter case, the metalanguage was MetaSoft, primarily based on VDM.

Unfortunately, none of these attempts created a denotational semantics of a widely used programming language. In our opinion, this situation was caused by the fact that for most language designers, the meaning of a program is a compiler’s behavior generated by the execution of this program. Also, programmers, when they explain to each other what a given piece of syntax “means”, describe what a compiler will “do” during the execution of this syntax. This machine-oriented understanding of program meanings has led to syntaxes that are not “suitable” for giving them denotational semantics. Technical arguments supporting this opinion are offered Sec. Sec. 6 and 7 of our book.

Independent of these problems, many researchers have found denotational models technically too complicated. Let us quote just one such opinion expressed by Cliff Johns in his book Understanding Programming Languages:

Denotational semantics is mathematically elegant but requires some fairly sophisticated mathematical concepts in order to describe programming languages of the sort that are used to build real applications.

Such opinions about denotational semantics were associated with their early-stage technicalities. One was a jump instruction goto, and the other — self-applicable procedures that can take themselves as parameters (Algol 60). The former had led to continuations, the latter to reflexive domains. Continuations were counterintuitive and reflexive domains — mathematically fairly complicated. Fortunately, although these mechanisms were considered necessary in the 1960s, they were abandoned ten years later.

In our approach, we use neither continuations nor reflexive domains. The idea of denotational semantics without these mechanisms was described by Andrzej Blikle and Andrzej Tarlecki in a joint paper in 1983. Besides the resignation of “historical” technicalities of denotational semantics, we use in our approach an idea proposed by Andrzej Blikle that in developing a programming language, we should start from its denotations DEN and derive from it a syntax SYN later. He proved that, in this case, a denotational semantics

DS : SYN → DEN

always exists and, additionally, is unique. Formally, SYN and DEN constitute many-sorted algebras, and the associated semantics DS is a (unique) homomorphism between them. As it turns out, there is a simple method — to a large extent algorithmizable — of deriving syntax from (the description of) denotations and, later, the semantics for both of them.

To illustrate our method, we designed a virtual programming language, Lingua. At the level of data structures, it includes booleans, integers, reals, texts, records, arrays, and their arbitrary combinations plus objects. It is equipped with a relatively strong mechanism of user-definable data types on the one hand and object types, i.e., classes, on the other. Control structures available in Lingua include structural instructions and multi-recursion procedures. The language has a complete error-reporting mechanism, by which we mean that every run-time error (except infinite looping) is signalized by an error message. Of course, errors will not occur in correct programs.

At the end of the book, we show how to enrich Lingua by two following mechanisms:

• an API for SQL,
• concurrency at the level of simple Petri nets.

Of course, Lingua is not developed/described in all detail since, in such a case, the book would hardly be readable. Our exercise with Lingua only illustrates a language-designing method that (hopefully) may be used in some future to design and implement practical programming languages.

Nevertheless, an experimental interpreter of Lingua has been developed by a group of students attending courses given commonly by Andrzej Blikle and Alex Schubert at the Department of Mathematics, Informatics, and Mechanics of Warsaw University in the academic years 2019/20 and 2020/21.  

Once we have a language with denotational semantics, we can define program-construction rules and prove their soundness. Our construction rules were sketched for the first time by Andrzej Blikle. In our book, they are developed for Lingua. Technically, the rules are used to build so-called metaprograms that syntactically include their specifications. Program construction rules guarantee that if we combine two or more correct programs into a new program or transform a correct program, we get a correct one again. Therefore, the correctness proofs of programs are implicit in how they are developed and in the soundness proofs of construction rules.