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