Discovery Sagaサイレントキーワード俯瞰

タイプ理論 / 線形論理 / 関数型言語 / プログラム言語理論 / 証明論 / 形式仕様 / 形式検証 / 実時間システム / プログラミング言語 / プログラム意味論 / 形式的プログラム検証 / 形式的仕様 / 情報科学の論理

第1年度は線形論理とタイプ理論を組み合わせた線形タイプ言語の計算モデルの理論を確立した。また第2年度は第1年度に確立した計算モデルの理論に基づいて、線形タイプ理論によるプログラミング言語の設計のための理論を構築した。
これらの研究を通じて、線形タイプ理論言語による並行計算プログラミング設計のための理論とこの言語とを用いた並行計算プログラミング方法論を考察した。また、実現可能計算量(多項式時間計算量及び多項式空間計算量)のための意味論的手法の確立、および我々の線形タイプ・プログラミング言語の設計への応用を行った。
線形論理とタイプ理論を組み合わせた線形タイプ言語に基づく線形タイプ・プログラム言語の線形理論証明システムとプログラム自動検証・自動抽出部分の設計の理論も構築した。特に今年度は米国側共同研究者たちとソフトウェアの形式仕様、形式検証のための方法論の開発を行った。また、フランスを中心とした欧州の共同研究者グループとは線形理論的手法のプログラミング方法論への応用に関する手法を共同で開発してきた。これらの成果はわれわれの言語設計に生かされている。
本研究課題で構築した新しいプログラミング言語をもとにして、フランス国立情報科学研究所(INRIA)などと協力して我々の言語の実装を計画している。

タイプ理論 / 線形理論 / 項書換理論 / プログラミング言語理論 / 証明論 / 形式仕様・形式検証 / 高階項書換系 / 実時間システム / 線形論理 / プログラミング言語 / 並行計算 / 正規化定理 / 相意味論 / 証明の正規化定理 / (強)停止性 / 計算モデル / 高階論理 / カット消去定理 / セマンティクス / 実現可能計算量

第1年度(平成9年度)においては一般的な論理体系の正規化定理の分析に対する意味論的方法論を確立した。申請者が与えた意味論的方法はGirardが線形論理の証明可能性概念を捉えるために導入した意味論を、証明の正規化定理のための意味論に造り替えて得られたものである。第2年度において、タイプ推論機構をタイプ付き関数型言語のプログラミングパラダイムと抽象データ型の発展的定義構造を持つ対数的仕様言語のプログラミングパラダイムを結合したマルチ・パラダイム言語の計算モデルを我々の意味論的枠組みを応用して構成した。この目的のためには、タイプ付き関数型言語の経産婦デルである高階(タイプ付き)ラムダ計算と代数的仕様言語の計算モデルである項書換え系との融合による統一的な計算モデルの確立が重要である。我々は第1年度に確立した意味論的手法で、高階ラムダ研鑽の正規化定理と項書き換え系の正規化定理を統合した融合言語に対する正規化定理を証明し、これによって融合言語の計算モデルを確立した。第3年度においては、第2年度までに形成されたマルチ・パラダイム・プログラミング言語の計算モデルをさらに線形論理の計算モデルと融合することにより、線形論理のプログラミング・パラダイムと取り込んだマルチ・パラダイム・プログラミング言語の計算モデルを構成した。そのため、まず線形論理の正規化定理と種々の並行計算プログラミング言語の計算モデルとの関係を確立した。そしてこの成果を用いて第2年目で完成させたマルチ・パラダイム言語の論理エンジンを線形論理に代えることにより、並行計算パラダイムを取り込んだマルチ・パラダイム言語を完成させた。
伝統的論理の正規化定理に基づいた種々の論理的計算モデルが得られるが、ここで得られる計算モデルはどれも伝統的な継起的計算モデルであった。これに対してGirardによって導入した線形論理は計算資源の消費関係を直接表し得る全く新しい論理である。よって、これまで用いたれていた伝統論理に代えてこの線形論理を用いることにより、種々の継起的計算モデルの代わりに種々の並行計算モデルが得られることとなった。この基本的アイデアをプログラミング言語の計算モデルの理論に適用して、伝統的な論理的プログラミング言語(関数型、論理型、等式(代数仕様)型)の計算モデルを構成した。この目的のために、線形論理の正規化定理を我々の意味論的枠組のなかで分析し、線形理論の正規化と並行計算プログラミングの計算モデルの一般論との関係を確立した。

線形論理 / 相意味論 / 並行計算 / 正規化定理 / カット消去定理 / 関数型プログラム言語 / 論理プログラム言語 / 論理的計算モデル / Phase Semantics / 証明論 / 正規化定性 / プログラミング言語

線形論理の特徴である(1)並行計算概念の内包、(2)計算資源の消費関係の顕在化、(3)計算状態の顕在化、等を利用して、線形論理に基づく種々の新しい計算モデルの構成を行った。(A)線形論理に対する証明検索手法を用いて、線形論理プログラミングの枠組を構成し、この中で非同期並行プロセス計算のモデルを形成し、これに線形論理の意味論的手法を適用して、並行プロセス計算の意味論を分析した。(B)線形論理に対する証明簡約手続きは関数型プログラム言語に対する強力な計算モデルを与えることが知られている。これまでに知られていた線形論理の“証明可能性"概念に対する論理的意味論(相意味論と呼ばれる)を“証明簡約手続き"に対する意味論へと自然に拡張し、この新しい意味論を用いて関数型プログラム言語の計算モデルに対する論理的意味論を与えた。(C)上の(B)の方法をLight Linear Logicに適用して、実現可能計算量に関する論理概念に対して意味論的枠組を確立した。

【研究分担者】
萩谷雅己 (萩谷昌己)	東京大学	大学院・理学研究科	教授	(Kakenデータベース)
米澤昭憲 (米澤明憲)	東京大学	大学院・理学研究科	教授	(Kakenデータベース)
林晋	神戸大学	工学部	教授	(Kakenデータベース)
大堀淳	京都大学	数理解析研究所	教授	(Kakenデータベース)
高橋正子	東京工業大学	理学部	教授	(Kakenデータベース)