Introduction to Metric Semantics

Our focus is on the semantics of programming and specification languages. Over the years, various different approaches to give semantics to these languages have been put forward. We restrict ourselves to the operational and the denotational approach, two main streams in the field of semantics.

Two notions which play an important role in this course are (non)determinism and (non)termination. Nondeterminism arises naturally in concurrent languages and it is a key concept in specification languages. Nontermination is usually caused by recursive constructs which are crucial in programming.

The operational models are based on labelled transition systems. The definition of these systems is given by structural induction on the language. This approach has been advocated in

G.D. Plotkin. A Structural Approach to Operational Semantics. Report DAIMI FN-19, Aarhus University, Aarhus, September 1981.

Metric spaces are an essential ingredient of our denotational models. We exploit the metric structure to model recursive constructs and to define operators on infinite entities. Furthermore, we also employ the metric structure to relate operational and denotational models for a given language. A textbook on this metric approach, covering a large variety of programming notions and providing illuminating bibliographic remarks, is

J.W. de Bakker and E.P. de Vink. Control Flow Semantics. Foundations of Computing Series. The MIT Press, Cambridge, 1996.

Besides metric spaces, various other mathematical structures, including ordered spaces, are used in denotational semantics, as is shown in, e.g.,

G. Winskel. The Formal Semantics of Programming Languages: an introduction. Foundations of Computing Series. The MIT Press, Cambridge, 1993.

On the basis of four toy languages, we develop some general theory for defining operational and denotational semantic models and for relating them. This theory is applicable to a wide variety of languages. We start with a very simple deterministic and terminating imperative programming language. By adding the recursive while statement, we obtain a deterministic and nonterminating language. Next, we augment the language with the parallel composition resulting in a bounded nondeterministic and nonterminating language. Finally, we add some timed constructs. We obtain an unbounded nondeterministic and nonterminating specification language.