Program synthesis through Gödel's interpretation

Shigeki Goto

doi:10.1007/3-540-09541-1_32

Program synthesis through Gödel's interpretation

Shigeki Goto^*

^*この研究の対応する著者

研究成果: Conference contribution

4 被引用数 (Scopus)

抄録

This paper develops a program synthesis method based upon intuitionistic logic. This method is essentially an application of Gödel's interpretation which is also called Dialectica interpretation. By the use of Gödel's interpretation, it is possible to transform proof figures of intuitionistic number theory into primitive recursive functionals. The present concept is that primitive recursive functionals can be represented by LISP programs. Consequently, proof figures can be transformed into computer programs. To confirm this idea experimentally, a program synthesizer GDL0, which is a PDP-11 (DEC) program, is implemented. GDL0 experimental applications results are presented.

本文言語	English
ホスト出版物のタイトル	Mathematical Studies of Information Processing - Proceedings of the International Conference
出版社	Springer-Verlag
ページ	302-325
ページ数	24
ISBN（印刷版）	9783540095415
DOI	https://doi.org/10.1007/3-540-09541-1_32
出版ステータス	Published - 1979 1月 1
外部発表	はい
イベント	International Conference on Mathematical Studies of Information Processing, 1978 - Kyoto, Japan 継続期間: 1978 8月 23 → 1978 8月 26

出版物シリーズ

名前	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
巻	75 LNCS
ISSN（印刷版）	0302-9743
ISSN（電子版）	1611-3349

Other

Other	International Conference on Mathematical Studies of Information Processing, 1978
国/地域	Japan
City	Kyoto
Period	78/8/23 → 78/8/26

ASJC Scopus subject areas

理論的コンピュータサイエンス
コンピュータサイエンス（全般）

文献へのアクセス

10.1007/3-540-09541-1_32

他のファイルとリンク

引用スタイル

Goto, S. (1979). Program synthesis through Gödel's interpretation. In Mathematical Studies of Information Processing - Proceedings of the International Conference (pp. 302-325). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 75 LNCS). Springer-Verlag. https://doi.org/10.1007/3-540-09541-1_32

Program synthesis through Gödel's interpretation. / Goto, Shigeki.
Mathematical Studies of Information Processing - Proceedings of the International Conference. Springer-Verlag, 1979. p. 302-325 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 75 LNCS).

研究成果: Conference contribution

Goto, S 1979, Program synthesis through Gödel's interpretation. in Mathematical Studies of Information Processing - Proceedings of the International Conference. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 75 LNCS, Springer-Verlag, pp. 302-325, International Conference on Mathematical Studies of Information Processing, 1978, Kyoto, Japan, 78/8/23. https://doi.org/10.1007/3-540-09541-1_32

@inproceedings{b29256594e064ff2b9406838cece4f35,

title = "Program synthesis through G{\"o}del's interpretation",

abstract = "This paper develops a program synthesis method based upon intuitionistic logic. This method is essentially an application of G{\"o}del's interpretation which is also called Dialectica interpretation. By the use of G{\"o}del's interpretation, it is possible to transform proof figures of intuitionistic number theory into primitive recursive functionals. The present concept is that primitive recursive functionals can be represented by LISP programs. Consequently, proof figures can be transformed into computer programs. To confirm this idea experimentally, a program synthesizer GDL0, which is a PDP-11 (DEC) program, is implemented. GDL0 experimental applications results are presented.",

author = "Shigeki Goto",

year = "1979",

month = jan,

day = "1",

doi = "10.1007/3-540-09541-1_32",

language = "English",

isbn = "9783540095415",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer-Verlag",

pages = "302--325",

booktitle = "Mathematical Studies of Information Processing - Proceedings of the International Conference",

note = "International Conference on Mathematical Studies of Information Processing, 1978 ; Conference date: 23-08-1978 Through 26-08-1978",

}

TY - GEN

T1 - Program synthesis through Gödel's interpretation

AU - Goto, Shigeki

PY - 1979/1/1

Y1 - 1979/1/1

N2 - This paper develops a program synthesis method based upon intuitionistic logic. This method is essentially an application of Gödel's interpretation which is also called Dialectica interpretation. By the use of Gödel's interpretation, it is possible to transform proof figures of intuitionistic number theory into primitive recursive functionals. The present concept is that primitive recursive functionals can be represented by LISP programs. Consequently, proof figures can be transformed into computer programs. To confirm this idea experimentally, a program synthesizer GDL0, which is a PDP-11 (DEC) program, is implemented. GDL0 experimental applications results are presented.

AB - This paper develops a program synthesis method based upon intuitionistic logic. This method is essentially an application of Gödel's interpretation which is also called Dialectica interpretation. By the use of Gödel's interpretation, it is possible to transform proof figures of intuitionistic number theory into primitive recursive functionals. The present concept is that primitive recursive functionals can be represented by LISP programs. Consequently, proof figures can be transformed into computer programs. To confirm this idea experimentally, a program synthesizer GDL0, which is a PDP-11 (DEC) program, is implemented. GDL0 experimental applications results are presented.

UR - http://www.scopus.com/inward/record.url?scp=84867632620&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84867632620&partnerID=8YFLogxK

U2 - 10.1007/3-540-09541-1_32

DO - 10.1007/3-540-09541-1_32

M3 - Conference contribution

AN - SCOPUS:84867632620

SN - 9783540095415

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 302

EP - 325

BT - Mathematical Studies of Information Processing - Proceedings of the International Conference

PB - Springer-Verlag

T2 - International Conference on Mathematical Studies of Information Processing, 1978

Y2 - 23 August 1978 through 26 August 1978

ER -

Program synthesis through Gödel's interpretation

抄録

出版物シリーズ

Other

ASJC Scopus subject areas

文献へのアクセス

他のファイルとリンク

フィンガープリント

引用スタイル