| 研究課題/領域番号 |
24700011
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
|
|---|
| キーワード | ラムダ計算 / 書き換え系 / 合流性 / 強正規化可能性 / ストリーム計算 / 型システム |
|---|
| 研究概要 |
本年度の研究では，ストリーム計算の計算モデルであるΛμ計算についてさらに研究を進め，以下の結果を得た．
1. Λμ-cons計算の提案．Λμ計算は，λ計算において成立していた多くの基本的性質を満たすことが，既にSaurinらによって証明されていたが，合流性が閉項に限られることなど，理論的に不充分な点があった．そこで，本研究ではΛμ計算の拡張として，明示的なストリーム表現を追加したΛμ-cons計算の等式論理と簡約体系を提案し，その基本的性質を証明した．とくに，体系の拡張によって既存の体系では表現が難しかった合理的な簡約規則を考えることができるため，既存のΛμ計算よりも単純な形で種々の性質が成立することを示した．具体的には，(1) 閉項に限らない合流性の証明，(2) Λμ計算に対する保守性，(3) 分離定理，を証明した．とくに(1)の証明においては，Dehornoyらと古森らによって独立に示された，一般化されたcomplete developmentを利用した合流性証明の手法を利用した．
2. Λμ-cons計算の型システムの研究．Λμ計算に対しては，Saurinやde'Liguoroによって型システムが提案されているが，これらのアイディアは自然にΛμ-cons計算にも適用できる．本研究では，とくにde'Liguoroの型システムを基本に，ストリームの型として制限された再帰型を含むような型システムを提案し，1で提案した簡約関係が (4) 主部簡約定理，(5) 強正規化可能性，を満たすことを示した．既存のΛμ計算の簡約体系は，型システムに対しては型依存の規則となっているが，本研究で与えた簡約体系は型に依存せずに定義され，(4)，(5)の基本定理を満たす．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
理論的な成果は予定以上の進捗を見せているが，実際のプログラミング言語への応用に関する研究は，未だ調査段階で明示的な結果が出ていない．
|
| 今後の研究の推進方策 |
理論的研究は現在の方向性を保ち，引き続き進める．さらに，実際のプログラミング言語への応用に関して，ストリーム変換などの技術との関連性などを調査し，言語設計に向けて研究を進める．
|
| 次年度の研究費の使用計画 |
計画していた海外での成果発表が中止となり、旅費支出の必要がなくなったため。
海外での成果発表旅費として使用する。
|
