Logo

Nola's Backyard

プログラム意味論って何？

投稿日 :2026/8/27

最終更新日 :2026/8/27

プログラマーのための圏論を読んでいて、(プログラム) 意味論なる概念が出てきた。

代表的なものとして、次の3つがあるらしい。

  1. 表示的意味論
  2. 操作的意味論
  3. 公理的意味論

これらの雰囲気を知りたくて調べていたところ、

「構文要素に対して何らかの (表示的、操作的、公理的) 方法で意味を与え、その方法の中でそれらを組み合わせることでプログラム全体の意味を構成している」と思えばわかりやすいのでは？

と思ったので、やってみる。(この記事の目的)

# そもそも

そもそもプログラム意味論って何なのか。とりあえずプログラム意味論 - Wikipedia を置いておきます。

置いておきましたが、このページは私にとってはとても難しかったので、私の理解も置いておきます。

プログラム意味論では、プログラムを記号と意味に分解して考える。つまり、プログラマが書くコードはただの記号であり、それだけでは意味を持たないと思うことにする。このとき、その記号に対してどのように意味を与えるのか、がプログラム意味論の仕事である。

なぜそんなことをするのかというと、ただの記号でしかないプログラムに対して意味を与え、数学と接続することで、プログラムの等価性や正しさを厳密に扱えるようにすること な気がする。 である。

# 構文要素に解釈を与える例

以下のような単純な代入に、それぞれの方法での解釈 (意味) を与えてみる。

x := x + 1

同時に、それぞれの方法の特性を簡単に紹介する。

# 表示的意味論

表示的意味論は、構文要素に対して数学的対象を対応づけることで意味を定める方法である。

x := x + 1 は写像として捉え、次のように書く。

[[x:=x+1]](σ)=σ[x↦σ(x)+1] x:=x + 1(\sigma) = \sigma[x\mapsto\sigma(x)+1]

ただし、プログラム全体の (変数の) 状態を σ\sigma と置いた。

Hint

これは、写像

[[x:=x+1]]:State⟶State x:=x+1:\mathrm{State}\longrightarrow\mathrm{State}

の定義と見る。

σ[x↦σ(x)+1]\sigma[x\mapsto\sigma(x)+1] は、状態 σ\sigma のうち、変数 xx の値だけを σ(x)+1\sigma(x)+1 に更新した状態を指す。

# 操作的意味論

操作的意味論は、プログラムの構文要素が、ある状態のもとでどの値または状態へ 評価 されるかを、推論規則によって定める方法。

ここで「評価」とは、構文要素 cc と実行前の状態 σ\sigma に対して、その実行結果 rr を、

⟨c,σ⟩⇓r \langle c,\sigma\rangle\Downarrow r

という評価関係によって結びつけることを指す。rr は、cc が式なら値、命令なら実行後の状態となる。

例えば、x := x + 1 は命令なので、その評価結果は実行後の状態となる。

⟨x:=x+1,σ⟩⇓σ[x↦σ(x)+1] \langle x := x+1,\sigma\rangle \Downarrow \sigma[x\mapsto\sigma(x)+1]

x = 3 で実行すれば、状態 σ\sigma は x = 3 であり、

⟨x:=x+1, [x↦3]⟩⇓[x↦4] \langle x := x+1,\,[x\mapsto3]\rangle \Downarrow [x\mapsto4]

となる。

Note

この段階では表示的意味論との違いが分かりづらいが、後述する「組み合わせて全体を解釈する例」パターンを見るとわかるといいな。

# 公理的意味論

公理的意味論は、プログラムの構文要素の実行前後にどのような命題が成り立つかを見て、間接的に意味を与える方法。

x := x + 1 は次のように書く。

{x=n}  x:=x+1  {x=n+1} \{x=n\}\;x:=x+1\;\{x=n+1\}

「実行前に x = n が成り立っていれば、x := x + 1 を実行した後には x = n + 1 が成り立つ」というふうに読む。

Note

このような記法をホーアトリプル (Hoare triple) といい、一般に次の形で表す。

{P}  C  {Q} \{P\}\;C\;\{Q\}
  • PP：実行前に成り立つ命題。事前条件と呼ぶ
  • CC：実行するプログラム
  • QQ：実行後に成り立つ命題。事後条件と呼ぶ

これは、「PP が成り立つ状態から CC を実行し、CC が停止したなら、実行後には QQ が成り立つ」と読む。

そして、ホーアトリプルを導くための公理と推論規則からなる体系をホーア論理 (Hoare logic) という。ホーア論理は、公理的意味論を与える代表的な方法の1つである。

# 組み合わせて全体を解釈する例

次にもう少し複雑な例、そして上述の意味づけを「組み合わせる」例として、簡単なwhile文に、それぞれの方法で解釈を与えてみる。

while x > 0 do
    x := x - 1

以下では、変数の値は整数であるとする。

# 表示的意味論

まず、条件式 x > 0 と代入文 x := x - 1 に、それぞれ数学的な意味を与える。

x > 0 は、状態 σ\sigma を真偽値に写す写像として捉える。

[[x>0]](σ)=(σ(x)>0) x>0(\sigma) = (\sigma(x)>0)

x := x - 1 は下記の写像と解釈する。

[[x:=x−1]](σ)=σ[x↦σ(x)−1] x:=x-1(\sigma) =\sigma[x\mapsto\sigma(x)-1]

この2つを使って、while文全体を表す写像 WW を次のように定める。

W(σ)={W([[x:=x−1]](σ))[[x>0]](σ)=trueσ[[x>0]](σ)=false W(\sigma)= \begin{cases} W(x:=x-1(\sigma)) & x>0(\sigma)=\mathrm{true}\\ \sigma & x>0(\sigma)=\mathrm{false} \end{cases}

つまり、x > 0 なら x := x - 1 が表す写像を適用してから再び WW を適用し、x > 0 でなければ現在の状態をそのまま返す。

一般に、実行前の x が正なら結果は x = 0 となり、x が0以下なら状態は変化しない。したがって、任意の状態 σ\sigma について、WW は次のようにも書ける。

W(σ)=σ[x↦min⁡(σ(x),0)] W(\sigma) =\sigma[x\mapsto\min(\sigma(x),0)]

このように、表示的意味論では、条件式と代入文に対応する数学的な意味 (写像) を組み合わせて、while文全体に対応する写像を構成する。

Note

一般のwhile文は停止しない可能性があるため、厳密な表示的意味論では部分関数や不動点を使って扱うらしい (知らない)。

# 操作的意味論

操作的意味論では、条件式と代入文の評価を、while文全体の評価へ組み合わせる規則を与える。

まず、条件式が偽なら、while文は本体を実行せず、元の状態をそのまま結果とする。

⟨x>0,σ⟩⇓false⟨while x>0 do x:=x−1,σ⟩⇓σ \frac{ \langle x>0,\sigma\rangle\Downarrow\mathrm{false} }{ \langle \mathbf{while}\ x>0\ \mathbf{do}\ x:=x-1,\sigma\rangle \Downarrow\sigma }
Note

この分数っぽい記法は、分子に当たる部分が前提で、分母に当たる部分が結論を表す。

つまり、これは、「もし x>0x > 0 が偽なら、while文を状態 σσで実行した結果は σσ である」と読める。

条件式が真なら、本体を実行し、その結果の状態からwhile文をもう一度実行する。

⟨x>0,σ⟩⇓true⟨x:=x−1,σ⟩⇓σ′⟨while x>0 do x:=x−1,σ′⟩⇓σ′′⟨while x>0 do x:=x−1,σ⟩⇓σ′′ \frac{ \langle x>0,\sigma\rangle\Downarrow\mathrm{true} \qquad \langle x:=x-1,\sigma\rangle\Downarrow\sigma' \qquad \langle \mathbf{while}\ x>0\ \mathbf{do}\ x:=x-1,\sigma'\rangle \Downarrow\sigma'' }{ \langle \mathbf{while}\ x>0\ \mathbf{do}\ x:=x-1,\sigma\rangle \Downarrow\sigma'' }
Hint

σ′\sigma^{\prime} と σ′′\sigma^{\prime\prime} は、中間結果に名前をつけたもの、と読む。
分子側の ⟨while x>0 do x:=x−1,σ′⟩⇓σ′′\langle \mathbf{while}\ x>0\ \mathbf{do}\ x:=x-1,\sigma'\rangle\Downarrow\sigma'' によって再帰的な定義となっている。

同様に、任意の状態 σ\sigma について、x > 0 が真である間は2つ目の規則を使い、偽になったところで1つ目の規則を使う。その評価結果は次のようにまとめられる。

⟨while x>0 do x:=x−1,σ⟩⇓σ[x↦min⁡(σ(x),0)] \langle \mathbf{while}\ x>0\ \mathbf{do}\ x:=x-1, \sigma \rangle \Downarrow \sigma[x\mapsto\min(\sigma(x),0)]

このように、操作的意味論では、各構文要素 (x > 0, x := x - 1) の評価についての規則を (再帰的にも) 組み合わせて、while文全体がどのように評価されるかを導く。

# 公理的意味論

公理的意味論では、while文についての性質を導くために、ループの各反復の前後で常に成り立つ命題を用いる。一般に、このような命題をループ不変条件という。

今回は、実行前の x の値を表す論理上の変数を nn と置き、x >= 0 から始まる場合と x < 0 から始まる場合に分けて考える。

まず、x >= 0 から始まる場合を考える。このとき、ループ不変条件として同じく x >= 0 を使える。

実際、x >= 0 かつ x > 0 の状態で x := x - 1 を実行しても、x >= 0 は保たれる。

{x≥0∧x>0}  x:=x−1  {x≥0} \{x\geq0\land x>0\}\; x:=x-1\; \{x\geq0\}

したがって、ループが終了した後には、ループ不変条件 x >= 0 と終了条件 x <= 0 の両方が成り立つ。よって、次のことが分かる。

{x=n∧n≥0}  while x>0 do x:=x−1  {x=0} \{x=n\land n\geq0\}\; \mathbf{while}\ x>0\ \mathbf{do}\ x:=x-1\; \{x=0\}

次に、x < 0 から始まる場合を考える。この場合は最初から条件式 x > 0 が偽なので、ループ本体は一度も実行されず、x の値は変化しない。

{x=n∧n<0}  while x>0 do x:=x−1  {x=n} \{x=n\land n<0\}\; \mathbf{while}\ x>0\ \mathbf{do}\ x:=x-1\; \{x=n\}

n >= 0 と n < 0 ですべての整数を網羅しているため、この2つは次の1つのホーアトリプルにまとめられる。

{x=n}  while x>0 do x:=x−1  {x=min⁡(n,0)} \{x=n\}\; \mathbf{while}\ x>0\ \mathbf{do}\ x:=x-1\; \{x=\min(n,0)\}

つまり、実行前の x が正なら実行後は0になり、0以下なら元の値のままとなる。

このように、公理的意味論では、代入文について成り立つ命題とwhile文の推論規則を組み合わせて、while文全体について成り立つ命題を導く。さらに、実行前の状態 (ホーアトリプルの左側) を場合分けして命題を与えることで、任意の初期値に対する実行後の状態を特徴づけられた。

# おわり

今回扱ったwhile文を CC と置く。

C≡while x>0 do x:=x−1 C\equiv \mathbf{while}\ x>0\ \mathbf{do}\ x:=x-1

3つの意味論から得られたものを並べると、次のようになる。

意味論 得られたもの
表示的意味論 [[C]](σ)=σ[x↦min⁡(σ(x),0)]C(\sigma)=\sigma[x\mapsto\min(\sigma(x),0)]
操作的意味論 ⟨C,σ⟩⇓σ[x↦min⁡(σ(x),0)]\langle C,\sigma\rangle\Downarrow\sigma[x\mapsto\min(\sigma(x),0)]
公理的意味論 {x=n}  C  {x=min⁡(n,0)}\{x=n\}\;C\;\{x=\min(n,0)\}

冒頭では、「構文要素に意味を与え、それらを組み合わせることで、プログラム全体の意味を構成する」と考えた。

実際、3つの意味論はどれも、プログラムの構造に沿って部分から全体を扱っていた。

ただし、そこで与え、組み合わせていた「意味」は方法により異なるものだった。

  • 表示的意味論では、構文要素に対応する数学的対象を組み合わせていた
  • 操作的意味論では、構文要素についての評価を組み合わせていた
  • 公理的意味論では、構文要素について成り立つ性質とその証明を組み合わせていた

プログラム意味論とは、すでに決まった意味を3つの方法で表現する分野ではなく、プログラムの何を意味として捉え、どのように厳密化するかを考える分野なのだと理解した。

次は、具体的なユースケースや、各方法の得手不得手を見ると良さそう。

前の記事

『プログラマーのための圏論』第3章 圏のさまざま

関連記事