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

Research Project

Project/Area Number	16700012
Research Category	Grant-in-Aid for Young Scientists (B)
Allocation Type	Single-year Grants
Research Field	Fundamental theory of informatics
Research Institution	Kyoto University
Principal Investigator	中澤巧爾京都大学, 情報学研究科, 助手 (80362581)
Project Period (FY)	2004 – 2005
Project Status	Completed (Fiscal Year 2005)
Budget Amount *help	¥1,600,000 (Direct Cost: ¥1,600,000) Fiscal Year 2005: ¥800,000 (Direct Cost: ¥800,000) Fiscal Year 2004: ¥800,000 (Direct Cost: ¥800,000)
Keywords	古典論理 / カリーハワード同型 / コントロールオペレータ / シーケント計算 / 強正規化性 / CPS変換 / 置換簡約 / 強正規化可能性
Research Abstract	本研究では,昨年度に引き続きカリーハワード同型の意味で古典論理と対応する型理論を持つ計算体系に関して以下の点について研究を行なった. コントロールオペレータを含む計算体系のCPS変換を用いた強正規化性の証明コントロールオペレータを含む計算体系の型理論は,古典理論と対応することが知られているが,そのような計算体系に対しては強正規化性と呼ばれる性質が基本的な性質として期待される.コントロールオペレータを含む計算体系の強正規化性の証明法としてCPS変換を用いて既知の強正規化性に帰着させる方法が知られているが,この方法を用いた多くの既存の証明には継続消滅と呼ばれる同様の原因に依る誤りが含まれていることが既に指摘されている.本研究では,昨年度この誤りに対する解決として提案した新しいCPS変換であるCGPS変換を用いる方法をさらに改善し,より広い体系に適用可能な証明方法を提案した.実際に,昨年度の方法では解決できなかった,選言と置換簡約を含むような古典論理に対応する計算体系の強正規化性を,新しいCGPS変換による方法で解決した.さらに,本方法が値呼びλμ計算や一般的除去規則を含む自然演繹古典論理の強正規化性の証明にも適用できるなど,本方法がより広汎な体系に適用可能であることを示した. またこれとは別に本研究では,既に中澤と龍田によって提案されている増加項と呼ぼれる概念を用いても置換簡約を含む自然演繹古典論理の強正規化性を証明できることを示した.