1997 Fiscal Year Annual Research Report

構成的プログラミング理論

Research Project

Project/Area Number	08458068
Research Institution	KYOTO UNIVERSITY
Principal Investigator	佐藤雅彦京都大学, 工学研究科, 教授 (20027387)
Co-Investigator(Kenkyū-buntansha)	竹内泉京都大学, 工学研究科, 助手 (20264583) 亀山幸義京都大学, 工学研究科, 助教授 (10195000) 龍田真京都大学, 理学研究科, 助教授 (80216994)
Keywords	構成的プログラミング / キャッチスロー機構 / 型理論
Research Abstract	研究代表者および研究分担者はそれぞれ独立して研究を行いながら、相互強力をするという形式により以下の各テーマに取り組んだ。一つ目は、キャッチスロー機構に対応する理論体系である。関数型プログラミング言語における制御機構であるキャッチスロー機構に対応する論理体系の構築、その性質の解析、その論理に対する表示的意味論についての研究を行った。その成果として、キャッチスロー機構に対応する推論規則を持った論理体系NJct、NKctを構築し、NJ、NKに対して保守的拡大であること、自然な計算規則が強正規化可能性を満たすこと、これらの体系を通じた構成的プログラミングが行えること、等を示した。また、古典論理による証明からのプログラム抽出についても基礎的な成果を得た。これらの研究は、主として研究代表者佐藤、研究分担者亀山が担当した。二つ目には、型なし理論に対する実現可能性解釈がある。型なしラムダ計算に基づく構成的理論に対して、実用可能性解釈を与え、構成的プログラミングへ応用する研究を行った。その成果として、この種の理論の中で最も有力な集合の理論に対して、従来の二重化変数の手法を大幅に改善した実現可能性解釈を与えた。また。単調オペレータに対する余帰納法に対する実現可能性解釈を与え、構成的プログラムへの具体的応用についても示した。これらの研究は、主として研究分担者龍田が担当した。三つ目には、多相型理論に対する構成的論理がある。二階の型理論であるジラールの体系Fおよびその周辺について、構成的プログラミングの観点から研究をおこなった。成果としては、Fにおけるパラメトリシティーを公理化した2階の体系に対する無矛盾性など種々の性質の証明,循環構造を持つ体系に対する型理論の枠組みでの定式化および体系Fへの解釈を与えたことなどがある。これらの研究は,主として研究分担者竹内が担当した。

Research Products
(6 results)

All Other

All Publications (6 results)

[Publications] Masahiko Sato: "Classical Brouwer-Heyting-Kolmogorov Interpretation" Lecture Notes in Artificial Intelligence. 1316. 176-196 (1997)
[Publications] Makoto Tatsuta: "Realizability of Monotone Coinducfive Definitions and its Application to Program Synthesis" Lecture Notes in Computer Science. (発表予定).
[Publications] Makoto Tatsuta: "Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis" Proc.13th IEEE Symposium on Logicin Computer Science. 13. (1998)
[Publications] Yukiyoshi Kameyama: "A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability" Proc.4th Austalasian Theory Symposium. 20-3. 183-197 (1998)
[Publications] Izumi Takeuti: "An Ayiomatic System of Parametricity" Lecture Notes in Computer Science. 1210. 354-372 (1997)
[Publications] Izumi Takeuti: "A Type Theory for Cyclic Structure" Proc.3rd Fuji Int'l Symp.on Func.and logic Programing. 3(発表予定). (1998)

1997 Fiscal Year Annual Research Report

構成的プログラミング理論

Principal Investigator

佐藤 雅彦 京都大学, 工学研究科, 教授 (20027387)

Research Products

[Publications] Masahiko Sato: "Classical Brouwer-Heyting-Kolmogorov Interpretation" Lecture Notes in Artificial Intelligence. 1316. 176-196 (1997)

[Publications] Makoto Tatsuta: "Realizability of Monotone Coinducfive Definitions and its Application to Program Synthesis" Lecture Notes in Computer Science. (発表予定).

[Publications] Makoto Tatsuta: "Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis" Proc.13th IEEE Symposium on Logicin Computer Science. 13. (1998)

[Publications] Yukiyoshi Kameyama: "A Classical Catch/Throw Calculus with Tag Abstractions and its Strong Normalizability" Proc.4th Austalasian Theory Symposium. 20-3. 183-197 (1998)

[Publications] Izumi Takeuti: "An Ayiomatic System of Parametricity" Lecture Notes in Computer Science. 1210. 354-372 (1997)

[Publications] Izumi Takeuti: "A Type Theory for Cyclic Structure" Proc.3rd Fuji Int'l Symp.on Func.and logic Programing. 3(発表予定). (1998)

佐藤雅彦京都大学, 工学研究科, 教授 (20027387)