表示的意味論

計算機科学における表示的意味論（ひょうじてきいみろん、denotational semantics）とは、プログラミング言語に代表される形式言語の意味付け理論の一つである。意味付けを行いたい文言や構文の世界とその意味の世界を用意し、意味関数で対応付けを行うという典型的な意味付け理論の形態を取るが、再帰的定義された構文についてはその集積点にあたるものを対応付けることで意味付けを行うというところに特徴がある。

概要

導入：無理数（実数）の発見

古代ギリシャの学者ピタゴラス（Pythagoras）は正方形の対角線の長さ d とその辺の長さ s の間の比 r = d/s は方程式

d² = (rs)² = s² + s²　（ピタゴラスの定理）

を満たさねばならないことを知っていた。そのためピタゴラスは r² = 1² + 1² = 2 を満たす”数” r があると考えた。

現代においてはよく知られているように r は無理数（実数体の元）である ${\sqrt {2}}$ = 1.412... であるが、”数”とは整数の比で表されるもの（有理数）であると信じていたピタゴラスにとって、整数の比で書き表す事ができない無限の小数点展開が必要な r は”数”を意味しなかった（認識されなかった）。他方、現代においては実数体（無理数の属する領域）の概念はほとんど最初からあたえられているものであり、整数、有理数と同列に認識されているため、ピタゴラスが直面したような困難にぶつかることはほとんどないが、数の実際の計算という観点からは実数体の元（特に無理数）とは非常に観念的な性質を持つものである。

歴史

表示的意味論の起源は、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₂>" の意味が導かれることを意味する。

脚注

参考文献

• 山崎 進『計算論理に基づく推論ソフトウェア論』コロナ社、2000年。 
• 横内寛文『プログラム意味論』1994年。 
• Dana Scott (1976), Data types as lattices, http://www.cs.ox.ac.uk/files/3287/PRG05.pdf 
• Dana Scott (1970), Outline of a Mathematical Theory of Computation, http://port70.net/~nsz/articles/classic/scott_theory_of_computation_1970.pdf 
• Christopher Strachey (1967), Fundamental Concepts in Programming Languages, http://www.itu.dk/courses/BPRD/E2009/fundamental-1967.pdf 
• Dana Scott , Christopher Strachey (1971), Toward a mathematical semantics for computer languages, http://ecee.colorado.edu/ecen5533/fall11/reading/PRG06.pdf 
• Alfred Tarski (1955), A lattice-theoretical fixpoint theorem and its applications, http://projecteuclid.org/DPubS/Repository/1.0/Disseminate?view=body&id=pdf_1&handle=euclid.pjm/1103044538 
• Joseph E. Stoy (1977). Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press 
• ガーレット・バーコフ, ソンダース・マクレーン『現代代数学概論 改訂第３版』白水社、1967年。  第IV章、XI章
• 前田 周一郎『束論と量子論理』槙書店、1980年。 
• Garrett Birkhoff (1979). Lattice Theory (3rd ed.) 
• George Grätzer (1979). Universal Algebra (2nd ed.) 
• George Grätzer (2003). General Lattice Theory (2nd ed.) 
• George Grätzer (2011). Lattice Theory: Foundation 
• 吉永 悦男『初等解析学―実数+イプシロン・デルタ+積分』1994年。ISBN 4563002305。 
• 上村 務 (1989), プログラムの表示的意味論, http://ci.nii.ac.jp/naid/110002762191 
• Bertland Russell (1905), On Denoting, http://revueltaredaccion.files.wordpress.com/2012/08/russell_on_denoting.pdf 
• G. Markowsky (1981), A motivation and generalization of Scott's notion of a continuous lattice, Springer, pp. 298–307, http://www.laptop.maine.edu/ContinuousLattices.pdf  CPO導入の経緯、その解説

関連項目

• ピタゴラス
• 有理数
• 実数
• 集積点
• コーシー列
• デデキント切断

• 束 (代数学)
• 順序集合
• 図式スキーム
• 普遍性
• モナド (プログラミング)