2014 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
ラムダ式のスタイルと2階存在型ラムダ計算の型問題の決定可能性を明らかにした．中間構造の一つであるタイプフリー・スタイルの型問題の決定可能性を2階単一化問題の観点から
研究して，叙述的な体系でも型問題が決定不能となることを示した．そして，この研究成果はTheoretical Computer Scienceの雑誌に発表した．さらに，この海外共同研究者A.Schubert（Warsaw大学）を群馬大学に招聘して型問題に関する議論を集中的に行った．
ラムダ式のスタイルの数学的定義を与えるために，インデックス付きの抽象構文を導入した．そして，抽象構文のインスタンスとして具体的なラムダ式のスタイルを定義して，その上に順序構造を与えて，ラムダ式のスタイルでラムダ式に関する性質や問題の分類を行った．この結果は，2014年度 京都大学数理解析研究所 研究集会「証明論・計算論とその周辺」で発表を行った．また，「ラムダ計算と論理の早春セミナー」を企画して，草津セミナーハウスで開催をした．ここでは，千葉大学，群馬県立女子大学，京都大学，法政大学の研究者，及び，東北大学，東京工業大学，京都大学，群馬大学の大学院生との議論，最新の情報交換も行った．このために，特に大学院生の参加旅費の一部については分担研究者からその補助を行った．
加えて，分担研究者，及び共同研究者による成果として次の成果が得られた．
分配具象領域と領域層の圏論的同等性に関する考察が倉田（法政大学）により与えられて，2014年度日本数学会秋季総合分科会，および2014年度 京都大学数理解析研究所 研究集会「証明論・計算論とその周辺」で発表が行われた．また，置換簡約を含むラムダ計算の合流性をシステマッテックに証明する手法について中澤（京都大学）と研究を行い第17回プログラミングおよびプログラミング言語ワークショップ(PPL2015)にてポスター発表を行った．
|
| Strategy for Future Research Activity |
インデックス付き抽象構文に基づきラムダ式の微細構造を統一的に記述可能なスタイルを導入したが，この観点から型問題の決定可能性を支配している本質的情報を解明する．ここで，叙述的な型レベルからの考察は部分構造論理における広い意味での計算・論理的性質に関する研究経験のある古森（千葉大学）と共同で行う．また，微細構造における計算と論理の意味論的観点からの考察は，計算構造に対する意味論を長く研究してきた倉田（法政大学）と共同で行う．これにより一般的には決定不応である型問題を決定可能とする付加情報に関する詳細な研究が意味を持ってくると考えられ，型問題に限らずラムダ式の性質・問題の本質的な難しさの原因の解明につながるものと期待している．そして，計算可能・不可能に対するより具体的な知見が得られるものと考えられる．
加えて，中澤（京都大学）と行った置換簡約を含むラムダ計算の合流性に関する研究は今後理論的に整備していくことが期待される．
さらに時間があるならば，「ラムダ計算と論理のセミナー」を企画・開催して，可能ならば旅費等のサポートを行い，関連する研究領域の研究者との議論を深め，情報交換を活発に行う．また，関係する情報は，メイリングリストに流したり，Webページから積極的に公開をする．
|
| Causes of Carryover |
分担者が計画的かつ効率的に執行にあたっていたが，予期せずに最終的に残高が発生してしまった．
|
| Expenditure Plan for Carryover Budget |
研究の遂行には支障がなく，次年度に繰り越しを行い分担者が計画的に執行する．
|
