古典論理に基づく非決定的計算体系

点击翻译按钮获取中文摘要

本研究では,昨年度に引き続きカリーハワード同型の意味で古典論理と対応する型理論を持つ計算体系に関して以下の点について研究を行なった.コントロールオペレータを含む計算体系のCPS変換を用いた強正規化性の証明コントロールオペレータを含む計算体系の型理論は,古典理論と対応することが知られているが,そのような計算体系に対しては強正規化性と呼ばれる性質が基本的な性質として期待される.コントロールオペレータを含む計算体系の強正規化性の証明法としてCPS変換を用いて既知の強正規化性に帰着させる方法が知られているが,この方法を用いた多くの既存の証明には継続消滅と呼ばれる同様の原因に依る誤りが含まれていることが既に指摘されている.本研究では,昨年度この誤りに対する解決として提案した新しいCPS変換であるCGPS変換を用いる方法をさらに改善し,より広い体系に適用可能な証明方法を提案した.実際に,昨年度の方法では解決できなかった,選言と置換簡約を含むような古典論理に対応する計算体系の強正規化性を,新しいCGPS変換による方法で解決した.さらに,本方法が値呼びλμ計算や一般的除去規則を含む自然演繹古典論理の強正規化性の証明にも適用できるなど,本方法がより広汎な体系に適用可能であることを示した.またこれとは別に本研究では,既に中澤と龍田によって提案されている増加項と呼ぼれる概念を用いても置換簡約を含む自然演繹古典論理の強正規化性を証明できることを示した.