| 研究概要 |
直観主義線形論理のカテゴリカルセマンティクスを,計算規則と解釈することを試みた.型つきラムダ計算の背後にある数学的理論として,カテゴリカルセマンティクスは古くから知られた基本的な理論である.実際,両者はある意味等価であり,そのことからいろいろな結果が得られる.しかし,このときの等価性はラムダ計算における計算規則を,等式として見たときのものである.いわば,計算規則を静的なものと見たときの関係として,従来は捉えられてきた.われわれは,計算規則を動的,すなわち操作的に捉えたときにも,カテゴリカルセマンティクスとの等価性が成り立っているのではないかと考えている.そのためには,型つきラムダ計算では困難につきあたるので,それを精密にした直観主義線形論理を対象の計算体系として選択した.そのカテゴリカルセマンティクスとしては,Biermannらによるものを考える.それを可換図式として記述した上で,その上に計算規則を導入した.カテゴリカルな計算規則が,もとの直観主義線形論理でどのような操作に対応しているか考察した.得られた体系の妥当性を検証する指標として,Church-Rosser性と正規性を証明することを試みている.これらの性質は,多くの型理論の体系で成り立つものであり,計算体系として妥当であることを強く主張する性質であるからである.現在のところ部分的な結果として,Church-Rosser性の仮定のもと,弱正規性が成り立つことが示されている.直観主義線形論理は,explicit substitutionやLamping graphなどの,実装の細部に踏み込んだ計算モデルと共通した考えかたに基づいている.それらの体系との比較を行った.
|
