| 研究課題/領域番号 |
09480058
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 慶應義塾大学 |
|---|
研究代表者 |
岡田 光弘 慶応義塾大学, 文学部, 教授 (30224025)
|
|---|
| 研究期間 (年度) |
1997 – 1999
|
| 研究課題ステータス |
完了 (1999年度)
|
| 配分額 *注記 |
2,300千円 (直接経費: 2,300千円)
1999年度: 1,300千円 (直接経費: 1,300千円)
1998年度: 1,000千円 (直接経費: 1,000千円)
|
|---|
| キーワード | タイプ理論 / 線形理論 / 項書換理論 / プログラミング言語理論 / 証明論 / 形式仕様・形式検証 / 高階項書換系 / 実時間システム / 線形論理 / プログラミング言語 / 並行計算 / 正規化定理 / 相意味論 / 証明の正規化定理 / (強)停止性 / 計算モデル / 高階論理 / カット消去定理 / セマンティクス / 実現可能計算量 |
|---|
| 研究概要 |
第1年度(平成9年度)においては一般的な論理体系の正規化定理の分析に対する意味論的方法論を確立した。申請者が与えた意味論的方法はGirardが線形論理の証明可能性概念を捉えるために導入した意味論を、証明の正規化定理のための意味論に造り替えて得られたものである。第2年度において、タイプ推論機構をタイプ付き関数型言語のプログラミングパラダイムと抽象データ型の発展的定義構造を持つ対数的仕様言語のプログラミングパラダイムを結合したマルチ・パラダイム言語の計算モデルを我々の意味論的枠組みを応用して構成した。この目的のためには、タイプ付き関数型言語の経産婦デルである高階(タイプ付き)ラムダ計算と代数的仕様言語の計算モデルである項書換え系との融合による統一的な計算モデルの確立が重要である。我々は第1年度に確立した意味論的手法で、高階ラムダ研鑽の正規化定理と項書き換え系の正規化定理を統合した融合言語に対する正規化定理を証明し、これによって融合言語の計算モデルを確立した。第3年度においては、第2年度までに形成されたマルチ・パラダイム・プログラミング言語の計算モデルをさらに線形論理の計算モデルと融合することにより、線形論理のプログラミング・パラダイムと取り込んだマルチ・パラダイム・プログラミング言語の計算モデルを構成した。そのため、まず線形論理の正規化定理と種々の並行計算プログラミング言語の計算モデルとの関係を確立した。そしてこの成果を用いて第2年目で完成させたマルチ・パラダイム言語の論理エンジンを線形論理に代えることにより、並行計算パラダイムを取り込んだマルチ・パラダイム言語を完成させた。
伝統的論理の正規化定理に基づいた種々の論理的計算モデルが得られるが、ここで得られる計算モデルはどれも伝統的な継起的計算モデルであった。これに対してGirardによって導入した線形論理は計算資源の消費関係を直接表し得る全く新しい論理である。よって、これまで用いたれていた伝統論理に代えてこの線形論理を用いることにより、種々の継起的計算モデルの代わりに種々の並行計算モデルが得られることとなった。この基本的アイデアをプログラミング言語の計算モデルの理論に適用して、伝統的な論理的プログラミング言語(関数型、論理型、等式(代数仕様)型)の計算モデルを構成した。この目的のために、線形論理の正規化定理を我々の意味論的枠組のなかで分析し、線形理論の正規化と並行計算プログラミングの計算モデルの一般論との関係を確立した。
|
