| 研究概要 |
本研究では,カリーハワード同型の意味で古典論理と対応する型理論を持つ計算体系に関して以下の二点の研究を行なった.
1.コントロールオペレータを含む計算体系の強正規化可能性の証明
コントロールオペレータを含む計算体系の型理論は,古典論理と対応することが知られている.このような体系の強正規化可能性の証明法としてCPS変換と呼ばれる変換を用いるものがあるが,従来試みられていたCPS変換を用いた証明方法は継続消滅と呼ばれる同じ原因による誤りが含まれている.本研究では,それらの誤りを修正し,CPS変換を用いた強正規化可能性の証明を与えた.さらに,この証明法を実際にde Grooteによる例外処理を表現する計算体系λ^→_<cxn>とParigotによるλμ計算という二つの異なる計算体系に適用することにより,本研究の提案する証明法が,古典論理に対応する計算体系の強正規化可能性の証明に広く応用できる汎用性のあるものであること示した.
2.シーケント計算とそのカット除去に対応する計算体系
シーケント計算に対する項割当て体系,およびカット除去に対応するような操作的意味論に関する研究を行なった.シーケント計算における対称性を,プログラムにおける値と継続の対称性に対応させることにより,「値渡し」と「継続渡し」をともに自由に行なえるような非決定的な計算体系を構築した.この計算手順はシーケント計算のカット除去手続きに対応するものとなることが期待されるが,現段階ではその対応関係は成立していない.
|
