| 研究課題/領域番号 |
25400192
|
|---|
| 研究種目 |
基盤研究(C)
|
| 研究機関 | 群馬大学 |
|---|
研究代表者 |
藤田 憲悦 群馬大学, 理工学研究院, 准教授 (30228994)
|
|---|
| 研究分担者 |
古森 雄一 千葉大学, 理学(系)研究科(研究院), 名誉教授 (10022302)
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2016-03-31
|
| キーワード | ラムダ計算 / 型検査 / 型推論 / 決定可能性 / チャーチ流 / カリー流 |
|---|
| 研究概要 |
ラムダ計算はチューリング機械と同様に万能な計算理論であり，関数型プログラミング言語の基礎理論でもある．そして，型付きラムダ計算の基本問題として型検査問題と型推論問題がある．
ここで，ラムダ計算の型問題の決定可能性はラムダ式の定式化に依存している．そこで，2階ラムダ計算の型検査問題，型推論問題の計算可能性・不可能性を特徴付ける本質的な条件を解明するために，決定可能であるチャーチ流と決定不能であるカリー流との間に位置する中間的な構造を持つラムダ式を導入した．そして，そのような式のスタイルでパラメータ化された一般的な型問題の定式化を与えた．
まず，式のスタイルに依存する問題と式のスタイルに依存しない問題との切り分けを行った．型が与えられた時に，その型を持つ閉ラムダ式を見つける問題は，知られている限りにおいて式のスタイルに無関係である．一方，型推論，型検査問題の決定可能性は，ラムダ式のスタイルに大きく依存することになった．そして，中間構造の観点から，型推論・型検査問題を決定可能・決定不能とする境界的条件を同定することができた．ここでは，ラムダ抽象の定義域の型が重要な役割を担っていることが明らかになった．そして，関数変数を含む方程式を解く問題である2階の単一化問題と密接に関係していた．
これにより，一般的には決定不能である型検査・型推論問題を決定可能とする付加情報に関するより詳細な研究が大きな意味を持ってくると考えられ，型推論，型検査問題の本質的な難しさの解明につながる．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
ラムダ式のスタイと型問題の決定可能性についての関係を，チャーチ流とカリー流の間の中間構造の観点から研究して，型問題が決定不能となる構造，及び決定可能となる構造を明らかにした．これらの成果は，国際会議RTA2013（オランダ），日本ソフトウェア科学会第３０回大会（東京大学），日本数学会2014年度年会（学習院大学）などで発表を行った．さらに，雑誌数学（岩波書店），京都大学数理解析研究所講究録（RIMS共同研究：証明論と複雑性）でも論文発表を行った．
加えて，共同研究者による成果として，カリー流の体系のSubject reduction性，concreat domainの層的表現，及び古典論理の体系であるλρ計算とチャーチ・ロッサーの定理の新しい証明法についても結果が得られた．これらは，論文誌（Information Processing Letters，Studia Logica, Tsukuba Journal of Mathematics），数理解析研究所講究録（RIMS共同研究：証明論と複雑性），日本数学会秋季総合分科会（愛媛大学）等でそれぞれ発表を行った．
|
| 今後の研究の推進方策 |
カリー・ハワード同型のもとでは，きちんと型の付くラムダ式は直観主義論理の証明のコードになっている．そして，ラムダ式に含まれている証明の情報を一つずつ捨象することにより，チャーチ流からカリー流のラムダ式に段階的に変換することができる．このアイディアに従って，ラムダ式のスタイルの観点から中間的な構造を持つラムダ式の特徴付けをより詳細に行う．特に，（１）ラムダ抽象のドメイン情報，（２）型の作用を表現しているホール，（３）多相型のインスタンス情報，（４）型束縛子の情報．以上の４種類の構成子に着目して，チャーチ流とカリー流の間に微細構造を統一的に導入する．そして，型問題の決定可能性を支配している本質的情報を解明する．
|
