プログラム意味論

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

プログラム意味論(Program Semantics)とは、理論計算機科学の一分野で、プログラミング言語の意味と計算モデルに関する厳密な数学的研究領域である。プログラミング言語の形式意味論とも呼ばれる。

ある言語の形式意味論は、その言語で表現可能な処理（計算）を表す数学的モデルによって与えられる。

[編集] 分類

プログラム意味論にはいくつかの手法があり、以下の 3 種類に大別される:

表示的意味論: 対象とする言語の語句それぞれを「表示」に変換、すなわち別の言語の語句に翻訳する。表示的意味論はコンパイルと対応すると考えることもできるが、通常翻訳先の言語は他のコンピュータ言語ではなく数学的形式言語であることが多い。例えば、関数型言語の表示的意味論では、領域理論の言語に翻訳する。
操作的意味論: 何らかの変換を施すのではなく、その言語の実行によって直接的に意味を説明する。操作的意味論はインタプリタと対応すると考えることもできるが、この場合の「インタプリタの実装」は何らかのコンピュータ上での実装ではなく、数学的形式主義によるものである。操作的意味論を抽象機械（例えばSECDマシン）と定義することも可能で、プログラムの語句の並びが抽象マシンの上で引き起こす状態変化を説明することによって各語句の意味を説明する。あるいは、純粋なラムダ計算のように、操作的意味論を対象言語の語句の並びの統語的変形過程と定義することもできる。
公理的意味論: 語句の並びに「論理学的公理」を適用することによって意味を明らかにする。公理的意味論では語句の意味とそれを表す論理式を区別しない。この場合、プログラムの意味は論理学で証明可能なものと等価である。公理的意味論の典型的な例としてホーア論理がある。

この分類は必ずしも完全ではないが、既存の手法は上記3種類のいずれかを使っているか、いくつかを組み合わせている。

上記分類とは別に、利用している数学的形式手法によってプログラム意味論を分類することもある。

[編集] 派生

プログラム意味論からの派生として以下のようなものがある:

「Action Semantics」は表示的意味論をモジュール化し、形式化プロセスを2段階（マクロ意味論とマイクロ意味論）に分け、意味の表示を単純化するために 3種類の意味論的実体（action、data、yielder）を予め定義したものである。
「属性文法」は、言語の様々な文法の「メタデータ」（属性）を系統立てて計算するシステムを定義する。属性文法を対象言語に属性を付与する表示的意味論の一種と見ることもできる。プログラム意味論以外でも、属性文法はコンパイラのコード生成に使われたり、正規文法や文脈自由文法を文脈依存言語に変換するのに使われる。
「関数的意味論」または「圏論的意味論」は圏論を基本とした形式意味論である。
「並行性意味論」は並行処理の形式意味論を扱う意味論一般を指す。特筆すべきものとしてはアクターモデルやプロセス代数がある。
「ゲーム意味論」はゲーム理論を基本とした形式意味論である。

[編集] 意味論間の関係

場合によっては、異なる意味論間の関係を説明する必要が生じる。例えば:

ある言語の操作的意味論の結果が、その言語の公理的意味論の論理式と矛盾しないことを証明する必要が生じるかもしれない。そのような証明は、特定の（公理的）「証明システム」を使って特定の（操作的）「インタプリタ」を論じることが健全であることを保証する。
ある言語について、高レベルの抽象機械と低レベルの抽象機械を定義したとする。ここで、後者は前者よりも基本的な操作を含む。両者における操作的意味が双模倣性によって関連していることを証明する必要が生じるかもしれない。そのような証明は、低レベルの抽象機械が高レベルの抽象機械を「忠実に実装」することを保証する。

複数の意味論の関連付けは、抽象インタプリタ理論による抽象によって行うことが可能な場合もある。

[編集] 領域

プログラム意味論の領域には、以下のようなものが含まれる:

意味論的モデルの定義
異なる意味論的モデル間の関係
意味についての異なるアプローチ間の関係
計算とその根底にある数学的構造（数理論理学、集合論、モデル理論、圏論）との関係

計算機科学の中で密接に関連する分野として、プログラミング言語設計、型理論、コンパイラ、インタプリタ、プログラム検証、モデル検査などがある。

[編集] 外部リンク

[編集] 参考文献

Shriram Krishnamurthi. Programming Languages: Application and Interpretation. (online, as PDF)
John C. Reynolds. Theories of Programming Languages. Cambridge University Press, 1998. (ISBN 0-521-59414-6)
Carl Gunter. Semantics of Programming Languages. MIT Press, 1992. (ISBN 0-262-07143-6)
Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993 (paperback ISBN 0-262-73103-7)