Advice on Structuring Compilers and Proving them Correct (1973)

F. Lockwood Morris

(Introductory paragraphs:)

The purpose of this paper is to advise an approach (and to support that advice by discussion of an example) towards achieving a goal first announced by John McCarthy: that compilers for higher-level programming lnguages should be made completely trustworthy by proving their correctness. The author believes that the compiler-correctness problem can be made much less general and better-structured than the unrestricted program-correctness problem; to do so will of course entail restricting what a compiler may be.

The essence of the present advice is that a proof of compiler correctness should be the proof that a diagram of the form

(A rectangular diagram, with top, left, right, bottom arrows labelled `compile', `source semantics', `target semantics', `decode', which I do not presently know how to reproduce in HTML)

commutes. It is of course not very startling to regard a compiler as a function assigning target language programs to source language programs; however, the rest of the diagram does have a non-vacuous content: it insists that `semantics' should be an actual function assigning definite mathematical objects (`meanings') to programs - usually partial functions of some fairly complicated type. That is, it rejects interpretive forms of semantic definition, such as those provided by the Vienna definition method, or by sets of reduction rules of some form, which only provide for any given pair of program and input data some prescription for finding the output (if any). The bottom, `decoding' side of the diagram is merely an allowance for the highly probable eventuality that the meanings of target language programs are not identical with, but only represent in some adequate way the meanings of the source language programs from which they were compiled.

There is one crucial elaboration to what has just been said: it is further advised that the corners of the diagram should be made not merely sets but algebras and that the arrows should be homomorphisms. Specifically, heterogeneous (universal) algebras, as defined in (1), seem to be the appropriate tool. Briefly, a heterogeneous algebra has a number of sets of elements of different types, its phyla, which are connected by a family of operations, each taking a finite number of arguments of specified types and producing a result of specified type. For a homomorphism to exist between two heterogeneous algebras, their operations must have corresponding argument and result types under a suitable pairwise correspondence of the phyla, and for a set of functions between the corresponding phyla to constitute a homomorphism, it must respect the operations in the same way as does a conventional homomorphism, e.g. of groups.

(The remainder of the paper is ``devoted to putting some flesh on the maxims just given by applying them to the statement and partial proof of a simple compiler correctness problem.'')

1. G. Birkhoff and J. D. Lipson, ``Heterogeneous Algebras'', J. Combinatorial Theory 8, pp. 115-133 (1970).