ML Anthology

Towards a Mathematical Theory of Program Synthesis

Masahiko Sato
IJCAI 1979 pp. 757-762
/ijcai/1979/sato1979ijcai-mathematical/

Abstract

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.

Semantic Scholar

Cite

Text

Sato. "Towards a Mathematical Theory of Program Synthesis." International Joint Conference on Artificial Intelligence, 1979.

Markdown

[Sato. "Towards a Mathematical Theory of Program Synthesis." International Joint Conference on Artificial Intelligence, 1979.](https://mlanthology.org/ijcai/1979/sato1979ijcai-mathematical/)

BibTeX

@inproceedings{sato1979ijcai-mathematical,
  title     = {{Towards a Mathematical Theory of Program Synthesis}},
  author    = {Sato, Masahiko},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1979},
  pages     = {757-762},
  url       = {https://mlanthology.org/ijcai/1979/sato1979ijcai-mathematical/}
}