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

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

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