Towards a Mathematical Theory of Program Synthesis

Abstract

This paper attempts to set a theoretical foundation for Program Synthesis. A programming language Prog is introduced together with its interpretation in the semantic domain D. A formal system QFT, which is an extension of the Heyting arithmetic, is then introduced in order to express specifications formally. Roughly stated, the main result is: Given a QFT-proof of the specification ~x~zA[x,z], it is possible to construct a program p such that A[x,p[x]] is true in D for any input x. Moreover, a formal proof of ~xA[x,p[x]] can also be obtained. Since any program p in Prog always terminates, the above result establishes the total correctness of the synthesized program at the same time. Finally, it is shown that any program p in Prog can be faithfully simulated by means of LISP.