シーケント計算に基づく型システムの研究

昨年度までの研究によって,古典論理の自然演繹における正規化手続きとシーケント計算におけるカット除去手続きの対応関係を明らかにすることができた.これを利用して,古典論理に対して,強正規化性と合流性をみたす局所ステップカット除去手続きを提案した.この結果は,国際ワークショップ(CL＆C'06)で発表し,現在,学術雑誌に投稿中である.一方,直観主義論理に対する通常のシーケント計算において,自然演繹の正規化手続きがどのようなカット除去手続きに対応するのかについても明らかにした.これにより,シーケント計算に対する項計算は,項構造と簡約関係の双方についてラムダ計算の保存拡大であることが明らかになった.この結果は,国際会議(LPAR'06)で発表した.このカット除去手続きは合流性をみたさないが,ラムダ計算のベータ簡約を模倣する能力を保ちつつ制限を加えたカット除去手続きの合流性を証明した.この結果は,国際会議(CiE'07)で発表する予定である.さらに,直観主義論理のシーケント計算から得られる項計算に対して,インターセクション型システムを定義し,その型付け可能性によって強正規化性を特徴づけることができることを示した.そこで用いられる手法は,従来知られていた明示的代入計算とインターセクション型に関する手法を大幅に簡略化したものである.この結果は,国際会議(RTA'07)で発表する予定である.この他,直観主義論理のクリプキ意味論を一般化することによって得られる様々な論理の述語拡大に対して,ツリーシーケント計算の手法を用いて完全性を証明した.この結果は,国際会議(TABLEAUX'07)と国際学術雑誌(Logic Journal of the IGPL)で発表する予定である.

昨年度までの研究によって,古典論理の自然演繹における正規化手続きとシーケント計算におけるカット除去手続きの対応関係を明らかにすることができた.これを利用して,古典論理に対して,強正規化性と合流性をみたす局所ステップカット除去手続きを提案した.この結果は,国際ワークショップ(CL＆C'06)で発表し,現在,学術雑誌に投稿中である.一方,直観主義論理に対する通常のシーケント計算において,自然演繹の正規化手続きがどのようなカット除去手続きに対応するのかについても明らかにした.これにより,シーケント計算に対する項計算は,項構造と簡約関係の双方についてラムダ計算の保存拡大であることが明らかになった.この結果は,国際会議(LPAR'06)で発表した.このカット除去手続きは合流性をみたさないが,ラムダ計算のベータ簡約を模倣する能力を保ちつつ制限を加えたカット除去手続きの合流性を証明した.この結果は,国際会議(CiE'07)で発表する予定である.さらに,直観主義論理のシーケント計算から得られる項計算に対して,インターセクション型システムを定義し,その型付け可能性によって強正規化性を特徴づけることができることを示した.そこで用いられる手法は,従来知られていた明示的代入計算とインターセクション型に関する手法を大幅に簡略化したものである.この結果は,国際会議(RTA'07)で発表する予定である.この他,直観主義論理のクリプキ意味論を一般化することによって得られる様々な論理の述語拡大に対して,ツリーシーケント計算の手法を用いて完全性を証明した.この結果は,国際会議(TABLEAUX'07)と国際学術雑誌(Logic Journal of the IGPL)で発表する予定である.