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

Research Project

Project/Area Number	17700003
Research Category	Grant-in-Aid for Young Scientists (B)
Allocation Type	Single-year Grants
Research Field	Fundamental theory of informatics
Research Institution	Tohoku University
Principal Investigator	菊池健太郎東北大学, 電気通信研究所, 助手 (40396528)
Project Period (FY)	2005 – 2006
Project Status	Completed (Fiscal Year 2006)
Budget Amount *help	¥1,000,000 (Direct Cost: ¥1,000,000) Fiscal Year 2006: ¥500,000 (Direct Cost: ¥500,000) Fiscal Year 2005: ¥500,000 (Direct Cost: ¥500,000)
Keywords	シーケント計算 / カット除去手続き / カリーハワード対応 / 合流性 / 強正規化性 / ラムダ計算 / 明示的代入計算 / 完全性 / 数理論理学 / プログラム理論
Research Abstract	昨年度までの研究によって,古典論理の自然演繹における正規化手続きとシーケント計算におけるカット除去手続きの対応関係を明らかにすることができた.これを利用して,古典論理に対して,強正規化性と合流性をみたす局所ステップカット除去手続きを提案した.この結果は,国際ワークショップ(CL＆C'06)で発表し,現在,学術雑誌に投稿中である. 一方,直観主義論理に対する通常のシーケント計算において,自然演繹の正規化手続きがどのようなカット除去手続きに対応するのかについても明らかにした.これにより,シーケント計算に対する項計算は,項構造と簡約関係の双方についてラムダ計算の保存拡大であることが明らかになった.この結果は,国際会議(LPAR'06)で発表した.このカット除去手続きは合流性をみたさないが,ラムダ計算のベータ簡約を模倣する能力を保ちつつ制限を加えたカット除去手続きの合流性を証明した.この結果は,国際会議(CiE'07)で発表する予定である. さらに,直観主義論理のシーケント計算から得られる項計算に対して,インターセクション型システムを定義し,その型付け可能性によって強正規化性を特徴づけることができることを示した.そこで用いられる手法は,従来知られていた明示的代入計算とインターセクション型に関する手法を大幅に簡略化したものである.この結果は,国際会議(RTA'07)で発表する予定である. この他,直観主義論理のクリプキ意味論を一般化することによって得られる様々な論理の述語拡大に対して,ツリーシーケント計算の手法を用いて完全性を証明した.この結果は,国際会議(TABLEAUX'07)と国際学術雑誌(Logic Journal of the IGPL)で発表する予定である.