表示的意味論のソースを表示

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

表示的意味論の起源は、[[1960年代]]の[[クリストファー・ストレイチー]]や[[デイナ・スコット]]の研究である。ストレイチーやスコットが開発した本来の表示的意味論は、プログラムの表示（意味）を入力を出力にマッピングする[[関数 (数学)|関数]]に変換するものである。後にこれはプログラムの表示（意味）を定義するには非力であることが証明され、例えば[[再帰呼び出し|再帰定義]]関数・データ構造を表現できないことが判明した。これを解決するため、スコットはより汎用的な[[領域理論]]に基づいた表示的意味論を提案した<ref name="abramsky1994">S. Abramsky and A. Jung: [http://www.cs.bham.ac.uk/~axj/pub/papers/handy1.pdf ''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)</ref>。その後、研究者らは[[:en:Power domains|Power Domains]]に基づいた手法を提案し、[[並行性|並行システム]]の意味論の困難さを克服する努力をしている<ref name=Plotkin1976>Gordon Plotkin. ''A powerdomain construction'' SIAM Journal of Computing. September 1976.</ref>。

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

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

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

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

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

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

{{Indent|<tt>'''Denote'''<sub>S</sub> ≡ ∨<sub>i∈ω</sub> '''progression'''<sub>S</sub><sup>i</sup>(⊥<sub>S</sub>)</tt>.}}

ここで、<tt>'''progression'''<sub>S</sub></tt> は「単調」であるべきで、<tt>x≤y</tt> であるとき <tt>'''progression'''<sub>S</sub>(x)≤'''progression'''<sub>S</sub>(y)</tt> である。さらに一般化すると次のように表される。

{{Indent|もし <tt>∀i∈ω x<sub>i</sub>≤x<sub>i+1</sub></tt> ならば <tt>'''progression'''<sub>S</sub>(∨<sub>i∈ω</sub> x<sub>i</sub>) <nowiki>=</nowiki> ∨<sub>i∈ω</sub> '''progression'''<sub>S</sub>(x<sub>i</sub>)</tt>}}

このような <tt>'''progression'''<sub>S</sub></tt> の特徴を ω-連続と呼ぶ。

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

そこで、<tt>'''progression'''<sub>S</sub></tt> が ω-連続であることから以下が成り立つ:
{{Indent|<tt>'''progression'''<sub>S</sub>('''Denote'''<sub>S</sub>) <nowiki>=</nowiki> '''Denote'''<sub>S</sub></tt>}}

これはつまり、<tt>'''Denote'''<sub>S</sub></tt> が <tt>'''progression'''<sub>S</sub></tt> の「不動点; fixed point」であることを意味する。

さらに、この不動点は <tt>'''progression'''<sub>S</sub></tt> の不動点の中で極小である。

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

=== 階乗関数の例 ===
関数 <tt>factorial</tt> が以下のように定義されているとする:
{{Indent|<tt>factorial ≡ λ(n)if (n<nowiki>==</nowiki>0)then 1 else n*factorial(n-1)</tt>}}
<tt>factorial</tt> の '''<tt>graph</tt>''' とは、引数と値のペアの順序集合であり、以下のようになる:
: <tt>'''graph'''(factorial) <nowiki>=</nowiki> {<n, factorial(n)>|n∈ω} <nowiki>=</nowiki> {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}</tt>
<tt>factorial</tt> プログラムの表示（意味） <tt>'''Denote'''<sub>factorial</sub></tt> は、以下のように構築される:
{{Indent|<tt>'''Denote'''<sub>factorial</sub> <nowiki>=</nowiki> '''graph'''(factorial) <nowiki>=</nowiki> ∪<sub>i∈ω</sub> '''progression'''<sub>factorial</sub><sup>i</sup>({})</tt>}}

ここで

{{Indent|<tt>'''progression'''<sub>factorial</sub>(g) ≡ λ(n)if (n<nowiki>==</nowiki>0)then 1 else n*g(n-1)</tt>}}

ただし、<tt>'''progression'''<sub>factorial</sub></tt> は不動点演算子であり、極小不動点 <tt>'''Denote'''<sub>factorial</sub></tt> は次のようになる:
{{Indent|<tt>'''Denote'''<sub>factorial</sub> <nowiki>=</nowiki> '''progression'''<sub>factorial</sub>('''Denote'''<sub>factorial</sub>)</tt>}}

また、<tt>'''progression'''<sub>factorial</sub></tt> は、ω-連続である。
<!--
=== アクター意味論からのスコット連続性の導出 ===
[[アクターモデル]]は、[[カール・ヒューイット]]と Henry Baker が 1977年に提案した理論であり、[[デイナ・スコット]]の関数の表示的意味論の基盤ともなっている。

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

{{Indent|<tt>'''graph'''(f) <nowiki>=</nowiki> ∪<sub>i∈ω</sub> '''progression'''<sub>f</sub><sup>i</sup>({})</tt></tt>}}

ここで

:|<tt>'''progression'''<sub>f</sub>(G)≡{<x, y>|<x, y>∈'''graph'''(f) ''and'' '''immediate-descendants'''<sub>f</sub>(<x, y>)⊆G}</tt>

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

== 完全抽象化 ==
プログラムの表示的意味論と操作的意味論が合致するかどうかを論じる際に、完全抽象化の概念が関わってくる。完全抽象化の特徴は次の通りである。
; '''抽象性'''
: 表示的意味論は数学的構造によって形式化され、それはプログラミング言語の操作的意味論や表現とは独立している。
; '''[[正当性 (計算機科学)|正当性]]'''
: 観測される動作が異なるプログラムは表示も異なる。
; '''完全性'''
: 表示が異なるプログラムは観測される動作も異ならなければならない。

その他に表示的意味論と操作的意味論について保持するのが望ましい特徴は以下の通りである。
; ''構築可能性''
: 意味モデルは、直観的に構成可能な要素のみから構築可能であるべきである。形式的に表現すれば、全要素は有限要素の有向集合の上限でなければならない。
; ''進歩性''
: 各システム <tt>S</tt> について、その意味論には <tt>'''progression'''<sub>S</sub></tt> 関数が存在する。システム <tt>S</tt> の表示（意味）は、<tt>∨<sub>i∈ω</sub>'''progression'''<sub>S</sub><sup>i</sup>(⊥<sub>S</sub>)</tt> であり、<tt>⊥<sub>S</sub></tt> は <tt>s</tt> の初期構成である。
; '''完全抽象性'''
: 意味モデルのあらゆる射はプログラムの表示であるべきである。

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

== 合成性 ==
プログラミング言語の表示的意味論の重要な観点として、合成性（Compositionality）がある。合成性とは、プログラムの表示が、各部分の表示の組み合わせで構築されることを意味する。例えば、式 "<tt><expression<sub>1</sub>> + <expression<sub>2</sub>></tt>" を考えて見よう。この場合の合成性は、<tt><expression<sub>1</sub>></tt> の意味と <tt><expression<sub>2</sub>></tt> の意味から "<tt><expression<sub>1</sub>> + <expression<sub>2</sub>></tt>" の意味が導かれることを意味する。
<!--
=== 環境 ===
[[アクターモデル]]は、プログラムの合成性を解析する汎用的な手法を提供する。その場合、各プログラムがアクターとなり、環境アクターのアドレスと共に <tt>Eval</tt> メッセージを送られる。そのため、プログラムはアクターモデルの表示的意味論を継承する（[Hewitt 2006a]）。環境は識別子の[[名前束縛|束縛]]を保持するものである。環境に識別子 '''x''' のアドレスと共に <tt>Lookup</tt> メッセージを送ると、語彙的に最近の '''x''' の束縛を返す。

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

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

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

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

'''C''' はメッセージ '''[1 2]''' を受け取ると、以下のような動作をする新たな環境アクター '''F''' を生成する:
# 識別子 <tt>lefSubTree</tt> に対応する識別子に対する <tt>Lookup</tt> メッセージを受け取ると、<tt>1</tt> を返す。
# 識別子 <tt>rightSubTree</tt> に対応する識別子に対する <tt>Lookup</tt> メッセージを受け取ると、<tt>2</tt> を返す。
# 他の識別子に対応する <tt>Lookup</tt> メッセージを受け取ると、<tt>Lookup</tt> メッセージを '''E''' に転送する。

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

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

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

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

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

*''delay''式は環境 '''E''' を伴った <Eval> メッセージに対して、ボディ <tt><Expression></tt> のアドレスと環境 '''E''' のアドレスを持つ[[クロージャ]]アクター '''C''' を生成する。
*'''C'''が '''Customer<sub>0</sub>''' を伴ったメッセージ '''M''' を受け取ると、新たなアクター（プロセス） '''Customer<sub>1</sub>''' を生成し、<tt><Expression></tt> に対して環境 '''E''' と '''Customer<sub>1</sub>''' のアドレスを伴った </tt>Eval</tt> メッセージを送る。
*'''Customer<sub>1</sub>''' が値 '''V''' を受け取ると、'''V''' に '''Customer<sub>0</sub>''' を伴ったメッセージ '''M''' を送る。

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

以上解説した表示的合成的意味論は汎用的であり、[[関数型言語]]、[[命令型言語]]、[[並行計算|並行型言語]]、[[論理プログラミング|論理型言語]]などに適用可能である。
-->
== 並行性の表示的意味論 ==
並行性に関する表示的意味論としては、[[プロセス代数]]に基づくものなどがある。表示的意味論の並行性への拡張は困難であることが証明されている（[[無制限の非決定性]]参照）。

== 計算機科学の他の領域との関連 ==
表示的意味論は[[領域理論]]を使って型を領域と解釈する。領域理論は[[計算模型|モデル理論]]からの派生と見ることもでき、そこから[[型理論]]や[[圏論]]とも関連付けられる。計算機科学では、[[抽象解釈]]、[[形式的検証|プログラム検証]]、[[関数型言語|関数プログラミング]]と関係が深く、[[モナド (プログラミング)|モナド]]（Monads）の概念などとも関連がある。また、[[継続]]の概念は、歴史的には手続き型プログラムの[[制御フロー]]（[[goto文]]）などの意味論を与えるために見出された<ref name="Reynolds1993">{{Cite journal |last=Reynolds |first=John C. |year=1993 |date=1993-11-01 |title=The discoveries of continuations |url=https://www.cs.cmu.edu/afs/cs/user/jcr/ftp/histcont.pdf |journal=LISP and Symbolic Computation |volume=6 |issue=3 |pages=233–247 |language=en |ref=harv |doi=10.1007/BF01019459 |issn=1573-0557}}</ref>。

== 出典・脚注 ==
<references />

== 参考文献 ==
{{参照方法|date=2022年5月|section=1}}
*{{Cite book |last=Milne |first=R.E. |title=A theory of programming language semantics |year=1976 |isbn=978-1-5041-2833-9 |last2=Strachey |first2=C.}}
*{{Cite book |last=Stoy |first=Joseph E. |title=Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics |year=1977 |publisher=MIT Press |isbn=978-0262191470}}
<!--
*{{Cite journal |last=Plotkin |first=G.D. |author-link=Gordon Plotkin |year=1976 |title=A powerdomain construction |journal=SIAM J. Comput. |volume=5 |issue=3 |pages=452–487 |DOI=10.1137/0205035 |doi=10.1137/0205035 |citeseerx=10.1.1.158.4318}}
-->
*{{Cite book |last=Dijkstra |first=Edsger W. |author-link=エドガー・ダイクストラ |title=A Discipline of Programming |series=Prentice-Hall series in automatic computation |date=1976 |isbn=0-13-215871-X |location=Englewood Cliffs, N.J. |oclc=1958445}}
*{{Cite book |last=Apt |first=Krzysztof R. |title=Exercises in denotational semantics |series=Afdeling Informatica |date=1976 |publisher=Mathematisch Centrum |language=English |location=Amsterdam |last2=de Bakker |first2=J. W. |oclc=63400684}}
*{{Cite journal |last=De Bakker |first=J.W. |year=1976 |date=1976 |title=Least Fixed Points Revisited |url=https://linkinghub.elsevier.com/retrieve/pii/0304397576900311 |journal=Theoretical Computer Science |volume=2 |issue=2 |pages=155–181 |language=en |DOI=10.1016/0304-3975(76)90031-1 |doi=10.1016/0304-3975(76)90031-1 |doi-access=free}}
<!--
* [[カール・ヒューイット|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.
-->
*{{Cite journal |last=Smyth |first=Michael B. |year=1978 |title=Power domains |journal=J. Comput. Syst. Sci. |volume=16 |pages=23–36 |DOI=10.1016/0022-0000(78)90048-X |doi=10.1016/0022-0000(78)90048-X |doi-access=free}}
*{{Cite journal |last=Hoare |first=C. A. R. |author-link=アントニー・ホーア |date=1978-08-01 |title=[[Communicating Sequential Processes]] |url=https://doi.org/10.1145/359576.359585 |journal=Communications of the ACM |volume=21 |issue=8 |pages=666–677 |DOI=10.1145/359576.359585 |doi=10.1145/359576.359585 |issn=0001-0782}}<!--''title-link='' がない-->
*{{Cite journal |last=Milne |first=George |last2=Milner |first2=Robin |date=1979-04-01 |title=Concurrent Processes and Their Syntax |url=https://doi.org/10.1145/322123.322134 |journal=Journal of the ACM |volume=26 |issue=2 |pages=302–321 |DOI=10.1145/322123.322134 |doi=10.1145/322123.322134 |issn=0004-5411 |author2-link=ロビン・ミルナー}}
*{{Cite journal |last=Francez |first=Nissim |last2=Hoare |first2=C.A.R |last3=Lehmann |first3=Daniel J |last4=De Roever |first4=Willem P |date=1979 |title=Semantics of nondeterminism, concurrency, and communication |url=https://hdl.handle.net/1874/24888 |journal=Journal of Computer and System Sciences |volume=19 |issue=3 |pages=290–308 |language=English |issn=0022-0000 |oclc=4640928019 |author2-link=アントニー・ホーア}}
*{{Cite book |ref={{harvid|Kahn|1979}} |last=Kahn |first=G. |title=Semantics of concurrent computation: proceedings of the international symposium, Évian, France, July 2-4, 1979 |url=https://books.google.com/books?id=lLgqAQAAIAAJ |series=Lecture Notes in Computer Science |date=1979-06-01 |publisher=Springer Berlin Heidelberg |language=en |isbn=978-3-540-09511-8 |location=Berlin |oclc=5101221 |lccn=79015956}}
**{{Cite book |last=Lynch |first=Nancy |title={{harvnb|Kahn|1979}} |year=1979 |chapter=On describing the behavior of distributed systems |last2=Fischer |first2=Michael J.}}
**{{Cite book |last=Schwartz |first=Jerald |title={{harvnb|Kahn|1979}} |year=1979 |chapter=Denotational semantics of parallelism}}
**{{Cite book |last=Wadge |first=William |title={{harvnb|Kahn|1979}} |year=1979 |chapter=An extensional treatment of dataflow deadlock}}
*{{Cite book |last=Back |first=Ralph-Johan |editor-last=de Bakker |editor-first=Jaco |title=Semantics of unbounded nondeterminism |url=https://link.springer.com/chapter/10.1007%2F3-540-10003-2_59 |series=Lecture Notes in Computer Science |date=1980 |publisher=Springer |language=en |isbn=978-3-540-39346-7 |pages=51–63 |location=Berlin, Heidelberg |oclc=476017025 |doi=10.1007/3-540-10003-2_59 |editor-last2=van Leeuwen |editor-first2=Jan}}
*{{Cite book |last=Park |first=David |editor-last=Bjøorner |editor-first=Dines |title=On the semantics of fair parallelism |url=http://link.springer.com/10.1007/3-540-10007-5_47 |date=1980 |publisher=Springer Berlin Heidelberg |isbn=978-3-540-10007-2 |pages=504–526 |volume=86 |location=Berlin, Heidelberg |doi=10.1007/3-540-10007-5_47}}
*{{Cite journal |last=Clinger |first=William Douglas |year=1981 |date=1981-05-01 |title=Foundations of Actor Semantics |url=https://hdl.handle.net/1721.1/6935 |journal=AI Technical Reports (1964 - 2004) |publisher=Massachusetts Institute of Technology |language=en-US |type=PhD |id=AITR-633 }}
*{{Cite book |last=Allison |first=L. |title=A Practical Introduction to Denotational Semantics |url=https://books.google.com/books?id=uIdF11msK58C |year=1986 |publisher=Cambridge University Press |isbn=978-0-521-31423-7}}
*{{Cite journal |last=America |first=P. |last2=de Bakker |first2=J. |last3=Kok |first3=J.N. |last4=Rutten |first4=J. |year=1989 |title=Denotational semantics of a parallel object-oriented language |url=https://ir.cwi.nl/pub/1602 |journal=Information and Computation |volume=83 |issue=2 |pages=152–205 |DOI=10.1016/0890-5401(89)90057-6 |doi=10.1016/0890-5401(89)90057-6}}
*{{Cite book |last=Schmidt |first=David A. |title=The Structure of Typed Programming Languages |year=1994 |publisher=MIT Press |isbn=978-0-262-69171-0}}
<!--
* 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.
-->
*{{Cite journal |last=Korff |first=Martin |last2=Ribeiro |first2=Leila |date=1995-01-01 |title=Concurrent Derivations as Single Pushout Graph Grammar Processes |url=https://www.sciencedirect.com/science/article/pii/S157106610580194X |journal=Electronic Notes in Theoretical Computer Science |volume=2 |pages=177–186 |language=en |DOI=10.1016/S1571-0661(05)80194-X |doi=10.1016/S1571-0661(05)80194-X |issn=1571-0661}}
*{{Cite journal |last=Thati |first=Prasanna |last2=Talcott |first2=Carolyn |last3=Agha |first3=Gul |editor-last=Rattray |editor-first=Charles |editor2-last=Maharaj |editor2-first=Savitri |editor3-last=Shankland |editor3-first=Carron |date=2004 |title=Techniques for Executing and Reasoning about Specification Diagrams |url=https://link.springer.com/chapter/10.1007%2F978-3-540-27815-3_39 |journal=Algebraic Methodology and Software Technology |pages=521–536 |publisher=Springer |location=Berlin, Heidelberg |language=en |DOI=10.1007/978-3-540-27815-3_39 |doi=10.1007/978-3-540-27815-3_39 |isbn=978-3-540-27815-3}}
*{{Cite journal |last=Baeten |first=J. C. M. |date=2005-05-23 |title=A brief history of process algebra |url=https://www.sciencedirect.com/science/article/pii/S0304397505000307 |journal=Theoretical Computer Science |volume=335 |issue=2 |pages=131–146 |language=en |DOI=10.1016/j.tcs.2004.07.036 |doi=10.1016/j.tcs.2004.07.036 |issn=0304-3975}}
*{{Cite journal |last=Baeten |first=J. C. M. |date=1989 |title=Algebra and communicating processes |url=https://research.tue.nl/en/publications/algebra-and-communicating-processes |journal=AMAST. Algebraic methodology and software technology. 1st international conference : proceedings, Iowa, USA, 1989 |pages=35–38 |language=English}}
*{{Cite journal |last=Jifeng |first=He |last2=Hoare |first2=C. A. R. |editor-last=Van Hung |editor-first=Dang |editor2-last=Wirsing |editor2-first=Martin |date=2005 |title=Linking Theories of Concurrency |url=https://link.springer.com/chapter/10.1007%2F11560647_20 |journal=Theoretical Aspects of Computing – ICTAC 2005 |pages=303–317 |publisher=Springer |location=Berlin, Heidelberg |language=en |DOI=10.1007/11560647_20 |doi=10.1007/11560647_20 |isbn=978-3-540-32072-2}}
*{{Cite book |last=Aceto |first=Luca |editor-last=Gordon |editor-first=Andrew D. |title=Algebraic Process Calculi: The First Twenty Five Years and Beyond |url=https://www.brics.dk/NS/05/3/index.html |series=BRICS Notes Series |date=June 2005 |publisher=BRICS publications |issn=0909-3206 |others=This volume contains short contributions from the workshop on "Algebraic Process Calculi: The First Twenty Five Years and Beyond", held in the period August 1-5, 2005, at the University Residential Centre of Bertinoro, Forlì, Italy |id=NS-05-3 |chapter-url=https://www.brics.dk/NS/05/3/BRICS-NS-05-3.pdf}}
*{{Cite book |last=Roscoe |first=Bill |title=The Theory and Practice of Concurrency |url=http://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf |date=April 2005 |publisher=Prentice-Hall}}
<!--
* 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) [http://www.pcs.usp.br/~coin-aamas06/10_commitment-43_16pages.pdf ''What is Commitment? Physical, Organizational, and Social''] COIN@AAMAS. 2006.
-->
* {{Cite journal |last=Mosses |author=Peter D. Mosses |first=Peter D. |editor-last=Van leeuwen |editor-first=JAN |year=1990 |date=1990-01-01 |title=CHAPTER 11 - Denotational Semantics |url=https://www.sciencedirect.com/science/article/pii/B9780444880741500160 |journal=Handbook of theoretical computer science Vol.B : Formal Models and Semantics |pages=575–631 |publisher=Elsevier |location=Amsterdam |language=en |doi=10.1016/b978-0-444-88074-1.50016-0 |isbn=978-0-444-88074-1}}
**（邦訳：{{Cite journal |和書 |author=Peter D. Mosses |editor=山田 眞市 |year=1994 |title=表示的意味論 |journal=コンピュータ基礎理論ハンドブックⅡ 形式モデルと意味論 |publisher=丸善株式会社 |ref=Mosses(1990)}}）

== 外部リンク ==
* [http://www.csse.monash.edu.au/~lloyd/tilde/Semantics/ ''Denotational Semantics''] by Lloyd Allison
* [http://www.risc.uni-linz.ac.at/people/schreine/courses/densem/densem.html ''Structure of Programming Languages I: Denotational Semantics''] by Wolfgang Schreiner
* [http://www.cis.ksu.edu/~schmidt/text/densem.html ''Denotational Semantics: A Methodology for Language Development''] by David Schmidt
* [http://www.honors.montana.edu/~jjc/presentation/contents.xhtml Presentation] by Josh Cogliati
* [http://www.hhm.com.ar/hql.htm HQL] by H. Hernan Moraldo &ndash; 小型言語の完全な表示的意味論

{{DEFAULTSORT:ひようしてきいみろん}}
[[Category:表示的意味論|*]]
[[Category:計算モデル]]
[[Category:プログラム意味論]]
[[Category:計算機科学における論理]]
[[Category:形式仕様記述言語]]
[[Category:数学に関する記事]]

[[es:Semántica denotacional]]