2016 Fiscal Year Annual Research Report
On decidability and undecidability of type-related problems of lambda-calculi
| Project/Area Number |
25400192
|
|---|
| Research Institution | Gunma University |
|---|
Principal Investigator |
藤田 憲悦 群馬大学, 大学院理工学府, 准教授 (30228994)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
古森 雄一 千葉大学, 大学院理学研究科, 名誉教授 (10022302)
倉田 俊彦 法政大学, 経営学部, 教授 (40311899)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | ラムダ計算 / 型検査 / 型推論 / チャーチ・ロッサーの定理 |
|---|
| Outline of Annual Research Achievements |
ラムダ計算はチューリング機械と等価で万能な計算モデルであり，関数型プログラミング言語の基礎理論でもある．そして，関数の定義域・値域に相当する概念を形式化した型付きラムダ計算があり，その基本問題として型推論問題と型検査問題がある．ここで，ラムダ計算の型問題の決定可能性はラムダ式の定式化に大きく依存していることが明らかになってきた．
そこで，２階ラムダ計算の型問題の計算可能性を特徴付ける本質的な条件を解明するために，チャーチ流とカリー流の中間的構造を持つラムダ式を導入した．そして，この定式化の観点からラムダ計算の基本問題の分類を行った．当初に想定していた，型検査問題，型推論問題に加えて，さらに，簡約に関する基本的性質についてもその研究対象を拡大していった．そして，ラムダ計算のチャーチ・ロッサーの定理が主張している合流点に至るまでの簡約列の長さに関する上限を与えことができた．この問題は，KetemaとSimonsenによる2013年のACM Transactions on Computational Logicの論文で未解決問題となったいたものである．なお，この研究成果は，国際会議において発表を行った．
さらに，分担研究者の倉田（法政大学）は，高階逐次アルゴリズムの分解に関する研究を行って，数学会で研究発表をした．また，中澤（名古屋大学）との共同研究により，ラムダ計算の合流性をシステマチックに証明する手法に関する研究を継続して，簡約列の長さとの関係付けを行った．そして，この研究結果は，日本ソフトウェア科学会で研究発表された．
これらの研究手法をさらに推し進めることにより，型問題に限らず様々な基本問題の可解性，及び計算量を特徴づける新たな研究の展開やその枠組みの構築につながることが大いに期待される．
|
