表示的意味論

表示的意味論（ひょうじてきいみろん、Denotational Semantics）とは、計算機科学（理論計算機科学）の一分野で、プログラミング言語の形式意味論（プログラム意味論）の手法のひとつである。初期には「数理的意味論」（mathematical semantics）、「スコット-ストレイチー意味論」（Scott–Strachey semantics）のようにも呼ばれた。プログラムの意味をあらわす数学的オブジェクト（これを「表示」（denotation）と呼ぶ）を構築することで、プログラミング言語の意味論を形式化する手法である。

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

不動点意味論

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

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

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

1. 下限の存在: 領域には必ず ⊥ で表される要素が含まれ、領域内の任意の要素 x について ⊥≤x が成り立つ。
2. 上限の存在: 計算を続けると表示は洗練されるが、限界を持つべきである。そのため、$\forall i\in \omega$ $x_{i}\leq x_{i+1}$ としたとき、上限 $\vee _{i\in \omega }x_{i}$ が存在する。これを $\omega$-完全と呼ぶ。
3. 有限要素は可算: 有向集合 A について ∨A が存在し $x\leq \vee A$ であるとき、$x\leq a$ であるような $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 は、ω-連続である。

完全抽象化

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

1. 抽象性: 表示的意味論は数学的構造によって形式化され、それはプログラミング言語の操作的意味論や表現とは独立している。
2. 正当性: 観測される動作が異なるプログラムは表示も異なる。
3. 完全性: 表示が異なるプログラムは観測される動作も異ならなければならない。

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

1. 構築可能性: 意味モデルは、直観的に構成可能な要素のみから構築可能であるべきである。形式的に表現すれば、全要素は有限要素の有向集合の上限でなければならない。
2. 進歩性: 各システム S について、その意味論には progression_S 関数が存在する。システム S の表示（意味）は、∨_i∈ωprogression_Sⁱ(⊥_S) であり、⊥_S は s の初期構成である。
3. 完全抽象性: 意味モデルのあらゆる射はプログラムの表示であるべきである。

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

合成性

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

並行性の表示的意味論

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

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

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

参考文献

• Irene Greif. Semantics of Communicating Parallel Professes MIT EECS Doctoral Dissertation. August 1975.
• Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
• Edsger Dijkstra. A Discipline of Programming Prentice Hall. 1976.
• Krzysztof R. Apt, J. W. de Bakker. Exercises in Denotational Semantics MFCS 1976: 1-11
• J. W. de Bakker. Least Fixed Points Revisited Theor. Comput. Sci. 2(2): 155-181 (1976)
• Michael Smyth. Power domains Journal of Computer and System Sciences. 1978.
• C.A.R. Hoare. Communicating Sequential Processes Communications of the ACM. August, 1978.
• George Milne and Robin Milner. Concurrent processes and their syntax JACM. April, 1979.
• Nissim Francez, C.A.R. Hoare, Daniel Lehmann, and Willem-Paul de Roever. Semantics of nondeterminism, concurrency, and communication Journal of Computer and System Sciences. December 1979.
• Nancy Lynch and Michael Fischer. On describing the behavior of distributed systems in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Jerald Schwartz Denotational semantics of parallelism in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• William Wadge. An extensional treatment of dataflow deadlock Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Ralph-Johan Back. Semantics of Unbounded Nondeterminism ICALP 1980.
• David Park. On the semantics of fair parallelism Proceedings of the Winter School on Formal Software Specification. Springer-Verlag. 1980.
• Lloyd Allison, A Practical Introduction to Denotational Semantics Cambridge University Press. 1987.
• P. America, J. de Bakker, J. N. Kok and J. Rutten. Denotational semantics of a parallel object-oriented language Information and Computation, 83(2): 152 - 205 (1989)
• David A. Schmidt, The Structure of Typed Programming Languages. MIT Press, Cambridge, Massachusetts, 1994. ISBN 0-262-69171-X.
• M. Korff and L. Ribeiro Concurrent derivations as single pushout graph grammar processes Proceedings of the Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation. ENTCS Vol 2, Elsevier. 1995.
• Thati, Prasanna, Carolyn Talcott, and Gul Agha. Techniques for Executing and Reasoning About Specification Diagrams International Conference on Algebraic Methodology and Software Technology (AMAST), 2004.
• J. C. M. Baeten. A brief history of process algebra Theoretical Computer Science. 2005.
• J.C.M. Baeten, T. Basten, and M.A. Reniers. Algebra of Communicating Processes Cambridge University Press. 2005.
• He Jifeng and C.A.R. Hoare. Linking Theories of Concurrency United Nations University International Institute for Software Technology UNU-IIST Report No. 328. July, 2005.
• Luca Aceto and Andrew D. Gordon (editors). Algebraic Process Calculi: The First Twenty Five Years and Beyond Process Algebra. Bertinoro, Forl`ı, Italy, August 1–5, 2005.
• Bill Roscoe. The Theory and Practice of Concurrency Prentice-Hall. 2005.

外部リンク

• Denotational Semantics by Lloyd Allison
• Structure of Programming Languages I: Denotational Semantics by Wolfgang Schreiner
• Denotational Semantics: A Methodology for Language Development by David Schmidt
• Presentation by Josh Cogliati
• HQL by H. Hernan Moraldo – 小型言語の完全な表示的意味論