『コンピュータサイエンスにおける様相論理』第１版第１刷の補遺（日付は項目ごとの更新日）

定理 3.4.4（CTL の有限モデル性）についての注意
本書で示した状態数は O(2Lh(φ)

O(22Lh(φ)(2022 年 2 月)

) であるが，下記の追加参考文献 [A1] 第 16 章の定理 6.14 では) が示されている．

参考文献の追加 (2022 年 2 月)

[A1] 広瀬健，野崎昭弘，小林孝次郎（監訳）．形式的モデルと意味論（コンピュータ基礎理論ハンドブック II）．丸善，1994. （J. van Leeuwen (ed.), Formal Models and Semantics (Handbookof Theoretical Computer Science, Volume B), Elsevier 1990 の翻訳）.
[A2] 徳山豪，小林直樹（編集），理論計算機科学事典．朝倉書店，2022．
文献 [A1] では CTL とその周辺の論理が第 16 章で，PDL が第 14 章で，ホーア論理が第 15 章で，それぞれ詳しく説明されている．
文献 [A2] の第 8 章ではさまざまな種類のモデル検査が説明されている．ホーア論理も説明されている．

3.6 節における EU の長さについて (2023 年 8 月)
3.6 節では EX は ¬AX¬ の省略形なので，Sub+ (pEUq) = {¬AX¬(pEUq), AX¬(pEUq), ¬(pEUq),
pEUq, p, q} である（{EX(pEUq), pEUq, p, q} ではない）．そのため，|Sub+ (ξ)| ≤ Lh(ξ) を保証する
ためには EU の長さは 2 ではなく 4 にする必要がある（つまり Lh(EX(αEUβ)) = Lh(α) + Lh(β) + 4）．
ただし 3.6 節の最後の段落（p.78 の一番下）で説明しているように，¬ はここで作るモデルの状態数に影響しないので，有限モデル性の文面では EU の長さは 2 としてよい．
補題 3.6.6(2) について (2023 年 8 月)
補題 3.6.6(2) には無駄がある．補題の文面から「かつ αEUβ ∈ Γ 」と「かつ αEUβ ∈ Γ ′ 」を削除して次の主張に変えればすっきりする．
1Q = E ならば，ある Γ ′ ⇒∆′ が存在して ⟨H, αEUβ, (Γ ⇒∆)⟩ ⇝ ⟨H∪{Γ ⇒∆}, αEUβ, (Γ ′ ⇒∆′ )⟩ ∈S + となる．
この補題は p.78 の 6 行目で使用されるが，上記に変えても問題なく使用できる．この補題の証明にはp.77 の式 (3.11) を用いるが，それは αEUβ を削除して次にすればよい．
(α′ ∧⟨|Γ ⇒∆|⟩)EUβ, γ1 , γ2 , . . . , γn ⇒(3.11)

演習問題 3.6.7 の解答（p.155）は，(i) を削除して (ii) から始めればよい．
ホーア論理の相対完全性の証明(2023 年 11 月)

定理 6.3.9 の後半，すなわちホーア論理の相対完全性を，本文と少し異なる方針で少し詳細に証明する．
任意のプログラム π と任意の表明 B に対して次の (I)(II) が成り立つことを，π に関する帰納法で示す．

1(I) ある表明 A0 が存在して次の (1)(2) が成り立つ（この A0 を「π と B に対する最弱前条件」と呼ぶ）．

(1) Hoare ⊢ {A0 }π{B}.
(2) 任意の変数解釈 J, I に対して次が成り立つ．
π J ′ かつ J ′ , I ̸|= B ．
J, I ̸|= A0 ならば，ある J ′ に対して J 7→
(II) 任意の表明 A に対して次が成り立つ．
|= {A}π{B} ならば Hoare ⊢ {A}π{B}．
この (II) が求める完全性である．ところで（I ⇒ II）が以下のように証明できる．

(I) と |= {A}π{B} を仮定する．まず |= A → A0 であることを示す．もし ̸|= A → A0 ならば，ある J, I に対して J, I |= A かつ J, I ̸|= A0 となっている．しかしこれは，(I) の (2) および仮定|= {A}π{B} と矛盾する．したがって |= A → A0 である．すると (I) の (1) と帰結規則によってHoare ⊢ {A}π{B} となる．
このことから実際には (I) だけを示せばよいことになる．以下では π に関する帰納法で，任意の B に対して (I) が成り立つことを示す．
【π が vi := t という代入文のとき】 B(t/vi) が求める A0 になっている．
【π が複合文のとき】 簡単のために π = begin π1 ; π2 end とする（3 個以上でも同様にできる）．このとき帰納法の仮定により π2 と B に対する最弱前条件 X が存在し，さらに π1 と X に対する最弱前条
件 Y が存在する．すると Y が begin π1 ; π2 end と B に対する最弱前条件になっていることは簡単に確認できる．
【π が if C then π1 else π2 のとき】帰納法の仮定により π1 と B に対する最弱前条件 A1 ，およびと π2と B に対する最弱前条件 A2 が存在する．すなわち次の４つが成り立つ．(1-1) Hoare ⊢ {A1 }π1 {B}.
′′(1-2) (∀ J, I)(J, I ̸|= A1 ⇒ (∃ J ′ )(J π7→1 J かつ J , I ̸|= B))．(2-1) Hoare ⊢ {A2 }π2 {B}. (2-2)′′(∀ J, I)(J, I ̸|= A2 ⇒ (∃ J ′ )(J π7→2 J かつ J , I ̸|= B))．このとき A0 = (C → A1 ) ∧ (¬C → A2 ) とす
れば，これが if C then π1 else π2 と B に対する最弱前条件になっている．A0 が最弱前条件の条件 (1) を満たすことは，(1-1), (2-1) と |= (C ∧ A0 ) → A1 および |= (¬C ∧ A0 ) → A2 という事実と，帰結規則と if 文規則で言える．A0 が最弱前条件の条件 (2) を満たすことは，J, I ̸|= A0 ならば

J, I |= C ∧ ¬A1 または J, I |= ¬C ∧ ¬A2 であることと，(1-2), (2-2) および if 文の動作の定義から言える．
【π が while C do π ′ のとき】 簡単のためこのプログラム中には変数がただひとつ（v と書く）しか使われていないとする（変数が複数あっても同様にできる）．このとき次が求める A0 である．

(∀k ≥ 0)∀x0 ∀x1 · · · ∀xk[()]v = (x0 ∧)→ C(xk /v) ∨ B(xk /v)
π ′ (v = xi+1 )”(∀i) (0 ≤ i < k) → C(xi /v) ∧ “(v = xi ) 7→
ただしここでは以下の事実を使用している．

• 可変個数の表明変数を用いた記法 ∀x0 ∀x1 · · · ∀xk は表明言語（算術の一階述語言語）を逸脱しているが，任意の長さの整数列をひとつの自然数で表現する技法（ゲーデル数化とも言う）を用いれば，固定した表明変数で同じ意味を表現できる．

π ′ (v = xi+1 )” は「変数 v の値が xi のときにプログラム π ′ を実行開始すると，v の値• “(v = xi ) 7→が xi+1 になって停止する」を表す表明であり，算術の一階述語言語で記述することができる．
これらの詳細は参考文献 [29,2,3] やゲーデルの不完全性定理を解説している教科書を見てほしい．A02

の直観的な意味は次の通りである：「変数 v の現在の値を x0 としてその後 x1 , . . . , xk とどのように変化しても，それがプログラム while C do π ′ の実行（の途中までまたは最後まで）に従った変化であるならば，v = xk のときに条件 C または B が成り立つ」．以下では A0 が while C do π ′ と B に対する最弱前条件の条件 (1) と (2) を満たすことを示す．(1)：まず A0 の内容をよく考えれば |= {C ∧ A0 }π ′ {A0 }であることが言える．したがって帰納法の仮定 (II) により Hoare ⊢ {C ∧ A0 }π ′ {A0 } となり，while
文規則で Hoare ⊢ {A0 } while C do π ′ {¬C ∧ A0 } を得る．一方 |= ¬C ∧ A0 → B も言える（A0 でk = 0, x0 = v とすればよい）．したがって帰結規則により Hoare ⊢ {A0 } while C do π ′ {B} が得られる．(2)：J, I ̸|= A0 であるとする．これはすなわち「プログラム while C do π ′ の実行に従った変数 v の値の遷移 x0 , x1 , . . . , xk が存在して，v = xk のときに C も B も成り立たない」ということであπ J ′ かつ J ′ , I ̸|= B となる J ′ が存在する．
る．すなわち J 7→3