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

2005 Fiscal Year Annual Research Report

• Project/Area Number: 17700003
• Research Institution: Tohoku University
• Principal Investigator: 菊池 健太郎 東北大学, 電気通信研究所, 助手 (40396528)
• Keywords: 数理論理学 / プログラム理論

Research Abstract

本年度の前半は,型付きラムダ計算に対する縮約可能性法を用いない強正規化性の証明を,合流性や標準化定理等,他の簡約の性質にも適用することに取り組んだ.これらの証明はシーケント計算の体系に基づく型システムを用いて与えることができる.また,それらの方法をインターセクション型システムに対する体系にも拡張し,ある種の型を持つラムダ項の弱正規化性や頭部正規化性の証明にも適用できることを示した.この結果は,オーストリアで行われた項書き換えワークショップで発表し,参加者からコメントを頂いた.
本年度の後半は,昨年度までの研究によって得られた直観主義論理に対するシーケント計算の体系と明示的代入計算の間の関係についての結果を,古典論理に対するシーケント計算の体系とラムダミュー計算へ拡張することに取り組んだ.具体的には,型付きラムダミュー計算のベータ簡約とミュー簡約が,古典論理に対するシーケント計算の体系においてどのような簡約に対応するのかを明らかにし,このシーケント計算に対する項計算は項構造と簡約関係の両方についてラムダミュー計算の保存拡大であることを示した.この結果は,従来自然演繹の体系で行われたきたことは全てシーケント計算の中で再現することができることを示す強力なものである.さらに,明示的代入計算の手法を用いてこの項計算体系の簡約の合流性と強正規化性を証明した.この結果の一部は,仙台で行われた項書き換えワークショップで発表し,参加者からコメントを頂いた.