Towards a mathematical theory of program synthesis
Masahiko Sato · International Joint Conference on Artificial Intelligence · 1979
This paper attempts to set a theoretical foundation for Program Synthesis. A Programming language Progis introduced together with its interpretation in the semantic domain D. A formal system QFT, which is an extension of the Heyting arithmetic, is then introdced in order to express specifications formally. Roughly stated, the main result is: Given a QFT-Proof of the specification A[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 A[x,p[x]] can also be obtained. Since any program p in Prog always terminates, the above result estabilishes 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.