論理学のプログラム言語理論への応用

1993 年度 実績報告書

• 研究課題/領域番号: 05808030
• 研究機関: 慶応義塾大学
• 研究代表者: 岡田 光弘 慶應義塾大学, 文学部, 助教授 (30224025)
• キーワード: 項書き換えシステム / タイプ理論 / 高階等式言語 / 論理的プログラム言語 / 証明論 / マルチ・パラダイム・プログラム言語 / 代数的仕様言語 / プログラム検証

研究概要

等式型代数的仕様言語と高階の関数型タイプ付言語との統合及び等式型代数的仕様言語と論理型言語との統合に関する証明論的計算モデルの理論をさらに発展させて、マルチ・パラダイム・プログラム言語の論理的計算モデルを与えた。この言語の特徴は強力な高階項書き換え規則を用いた高階代数的仕様の直接的実行が可能なことであり、この実行可能性を利用して高階代数的仕様に対するプログラミング(=仕様)レベルでの種々の検証が論理的計算を通して可能となることである。又、我々が開発した高階等式論理による項書き換えシステムの基礎論理により、これまでの一階の代数的仕様言語では得られなかったパラメータ化が可能となると同時に、これまでの(MLのような)伝統的関数型言語では不可能であった非帰納的な代数的仕様及びコンテクスト・センシテイブな関数の定義等が可能となった。

研究成果

• [文献書誌] 岡田光弘: "Note on the Strong Normalizability of the Logic with Self‐Referential Predicates" Philosophy95(1993)Mita Philosophi cal Soc.95. 1-14 (1993)
• [文献書誌] 岡田光弘: "Lambdaly-Higher Order Algebraic Specification Langvages" Springer Lecture Notes(Proc.RTA93). (1993June). 712-715 (1993)
• [文献書誌] 岡田光弘: "線形論理とその応用I,II,III,IV" 日本ソフトウエア科学会誌. 近刊. (1994)
• [文献書誌] 岡田光弘(共著): "Longuage,Information and Computation" Thaehaksa Publishing Co.Seoul, 234 (1993)
• [文献書誌] 岡田光弘: "Girardの線形論理,チュートリアル レイチャーノート" 日本ソフトウエア科学会, 43 (1993)