操作的意味論

操作的意味論（そうさてきいみろん、Operational Semantics）とは、プログラムの意味を数学的に厳密に与える計算機科学の手法の一種（プログラム意味論参照）。

概要

プログラミング言語の操作的意味論は、有効なプログラムを計算ステップのシーケンスとして解釈する様子を記述する。そのようなシーケンスがプログラムの意味となる。関数型言語では、シーケンスの最後にはプログラムの値が返される。（一般にプログラムには非決定性があるため、ひとつのプログラムが返す値はひとつではなく、計算シーケンスも様々であることがある。）

典型的な操作的意味論の厳密な定義を与えたのは Gordon Plotkin の1981年の論文 "A Structural Approach to Operational Semantics"（操作的意味論への構造的アプローチ）が最初である。それは、対象言語に対応する状態遷移系を用意するものであった。そのような定義により言語の形式的分析が可能となり、プログラム間の関係を研究することが可能となった。重要な関係として Simulation Preorderと双模倣性がある。これらは特に並行性を扱う場合に有用である。並行性に関する意味論を扱う別の方法として、アクターモデルのイベント構造を利用する方法がある。

状態遷移系による操作的意味論の定義は、一般に可能な遷移の集合の帰納的定義を与えることによってなされる。これは通常、系の正しい遷移群を定義する推論規則の形式となる。

世界初の操作的意味論はラムダ計算のそれであった。SECDマシンの流れを汲む抽象機械も極めて近い関係にある。

参考文献

• Gordon D. Plotkin. A Structural Approach to Operational Semantics. (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark.
• Gordon D. Plotkin. A Structural Approach to Operational Semantics. (2004) Preprint submitted to Journal of Logic and Algebraic Programming.