表示的意味論

計算機科学における表示的意味論（ひょうじてきいみろん、英: Denotational Semantics）とは、プログラミング言語の意味を形式的に記述する形式意味論（プログラム意味論）の一つの枠組みである。初期には「数理的意味論」（mathematical semantics）、「スコット＝ストレイチー意味論」（Scott–Strachey semantics）のようにも呼ばれた。表示的意味論では、記述された言語の各語句に、表示的意味（denotation）、すなわちプログラム全体の意味に対してその中に現れる各語句が担う役割を表す数学的対象（object）を与える方法をとる^[1]。

表示的意味論の起源は、1960年代のクリストファー・ストレイチーやデイナ・スコットの研究である。ストレイチーやスコットが開発した本来の表示的意味論は、プログラムの表示（意味）を入力を出力にマッピングする関数に変換するものである。後にこれはプログラムの表示（意味）を定義するには非力であることが証明され、例えば再帰定義関数・データ構造を表現できないことが判明した。これを解決するため、スコットはより汎用的な領域理論に基づいた表示的意味論を提案した^[2]。その後、研究者らはPower Domainsに基づいた手法を提案し、並行システムの意味論の困難さを克服する努力をしている^[3]。

概要

表示的意味論は、クリストファー・ストレイチーが1964年に形式言語記述言語（formal language description language）に関するIFIP作業部会のために書いた論文"Towards a formal semantics"に始まる。この論文は、抽象構文を関数（便宜的に関数は型無しラムダ計算で表現されていた）へ写像し、関数の合成で定義された意味関数を導入し、Y 不動点コンビネータを使ってループの意味を表示させるものであった。ここで理論的に問題であったのは、プログラムの要素の表示的意味（denotation）は、形式的には、型無しのラムダ計算（type-free lambda calculus）に写像される形になっていたが、その肝心の型無しのラムダ計算の数学的モデルがわかっていないということであった。これは、すなわち、Y 不動点コンビネータは操作的に規則として解釈することはできたが、表示的意味としてなにか関数を表すと考えることができなかった^[4]。

1969年に至って、ストレイチーの理論に興味を抱いたデイナ・スコットは、ストレイチーとの共同研究の末、当初期待していなかった型無しラムダ計算のモデルについて、結局、型無しラムダ計算が実は数学的モデルを持つことを発見することになった。その後すぐに、スコットは、意味の記述法の基礎となる領域理論を構築した。

不動点意味論

表示的意味は、システムが行うことを表現する数学的オブジェクトを探すことに関心がある。この理論は計算の数学的領域（ドメイン）を利用する。そのような領域の例として完備半順序集合などがある。

関係 x≤y は、x が y に計算的に発展する可能性があることを意味する。表示が完備半順序集合の要素ならば、例えば f≤g は f が定義されている全ての値について g と等しいことを意味する。

計算領域は次のような特徴を持つ:

1. 下限の存在: 領域には必ず ⊥ で表される要素が含まれ、領域内の任意の要素 x について ⊥≤x が成り立つ。
2. 上限の存在: 計算を続けると表示は洗練されるが、限界を持つべきである。そのため、${\displaystyle \forall i\in \omega }$ ${\displaystyle x_{i}\leq x_{i+1}}$ としたとき、上限 ${\displaystyle \vee _{i\in \omega }x_{i}}$ が存在する。これを ${\displaystyle \omega }$-完全と呼ぶ。
3. 有限要素は可算: 有向集合 A について ∨A が存在し ${\displaystyle x\leq \vee A}$ であるとき、${\displaystyle x\leq a}$ であるような ${\displaystyle a\in A}$ が存在する。そのとき、要素 x は有限であるという（領域理論的に言えば、isolated）。換言すれば、x に到達あるいは x を超えるのに有限のプロセスで可能であるなら、x は有限である。
4. 全ての要素は有限要素の順序列の上限である: 任意の要素に有限の計算手順で到達することを意味している。
5. 領域は downward closed である

システム S に関する数学的表示は、初期の空の表示 ⊥_S から始めて、表示近似関数 progression_S を使って S の表示（意味）を構築していくことでよりよい近似を作っていくことで構築される。これは以下のように表される:

Denote_S ≡ ∨_i∈ω progression_Sⁱ(⊥_S).

ここで、progression_S は「単調」であるべきで、x≤y であるとき progression_S(x)≤progression_S(y) である。さらに一般化すると次のように表される。

もし ∀i∈ω x_i≤x_i+1 ならば progression_S(∨_i∈ω x_i) = ∨_i∈ω progression_S(x_i)

このような progression_S の特徴を ω-連続と呼ぶ。

表示的意味論では、Denote_S の方程式に従って表示（意味）を作成可能かどうかを主題とする。計算領域理論の基本的定理は、progression_S が ω-連続ならば、Denote_S が存在するというものである。

そこで、progression_S が ω-連続であることから以下が成り立つ:

progression_S(Denote_S) = Denote_S

これはつまり、Denote_S が progression_S の「不動点; fixed point」であることを意味する。

さらに、この不動点は progression_S の不動点の中で極小である。

関数型言語の表示的意味論の実例を次節に示す。

階乗関数の例

関数 factorial が以下のように定義されているとする:

factorial ≡ λ(n)if (n==0)then 1 else n*factorial(n-1)

factorial の graph とは、引数と値のペアの順序集合であり、以下のようになる:

graph(factorial) = {<n, factorial(n)>|n∈ω} = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}

factorial プログラムの表示（意味） Denote_factorial は、以下のように構築される:

Denote_factorial = graph(factorial) = ∪_i∈ω progression_factorialⁱ({})

ここで

progression_factorial(g) ≡ λ(n)if (n==0)then 1 else n*g(n-1)

ただし、progression_factorial は不動点演算子であり、極小不動点 Denote_factorial は次のようになる:

Denote_factorial = progression_factorial(Denote_factorial)

また、progression_factorial は、ω-連続である。

完全抽象化

プログラムの表示的意味論と操作的意味論が合致するかどうかを論じる際に、完全抽象化の概念が関わってくる。完全抽象化の特徴は次の通りである。

抽象性

表示的意味論は数学的構造によって形式化され、それはプログラミング言語の操作的意味論や表現とは独立している。

正当性

観測される動作が異なるプログラムは表示も異なる。

完全性

表示が異なるプログラムは観測される動作も異ならなければならない。

その他に表示的意味論と操作的意味論について保持するのが望ましい特徴は以下の通りである。

構築可能性

意味モデルは、直観的に構成可能な要素のみから構築可能であるべきである。形式的に表現すれば、全要素は有限要素の有向集合の上限でなければならない。

進歩性

各システム S について、その意味論には progression_S 関数が存在する。システム S の表示（意味）は、∨_i∈ωprogression_Sⁱ(⊥_S) であり、⊥_S は s の初期構成である。

完全抽象性

意味モデルのあらゆる射はプログラムの表示であるべきである。

表示的意味論での長年の懸案は、再帰データ型のある場合の完全抽象化であった。特に再帰に利用可能な自然数型である。この問題は従来、PCF（プログラミング言語）（英語版）の意味論の構築の問題として捉えられてきた。1990年代、ゲーム意味論によって PCF の完全抽象モデルが構築され、表示的意味論の手法に根本的な変化をもたらした。

合成性

プログラミング言語の表示的意味論の重要な観点として、合成性（Compositionality）がある。合成性とは、プログラムの表示が、各部分の表示の組み合わせで構築されることを意味する。例えば、式 "<expression₁> + <expression₂>" を考えて見よう。この場合の合成性は、<expression₁> の意味と <expression₂> の意味から "<expression₁> + <expression₂>" の意味が導かれることを意味する。

並行性の表示的意味論

並行性に関する表示的意味論としては、プロセス代数に基づくものなどがある。表示的意味論の並行性への拡張は困難であることが証明されている（無制限の非決定性参照）。

計算機科学の他の領域との関連

表示的意味論は領域理論を使って型を領域と解釈する。領域理論はモデル理論からの派生と見ることもでき、そこから型理論や圏論とも関連付けられる。計算機科学では、抽象解釈、プログラム検証、関数プログラミングと関係が深く、モナド（Monads）の概念などとも関連がある。また、継続の概念は、歴史的には手続き型プログラムの制御フロー（goto文）などの意味論を与えるために見出された^[5]。