表示的意味論

出典: フリー百科事典『ウィキペディア（Wikipedia）』

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

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

[編集] 不動点意味論

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

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

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

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

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

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 は、ω-連続である。

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

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

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

graph(f) = ∪_i∈ω progression_fⁱ({})

ここで

progression_f(G)≡{<x, y>|<x, y>∈graph(f) and immediate-descendants_f(<x, y>)⊆G}

ヒューイットと Baker の論文には immediate-descendants_f の定義に小さな誤りがあったが、Will Clinger [1981] によって修正された。

[編集] 完全抽象化

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

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

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

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

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

[編集] プログラミング言語の合成性

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

[編集] 環境

アクターモデルは、プログラムの合成性を解析する汎用的な手法を提供する。その場合、各プログラムがアクターとなり、環境アクターのアドレスと共に Eval メッセージを送られる。そのため、プログラムはアクターモデルの表示的意味論を継承する（[Hewitt 2006a]）。環境は識別子の束縛を保持するものである。環境に識別子 x のアドレスと共に Lookup メッセージを送ると、語彙的に最近の x の束縛を返す。

例として、木構造のデータを実装したラムダ式 <L> を以下に示す。このラムダ式は下位の木構造 leftSubTree と rightSubTree を引数として木構造を構築する。また、引数 message として "getLeft" が与えられると leftSubTree を返し、"getRight" が与えられると rightSubTree を返す。

 λ(leftSubTree, rightSubTree)
   λ(message)
     if (message == "getLeft") then leftSubTree
     else if (message == "getRight") then rightSubTree

"(<L> 1 2)" という式に対して、環境 E に Eval メッセージを送る場合を考える。この場合の意味は次のようになる。<L>, 1, 2 それぞれに、環境 E と共に Eval メッセージが送られる。整数 1 と 2 は Eval メッセージに対して即座に応答し、自分自身を返す。

しかし、<L> に Eval メッセージを送るとクロージャアクター（プロセス）C を生成する。Cは、<L>のアドレス（これを「ボディ」と呼ぶ）と E（環境）のアドレスから構成される。アクター "(<L> 1 2)" は、C にメッセージ [1 2]を送る。

C はメッセージ [1 2] を受け取ると、以下のような動作をする新たな環境アクター F を生成する:

識別子 lefSubTree に対応する識別子に対する Lookup メッセージを受け取ると、1 を返す。
識別子 rightSubTree に対応する識別子に対する Lookup メッセージを受け取ると、2 を返す。
他の識別子に対応する Lookup メッセージを受け取ると、Lookup メッセージを E に転送する。

アクター（プロセス） C は、環境 F と共に Eval メッセージを以下のアクター（プロセス）に送る:

   λ(message)
     if (message == "getLeft") then leftSubTree
     else if (message == "getRight") then rightSubTree

[編集] 算術式

別のアクターの例として、式 "<expression₁> + <expression₂>" を考える。このアクターは2つのアクター（プロセス） <expression₁> と <expression₂> のアドレスを持つ。この複合式アクター（プロセス）が環境アクター E とカスタマー C のアドレスを伴った Eval メッセージを受け取ると、expression₁ と <expression₂ に対して環境アクター E と新たなカスタマーアクター（プロセス） C₀ のアドレスを伴った Eval メッセージを送る。C₀ が2つの式の値 N₁ と N₂ を受け取ると、C に値 N₁ + N₂ を送る。このようにして、プロセス代数とアクターモデルは、<expression₁> と <expression₂> の意味から "<expression₁> + <expression₂>" の表示的意味を提供する。

[編集] 遅延評価

遅延評価に表示的合成的意味論を提供することは、表示的意味論にとっては1つの課題である。従来からの手法では、"delay <Expression>" の表示（意味）を問うことは <Expression> を評価することを意味論的に形式化することに他ならなかった。

プロセス代数やアクターモデルの表示的意味論は、これに以下のように完全な説明をすることができる。

delay式は環境 E を伴った <Eval> メッセージに対して、ボディ <Expression> のアドレスと環境 E のアドレスを持つクロージャアクター C を生成する。

Cが Customer₀ を伴ったメッセージ M を受け取ると、新たなアクター（プロセス） Customer₁ を生成し、<Expression> に対して環境 E と Customer₁ のアドレスを伴った Eval メッセージを送る。

Customer₁ が値 V を受け取ると、V に Customer₀ を伴ったメッセージ M を送る。

他のプログラミング言語の構成要素についても同様の方法で合成的意味論を提供することができる。

以上解説した表示的合成的意味論は汎用的であり、関数型言語、命令型言語、並行型言語、論理型言語などに適用可能である。

[編集] 並行性の表示的意味論

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

[編集] 計算機科学の他の領域との関連

表示的意味論は領域理論を使って型を領域と解釈する。領域理論はモデル理論からの派生と見ることもでき、そこから型理論や圏論とも関連付けられる。計算機科学では、抽象インタプリタ、プログラム検証、関数プログラミングと関係が深く、「モナド; Monads」の概念などとも関連がある。特に表示的意味論は関数型言語の意味論における逐次プログラミングの制御構造を表現するのに継続の概念を使用する。

[編集] 参考文献

↑ S. Abramsky and A. Jung: Domain theory. In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, vol. III. Oxford University Press, 1994. (ISBN 0-19-853762-X)
↑ Will Clinger, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation, June 1981.

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.)
Gordon Plotkin. A powerdomain construction SIAM Journal of Computing September 1976.
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)
Carl Hewitt and Henry Baker Actors and Continuous Functionals Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1–5, 1977.
Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
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 True concurrency semantics for single pushout graph transformations with applications to actor systems Working papers of the Int. Workshop on Information Systems - Correctness and Reusability. World Scientific. 1995.
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.
Carl Hewitt (2006a). The repeated demise of logic programming and why it will be reincarnated What Went Wrong and Why: Lessons from AI Research and Applications. Technical Report SS-06-08. AAAI Press. March 2006.
Carl Hewitt (2006b) What is Commitment? Physical, Organizational, and Social COIN@AAMAS. 2006.

[編集] 外部リンク

Denotation 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 – 小型言語の完全な表示的意味論

"http://ja.wikipedia.org../../../%E8%A1%A8/%E7%A4%BA/%E7%9A%84/%E8%A1%A8%E7%A4%BA%E7%9A%84%E6%84%8F%E5%91%B3%E8%AB%96.html" より作成

カテゴリ: 理論計算機科学 | 計算モデル