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