| Project/Area Number |
09245224
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas
|
| Allocation Type | Single-year Grants |
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Project Period (FY) |
1997
|
| Project Status |
Completed (Fiscal Year 1997)
|
| Budget Amount *help |
¥1,500,000 (Direct Cost: ¥1,500,000)
Fiscal Year 1997: ¥1,500,000 (Direct Cost: ¥1,500,000)
|
|---|
| 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な一般化が望まれる。また、より一般的な高階データ型の導入が望まれる。これらの表現力の拡張を行いその正規化定理を証明し、拡張された融合言語に対する計算モデルを確立した。
|
