表示的意味論（ひょうじてきいみろん、Denotational Semantics）とは、システムの意味論を表す（表示または意味と称する）数学的オブジェクトを構築することにより、情報システムの意味論を形式化する計算機科学の手法である。プログラム意味論のその他の手法として、公理的意味論と操作的意味論がある。表示的意味論は本来単一のプログラムで定義されるシステムだけを扱うよう開発された。後に複数のプログラムから成るシステムにも拡張され、コンピュータネットワークや並行システムも扱うようになった。

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

1 不動点意味論

1.1 階乗関数の例

1.2 アクター意味論からのスコット連続性の導出


2 完全抽象化

3 プログラミング言語の合成性

3.1 環境

3.2 算術式

3.3 遅延評価


4 並行性の表示的意味論

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

6 参考文献

7 外部リンク

//

不動点意味論

計算システム意味論の表示的理論は、システムが行うことを表現する数学的オブジェクトを探すことを目的としている。この理論は計算の数学的領域を利用する。そのような計算領域の例として部分関数やアクターのイベント図シナリオなどがある。

関係 x?y は、x が y に計算的に発展する可能性があることを意味する。表示が部分関数なら、例えば f?g は f が定義されている全ての値について g と等しいことを意味する。表示がアクターのイベント図シナリオなら、x?y は x を満足するシステムが y を満足するシステムに発展する可能性があることを意味する。

計算領域は次のような特徴を持つ:
下限の存在: 領域には必ず ⊥ で表される要素が含まれ、領域内の任意の要素 x について ⊥?x が成り立つ。

上限の存在: 計算を続けると表示は洗練されるが、限界を持つべきである。そのため、 としたとき、上限 が存在する。これを ω-完全と呼ぶ。

有限要素は可算: 有向集合 A について ∨A が存在し であるとき、 であるような が存在する。そのとき、要素 x は有限であるという（領域理論的に言えば、isolated）。換言すれば、x に到達あるいは x を超えるのに有限のプロセスで可能であるなら、x は有限である。

全ての要素は有限要素の順序列の上限である: 任意の要素に有限の計算手順で到達することを意味している。

領域は downward closed である

システム S に関する数学的表示は、初期の空の表示 ⊥S から始めて、表示近似関数 progressionS を使って S の表示（意味）を構築していくことでよりよい近似を作っていくことで構築される[Hewitt 2006b]。これは以下のように表される:DenoteS ≡ ∨i∈ω progressionSi(⊥S).

ここで、progressionS は「単調」であるべきで、x?y であるとき progressionS(x)?progressionS(y) である。さらに一般化すると次のように表される。もし ∀i∈ω xi?xi+1 ならば progressionS(∨i∈ω xi) = ∨i∈ω progressionS(xi)

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

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

そこで、progressionS が ω-連続であることから以下が成り立つ:progressionS(DenoteS) = DenoteS

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

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

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

階乗関数の例

関数 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 プログラムの表示（意味） Denotefactorial は、以下のように構築される:Denotefactorial = graph(factorial) = ∪i∈ω progressionfactoriali({})

ここでprogressionfactorial(g) ≡ λ(n)if (n==0)then 1 else n*g(n-1)

ただし、progressionfactorial は不動点演算子であり、極小不動点 Denotefactorial は次のようになる:Denotefactorial = progressionfactorial(Denotefactorial)

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

アクター意味論からのスコット連続性の導出

アクターモデルは、カール・ヒューイットと Henry Baker が 1977年に提案した理論であり、デイナ・スコットの関数の表示的意味論の基盤ともなっている。

アクター f が数学的関数のように振舞うとき、progressionf をスコット連続関数と呼び、その極小不動点は次の通りである。