| 研究課題/領域番号 |
15K00012
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
中澤 巧爾 名古屋大学, 情報科学研究科, 准教授 (80362581)
|
|---|
| 研究期間 (年度) |
2015-04-01 – 2018-03-31
|
| キーワード | ラムダ・ミュー計算 / 合流性 |
|---|
| 研究実績の概要 |
本年度は古典論理に対応する計算体系に関して、以下のような成果を得た。
1. 前年度に続き、計算体系の基本性質である合流性を証明するためのZ定理の拡張である合成的Z定理について調査した。その成果として、アカトーリとケスナーにより提案された値呼びラムダ計算の合流性が合成的Z定理を利用することによって証明できることを示した。この体系は、置換簡約に似た簡約規則を含んでおり、並行簡約を使った従来の証明方法や、通常のZ定理によって証明することは難しい。アカトーリとケスナーは、通常のベータ簡約と置換簡約の可換性によって証明しているが、本研究の結果は合成的Z定理を用いたさらに単純な証明を与えている。
2. 同値関係による剰余によって得られる体系の合流性について、Z定理を用いて証明する手法を考察した。同値関係のもとでの合流性（もしくはチャーチ・ロッサー性）は、同値関係の扱いによりいくつかの定式化が考えられるが、簡約の後の同値性を要求するチャーチ・ロッサー性（Church-Rosser modulo）と、同値関係による剰余集合上での簡約に関するチャーチ・ロッサー性ともに、Z性をもつ写像にさらに条件を付加することによってそれらの充分条件が与えられることを示した。とくに、後者の証明方法は、合成的Z定理の特殊な場合と考えられることを示した。
3. Saurinによるラムダ・ミュー計算のための木構造解釈について、前年度に与えた項による表現可能性のための必要充分条件の誤りを訂正し、その結果を高階書換え系に関する国際ワークショップである HOR 2016 において発表した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
興味深い理論的成果は得られているが、当初目標としていた、古典論理がもつ計算的側面としての無限構造については、ベーム木に関する知見が得られている他は重要な結果が得られていない。
|
| 今後の研究の推進方策 |
ベーム木がもつ無限構造と、ベラルディらによる古典論理に対する実現可能性解釈などとの関係性をより深く考察することにより、古典論理がもつ計算の無限概念について明らかにする。
|
| 次年度使用額が生じた理由 |
書籍購入費として2017年度に利用する必要があるため。
|
| 次年度使用額の使用計画 |
書籍購入費として使用する。
|
