Assignment Calculus: A Pure Imperative Language

We undertake a study of imperative computation. Beginning with a philosophical analysis of the distinction between imperative and functional language features, we define a (pure) imperative language as one whose constructs are (inherently) referentially opaque. We then give a definition of a computation language by identifying desirable properties for such a language.We present a new pure imperative computation language, Assignment CalculusAC. The main idea behind AC is based on the insight of T. Janssen that Montague’s modal operators of intension and extension, developed for the study of natural language semantics, are also useful for the semantics of programming language features such as assignments and pointers. AC consists of only four basic constructs, assignment ‘X: = t’, sequence ‘t;u’, procedure formation ‘¡t’ and procedure invocation ‘!t’. Two interpretations are given for AC: an operational semantics and a term-rewriting system; these interpretations turn out to be equivalent.