1997 Fiscal Year Annual Research Report
構成的論理言語と代数的仕様言語を融合した発展的ソフトウェア開発言語
| Project/Area Number |
09245224
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Keywords | 高階項書換え系 / タイプ理論 / プログラミング言語 / 高階論理 / 理論情報科学 / 形式的検証 / 形式的仕様 / 正規化定理 |
|---|
| Research Abstract |
タイプ推論(構成的証明)機構を持つタイプ付き関数型(構成的論理)言語のプログラミングパラダイムと抽象データ型の発展的定義構造を持つ代数的仕様言語のプログラミングパラダイムとを結合したマルチ・パラダイム言語の計算モデルを構成した。この目的のためには、タイプ付き関数型言語の計算モデルである高階(タイプ付き)ラムダ計算と代数的仕様言語の計算モデルである項書換え系との融合による統一的な計算モデルの確立が重要である。高階ラムダ計算の正規化定理と項書換え系の正規化定理を統合した融合言語に対する正規化定理を証明し、これによって融合言語の計算モデルを確立した。申請者のこれまでの準備的研究によって(1)一階の項書き換え系と単純タイプ付きラムダ計算の融合に関しては正規化定理が成立すること(Meyer-Breazu Tannen問題への解答;Okada:ACM-ISSAC89,Dershowits-Okada:Theoretical Computer Science(1991))、(2)文脈依存的高階ゲ-デル汎関数により拡張させた項書き換え系と高階タイプ(Polymorphic Types)に拡張されたラムダ計算の融合に関しても正規化定理が成立すること(Jouannaud-Okada:IEEE-LICS91),(3)さらに高階データ型定義をInductive Type推論とともに加えても正規化定理が成立することの意味論的証明(1996))、等が得られてきたが、本年度はこれらの成果を統合して、正規化定理を意味論的枠組を通して統一的に整理・分析して融合言語に対するcleanな計算モデルを構築した(例えばJouannaud-Okada:Theoretical Computer Science(1997)を参照)。また、このマルチ・パラダイム言語上で得られるマルチ・パラダイムの機能を充分に用いて新しいプログラミング方法論を開発するためには、この融合言語に対してより強力な表現力を与えることが望まれる。特に関数型言語のパラダイムである高階関数の定義と代数的仕様言語のパラダイムである関数の文脈依存的定義とを真の意味で組み合わせるには、ゲ-デル汎関数などの高階帰納的関数のよりflexibleな一般化が望まれる。また、より一般的な高階データ型の導入が望まれる。これらの表現力の拡張を行いその正規化定理を証明し、拡張された融合言語に対する計算モデルを確立した。
|
Research Products
(8 results)
-
[Publications] M.Okada: "Phase Semantics for Higher Order Completeness,Cut-Elimination and Normalization Proofs of Classical Linear Logic" Theoretical Computer Science. (to appear). (1998)
-
[Publications] M.Okada-K.Terui: "The Finite Model Property for Various Fragments of Intuitionistic Linear Logic" J.Symbolic Logic. (to appear). (1998)
-
[Publications] M.Hamano-M.Okada: "A Direct Independence Proof of Buhholz's Hydra Game" Archiev for Mathematical Logic. (to appear). (1998)
-
[Publications] J-P.Jouannaud,M.Okada: "Abstract Data Type Systems" Theoretical Computer Science. 173. 349-391 (1997)
-
[Publications] M.Hamano-M.Okada: "A Relationship Among Gentzen's Proof Reduction,Kirby-Paris Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 43. 103-120 (1997)
-
[Publications] M.Kanovitch,M.Okada,A.Scedrov: "Phase Semantics for Light Linear Logic" Electronic Notes of Theoretical Computer Science. 6. 1-14 (1997)
-
[Publications] M.Okada: "Types and Proofs(2chapters分担)" Mathematical Sciety of Japan(近刊), (1998)
-
[Publications] 岡田光弘: "情報科学のための論理学" 産業図書, 250 (1998)
