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
More intriguing information
1. Peer Reviewed, Open Access, Free2. Reputations, Market Structure, and the Choice of Quality Assurance Systems in the Food Industry
3. Testing Hypotheses in an I(2) Model with Applications to the Persistent Long Swings in the Dmk/$ Rate
4. The name is absent
5. Migration and employment status during the turbulent nineties in Sweden
6. Popular Conceptions of Nationhood in Old and New European
7. Natural Resources: Curse or Blessing?
8. The name is absent
9. An Efficient Secure Multimodal Biometric Fusion Using Palmprint and Face Image
10. The name is absent