Denotational Semantics of IMP

Abstract

In this chapter we give a more abstract, purely mathematical semantics to IMP, called denotational semantics. The operational semantics is close to the memory-based, executable machine-like view: given a program and a state, we derive the state obtained after the execution of that program. The denotational semantics takes a program and returns the transformation function over memories associated with that program: given an initial state as the argument, the final state is returned as the result. Since functions will be written in some fixed mathematical notation, i.e., they can also be regarded as “programs” of a suitable formalism, we can say that, to some extent, the operational semantics defines an “interpreter” of the language (given a program and the initial state it returns the final state obtained by executing the program), while the denotational semantics defines a “compiler” for the language (from programs to functions, i.e., programs written in a more abstract language). We conclude the chapter by reconciling the equivalences induced by the operational and the denotational semantics and by stating the principle of computational induction.

The point is that, mathematically speaking, functions are independent of their means of computation and hence are “simpler” than the explicitly generated, step-by-step evolved sequences of operations on representations. (Dana Scott)