2014 Fiscal Year Annual Research Report
| Project/Area Number |
24700011
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
|
|---|
| Project Period (FY) |
2012-04-01 – 2015-03-31
|
| Keywords | ラムダ計算 / 書き換え系 / 合流性 / ストリーム計算 |
|---|
| Outline of Annual Research Achievements |
引き続き、ストリーム計算の計算モデルであるラムダ・ミュー計算について研究を進め、とくに計算体系の合流性に関する以下の結果を得た。
1. ラムダ・ミュー計算のような、置換簡約と呼ばれるタイプの簡約規則を持つ計算体系の合流性に対する証明手法を提案した。合流性はプログラムの評価結果がその計算順序に依存しないことを示す基本的性質であるが、置換簡約を含むラムダ計算の合流性は既存の手法の単純な適用では証明できないことが指摘されていた。本研究では、Dehornoyや古森によるZ定理を合成関数に適用することにより、置換簡約を含むラムダ計算の合流性を比較的単純に証明できることを示した。また、同様の手法が、明示的代入を含むラムダ計算に対しても適用可能であることを示した。
2. 合流性は基本的な性質であるが、正規化性などの他の性質に比べて、とくにモジュラリティの面で証明が困難である。本研究では、1で提案した合成関数に対するZ定理をもとに、よりモジュラーな合流性の証明のための枠組みを与えた。とくに、Z性をもつ簡約体系に対して、その拡張がZ性をもつための充分条件を整理した。1の結果はこの枠組の一例になっている。
|
