Program Semantics and Classical Logic

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

1   2   3   4   >>

More intriguing information