Axiomatic Synthesis of a Prime Number Generator and Other Number Theoretic Programs Using a Program Calculus

We examine the problem of Automatic Programming, in which a computer program is generated from a nonprocedural definition of the desired functionality. We propose a system in which programs are represented by 1st order Predicate Calculus wffs. A set of 8 universal rules of inference is introduced, which transform a fixed set of known primitive programs into new programs, in the same manner as classic axiomatic theorem-proving. It is shown that existing Automatic Programming systems either require the user to write a program in a high level language, or generate only a few specific trivial programs. Furthermore, to synthesize programs with loops requires a proof by induction using quantifiers, a task that many researchers consider to be unsolved and not amenable to automation. We avoid this problem by treating programs as primitive objects, with the details of generic loops hidden within axiomized primitive programs. We formally synthesize several programs from number theory, including prime number testing and generation. We note that prior research in the generation of programs of this complexity has been limited to informal discussion of a prime number generator. We show that our approach is also applicable to programs that retrieve from databases. An extension of this system, using 2nd order predicate calculus to represent properties of formal systems, has been used to synthesize theorems from Recursion Theory, Incompleteness in Logic, and the Semantic Paradoxes