プログラム意味論

プログラム意味論（プログラムいみろん、英: program semantics）とは、計算機科学（特に理論計算機科学と分類されることもある）の一分野で、プログラミング言語の意味と計算モデルに関する分野である。形式的なものは、プログラミング言語の形式意味論とも呼ばれる。標準規格等では形式的でなく意味論を与えているものも多い。

形式的意味論

形式化にはいくつかの手法があり、以下の 3 種類に大別される:

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

この分類は必ずしも完全ではなく、また明確に分類できるものでもないが、既存の、意味論を形式化する手法は上記3種類のいずれかを使っているか、いくつかを組み合わせている。上記分類とは別に、利用している数学的形式手法によってプログラム意味論を分類することもある。

派生

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

「Action Semantics」は表示的意味論をモジュール化し、形式化プロセスを2段階（マクロ意味論とマイクロ意味論）に分け、意味の表示を単純化するために 3種類の意味論的実体（action、data、yielder）を予め定義したものである。
「属性文法」は、言語の様々な文法の「メタデータ」（属性）を系統立てて計算するシステムを定義する。属性文法は、対象言語の構文に基づきそれに属性という形で意味を付与する、表示的意味論の一種と見ることもできる。プログラム意味論以外の応用・活用例としては、正規文法や文脈自由文法を文脈依存言語に変換する手法や、yaccの定義などがある（yaccにおいてCFGの規則に付随する「アクション」は、属性文法における「属性値」を得るための規則に他ならず、CFGの規則に「意味規則」が付いているyaccの定義は、属性文法となっている^[1]）。
「関数的意味論」または「圏論的意味論」は圏論をベースとした形式意味論である。
「並行性意味論」は並行処理の形式意味論を扱う意味論一般を指す。特筆すべきものとしてはアクターモデルやプロセス代数がある。
「ゲーム意味論」はゲーム理論をベースとした形式意味論である。

意味論間の関係

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

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

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

分野

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

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

コンピュータ科学の中で密接に関連する分野として、プログラミング言語、型理論、コンパイラやインタプリタ等のプログラミング言語処理系、形式的検証、モデル検査などがある。

注

^ 実用上は一般的な使い方とはなっていないが、yacc（Yet Another Compiler Compiler）の言葉通り、yaccが定義から生成するコードがそれだけで完備した言語処理系になるように使えば、それは属性文法によってその言語の意味論を定義して、yaccにより自動的に処理系を生成した、ということになり、実はプログラム意味論そのものの応用となる。

外部リンク

参考文献

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)

[1] 実用上は一般的な使い方とはなっていないが、yacc（Yet Another Compiler Compiler）の言葉通り、yaccが定義から生成するコードがそれだけで完備した言語処理系になるように使えば、それは属性文法によってその言語の意味論を定義して、yaccにより自動的に処理系を生成した、ということになり、実はプログラム意味論そのものの応用となる。

[1]