2015 Fiscal Year Research-status Report
ラムダ計算の型問題に対する可解性・非可解性の特徴付け
| 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 |
ラムダ計算は帰納的関数やチューリング機械と同様に万能な計算モデルであり，関数型プログラミング言語の基礎理論でもある．そして，関数の定義域・値域に相当する概念を形式化した型付きラムダ計算もあり，その基本問題として型検査・推論問題が重要である．
ラムダ計算の型問題の決定可能性はラムダ式の定式化・スタイルに大きく依存していることが明らかになってきた．ここで代表的なスタイルを持つ例としてチャーチ流とカリー流のラムダ式がある．そして，2階ラムダ計算の型問題の計算可能性を特徴付ける本質的な条件を解明するために，チャーチ流とカリー流の中間構造を持つラムダ式を導入した．まず，ラムダ式の構成子がインデックスを持つように拡張した抽象構文を与えて，一般化したラムダ式の概念を定義した．そして，インデックスの順序関係によりスタイルの順序関係が自然に定義されて，インデックスを具体化することにより様々なラムダ式の例が得られた．これにより，型問題とラムダ式の基本的性質は式のスタイルでパラメタ化されて，決定可能性・基本性質とスタイルの関係が定式化可能になった．そして，多相型ラムダ計算から存在型ラムダ計算への変換を導入した．この変換はスタイル間の順序関係を保存することにより，多相型ラムダ計算における型問題の決定不能性が存在型ラムダ計算のそれにも遺伝することが示された．
加えて，分担研究者・共同研究者と共に，古典論理の体系を直観主義論理に限定する自然な構文的条件について明らかにした．これまでは可能世界モデルを活用していたが，簡約だけで直観主義論理の証明かどうかを区別することが出来た．
さらに，共同研究者と共に，書換え系が合流性を持つための十分条件について解明した．これにより，複雑なシステムの合流性の証明方法の一つとして分割法の道が示された．
これらの実績により計算可能性・計算量に関係する研究の新たな展開が期待される．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
ラムダ式のスタイルと型問題の決定可能性・基本的性質に関する成果は京都大学数理解析研究所講究録に発表した．また，古典論理の構文的制約についての研究成果はStudia Logicaに発表された．さらに，書換え系の合流性に関する成果は日本ソフトウェア科学会で共同研究者により発表された．
2015年9月にはラムダ計算と論理の晩夏セミナーに参加して"On Least Upper Bounds on the Church-Rosser Theorem"に関する研究発表を行い研究テーマに関して深い議論を行った．2016年3月にはラムダ計算と論理の早春セミナーに参加をして”定理証明とモデル検査”に関する研究発表を行い参加研究者と議論を深めた．この情報はWebページでも公開されている．さらに，電子情報通信学会2016年総合大会のビッグデータの解析と基盤に関わる科学技術の俯瞰と展開のシンポジウムでは招待講演を行った．
2015年6月にPreining Norbert (JAIST) 先生を群馬大学に招聘して"Godel logics, Hyper Sequent Calculus, and Hyper Natural Deduction"と題する講演会を開催して情報交換を行った．2016年2月にはAart Middeldorp (University of Innsbruck, Austria)先生による“Automating the First-Order Theory of Rewriting for Left-Linear Right-Ground Rewrite Systems”と題する講演会を開催して研究テーマに関連する活発な議論を行った．
2015年11月には共同研究者のAleksy Schubert(Warsaw大学)先生を訪問して研究発表を行い研究テーマに関する共同研究を継続した．
|
| Strategy for Future Research Activity |
これまでの研究成果を積極的に発表していく計画である．
また，これまでに行った合流性に関する研究，2015年11月に行ったWarsaw大学でのSchubert博士との共同研究，及び2016年2月に行ったMiddeldorp先生との研究討議は，今後の研究の推進方策にとって極めて重要な結果をもたらした．さらに議論を重ねることにより，計算可能性・計算量に関する興味深く新たな研究の展開につながるものと期待される．
|
| Causes of Carryover |
本研究の目的をより精緻に達成するための研究の実施，国際会議への参加，及び論文投稿を行い，研究成果を効果的に発表するために次年度使用額が生じた．
|
| Expenditure Plan for Carryover Budget |
本研究目的に深く関連する国際会議への論文投稿，参加，及び研究成果の発表を行う計画である．
|
