表示的意味論

計算機科学における表示的意味論（ひょうじてきいみろん、）とは、プログラミング言語の意味を形式的に記述する形式意味論（プログラム意味論）の一つの枠組みである。初期には「数理的意味論」（mathematical semantics）、「スコット＝ストレイチー意味論」（Scott–Strachey semantics）のようにも呼ばれた。表示的意味論では、記述された言語の各語句に、表示的意味（denotation）、すなわちプログラム全体の意味に対してその中に現れる各語句が担う役割を表す数学的対象（object）、を与える方法をとる。
表示的意味論の起源は、1960年代のクリストファー・ストレイチーやデイナ・スコットの研究である。ストレイチーやスコットが開発した本来の表示的意味論は、プログラムの表示（意味）を入力を出力にマッピングする関数に変換するものである。後にこれはプログラムの表示（意味）を定義するには非力であることが証明され、例えば再帰定義関数・データ構造を表現できないことが判明した。これを解決するため、スコットはより汎用的な領域理論に基づいた表示的意味論を提案した。その後、研究者らはに基づいた手法を提案し、並行システムの意味論の困難さを克服する努力をしている。
概要.
表示的意味論は、クリストファー・ストレイチーが1964年に形式言語記述言語（formal language description language）に関するIFIP作業部会のために書いた論文"Towards a formal semantics"に始まる。この論文は、抽象構文を関数（便宜的に関数は型無しラムダ計算で表現されていた）へ写像し、関数の合成で定義された意味関数を導入し、不動点組合せ演算子 Y を使ってループの意味を表示させるものであった。ここで理論的に問題であったのは、プログラムの要素の表示的意味（denotation）は、形式的には、型無しのラムダ計算（type-free lambda calculus）に写像される形になっていたが、その肝心の型無しのラムダ計算の数学的モデルがわかっていないということであった。これは、すなわち、不動点組合せ演算子 Y は操作的に規則として解釈することはできたが、表示的意味としてなにか関数を表すと考えることができなかった。
1969年に至って、ストレイチーの理論に興味を抱いたデイナ・スコットは、ストレイチーとの共同研究の末、当初期待していなかった型無しラムダ計算のモデルについて、結局、型無しラムダ計算が実は数学的モデルを持つことを発見することになった。その後すぐに、スコットは、意味の記述法の基礎となる領域理論を構築した。
不動点意味論.
表示的意味は、システムが行うことを表現する数学的オブジェクトを探すことに関心がある。この理論は計算の数学的領域（ドメイン）を利用する。そのような領域の例として完備半順序集合などがある。
関係 x≤y は、x が y に計算的に発展する可能性があることを意味する。表示が完備半順序集合の要素ならば、例えば f≤g は f が定義されている全ての値について g と等しいことを意味する。
計算領域は次のような特徴を持つ:
システム S に関する数学的表示は、初期の空の表示 ⊥S から始めて、表示近似関数 progressionS を使って S の表示（意味）を構築していくことでよりよい近似を作っていくことで構築される。これは以下のように表される:
ここで、progressionS は「単調」であるべきで、x≤y であるとき progressionS(x)≤progressionS(y) である。さらに一般化すると次のように表される。
このような progressionS の特徴を ω-連続と呼ぶ。
表示的意味論では、DenoteS の方程式に従って表示（意味）を作成可能かどうかを主題とする。計算領域理論の基本的定理は、progressionS が ω-連続ならば、DenoteS が存在するというものである。
そこで、progressionS が ω-連続であることから以下が成り立つ:
これはつまり、DenoteS が progressionS の「不動点; fixed point」であることを意味する。
さらに、この不動点は progressionS の不動点の中で極小である。
関数型言語の表示的意味論の実例を次節に示す。
階乗関数の例.
関数 factorial が以下のように定義されているとする:
factorial の graph とは、引数と値のペアの順序集合であり、以下のようになる:
factorial プログラムの表示（意味） Denotefactorial は、以下のように構築される:
ここで
ただし、progressionfactorial は不動点演算子であり、極小不動点 Denotefactorial は次のようになる:
また、progressionfactorial は、ω-連続である。
完全抽象化.
プログラムの表示的意味論と操作的意味論が合致するかどうかを論じる際に、完全抽象化の概念が関わってくる。完全抽象化の特徴は次の通りである。
その他に表示的意味論と操作的意味論について保持するのが望ましい特徴は以下の通りである。
表示的意味論での長年の懸案は、再帰データ型のある場合の完全抽象化であった。特に再帰に利用可能な自然数型である。この問題は従来、の意味論の構築の問題として捉えられてきた。1990年代、ゲーム意味論によって PCF の完全抽象モデルが構築され、表示的意味論の手法に根本的な変化をもたらした。
合成性.
プログラミング言語の表示的意味論の重要な観点として、合成性（Compositionality）がある。合成性とは、プログラムの表示が、各部分の表示の組み合わせで構築されることを意味する。例えば、式 "<expression1> + <expression2>" を考えて見よう。この場合の合成性は、<expression1> の意味と <expression2> の意味から "<expression1> + <expression2>" の意味が導かれることを意味する。
並行性の表示的意味論.
並行性に関する表示的意味論としては、プロセス代数に基づくものなどがある。表示的意味論の並行性への拡張は困難であることが証明されている（無制限の非決定性参照）。
計算機科学の他の領域との関連.
表示的意味論は領域理論を使って型を領域と解釈する。領域理論はモデル理論からの派生と見ることもでき、そこから型理論や圏論とも関連付けられる。計算機科学では、抽象解釈、プログラム検証、関数プログラミングと関係が深く、モナド（Monads）の概念などとも関連がある。また、継続の概念は、歴史的には手続き型プログラムの制御フロー（goto文）などの意味論を与えるために見出された。