to, and can in fact be identified with, the function space [D → D] of all
continuous functions from D to D. This guarantees that any object d ∈
D is also a function d : D → D and hence that it is meaningful to talk
about d(d). Scott domains thus support the interpretation of self-application
and in fact are essential for the interpretation of functional languages which
are based on the untyped lambda calculus and in which self-application is
possible. But, although there are some imperative languages which allow
self-application, it seems that the bulk of constructs normally encountered
in imperative languages, including iteration and recursion, can be treated
without the use of reflexive domains. As we shall see in this paper, imperative
programs containing iteration and recursion can be interpreted in the models
of classical type logic via a translation into the second-order fragment of that
logic.
Classical type logic itself then can function as a kind of universal specifi-
cation language in the design of programming languages: In order to specify
the intended semantics of some construct, the language designer may simply
write down its intended logical translation. On a more theoretical level, we
consider it an advantage to be able to describe the semantics of programming
constructs with the help of the language and the models which also underly
mainstream mathematical logic. True, there are important differences be-
tween the semantics of mathematics and the semantics of programming, in
the sense that the model theory of, say, the natural numbers is ‘static’, while
the model theory of a program must needs be ‘dynamic’. But these differ-
ences, important as they are, should not blind us to the fact that the two
forms of semantics are essentially one. We shall model the difference be-
tween ‘static’ and ‘dynamic’ semantics as a difference in type here. While
static theories are sets of sentences, i.e. closed terms of type t, the logical
translation of a program must have a more complex type. If we choose to
treat programs as relations between input and output states, as we shall do
here (other choices are very well possible), the type of programs becomes
s × s → t. It is this type difference which constitutes the difference between
static and dynamic semantics, but the type difference is already present in
standard logic.
Treating the semantics of a programming language with the help of clas-
sical logic should not be construed as being in opposition to the effort of
Dynamic Logic ([18, 7]), the modal logic of programs, however. In Dynamic
Logic one typically studies logics containing only a very few programming
constructs. The goals here are of a purely logical nature and the primary