2015 Fiscal Year Research-status Report
| Project/Area Number |
15K00012
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
中澤 巧爾 名古屋大学, 情報科学研究科, 准教授 (80362581)
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Keywords | 古典論理 / 合流性 / 交叉型 |
|---|
| Outline of Annual Research Achievements |
本年度は古典論理に対応する計算体系に関して、主にその基礎理論に関する研究を行ない、以下のような成果を得た。
1. 計算体系の基本性質である合流性を証明するための手法であるZ定理に関してさらに調査を行なった。変換を用いた合流性の証明手法をZ定理に応用し、変換の条件を少し強めることによってある体系のZ定理を他の体系に帰着できることを示した。古典論理に対応する計算体系を含む、幅広い計算体系の合流性証明に利用できること考えられる。
2. 古典シーケント計算に対応する計算体系の交叉型理論を構築した。シーケント計算の対称性を反映した計算体系に対する交叉型理論として、完全性、すなわち簡約の前後で型が保存される性質をもつものを構築し、さらにこの型理論において強正規化性を特徴づけることができることを証明した。
3. SaurinによるΛμ計算のための木構造解釈について、項による表現可能性のための必要充分条件を与えた。従来のラムダ計算の木構造解釈、すなわちベーム木による解釈では、幅の上限がωであるような無限木として項が表現されたが、Λμ計算では幅の上限がω^2の無限木として表現されることがSaurinによって示されている。本研究では、一般のこのような木構造のうち、Λμ項を表現するための必要充分条件を与えた。これはSaurinが国際会議FLOPS 2010において提示した問題に対する解を与えるものである。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
計画していた拡張ラムダ・ミュー計算の型システムやその外延的モデルについて大きな知見を得ることはできなかったが、その調査の過程において、ベーム木意味論に関する結果や、交叉型理論に関する結果など興味深い関連の成果を得ることができた。
|
| Strategy for Future Research Activity |
引き続き、計画に沿って研究を行なう。とくに、拡張ラムダ・ミュー計算の理論について今年度得られた知見をもとに、そのベーム木の無限構造の性質を明らかにし、古典論理と計算の無限概念に関して既に知られている結果との関連を調べる。また、拡張ラムダ・ミュー計算の型システムと古典論理との関連についてさらなる調査を続ける。
|
| Causes of Carryover |
国際会議における成果発表と旅費として2016年度に使用する必要が発生したため。
|
| Expenditure Plan for Carryover Budget |
前年度未使用分は、国際会議における成果発表のための旅費、および会議参加費として利用する。
|
