|
表示的意味論（ひょうじてきいみろん、Denotational Semantics）とは、計算機科学（理論計算機科学）の一分野で、プログラミング言語の形式意味論（プログラム意味論）の手法のひとつである。初期には「数理的意味論」（mathematical semantics）、「スコット-ストレイチー意味論」（Scott–Strachey semantics）のようにも呼ばれた。プログラムの意味をあらわす数学的オブジェクト（これを「表示」（denotation）と呼ぶ）を構築することで、プログラミング言語の意味論を形式化する手法である。 表示的意味論の起源は、1960年代のクリストファー・ストレイチーやデイナ・スコットの研究である。ストレイチーやスコットが開発した本来の表示的意味論は、プログラムの表示（意味）を入力を出力にマッピングする関数に変換するものである。後にこれはプログラムの表示（意味）を定義するには非力であることが証明され、例えば再帰定義関数・データ構造を表現できないことが判明した。これを解決するため、スコットはより汎用的な領域理論に基づいた表示的意味論を提案した〔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)〕。その後、研究者らはPower Domainsに基づいた手法を提案し、並行システムの意味論の困難さを克服する努力をしている〔Gordon Plotkin. ''A powerdomain construction'' SIAM Journal of Computing. September 1976.〕。 == 不動点意味論 == 表示的意味は、システムが行うことを表現する数学的オブジェクトを探すことに関心がある。この理論は計算の数学的領域（ドメイン）を利用する。そのような領域の例として完備半順序集合などがある。 関係 x≤y は、x が y に計算的に発展する可能性があることを意味する。表示が完備半順序集合の要素ならば、例えば f≤g は f が定義されている全ての値について g と等しいことを意味する。 計算領域は次のような特徴を持つ: # ''下限の存在'': 領域には必ず ⊥ で表される要素が含まれ、領域内の任意の要素 x について ⊥≤x が成り立つ。 # ''上限の存在'': 計算を続けると表示は洗練されるが、限界を持つべきである。そのため、 としたとき、上限 が存在する。これを -完全と呼ぶ。 # ''有限要素は可算'': 有向集合 A について ∨A が存在し であるとき、 であるような が存在する。そのとき、要素 x は有限であるという（領域理論的に言えば、isolated）。換言すれば、x に到達あるいは x を超えるのに有限のプロセスで可能であるなら、x は有限である。 # ''全ての要素は有限要素の順序列の上限である'': 任意の要素に有限の計算手順で到達することを意味している。 # ''領域は downward closed である'' システム S に関する数学的表示は、初期の空の表示 ⊥S から始めて、表示近似関数 progressionS を使って S の表示（意味）を構築していくことでよりよい近似を作っていくことで構築される。これは以下のように表される: ここで、progressionS は「単調」であるべきで、x≤y であるとき progressionS(x)≤progressionS(y) である。さらに一般化すると次のように表される。 このような progressionS の特徴を ω-連続と呼ぶ。 表示的意味論では、DenoteS の方程式に従って表示（意味）を作成可能かどうかを主題とする。計算領域理論の基本的定理は、progressionS が ω-連続ならば、DenoteS が存在するというものである。 そこで、progressionS が ω-連続であることから以下が成り立つ: これはつまり、DenoteS が progressionS の「不動点; fixed point」であることを意味する。 さらに、この不動点は progressionS の不動点の中で極小である。 関数型言語の表示的意味論の実例を次節に示す。 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「表示的意味論」の詳細全文を読む スポンサード リンク
|