形式的意味論（操作的・表示的・公理的）

「このプログラムの意味」を数学で固定する

x := x + 1 という代入の意味は何か。日本語で「x に1を足す」と書けば人間には伝わりますが、評価順序や副作用、未定義動作の境界までは曖昧なままです。言語仕様が散文で書かれていると、実装ごとに解釈が割れ、コンパイラのバグや移植性の問題が生まれます。形式的意味論（formal semantics）は、構文（プログラムの形）に対して意味を数学的に厳密に割り当てることで、この曖昧さを根絶する枠組みです。構文を定める文法（字句解析・構文解析の外側）に対し、形式的意味論は「その構文が何を意味するか」を担います。

意味の与え方には伝統的に3つのアプローチがあります。同じ言語を3つの異なる視点から定義するもので、どれが正しいというより、目的に応じて使い分け、互いに整合性を確認し合う関係にあります。

操作的意味論：実行を遷移規則で定義する

操作的意味論（operational semantics）は、プログラムが「どう動くか」を抽象的な実行ステップの列として定義します。中心概念は状態（store、変数から値への写像）と遷移関係です。代表的な2つのスタイルがあります。

• 小ステップ意味論（small-step / 構造的操作的意味論, SOS）：1ステップの計算を <式, 状態> → <式', 状態'> という遷移で定義し、これを繰り返して実行を進める。簡約の途中状態が見えるため、並行性や停止しない計算を扱いやすい。
• 大ステップ意味論（big-step / 自然意味論）：「式が状態のもとで最終的にこの値に評価される」を <式, 状態> ⇓ 値 の形で一気に定義する。インタプリタの構造に近く読みやすいが、途中で詰まる計算や無限ループの区別は苦手。

遷移規則は推論規則（前提が線の上、結論が下）の形で書きます。たとえば代入文の大ステップ規則は次のように読めます。

       <e, σ> ⇓ n
------------------------------     （e を現在の状態 σ で評価して n を得たら、
 <x := e, σ> ⇓ σ[x ↦ n]              状態を「x を n に更新したもの」へ変える）

ここで σ[x ↦ n] は「σ のうち x だけを n に差し替えた新しい状態」を表す記法です。条件分岐やループも同様に規則で定義され、while は「条件が真なら本体を実行して再び while に戻る」という自己参照的な規則になります。操作的意味論の強みは、実装に直結することです。規則をそのままコードに落とせばリファレンス・インタプリタになり、型安全性の証明で使う「型保存」「進行」もこの遷移関係の上で述べられます。

表示的意味論：プログラムを数学的対象へ写す

表示的意味論（denotational semantics）は、各プログラム断片に対して、それが「表す」数学的対象を直接割り当てます。中心にあるのが意味関数 [[ ]]（二重角括弧、semantic brackets）で、たとえば算術式 e の意味は「状態を受け取って数を返す関数」 [[e]] : 状態 → 数 として定義されます。文の意味は「状態を受け取って新しい状態を返す関数」 [[S]] : 状態 → 状態 です。

最大の特徴は合成性（compositionality）です。複合式の意味は、その部分式の意味だけから組み立てられます。[[S1 ; S2]] = [[S2]] ∘ [[S1]]（順次実行は意味関数の合成）のように、構文の構造に沿って意味が決まる。これにより「部品の意味を理解すれば全体が分かる」というモジュール性が保証され、言語設計時に各構文が何を意味するかを独立に検討できます。

問題になるのが while のような再帰的な構文です。「ループの意味」は「ループの意味」自身を使って定義したくなり、循環します。これを解決するのが領域理論（domain theory）で、ループの意味を「ある写像の最小不動点」として与えます。

W = [[while b do S]] とおくと、W は次を満たす関数（不動点方程式）：

W(σ) = if [[b]](σ) then W([[S]](σ)) else σ
        └─ 条件が真なら本体を1回実行して再び W、偽ならそのまま終了 ─┘

この方程式を満たす関数のうち「最も情報の少ない（停止しない箇所を未定義 ⊥ とする）」
ものを最小不動点として採用する。

未定義（発散）を表す底元 ⊥ を含む順序付き集合（ドメイン）を用意し、連続関数の最小不動点が必ず存在することを保証するのがクリーネの不動点定理です。停止しないループはきちんと「⊥ を返す関数」として意味づけられ、表示的意味論は無限ループも数学的にごまかさず扱えます。

公理的意味論：成り立つ性質で意味を定める

公理的意味論（axiomatic semantics）は、プログラムが「どう動くか」「何を表すか」ではなく、「実行の前後で何が成り立つか」で意味を捉えます。中核がホーア論理（Hoare logic）のホーア三つ組 {P} S {Q} です。

{P} S {Q}    の読み方：

「事前条件 P が成り立つ状態で文 S を実行し、もし S が停止するなら、
 停止後の状態では事後条件 Q が必ず成り立つ」

P Q は状態についての論理式（表明, assertion）です。たとえば {x = 5} x := x + 1 {x = 6} は「x が5の状態で x := x + 1 を実行すれば、後で x は6になる」という主張で、これが証明可能であることがこの文の正しさを意味します。各構文には推論規則があり、代入規則が最も基本的です。

代入の公理：  { Q[x ↦ e] } x := e { Q }

事後条件 Q の中の x を e で置き換えたものが事前条件になる。
例： Q が「x = 6」なら、x を x+1 で置換した「x+1 = 6」つまり「x = 5」が事前条件。

ループにはループ不変条件（loop invariant）という強力な道具があります。「ループの各反復の前後で常に成り立つ性質」を1つ見つければ、何回反復しても成り立つことが帰納的に保証され、ループ全体の事後条件が導けます。さらに、停止性まで保証する版を全正当性（total correctness）、停止すれば正しいだけの版を部分正当性（partial correctness）と区別します。停止性は反復ごとに減る整礎な「測度（variant）」を示すことで証明します。

3者の関係と、現場での役割

3つは独立した別物ではなく、互いを裏打ちする関係にあります。公理的意味論の規則が「正しい」とは、それで証明できる三つ組が表示的（または操作的）な意味のもとで実際に成立すること、つまり健全性（soundness）を指します。逆に、成立する三つ組はすべて証明できるという完全性も問われます。表示的と操作的のあいだは前述の完全抽象性で結ばれます。つまり同じ言語に対する3つの定義は、整合性を相互検証できる三角形を成しています。

実務での価値は具体的です。言語仕様を形式的意味論で書けば、実装間の解釈の食い違い（移植性バグの温床）が消えます。C言語の未定義動作のような落とし穴も、本来はここで境界を定めるべき領域です。コンパイラ検証では、操作的意味論を使って「最適化前と後でプログラムの意味が変わらない」を証明します（CompCertが実機で達成した成果です）。プログラム検証ツールは公理的意味論を基盤に、関数の事前・事後条件から正しさを機械的に確かめます。さらに、入力を生成して性質を検査するプロパティベーステストが表明する「性質」は、公理的意味論の事後条件を実行可能にしたものと見なせます。

まとめ

形式的意味論は、構文に数学的な意味を割り当ててプログラムの挙動を曖昧さなく固定する枠組みです。操作的意味論は遷移規則で「どう実行されるか」を定義し、インタプリタと型安全性証明の土台になります。表示的意味論はプログラムを数学的関数へ写し、合成性と（ループは最小不動点で扱う）厳密な意味を与えます。公理的意味論はホーア論理で事前・事後条件による「何が成り立つか」を述べ、最弱事前条件を通じて検証を機械化します。3者は健全性・完全抽象性で互いに整合し、言語仕様の厳密化・コンパイラ検証・プログラム検証という現場の信頼性を、根拠を持って支えています。意味を散文でなく数学で語れることが、「本当にこう動く」と言い切るための土台になります。