| 研究課題/領域番号 |
15500003
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報学基礎
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
長谷川 立 東京大学, 大学院・数理科学研究科, 助教授 (20243107)
|
|---|
| 研究分担者 |
長谷川 真人 京都大学, 数理解析研究所, 助教授 (50293973)
|
|---|
| 研究期間 (年度) |
2003 – 2004
|
| 研究課題ステータス |
完了 (2004年度)
|
| 配分額 *注記 |
1,500千円 (直接経費: 1,500千円)
2004年度: 700千円 (直接経費: 700千円)
2003年度: 800千円 (直接経費: 800千円)
|
|---|
| キーワード | カテゴリカルセマンティクス / 線形論理 / 正規性 / ラムダ計算 / 線形倫理 / 強正規性 |
|---|
| 研究概要 |
直観主義線形論理のカテゴリカルセマンティクスを、計算規則と解釈することを試みた。型付きラムダ計算の背後にある数学的理論として、カデゴリカルセマンティクスは古くから知られた基本的な理論である。実際、両者はある意味等価であり、そのことからいろいろな結果が得られる。しかし、このときの等価性はラムダ計算における計算規則を等式として見たときのものである。いわば、計算規則を静的なものと見たときの関係として、従来はとらえられてきた。われわれは、計算規則を動的、すなわち操作的にとらえたときにも、カテゴリカルセマンティクスとの等価性が成り立っているのではないかと考えている。そのためには、型付きラムダ計算では困難につきあたるので、それを精密にした直観主義線形論理を対象の計算体系として選択した。そのカテゴリカルセマンティクスとしては、biermannらによるものを考える。それを可換図式として記述した上で、その上に計算規則を導入した。カテゴリカルな計算規則が、もとの直観主義線形論理でどのような操作に対応しているか考察した。得られた体系の妥当性を検証する指標として、Church-Rosser性と正規性を証明することを訟みている。これらの性質は、多くの型理論の体系で成り立つものであり、計算体系として妥当であることを強く主張する性質だからである。現在のところ部分的な結果として、弱正規性が成り立つことが示されている。直観主義線形論理は、explicit substitution Looping graphなどの、実装の細部に踏み込んだ計算モデルと共通した考え方に基づいている。それらの体系との比較を行った。
|
