タイプ理論及び線形論理のプログラム言語理論への応用

1995 年度 実績報告書

• 研究課題/領域番号: 07044093
• 研究機関: 慶応義塾大学
• 研究代表者: 岡田 光弘 慶応義塾大学, 文学部, 助教授 (30224025)
• 研究分担者: 林 普 神戸大学, 理工学部, 教授 (40156443) ; 高橋 正子 東京工業大学, 理学部, 助教授 (00015588) ; 大堀 淳 京都大学, 数理解析研, 助教授 (60252532) ; 萩谷 昌巳 東京大学, 理学系研究科, 教授 (30156252) ; 佐藤 雅彦 東北大学, 電通研, 教授 (20027387)
• キーワード: 線形論理 / タイプ理論 / プログラム言語

研究概要

タイプ理論と線形論理を用いた新しいマルチパラダイムプログラム言語の設計のための基礎理論を与えることを本年度の主な目的とした。この目的のために特に、Phase Semantics及びCoherence Semantics等の線形論理の基本的なSemantics理論の整備をするとともに、それらのSemantics理論のタイプ付高階プログラミング言語理論への応用を与えた。特に、CDherence Semanticsは、我々の線形論理に基づいたタイプ付プログラミング言語において、Denotational Semanticsとしての役割を果たすものであり、又Phase Semanticsは、これまで考えられてきたように単に証明可能性概念に対する完全性を与えるだけではなく、証明概念自身についての完全性も与えることが示された。特に、後者の考え方から、Phase Semanticsを用いた証明の正規化定理の証明が得られることが示された。証明の正規化はタイプ付プログラミング言語の計算モデルを与えることから、上記のPhase Semantics理論は、我々のマルチパラダイムプログラミング言語の計算モデルの基礎となることが示された。一方、線形論理を基にした並行計算モデルの定式化、及びInteraction Nets及びProof netsの理論が与えられた。これらは線形論理による並行計算及び (ラムグ計算等の) sequentialな計算の分析手法を与えるものであり、これらの理論を我々のマルチパラダイム言語に内臓することにより、我々のマルチパラダイム言語が、並行計算プログラムや計算処理のコントロールに非常に適したものとなることが示された。

研究成果

• [文献書誌] Jouannaud,Jean-Pierre 岡田光弘: "Abstract Data Type Systems" Theoretical Computer Science. (近刊). (1996)
• [文献書誌] 岡田光弘(浜野と共著): "A Direct Proof of Buchholz's Hydra Game" Archiev for Mathematical Logic. (近刊). (1996)
• [文献書誌] Susumu Hayashi(林晋)and S.Kobayashi: "A new formalization of Feferman's system of functions and classes and its velation to Frege structure." International J. of Foundations of Computer Science.6(No.3). 187-202 (1995)
• [文献書誌] M.Hagiya et al.: "Formalization of Planar Graphs" Proc.of Higher Order Theorem Proving and its Applications,Lecture Notes in Computer Science(Springer). 971. 369-384 (1995)
• [文献書誌] M.Takahashi: "Parallel reduction in λ-calculus" Information and Computation. 118. 120-127 (1995)
• [文献書誌] 佐藤雅彦(亀山との共著): "自己反映的証明体系RPTの理論と実現" コンピュータソフトウエア. 12(2). 32-51 (1995)
• [文献書誌] 岡田光弘: "情報科学のための論理" 産業図書, 240 (1996)
• [文献書誌] Girard,Jean-Yves 岡田光弘 Scedrov,Andre: "Special Issue on Linear Logic (ENTCS series)" Elsevier社(オランダ), 420 (1996)
• [文献書誌] Girard,Jean-Yves(フランス側代表者): "Advances in Linear Logic" Cambridge University Press, 340 (1995)
• [文献書誌] 林普: "プログラム検証論" 共立出版, 208 (1995)