古典論理に基く構成的プログラミングの実現

1998 Fiscal Year Annual Research Report

• Project/Area Number: 10480061
• Research Institution: Kyoto University
• Principal Investigator: 佐藤 雅彦 京都大学, 情報学研究科, 教授 (20027387)
• Co-Investigator(Kenkyū-buntansha): 竹内 泉 京都大学, 情報学研究科, 助手 (20264583) ; 亀山 幸義 京都大学, 情報学研究科, 助教授 (10195000)
• Keywords: 構成的プログラミング / 古典論理 / 算術 / キャッチ・スロー機構

Research Abstract

本研究の目的は、古典論理に基く構成的プログラミングに関する理論的な研究をすることである。これは即ち、古典論理に基く算術等の論理体系から関数型言語によるプログラムを抽出することの研究である。研究代表者および研究分担者はそれぞれ独立して研究を行いながら、相互協力をするという形式により以下の各テーマに取り組んだ。研究代表者・佐藤雅彦は、関数型言語の中での環境というものに注目し、その理論的基礎を研究する為に、λεという計算体系を提案した。関数型言語では環境とは、変数への値の割当をする機構である。λεは、関数型言語の理論的計算モデルであるλ計算に、環境を扱えるように改良されたものである。これは1999年4月にイタリアで開催される第4回「型付ラムダ計算とその応用」国際学会にて発表される。研究分担者・亀山は、古典論理の推論規則に対応する計算規則に対して、計算体系としてよい性質が充されるかどうかを研究した。そして、古典論理の推論規則に対応する各種の計算規則に対して強正規化可能性を証明する統一的な証明方法があることが解った。この成果は1998年10月に仙台で開催された第15回「記号論理と情報科学」研究集会にて発表された。研究分担者・竹内は、古典論理に基く算術等の弱い論理体系に於て、通常の数学がどのように展開されるかを研究した。そして、多項式時間計算可能性に対応する算術の理論で、自己相似図形に関する幾つかの定理が証明されることが解った。この成果は1998年-8月にチェコで開催された「98年計算可能性解析学」国際会議にて発表された。

Research Products

• [Publications] 佐藤雅彦、桜井貴文、ロッド・バーストール: "Explicit Environments" Typed Lambda Calculus And Aplications. (発表予定). (1999)
• [Publications] 鴨浩靖・河邑紀子・竹内泉: "Hausdorff Dimension & Computational Complexity" INFORMATIK BERICHTE, Compulerity in Analysis Fern University. 235-8. 41-50 (1998)