2001 Fiscal Year Annual Research Report
線形論理を用いた新しいプログラミング言語理論について
| Project/Area Number |
12740075
|
|---|
| Research Institution | Tokyo Woman's Christian University |
|---|
Principal Investigator |
永山 操 東京女子大学, 文理学部, 助教授 (30237557)
|
|---|
| Keywords | 証明探索 / Computer Science / Mathematical Logic / 線形論理 / 意味論 / Proof net / Full-Abstraction / Linear Logic |
|---|
| Research Abstract |
今年度は、証明網の研究をさらに深めるため、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の定理がどのように反映され、さらに発展する方向を定めていくのか大変興味深い。
|
