論理学的手法を用いたプログラミング言語の理論

1999 年度 実績報告書

• 研究課題/領域番号: 09480058
• 研究機関: 慶應義塾大学
• 研究代表者: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• キーワード: 線形論理 / プログラミング言語 / 並行計算 / 正規化定理

研究概要

第2年度までに形成されたマルチ・パラダイム・プログラミング言語の計算モデルをさらに線形論理の計算モデルと融合することにより、線形論理のプログラミング・パラダイムを取り込んだマルチ・パラダイム・プログラミング言語の計算モデルを構成した。そのため、まず線形論理の正規化定理と種々の並行計算プログラミング言語の計算モデルとの関係を確立した。そしてこの成果を用いて第2年目で完成させたマルチ・パラダイム言語の論理エンジンを線形論理に代えることにより、並行計算パラダイムを取り込んだマルチ・パラダイム言語を完成させた。
伝統的論理の正規化定理に基づいた種々の論理的計算モデルが得られるが、ここで得られる計算モデルはどれも伝統的な継起的計算モデルであった。これに対してGirardによって導入された線形論理は並行計算や計算資源の消費関係を直接表し得る全く新しい論理である。よって、これまで用いられていた伝統論理に代えてこの線形論理を用いることにより、種々の継起的計算モデルの代わりに種々の並行計算モデルが得られることとなった。この基本的アイデアをプログラミング言語の計算モデルの理論に適用して、伝統的な論理的プログラミング言語(関数型、論理型、等式(代数仕様)型)の計算モデルから種々の並行計算プログラミング言語(関数型並行計算言語、論理型並行計算言語、等式型並行計算言語)の計算モデルを構成した。この目的のために、線形論理の正規化定理を我々の意味論的枠組のなかで分析し、線形論理の正規化と並行計算プログラミングの計算モデルの一般論との関係を確立した。

研究成果

• [文献書誌] M.Okada and K.Terui: "Finite Model Property for Various Fragments of Intuitionistic Linear Logic"Journal of Symbolic Logic. 64. 790-801 (1999)
• [文献書誌] M.Okada: "A phase-Semantic Higher Cut-elimination and Normalization Proofs of Classical Linear Logic"Theoretical Computer Science. 227. 333-396 (1999)
• [文献書誌] M.Okada and P.J.Scott: "A Note on Rewriting Theory for Uniqueness of Iteration"Journal of Theory and Applications of Categories. 6. 47-64 (1999)
• [文献書誌] F.Blanqui,J-P.Jouannaud and M.Okada: "Inductive Data Type Systems"Theoretical Computer Science. (近刊).
• [文献書誌] F.Blanqui,J-P.Jouannaud and M.Okada: "Calculus of Inductive Construction"Proc.of Rewriting Technique and Application(RTA99),Springer-Lecture Note in Computer Science. 1631. 301-316 (1999)
• [文献書誌] M.Kanovitch,M.Okada and A.Scedrov: "Phase Semantics for Light Linear Logic"Theoretical Computer Science. (近刊).
• [文献書誌] M.Okada: "Theories of Types and Proofs,second edition,Memoir of Mathematical Society of Japan vol.2"Mathematical Society of Japan. (1999)
• [文献書誌] 岡田 光弘: "法律人工知能(共著)"創成社出版. (2000)