| 研究課題/領域番号 |
12740075
|
|---|
| 研究種目 |
奨励研究(A)
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
数学一般(含確率論・統計数学)
|
|---|
| 研究機関 | 東京女子大学 |
|---|
研究代表者 |
永山 操 東京女子大学, 文理学部, 助教授 (30237557)
|
|---|
| 研究期間 (年度) |
2001 – 2002
|
| 研究課題ステータス |
完了 (2001年度)
|
| 配分額 *注記 |
2,300千円 (直接経費: 2,300千円)
2001年度: 1,300千円 (直接経費: 1,300千円)
2000年度: 1,000千円 (直接経費: 1,000千円)
|
|---|
| キーワード | 証明探索 / Computer Science / Mathematical Logic / 線形論理 / 意味論 / Proof net / Full-Abstraction / Linear Logic / 証明論 / 数理論理学 / プログラシング言語 / 関数型プログラシング / 論理型プログラシング / 平列計算 |
|---|
| 研究概要 |
今年度は、証明網の研究をさらに深めるため、J.-Y.Girard"Locus Solum"を研究し、さらにケンブリッジ大のM.Hyland,エジンバラ大のG.Plotkin,J.Power及びパリ大のP.-L.Gurienとの共同研究を行った。その結果まず論理式の役割が
(1)証明の構成要素として位置(ロケーション)を表す(証明論的役割)
(2)証明の推論プロセスを表す半順序構造を表す(ドメイン理論的役割)
(3)証明を真とする空間(通常To-分離公理を満たす)(型理論的役割)
となることがわかった。また。計算の意味論を深める上で、論理学におけるドモルガン性をゲームセマンティクスにより新解釈を与えることが重要であると認識した。今後、並列計算のモデルとして評価されてきた証明網の意味論の研究に、型理論的"Fully-Abstract"であるCurry-Howard同型対応とドメイン理論的"Fully-Abstract"であるBohmの定理がどのように反映され、さらに発展する方向を定めていくのか大変興味深い。
|
