Operational semantics

構造的操作意味論（SOS、構造化操作意味論または小ステップ意味論とも呼ばれる）は、操作意味論を定義する論理的な手段として、ゴードン・プロトキンによって（Plotkin81）に導入されました。SOSの基本的な考え方は、プログラムの動作をその構成要素の動作に基づいて定義し、操作意味論に対する構造的、つまり構文指向かつ帰納的な視点を提供することです。SOS仕様は、遷移関係（の集合）に基づいてプログラムの動作を定義します。SOS仕様は、構成要素の遷移に基づいて、複合構文の有効な遷移を定義する推論規則の集合の形式をとります。

簡単な例として、単純なプログラミング言語のセマンティクスの一部を考えてみましょう。適切な図解は、Plotkin81、Hennessy90、およびその他の教科書に記載されています。${\displaystyle C_{1},C_{2}}$言語のプログラムの範囲を、${\displaystyle s}$状態の範囲 (例えば、メモリ位置から値への関数)。式 (範囲が${\displaystyle E}$）、値（${\displaystyle V}$）と場所（${\displaystyle L}$) ならば、メモリ更新コマンドには次のような意味論が成り立つだろう。

${\displaystyle {\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}}$

非公式には、このルールは「表現が${\displaystyle E}$州内${\displaystyle s}$価値を下げる${\displaystyle V}$するとプログラム​${\displaystyle L:=E}$状態を更新します${\displaystyle s}$課題と共に${\displaystyle L=V}$「。

シーケンスの意味論は、以下の3つの規則によって規定される。

1.${\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}}$

2.${\displaystyle {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}}$

3.${\displaystyle {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}}$

非公式には、最初のルールは、プログラムが${\displaystyle C_{1}}$州内${\displaystyle s}$州大会で優勝${\displaystyle s'}$するとプログラム${\displaystyle C_{1};C_{2}}$州内${\displaystyle s}$プログラムを削減します${\displaystyle C_{2}}$州内${\displaystyle s'}$（これは「実行できます」を形式化したものと考えることができます）${\displaystyle C_{1}}$そして、${\displaystyle C_{2}}$ 結果として得られるメモリ ストアを使用する。）2 番目のルールは、プログラムが${\displaystyle C_{1}}$州内${\displaystyle s}$プログラムを削減できます${\displaystyle C_{1}'}$状態とともに${\displaystyle s'}$するとプログラム${\displaystyle C_{1};C_{2}}$州内${\displaystyle s}$プログラムを削減します${\displaystyle C_{1}';C_{2}}$州内${\displaystyle s'}$（これは最適化コンパイラの原理を形式化したものと考えることができます。「変換は許可されています」）${\displaystyle C_{1}}$（たとえそれがプログラムの最初の部分であっても、独立したプログラムであるかのように）意味論は構造的である。なぜなら、逐次プログラムの意味は${\displaystyle C_{1};C_{2}}$は、の意味によって定義されます。${\displaystyle C_{1}}$そしてその意味は${\displaystyle C_{2}}$。

状態に対するブール式も持っている場合、${\displaystyle B}$そうすれば、 whileコマンド の意味を定義できます。${\displaystyle {\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}}$

このような定義により、プログラムの動作を形式的に分析することが可能になり、プログラム間の関係を研究することができる。重要な関係としては、シミュレーションの順序関係や双模倣性などが挙げられる。これらは特に並行性理論の分野で有用である。

直感的な外観と分かりやすい構造のおかげで、SOSは大きな人気を集め、操作的意味論を定義する事実上の標準となっています。その成功の証として、SOSに関する最初の報告書（いわゆるオーフス報告書）（Plotkin81）は、CiteSeerによると1000件以上の引用を集めています。そのため、コンピュータサイエンス分野で最も引用されている技術レポートの一つとなっている。

還元意味論は、操作意味論の別の表現です。その主要なアイデアは、1975 年にGordon Plotkinによってラムダ計算の純粋関数型の名前渡しと値渡しのバリアントに初めて適用され^{[ 3 ]} 、 1987 年の博士論文でMatthias Felleisenによって命令型機能を持つ高階関数型言語に一般化されました。 ^{[ 4 ]}この方法は、1992 年に Matthias Felleisen と Robert Hieb によって、制御と状態のための完全な等式理論へとさらに発展しました。^{[ 2 ]} 「還元意味論」というフレーズ自体は、1987 年の PARLE の論文でFelleisen とDaniel P. Friedmanによって初めて造語されました。 ^{[ 5 ]}

縮約意味論は、それぞれが単一の潜在的な縮約ステップを指定する一連の縮約規則として与えられます。たとえば、次の縮約規則は、代入文が変数宣言のすぐ隣にある場合に縮約できることを示しています。

${\displaystyle \mathbf {let\ rec} \ x=v_{1}\ \mathbf {in} \ x\leftarrow v_{2};\ e\ \ \longrightarrow \ \ \mathbf {let\ rec} \ x=v_{2}\ \mathbf {in} \ e}$

代入文をそのような位置に配置するには、関数適用と代入文の右辺を通って「バブルアップ」し、適切な位置に到達するまで続けます。${\displaystyle \mathbf {let} }$式は異なる変数を宣言することができ、計算では押し出し規則も要求される。${\displaystyle \mathbf {let} }$表現。還元意味論の公開されている使用例のほとんどは、このような「バブルルール」を評価コンテキストの利便性で定義しています。たとえば、単純な値渡し言語における評価コンテキストの文法は次のように表すことができます。

${\displaystyle E::=[\,]\ {\big |}\ v\ E\ {\big |}\ E\ e\ {\big |}\ x\leftarrow E\ {\big |}\ \mathbf {let\ rec} \ x=v\ \mathbf {in} \ E\ {\big |}\ E;\ e}$

どこ${\displaystyle e}$は任意の式を表し、${\displaystyle v}$は完全に縮小された値を表します。各評価コンテキストには、正確に1つの穴が含まれます。${\displaystyle [\,]}$そこに、ある項が捕捉的な方法で差し込まれる。文脈の形状は、この穴によって削減が起こりうる場所を示している。評価文脈を用いて「バブリング」を説明するには、次の単一の公理で十分である。

${\displaystyle E[\,x\leftarrow v;\ e\,]\ \ \longrightarrow \ \ x\leftarrow v;\ E[\,e\,]\qquad {\text{(lift assignments)}}}$

この単一の簡約規則は、フェライゼンとヒーブによる代入文のためのラムダ計算におけるリフト規則である。評価コンテキストによってこの規則は特定の項に限定されるが、ラムダ式を含むあらゆる項に自由に適用できる。

プロトキンによれば、一連の還元規則から導出された計算体系の有用性を示すには、（1）評価関数を誘導する単段階関係に対するチャーチ・ロッサー補題と、（2）評価関数における非決定的な探索を決定的な左端／最外側探索に置き換える単段階関係の推移的反射閉包に対するカリー・フェイズ標準化補題が必要である。フェライゼンは、この計算体系の命令的拡張がこれらの定理を満たすことを示した。これらの定理の帰結として、等式理論（対称推移的反射閉包）は、これらの言語にとって健全な推論原理である。しかし実際には、還元意味論のほとんどの応用では、この計算体系は不要となり、標準的な還元（およびそこから導出できる評価器）のみを使用する。

還元意味論は、評価コンテキストが状態や特殊な制御構造（例えば、第一級継続）を容易にモデル化できることから特に有用です。さらに、還元意味論は、オブジェクト指向言語^{[ 6 ]} 、契約システム、例外、フューチャー、必要に応じた呼び出し、その他多くの言語機能のモデル化に使用されてきました。還元意味論に関する徹底的かつ現代的な解説で、そのような応用例を詳しく論じているのは、Matthias Felleisen、Robert Bruce Findler、Matthew Flattによる『Semantics Engineering with PLT Redex』^{[ 7 ]}です。

ビッグステップ構造操作意味論は、自然意味論、関係意味論、評価意味論という名称でも知られています。^{[ 8 ]}ビッグステップ操作意味論は、 MLの純粋な方言である Mini-ML を発表した際に、ジル・カーンによって自然意味論という名称で導入されました。

大きなステップの定義は、関数の定義、あるいはより一般的には関係の定義と見なすことができ、各言語構成要素を適切なドメインで解釈します。その直感性から、プログラミング言語のセマンティクス仕様としてよく用いられますが、制御集約型機能や並行処理を備えた言語など、多くの状況で不便または使用不可能となる欠点もいくつかあります。^{[ 9 ]}

ビッグステップ意味論は、言語構成要素の最終的な評価結果が、それらの構文上の対応物（部分式、部分文など）の評価結果を組み合わせることによってどのように得られるかを、分割統治法を用いて記述する。