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