線形論理を用いた新しいプログラシング言語理論の基礎について

2000 Fiscal Year Annual Research Report

• Project/Area Number: 12740075
• Research Institution: Tokyo Woman's Christian University
• Principal Investigator: 永山 操 東京女子大学, 文理学部, 助教授 (30237557)
• Keywords: 証明探索 / 証明論 / 数理論理学 / プログラシング言語 / 線形論理 / 関数型プログラシング / 論理型プログラシング / 平列計算

Research Abstract

昨年度までの研究を踏まえて今年は証明探索との関連を通いてproofnetの特徴付け定理の意義を吟味した。線形論理ではparaproofと呼はれる証明より広い概念を用い、paraproofの中で特徴付け定理による条件を満たすものが証明であると評定される。また、プログラシング言語理論において重要な関数の性質である合流性を保証する論理学的な性質が特徴付け定理ということもできるのではないか。また証明に関する研究を論理体系(構文的)に対する分析的アプローチと一貫性空間(意味的)に対する大域主義的アプローチの観点から行い、証明探索における2大要素として、分解と分割を得るに到った。
今後線形論理を発展させたlocative logicに関する様様な研究がなされるであろうが少なくとも以下の観点は注目に値するであろう。
1.対話型証明探索はサーバクライコントモデルの理論となりうるか
2.論理学から"記憶機能"を提供できるか
3.論理はソフトウェア工学の基礎となりうるか
アブストラクション(描象)…オブジュクト指向
リプリゼンテーション(表現)…効率的なメモリ管理に適切な型(共用型)の理論

Research Products

• [Publications] M.Nagayama and M.Okada: "A New Correctness Criterion for the Proof Nets of Non-Commutative Linear Logics"Journal of Symbolic Logic. (to appear).
• [Publications] S.Hirokawa,Y.Komori and M.Nagayama: "A Lambda Proof of the P-W Theorem"Journal of Symbolic Logic. (to appear).
• [Publications] M.Nagayama and M.Okada: "A Graph-Theoretic Characterization Theorem for Multiplicative Frogment of Non-Commutative Linear Logic"Theoretical Computer Science. (to appear).