Program Semantics and Classical Logic
Reinhard Muskens
Abstract
In the tradition of Denotational Semantics one usually lets program
constructs take their denotations in reflexive domains, i.e. in domains
where self-application is possible. For the bulk of programming con-
structs, however, working with reflexive domains is an unnecessary
complication. In this paper we shall use the domains of ordinary clas-
sical type logic to provide the semantics of a simple programming
language containing choice and recursion. We prove that the rule of
Scott Induction holds in this new setting, prove soundness of a Hoare
calculus relative to our semantics, give a direct calculus C on programs,
and prove that the denotation of any program P in our semantics is
equal to the union of the denotations of all those programs L such that
P follows from L in our calculus and L does not contain recursion or
choice.
1 Introduction
In this paper we translate a simple but non-trivial imperative programming
language into an axiomatic extension of classical second order logic. Since
classical logic comes with a modeltheoretic interpretation, we get an interpre-
tation for our programming language too, as we may identify the denotation
of any programming construct in a given model with the denotation of its
translation in that model. The resulting semantics thus assigns a mathemat-
ical object to each programming construct in each model.
This last aspect makes the paper fall within the tradition of Denotational
Semantics [21, 20, 3, 19, 13, 22]. But we shall deviate considerably from
the usual denotational approach by not making any use of the Scott domains
which are ubiquitous in that tradition. A characteristic property of such
domains is that they can be reflexive, i.e. a domain D can be isomorphic
1