逐次一貫性下の知識伝達を表す直観主義様相論理平井 洋一 1
1 東京大学大学院 情報理工学系研究科コンピュータ科学専攻

yh@is.s.u-tokyo.ac.jp
概要
Herlihy と Shavit は，wait-free 計算を単体的複体で幾何的に特徴づけた．この論文では，wait-free 計算を論理的に特徴づける．まず，非同期通信のための直観主義知識論理を与える．この論理の意味論は，Herlihy と Shavit が用いた単体的複体の分割の一般化である．次に，この直観主義知識論理の上に，Lamport が定義した共有メモリの逐次一貫性を特徴づける公理型を与える．最後に，逐次一貫性のもとで，wait-free 仕様と呼ぶある種の論理式と wait-free 計算のスケジュールが成すモデルとの間での健全性と完全性とを示す．おもしろいことに，逐次一貫性を特徴づける公理型は，Kripke フレー
ムの擬線形性を特徴づける公理型 (ϕ ⊃ ψ) ∨ (ψ ⊃ ϕ) と類似している．この類似は，共有メモリの逐次一貫性も Kripke フレームの擬線形性も，スケジュールやモデルに，ある種の全順序性を求めることが似ていることによる．(LPAR-16 に類似の論文を投稿した．)

導入

1

Wait-free 計算を，できる限り単純な論理で特徴付けたい．Herlihy と Shavit による wait-free 計
算の特徴づけは，共有メモリの逐次一貫性を暗黙のうちに前提にしているので，まずは逐次一貫性を特徴づける知識論理をつくりたい．なるべく単純な枠組みで特徴づけできるとよいので，既存研究をみてみる．
知識伝達を扱うための論理で，知識様相をもつものは，多数ある．[3–6, 10, 13, 17, 20, 21, 27]．直観主義様相論理も多数ある [1, 7, 19, 20, 22]．どちらの場合も，Kripke 意味論で考えると，論理が多数あるのは，状態間の二項関係二種類について，相互の制限を多種類考えられるからである．直観主義様相論理で二種類の二項関係とは，(a) 直観主義の意味論をつけるための順序と (b) どの状態
で様相がどの状態を指すのかを表す二項関係のことである．知識伝達のための論理たちでは，二種類の二項関係とは，(a’) どの状態がどの状態より時間的に先行するかを表す順序と (b’) どの状態か
らどの状態に (どんな種類の) 知識伝達が起きたのかを表す二項関係のことである．
この状況を単純にするために，この論文では，状態空間上の二項関係に加えて，もうひとつの二項関係の代わりに状態空間上の関数を用いて意味論を記述できるような論理を考える．こうすることによって，論理を設計するさいの選択の余地が少なくなるために，状況が単純になる．選択の余地が少なくなるといえるのは，状態集合上のほとんどの二項関係は状態集合上の関数としては書き表せないけれども，逆に状態集合上の関数を二項関係とみなすことは，いつでもできるからである．
さらに，順序 (a) と (a’) を同一視し，二項関係 (b) と (b’) とを同一視する．
逐次一貫性がスケジュールに対する制限であるのに対して，wait-free という概念は並列プログラ
ムに対する制限である．並列プログラムの振舞いは，スケジュールによって左右される1 ．並列プロ
グラムの正しさは，任意のスケジュールについて，正しい振舞いをするという形で定義できる．この定義の形は，論理式の恒真性の，任意のモデルによって充足されるという定義の形に類似しているので，スケジュールと並列プログラムとの対決は，論理式とモデルの対決に類似していると考える．第 3 節では，スケジュールの制限である逐次一貫性をモデルのクラスとして表現し，そのうえで第 3.5 小節で並列プログラムの制限である wait-free 性を，論理式のクラスとして表現する．
1

このことにより並列プログラムのテストが極めて難しいことが，本研究のような形式的手法を導入する動機である．

(axiom)ϕ`ϕ(exchange)(∨-I1 )

(weakening)

Γ, ϕ, ψ, Γ0 ` ϕ0
Γ, ψ, ϕ, Γ0 ` ϕ0

(∧-I)

Γ`ϕ
Γ`ψ∨ϕ

(∧-E0 )

(∨-E)

(⊃-I)

ϕ, Γ ` ψΓ`ϕ⊃ψΓ ` ψ0 ∨ ψ1(⊃-E)

Ka ϕ ` Ka Ka ϕ(contraction)(nec)

ϕ, ϕ, Γ ` ϕ0ϕ, Γ ` ϕ0Γ`ϕ
Γ0 ` ψ
0Γ, Γ ` ϕ ∧ ψ(∨-I0 )

Γ`ϕ
Γ`ϕ∨ψ

Γ`ϕ∧ψ
Γ`ϕ

(∧-E1 )Γ`ϕ∧ψΓ`ψΓ, ψ0 ` ϕΓ`ϕΓ, ψ1 ` ϕ

Γ ` ψ0 ⊃ ψ1
Γ ` ψ0Γ ` ψ1(T)(introspection)Γ`ϕψ, Γ ` ϕ(⊥-E) Γ ` ⊥Γ`ϕ

Ka ϕ ` ϕΓ`ϕKa Γ ` Ka ϕ(∨K)

Ka (ϕ ∨ ψ) ` Ka ϕ ∨ Ka ψ

図 1. K∨ の推論規則たち

2

非同期通信のための直観主義知識論理

2.1

統語論

命題変項の集合 P V ar と，主体の集合 A とを固定する．メタ変項 P, Q, . . . は，命題変項を走ることとする．
定義 1 論理式 ϕ を BNF で定義する:

ϕ ::= ⊥ | P | (Ka ϕ) | (ϕ ∨ ϕ) | (ϕ ∧ ϕ) | (ϕ ⊃ ϕ)
(ここで a ∈ A とする)．論理式の集合を Fml と書く．
単項演算子は二項演算子よりも強く結び付く．曖昧にならないときには，括弧を省略することがある．論理式同士を = で結んだら，統語論的な等しさを表すこととする．記法 (¬ϕ) は (ϕ ⊃ ⊥) の略記とする．論理式の列 Γ = (ϕi ) について，記法 Ka Γ は列 (Ka ϕi ) の略記とする．命題変項と ⊥とをあわせて，原子論理式と呼ぶ．
定義 2 論理 K∨ の演繹体系を図 1 により定義する．
論理式の集合 Γ と論理式 ϕ について，関係 Γ ` ϕ が成り立つのは，Γ の元の有限列 Γ0 があって，
Γ0 ` ϕ が導出可能であるときである．
モデルと，モデルの中の状態を決めると，論理式が充足されるか否かが定まる．モデルとは，Kripke
フレームに写像 fa たちが，それぞれの主体 a ∈ A について，追加されたものである．
写像が fa 状態 w を状態 v に写すのはどういうときかというと，気分として2 ，実際の状態が w であるときに，主体 a は状態が v に逹したことにしか気付いていないようなときである．
定義 3 モデル hW, ¹, (fa )a∈A , ρi とは，こういうものの組である:
2

この説明が気分に過ぎないと述べるのは，我々は「実際の状態」を定義しようとしないからである．

1. hW, ¹i は順序である．
2. 各 fa : W → W は，任意の w ∈ W について，(a) (減少性) fa (w) ¹ w,(b) (巾等性) fa (fa (w)) = fa (w),(c) (単調性) w ¹ v ならば fa (w) ¹ fa (v)を満たす関数である．

3. ρ : P V ar → P(W ) は関数で，各 ρ(P ) が ¹ に関して上のほうに閉じている, つまり， w0 º
w ∈ ρ(P ) ならば w0 ∈ ρ(P ) である．
先の気分の説明をふまえると，fa たちに課された条件の気分を，このように説明できる:• 減少性は，主体 a は真実しか認識しないことを表している．
• 巾等性は，主体 a がなにかを認識するならば，a はまた，a 自身がそのことを認識していることを認識するはずであるというとを表している．
• 単調性は，a はいちど認識したことを忘れないということを表している．
定義 4 充足関係 |= を定義する．充足関係は，モデル hW, ¹, (fa )a∈A , ρi と，状態 w ∈ W と，論理式 ϕ との関係である．モデルを固定しよう: M = hW, ¹, (fa )a∈A , ρi． 関係 |= の定義は，ϕ の構造に関して帰納的になされる:(ϕ = ⊥ の場合) M, w |= ⊥ はどうあれ成立しない．
(ϕ = P の場合) M, w |= P が成立するのは，ただ w ∈ ρ(P ) なときである．
(ϕ = Ka ψ の場合) M, w |= Ka ψ が成立するのは，ただ M, fa (w) |= ψ なときである．
(ϕ = ψ0 ∧ ψ1 の場合) M, w |= ψ0 ∧ ψ1 が成立するのは，ただ M, w |= ψ0 と M, w |= ψ1 とが両方成立するときである．
(ϕ = ψ0 ∨ ψ1 の場合) M, w |= ψ0 ∨ ψ1 が成立するのは, M, w |= ψ0 か M, w |= ψ1 の少なくとも片方が成立するときに限る．
(ϕ = ψ0 ⊃ ψ1 の場合) M, w |= ψ0 ⊃ ψ1 が成立するのは，いかなる w0 ∈ W についても，w0 º wと M, w0 |= ψ0 が M, w0 |= ψ1 を含意するときに限る．
定理 5 (Kripke 単調性) M, w |= ϕ かつ w ¹ v とすると，M, v |= ϕ が成立する．
証明 主張に現れる ϕ の構成に関する帰納法で示せる．fa の単調性を用いる．

2.2

判断の意味論定義 6 モデル M とそのモデルの状態 w と論理式の集合 Γ とについて，M, w |= Γ と書くのは，Γ
に属する任意の論理式 ϕ について M, w |= ϕ が成立するときである．
定義 7 記法 Γ |= ϕ は，論理式の列 Γ と論理式 ϕ の右の関係を表す: 任意のモデル M と任意の状
態 w ∈ M について，M, w |= Γ ならば M, w |= ϕ である．

2.3

健全性

定理 8 (健全性) Γ ` ϕ は Γ |= ϕ を含意する．
証明 健全性を，` の定義に関する帰納法で示す．

(introspection) fa が巾等であることを用いる．
(nec) |= の定義が，あらゆるモデルのあらゆる状態についての言明であることから，導ける．
(∨Ka ) Γ |= Ka (ϕ∨ψ) を仮定する．任意のモデル M の 任意の状態 w について，M, w |= Γ を仮定す
ると M, w |= Ka (ϕ ∨ ψ) である．|= の定義から，M, fa (w) |= ϕ ∨ ψ である．|= の定義をもう一度使うと，M, fa (w) |= ϕ か M, fa (w) |= ψ の少くとも片方が成り立つ．つまり，M, w |= Ka ϕ
か M, w |= Ka ψ の少なくとも片方が成り立つ．|= の定義より，M, w |= Ka ϕ ∨ Ka ψ を示せた．
(他) 標準的な証明 [26, Th. 5.10] を使える．

2.4

強い完全性

定義 9 論理式の集合 Γ が飽和しているのは，下記のすべてを満たすときである:

1. Γ が演繹について閉じている．つまり，Γ ` ϕ ⇒ ϕ ∈ Γ である．
2. ϕ ∨ ψ ∈ Γ とすると，ϕ ∈ Γ または ψ ∈ Γ が成立する．
3. Γ 6` ⊥ である．
補題 10 (飽和補題) 論理式の集合 Γ で Γ 6` ϕ を満たすものに対して，論理式の飽和集合 Γω で，
Γω 6` ϕ と Γ ⊆ Γω を満たすものがある3 ．
証明 標準的な証明 [26, Lem. 6.3] をそのまま使える．
定義 11 (正準モデルの候補) 組 M c = hW c , ¹c , (fac )a∈A , ρc i を定義する．
• W c を，論理式の飽和集合たちの集合とする．

• Γ ¹c ∆ を Γ ⊆ ∆ で定義する．
• f c (Γ) = {ϕ ∈ Fml | K ϕ ∈ Γ} と定義する．
aa• ρc (P ) = {Γ ∈ W c | P ∈ Γ} とする．
補題 12 (正準モデル) 組 M c = hW c , ¹c , (fac )a∈A , ρc i はモデルである．
証明 まず，fac が実際に関数 W c → W c であることを確かめよう．仮定: Γ ∈ W c ．主張: fac (Γ) は論理式の飽和集合である．主張を示すために，飽和集合の定義の条件をいちいち確かめる．
1. fac (Γ) ` ϕ を仮定する．規則 (introspection) があるので， Ka (fac (Γ)) ` Ka ϕ である．このことに加えて，Ka (fac (Γ)) ⊆ Γ であるから，関係 Γ ` Ka ϕ が成立する．Γ は演繹に関して閉じているので，K ϕ ∈ Γ である．f c の定義から，ϕ ∈ f c (Γ) である．
aaa2. ϕ ∨ ψ ∈ f c (Γ) を仮定する．f c の定義から，K (ϕ ∨ ψ) ∈ Γ である．規則 (∨K ) により，
a

a

a

a

Ka (ϕ ∨ ψ) ` Ka ϕ ∨ Ka ψ が成立する．Γ は演繹に関して閉じているから，Ka ϕ ∨ Ka ψ ∈ Γ である．Γ は飽和しているので，Ka ϕ ∈ Γ または Ka ψ ∈ Γ の少なくとも片方は成立する．facの定義から，ϕ ∈ fac (Γ) か ψ ∈ fac (Γ) の少なくとも片方は成立する．

3

Saturation Lemma.

3. 矛盾を求めて，fac (Γ) ` ⊥ を仮定する．fac (Γ) は演繹に関して閉じているので，⊥ ∈ fac (Γ) である．fac の定義から， Ka ⊥ ∈ Γ である．規則 (T) によって，Γ ` ⊥ である．Γ が飽和集合という仮定に反する．
次に，定義 3 の条件をいちいち確かめよう．
1. ¹c は順序である．なぜならば集合の包含関係 ⊆ が順序だからである．

2. (a) 規則 (T) によって fac (Γ) ¹ Γ である．
(b) f c (f c (Γ)) ⊆ f c (Γ) は，前項から明らかである．逆を示そう．ϕ ∈ f c (Γ) を仮定する．f c
a

a

a

a

a

の定義から， Ka ϕ ∈ Γ である．規則 (introspection) から，Γ ` Ka Ka ϕ である．Γ は演
繹に関して閉じているから，Ka Ka ϕ ∈ Γ である．従って ϕ ∈ fac (fac (Γ)) である．
(c) Γ ¹ ∆ を仮定する．どの K ϕ ∈ ∆ も，Γ にも入っている．従って， f c (Γ) ¹ f c (∆) で
a

a

a

ある．
3. Γ0 º Γ ∈ ρc (P ) を仮定する．P ∈ Γ である．よって P ∈ Γ0 である．従って Γ0 ∈ ρc (P ) である．
補題 13 論理式の飽和集合 Γ と正準モデル M c について，ϕ ∈ Γ ⇔ M c , Γ ` ϕ が成り立つ．
証明 ϕ の構成に関する帰納法で示す．

(ϕ = ⊥ の場合) 左右どちらも，決して成立しない．
(ϕ = P の場合) ρc の定義より，ϕ ∈ Γ ⇔ Γ ∈ ρ(P ) ⇔ M c , Γ |= P である．
(ϕ = ψ0 ∧ ψ1 , ψ0 ∨ ψ1 の場合) 帰納法の仮定から直接示せる．
(ϕ = Ka ψ の場合) (⇒) M c , Γ |= Ka ψ を仮定する．|= の定義から，M c , fac (Γ) |= ψ である．帰納法の仮定から，ψ ∈ fac (Γ) である．fac の定義から， Ka ψ ∈ Γ である．
(⇐) K ψ ∈ Γ を仮定する．f c の定義から，ψ ∈ f c (Γ) である．帰納法の仮定から，f c (Γ) |= ψ
a

a

a

a

である．|= の定義より，Γ |= Ka ψ である．
(ϕ = ψ0 ⊃ ψ1 の場合) (⇒) M c , Γ |= ψ0 ⊃ ψ1 を仮定する．矛盾を求めて，ψ0 ⊃ ψ1 ∈/ Γ と仮定する．Γ は演繹に関して閉じているので，Γ, ψ0 6` ψ1 である．補題 10 より，飽和集合 Γ0 が存在して，Γ0 ⊇ Γ ∪ {ψ0 } かつ Γ0 6` ψ1 を満たす．帰納法の仮定から，M c , Γ0 |= ψ0 であるが，
M c , Γ0 |= ψ1 ではない．Γ0 º Γ であるから，これは M c , Γ |= ψ0 ⊃ ψ1 に矛盾する．
(⇐) ψ0 ⊃ ψ1 ∈ ∆ を仮定する．∆0 º ∆ かつ M c , ∆0 |= ψ0 である．M c , ∆0 |= ψ1 を示せばよい．帰納法の仮定から，ψ0 ∈ ∆0 である．∆0 は演繹に関して閉じていて，かつ ψ0 ⊃ ψ1 ∈ ∆0なので，ψ1 ∈ ∆0 である．帰納法の仮定より， M c , ∆0 |= ψ1 である．
これで補題を示せた．
定理 14 (強い完全性) Γ |= ϕ は Γ ` ϕ を含意する．
証明 対偶を示す: Γ 6` ϕ を仮定して，Γ 6|= ϕ を示す．補題 10 より，論理式の飽和集合 Γ0 が存在して Γ0 6` ϕ と Γ0 ⊇ Γ を満たす．補題 13 より，M c , Γ0 |= Γ だが，M c , Γ0 6|= ϕ である．これは Γ |= ϕ
に反する．

3

逐次一貫性のための公理型

この節では，ある公理型で，逐次一貫性を特徴づける．逐次一貫性 [16] は，メモリの状態が時間的に全順序に並ぶことを要求する条件である．我々は K∨ に推論規則を追加することによって演繹
体系 `SC を定義して，逐次一貫性を表す．

3.1

逐次一貫モデル

逐次一貫性は，メモリの状態が時間的に全順序に並ぶことを要求する．直観主義知識論理のモデルでメモリの状態を特徴づけるには，状態 w ∈ W のうち fm (w) = w を満たすものを，w から見たメモリの状態が w 自身であることを根拠にして，メモリの状態とみなせばよい．このように定義したメモリの状態たちに制限した ¹ が全順序であることを，逐次一貫モデルと呼ぶ．
定義 15 逐次一貫モデルとは，任意の状態 v と w とについて，fm (v) = v と fm (w) = w とが成り立つならば，v ¹ w または w ¹ v が成立するモデルである．
加えて技術的な理由から，擬逐次一貫モデルを定義する．擬逐次一貫モデルは，大雑把には，逐次一貫モデルをいくつか互いに無関係に並べて得られるようなモデルのことである．
定義 16 擬逐次一貫モデルとは，任意の状態 v と w と x とについて，fm (v) = v と fm (w) = w とが成り立ちかつ x が x ¹ v と x ¹ w とを満たすならば，v ¹ w または w ¹ v が成立するモデルで
ある．

3.2

公理型の定義SC を，右のような形をした論理式の集合とする: (Km ϕ ⊃ Km ψ) ∨ (Km ψ ⊃ Km ϕ).
K∨ の演繹体系に規則 (SC) を追加して，Γ `SC ϕ を定義する． (SC) ` ϕ (ϕ ∈ SC)
集合 SC に属する任意の論理式は古典論理のトートロジーであるために，これらの論理式を古典論理に追加しても無意味であることに注意されたい．このことが，古典論理でなく直観主義論理を用いた利点である．

3.3

健全性

補題 17 `SC ϕ ⇒ M |= ϕ が任意の逐次一貫モデル M について成り立つ．
証明 補題 8 を示すときに使った数学的帰納法に，規則 (SC) に関する条を追加すれば，証明できる．

(SC) 矛盾を求めて，M, w 6|= (Km ϕ ⊃ Km ψ) ∨ (Km ψ ⊃ Km ϕ) と仮定する．関係 |= の定義によると，状態 w0 , w1 º w があって，M, w0 |= Km ϕ と M, w1 |= Km ψ とを満たし，さらにM, w1 6|= Km ψ と M, w0 6|= Km ϕ とを満たす．これらと Kripke 単調性 (補題 5) は，M が逐次一貫モデルという仮定に矛盾する．

3.4

強い完全性

まず，擬逐次一貫モデルに対する強い完全性を言ってから，逐次一貫モデルに対する強い完全性を言う．
定義 18 論理式の集合 Γ が SC-飽和であるとは，これらの条件をみたすことである:

1. Γ は演繹に関して閉じている，すなわち，Γ `sc ϕ ⇒ ϕ ∈ Γ を満たす．
2. ϕ ∨ ψ ∈ Γ ならば ϕ ∈ Γ または ψ ∈ Γ である．
3. Γ 6`sc ⊥ である．
補題 19 (飽和補題) 論理式の集合 Γ で Γ 6`sc ϕ を満たすものについて，論理式の SC-飽和な集合
Γω で， Γω 6`sc ϕ と Γ ⊂ Γω とを満たすものがある．
証明 補題 10 の証明と同じで，ただ，` を `sc で置き換えればよい．
定義 20 (擬逐次一貫な正準モデルの候補) 組 M sc = hW sc , ¹sc , (fasc )a∈A , ρsc i を定義する．

• W sc は論理式の SC-飽和集合たちの集合とする．
• Γ ¹sc ∆ を Γ ⊂ ∆ で定義する．
• fasc (Γ) = {ϕ | Ka ϕ ∈ Γ} とする．
• ρsc (P ) = {Γ | P ∈ Γ} とする．
補題 21 (擬逐次一貫な正準モデル) 組 M sc = hW sc , ¹sc , (fasc )a∈A , ρsc i は擬逐次一貫モデルである．
証明 最初に，前と同じようにして，fasc が実際に関数 W sc → W sc であることを確かめることができる．さらに，定義 3 のいちいちの条件を確かめるのも，前と同様にできて，M sc がモデルであることがわかる．最後に，モデル M sc が擬逐次一貫モデルであることを示す．Γ, ∆, Θ をモデル
sc (Γ) = Γ と仮定 f sc (∆) = ∆ をおく．
M sc の状態とし，仮定 Θ ¹sc ∆ と仮定 Θ ¹sc ∆ と仮定 fmmsc
sc∆ ¹ Γ か Γ ¹ ∆ の少なくとも片方が成立すると主張する．矛盾を求めて，主張の否定を仮定する．関係 ¹sc が実際には集合の包含関係なので，論理式 ϕ と ψ が存在して，ϕ ∈ Γ と ϕ ∈/ ∆とscψ ∈ ∆とψ ∈/ Γ とを満たす．fm (Γ) = Γ であるので，Ka ψ ∈/ Γ と Ka ϕ ∈ Γ が成立する．同様に，
Ka ϕ ∈/ ∆ と Ka ψ ∈ ∆ が成立する．集合 Θ は SC 飽和なので， (Ka ϕ ⊃ Ka ψ) ∨ (Ka ϕ ⊃ Ka ψ) は
Θ の元である．飽和の定義によると，Ka ϕ ⊃ Ka ψ ∈ Θ か Ka ψ ⊃ Ka ϕ ∈ Θ の少なくとも片方が成立する．結果として，Ka ϕ ⊃ Ka ψ ∈ Γ か Ka ψ ⊃ Ka ϕ ∈ ∆ の少なくとも片方が成立する．それぞれの場合が，Γ も ∆ も演繹に関して閉じていることから，矛盾に至る．
補題 22 論理式の飽和集合 Γ と擬逐次一貫正準モデル M sc について，ϕ ∈ Γ ⇐⇒ M sc , Γ `sc ϕが成立する．
証明 補題 13 と同じである．
補題 23 (擬逐次一貫モデルへの強い完全性) 任意の擬逐次一貫モデル M について M |= Γ ならば
M |= ϕ とすると，Γ `sc ϕ である．
証明 対偶を示す．Γ 6`sc ϕ を仮定して，擬逐次一貫モデル M が存在して M |= Γ を満たすが M |= ϕは満たさないということを示す．補題 19 によって，SC 飽和な論理式の集合 Γ0 で Γ0 6` ϕ と Γ0 ⊃ Γとを満たすものがある．補題 22 によって，M sc , Γ0 |= Γ であるけれども M sc , Γ0 |= ϕ ではない．

定理 24 (逐次一貫モデルへの強い完全性) 任意の逐次一貫モデル M について M |= Γ ならば M |=ϕ とすると，Γ `sc ϕ である．
証明 対偶を示す．Γ 6`sc ϕ を仮定すると，補題 23 によって擬逐次一貫モデル M と M の状態 w が存在して，M, w |= Γ を満たすが M, w |= ϕ を満たさない．ここで M の状態のうち，¹ に関して w
以下のある状態 v について，¹ に関して v 以上である状態だけを集めて制限すると，逐次一貫モデ
ル M̄ が得られ，M̄ , w |= Γ は成立するが，M̄ , w |= ϕ は成立しない．

3.5

Wait-free 計算

スケジュールは，ステップをプロセスに割りふる．Wait-free な並列プログラムとは，ある定数 kが存在して，どのようなスケジュールのもとでも，参加するすべてのプロセスが k ステップ与えられる前に終了するような並列プログラムのことである．この条件の狙いは，プロセスが他のプロセ
スを待つことを禁止することである．仮にプロセス p がプロセス q が何かをするのを待つとすると，いじわるなスケジュールのもとで，wait-free の条件は破れてしまう．実際，最初からプロセス p に

連続して k ステップ与えてしまうようなスケジュールのもとで，最初の k ステップの間，プロセス
q は何もできない一方で，プロセス p は k ステップの間プロセス q が何かをするのを polling して待ちつづけ，wait-free の条件に反してしまう．
並列プログラムは，完了するとどのプロセスからどのプロセスに信号が伝達されるか，保証する．
プロセスからプロセスへの信号伝達を，論理式で表現することを考える．プロセスを主体とみなす．
プロセス p が起動したことを表す命題記号を Ip と書く．論理式 Kq Kp Ip を，「プロセス p が起動したことをプロセス p が知って，それをプロセス q に伝えた」と読める．同様に，論理式 Kp Kq Kp Ip
を「プロセス p が起動したことをプロセス p が知って，それをプロセス q に伝達したら，プロセス
q がプロセス p に返事して伝達を受理したことを伝えた」と読める．このような信号伝達を実現す
る並列プログラムを，いろいろなプログラミング言語で，下のように記述することができる4 ．

1. プロセス p は，起動したらプロセス q に信号を送り，q からの返事を待って終了する．
2. プロセス q は，起動したらプロセス p の信号を待ち，p あてに返事を送って終了する．
残念ながら，このような並列プログラムは wait-free ではないので，論理式 Kp Kq Kp Ip を wait-free 性を表す論理式のクラスに含めることはできない．このような気分で定まる論理式のクラスを，wait-free
動作と名付けて，下のほうで定義したい．
ところで，wait-free 計算といえども，プロセスは共有メモリを待つことだけは許されている5 ．共有
メモリに値の読み込みを求めてから読み込めた値を待ったり，共有メモリに値の書き込みを求めてから書き込み完了の信号を待ったりすることはできる．この節では，メモリを表す特殊な主体 m があって，メモリ以外の主体はプロセスの集合 P の元であるとする．要するに，A = {m} ∪ P (m ∈
/ P)
とおく．
固定した wait-free な分散プログラムについて興味があるとき，ある定数があってその定数回しかメモリにアクセスできないはずである．しかも，プロセスとメモリ間の通信はあってもプロセス間の通信はないので，プロトコルが保証できる知識伝達は，Kp Km Kp · · · Km Kp Ip とメモリとプロセスの二種類の様相が交互に現れる形の論理式だけである．
スケジュールと分散プログラム以外に，実行が完了した状況が満たすべき性質も，論理式で記述したい．なにか知識が無いことを保証させたい場面は無いと勝手に決めて，プロトコル実行後に欲しい性質として positive な論理式 (wait-free 性質) だけ考えることにする．
定義 25 各プロセスに相異なる原子論理式が割り当てられていることにする (Ip )p∈P ．

Wait-free 動作 ϕ とは，下の形をした論理式である:^
ϕ=
Kp Km Kp · · · Kp Ipp∈P

ただし Kp と Km は，· · · の中で交互に現れることとする．

Wait-free 性質 ψ とは，下の BNF で定義される形をした論理式である:
ψ ::= Kp ψ | (ψ ∧ ψ) | (ψ ∨ ψ) | Ip .
Wait-free 仕様 とは 論理式 ϕ ⊃ ψ で，ϕ は wait-free 動作であり ψ は wait-free 性質であるもののことである．
Wait-free 仕様は，特殊な有限モデル性を持っている．Wait-free 仕様が体系 `sc の定理でないな
らば，特殊な形をした有限モデルが存在して，そのモデルには，定理でない wait-free 仕様が充足されない状態がある．特殊な形をした有限モデルというのは，Saks と Zaharoglou [23] によって定義された共有メモリのスケジューリングを真似したものである．
4

互いのプロセス ID を知ったりする手順は，省く．このことは，主体の集合が固定されている直観主義知識論理の制
限による．
5
さもなくば，いかなる通信も不可能になってしまっただろう．

図 2. スケジュール σ = ({a, b}, {a}, {b}) が定めるモデル R(-, σ) の形．実線の矢印の先が (x, ·) を指すときは，その矢印の元の状態を fx によって写すとその矢印の先へ写ることを表す．点線の矢印は，それ以外の，¹ を表す．推論できる矢印を省いた．

定義 26 スケジュール6 (σi )i∈I とは， P の部分集合の有限列のことである．
定義 27 プロセス p ∈ P とスケジュール (σi )i∈I について，countp (σ) を集合の濃度 |{i ∈ I | p ∈ σi }|と定義する．
V
Wait-free 動作 ϕ = p∈P Kp Km · · · Kp Ip について，countp (ϕ) を Kp Km · · · Kp Ip における Kmの出現の個数と定義する．
スケジュール σ が wait-free 動作 ϕ と整合的であるとは， 任意のプロセス p について countp (ϕ) =countp (σ) であることである．
定義 28 Wait-free 動作 ϕ と整合的なスケジュール (σi )i∈I について，スケジュールに従って定まる
モデル R(ϕ, σ) = hW, ¹, (fx )x∈P ∪{m} i を下のように定義する:• W = {(p, i) ∈ P × N | a ∈ σi } ∪ {(p, i)0 ∈ P × N | a ∈ σi } ∪ {(m, i) | i ∈ I} ∪ {(o, i) | i ∈I} ∪ {⊥}. ただし o ∈/ P ∪ {m} とする．
• ⊥ ¹ w は任意の w ∈ W について成り立つ．
• (p, i) ¹ (m, i) ¹ (p, i)0 である (p ∈ P,

i ∈ I)．

• (p, i)0 ≤ (p, j) であるのは，ちょうど i < j なときである (p ∈ P,

i, j ∈ I)．

• (x, j) ¹ (o, i) であるのは j ≤ i なときである (x ∈ P ∪ {m, o})．
• (p, j)0 ¹ (o, i) であるのは j ≤ i のときである (p ∈ P,

i, j ∈ I)．

• x ∈ P ∪ {m} について，0(x, j) か (x, j) の形をした状態 v が存在して v ¹ w を満たすとき，その最大のもの
fx (w) =(¹ の定義により，最大のものは存在する).

そのような (x, j) が存在しないとき，⊥.
さらに付値 ρ を定義する: ρ(Ip ) = {w ∈ W | (p, 0) ¹ w} (p ∈ P )．
スケジュールに従って定まるモデルの例を図 2 に示す．
定理 29 (Wait-free 計算への wait-free 仕様の完全性) ϕ ⊃ ψ が wait-free 仕様であると仮定する．
任意の整合的なスケジュール σ について関係 R(ϕ, σ), (o, n) |= ψ が成りたつならば関係 `SC (ϕ ⊃ ψ)が成立する．ただし状態 (o, n) はモデル R(ϕ, σ) の最後の状態であるとする．
6
Saks と Zaharoglou [23] は，無限列を schedule とし有限列を partial schedule としているが，本稿では有限列しか用いないので，有限列をスケジュールと呼んでしまう．

完全性を示すために，順列スケジュールモデルという特殊なモデルだけを用いる．プロセスの集
合上の順列が定める特殊な形のスケジュールを定義 34 で定めた上で，その特殊なスケジュールの定めるモデルを順列スケジュールモデルと名付ける．この完全性の証明は，逐次一貫性をメタに利用しているともいえる．
定義 30 有限集合 P について， S(P ) は，P 上の順列の集合を表すものとする．
定義 31 順列 π ∈ S(P ) について，SC(π) をこの集合だと定義する: {Km Ka Ia ⊃ Km Kb Ib |π に b が a 以前に登場する }．
ただし Index が小さいほうが前である．
定義 32 順列 π ∈ S(P ) と 0 ≤ k ≤ |P | について，論理式の集合 SC(π, k) を，{Km Ka Ia ⊃ Km Kb Ib |(π0 · · · πk ) に b が a 以前に登場する } と定義する．
補題 33 `sc

W

π∈S(A) SC(π) が成り立つ．

証明 規則 (SC) を多用すればよい．
定義 34 P の順列 π と，wait-free 動作 ϕ について，スケジュール σ(ϕ, π) を
countπ1 (ϕ)

countπ0 (ϕ)

countπn (ϕ)

z }| {z }| { z }| {σ(ϕ, p) = π0 , · · · , π0 , π1 , · · · , π1 , · · · · · · · · · , πn , · · · , πnと定義する．
下の定義で，fx (w) = w なる状態 w のことを x 状態と呼ぶことにする．それとは別に，外部観察者状態とは，(o, i) という形の状態のことである．
定義 35 順列スケジュールモデルとは， R(ϕ, σ(ϕ, π)) と作れるモデルのことである．このモデルのことを R(ϕ, π) とも書く．順列スケジュールモデルと，インデックス k ∈ I について，wk は，任意の j < k について，¹ に関して任意の πj 状態以上であるような状態 (o, l) のうち，l が最小のものを指す．
完全性の証明のために，順列スケジュールモデル上の各状態が充足する論理式を，証明可能性で特徴づけていきたい．順列スケジュールの途中の状態で成立する論理式を，証明可能性で特徴づけるために，Wait-free プログラムを途中まで実行したことにより保証される性質を，wait-free 動作の制限と名付けて定義する．
定義 36 Wait-free 動作 ϕ =

V

np

z
}|
{
K
K
K
·
·
·
K
p
m
p
p Ip について，制限を定義する:
p∈P
ϕ ¹π,k =

^

np

z
}|
{
Kp Km Kp · · · Kp Ip .

p∈P ¹π,k

ただし P ¹π,k = {p ∈ P | πj = p がある j < k について成り立つ } とする．
補題 37 Wait-free 性質 ψ について，R(ϕ, π), wk |= ψ =⇒ SC(π, k) ` ϕ ¹π,k ⊃ ψ.
一般化されたこの補題を示したのちに，定理 29 を証明するのは簡単である．
定理 29 の証明 R(ϕ, π), wn |= ψ より SC(π, n) ` ϕ ⊃ ψ(補題 37)．補題 33 より ` ϕ ⊃ ψ ．

残りは補題 37 の証明だけである．Wait-free 性質には含意の結合子 ⊃ が現れないので，モデルのどの状態でどの wait-free 性質が充足されるかは，¹ に関して下のほうから決めていくことができる．
充足される wait-free 性質を，スケジュールに関する情報 SC(π, k) とプログラムに関する情報 ϕ ¹π,kから，形式的に証明可能であるということを示していく．
補題 37 の証明 k に関する帰納法で示す．この証明の中では，R(ϕ, π), w |= ϕ を w |= ϕ と略して書く．

(k = 0 の場合) より強い命題
w0 |= ψ=⇒fπ0 (w0 ) |= ψ かつ SC(π, 0) ` ϕ ¹π,0 ⊃ ψ かつ SC(π, 0) ` ϕ ¹π,0 ⊃ Kπ0 ψ.

を，ψ の構成に関する内側の帰納法で示す．

(ψ が原子論理式であるとき) R(ϕ, π) の付値の定義より ψ = Ip0 のはずである．ϕ ¹π,0 =Kp0 Km Kp0 · · · Km Kp0 Ip0 であるから，` ϕ ¹π,0 ⊃ Kπ0 P が成り立つ．よって，SC(π, 0) `ϕ ¹π,0 ⊃ Kπ0 P が成り立つ．結果として，SC(π, 0) ` ϕ ¹π,0 ⊃ P も成り立つ．
(ψ の最上位の論理結合子が ∨ か ∧ であるとき) 帰納法の仮定を素直に使える．
(ψ = Kp ψ 0 であるとき) w0 |= Kp ψ 0 を仮定する．主張: p = π0 である．矛盾を求めて，p 6= π0と仮定する．すると fp (w0 ) = ⊥ となる．しかし，どの wait-free 性質も状態 ⊥ では成立しないので，矛盾である．p = π0 を示せた．これを使って，fp (w0 ) |= ψ 0 であることをしめせる．fp が巾等なので，fp (fp (w0 )) |= ψ 0 も成り立つ．つまり fp (w0 ) |= Kp ψ 0である．w0 |= ψ 0 より，内側の帰納法の仮定より，` ϕ ¹π,0 ⊃ Kp ψp0 である．推論規則(introspection) より，` ϕ ¹π,0 ⊃ Kp Kp ψ 0 も成り立つ．` の左に SC(π, 0) を追加できる．
(k = k 0 + 1 の場合) k = 0 の場合とおなじように，強めの命題
wk |= ψ ⇔ fπk (wk )) |= ψ ⇒ SC(π, k) ` ϕ ¹π,k ⊃ ψ かつ SC(π, k) ` ϕ ¹π,k ⊃ Kπk ψ,を，ψ についての帰納法を使って示す．

(ψ が原子論理式であるとき) R(ϕ, π), wk0 |= ψ または Iπk = ψ の少なくとも片方は成立する．
最初の場合には，帰納法の仮定による．二番目の場合には，k = 0 の場合と同様である．
(ψ の最上位の論理結合子が ∨ か ∧ であるとき) 帰納法の仮定を素直に使える．
(ψ = Kp ψ 0 のとき) 場合分けをする．πk 6= p の場合には，fπk (wk ) |= Kp ψ 0 は wk0 |= Kp ψ 0を含意する．外側の帰納法の仮定より，SC(π, k 0 ) ` ϕ ¹π,k0 ⊃ Kp ψ 0 が成立し，かつSC(π, k 0 ) ` ϕ ¹π,k0 ⊃ Kp ψ 0 が成立する．SC(π, k) は SC(π, k 0 ) を包含し，かつ，ϕ ¹π,kは ϕ ¹π,k0 よりも強いので，これらの命題は，k 0 を k に置き換えてもやはり成り立つ．一方で πk = p の場合には，wk |= Kp ψ 0 は wk |= ψ 0 を含意する．内側の帰納法の仮定により，SC(π, k) ` ϕ ¹π,k ⊃ Kp ψ 0 を得る．さらにこれにより，SC(π, k) ` ϕ ¹π,k ⊃ Kp Kp ψ 0
を得る．

3.6

定理の例

逐次一貫性のもとで，通信に沿ってあらゆる知識が伝達されると仮定すると，• p が m に ϕ であると伝える通信をし，m から p に返事があった．
• q が m に ψ であると伝える通信をし，m から q に返事があった．
この二つの前提から，q から p に ψ が伝わったか，p から q に ϕ が伝わったかどちらかであるということが言える．これを意味するのが，`sc で導出可能な Kp Km Kp ϕ, Kq Km Kq ψ `sc Kp Kq ψ ∨ Kq Kp ϕである．この判断の証明図を図 3 に示す．

∨E

(⊃-E)

.
.
. Part A

図 3. 逐次一貫性下での判断の例の証明図．対称性により補完できる部分を省略した．

Kp Km Kp ϕ, Kq Km Kq ψ `sc Kp Kq ψ ∨ Kq Kp ϕ.
.
. (同左．p と q とを，ϕ と ψ とを入れ替える．)`sc Kp Km Kq ψ ⊃ Kp Kq ψ

Kp Km Kq ψ `sc Kp Kq ψ

Km Kq ψ `sc Kq ψ

Km Kq ψ `sc Km Kq ψ

Km Kp ϕ ⊃ Km Kq ψ, Kp Km Kp ϕ `sc Kp Kq ψ ∨ Kq Kp ϕ.
.
. Part C
Km Kp ϕ ⊃ Km Kq ψ, Kp Km Kp ϕ `sc Kp Kq ψ

Kp Km Kp ϕ ⊃ Kp Km Kp ψ, Kp Km Kp ϕ `sc Kp Kq ψ

(⊃-I)

(nec)

(T)

(axiom).
.
. (同左．p と q とを，ϕ と ψ とを入れ替える．)

Kp Km Kp ϕ ⊃ Kp Km Kq ψ `sc Kp Km Kp ϕ ⊃ Kp Km Kq ψ

Kp Km Kp ϕ ⊃ Kp Km Kq ψ, Kp Km Kp ϕ `sc Kp Km Kq ψ(axiom).
.
. Part B(Kp Km Kp ϕ ⊃ Kp Km Kq ψ) ∨ (Kq Km Kq ψ ⊃ Kq Km Kp ϕ)

Main Part(⊃-E)

Kp Km Kp ϕ `sc Kp Km Kp ϕ

Kp Km Kp ϕ, Kp (Km Kp ϕ ⊃ Km Kq ψ) `sc Kp Km Kq ψ

`sc (Kp Km Kp ϕ ⊃ Kp Km Kq ψ) ∨ (Kq Km Kq ψ ⊃ Kq Km Kp ϕ)`sc Kq Kp (Km Kp ϕ ⊃ Km Kq ψ) ∨ Kq Kp (Km Kq ψ ⊃ Km Kp ϕ)(axiom)Part C(∨E)(∨K)

Km Kp ϕ ⊃ Km Kq ψ `sc Km Kp ϕ ⊃ Km Kq ψ

Kp Km Kp ϕ `sc Kp (Km Kp ϕ ⊃ Km Kq ψ) ⊃ Kp Km Kq ψ

Kq Kp (Km Kp ϕ ⊃ Km Kq ψ) `sc (Km Kp ϕ ⊃ Km Kq ψ) ∨ (Km Kq ψ ⊃ Km Kp ϕ)`sc Kp (Km Kp ϕ ⊃ Km Kq ψ) ∨ Kp (Km Kq ψ ⊃ Km Kp ϕ)`´`sc Kq Kp (Km Kp ϕ ⊃ Km Kq ψ) ∨ Kp (Km Kq ψ ⊃ Km Kp ϕ)

(∨K)

(nec)

(nec)
(⊃-I)

(axiom)Km Kp ϕ, Km Kp ϕ ⊃ Km Kq ψ `sc Km Kq ψ

Km Kp ϕ `sc Km Kp ϕ

Kq Kp (Km Kp ϕ ⊃ Km Kq ψ), Kp Km Kp ϕ `sc Kp Km Kq ψ(⊃-E)(axiom)Kq Kp (Km Kp ϕ ⊃ Km Kq ψ) `sc Kp Km Kp ϕ ⊃ Kp Km Kq ψ

`sc (Km Kp ϕ ⊃ Km Kq ψ) ∨ (Km Kq ψ ⊃ Km Kp ϕ)`´`sc Kp (Km Kp ϕ ⊃ Km Kq ψ) ∨ (Km Kq ψ ⊃ Km Kp ϕ)

(SC)

(nec)

Part B

(∨-I)

(⊃-I)

Kq Kp (Km Kp ϕ ⊃ Km Kq ψ) ` Kp (Km Kp ϕ ⊃ Km Kq ψ)

Kq Kp (Km Kp ϕ ⊃ Km Kq ψ) `sc Kq Kp (Km Kp ϕ ⊃ Km Kq ψ)

(⊃-E)

(T)

(axiom)Part A

4

関連研究

4.1

Wait-free 計算の幾何的特徴付けとの関連

2004 年のゲーデル賞は，Herlihy と Shavit と [11] と，Saks と Zaharoglou と [23] とに与えられた．本研究は，これらの研究を道標として進んだ．
Helihy と Shavit [11] は，彩色単体的複体の分割を用いて，wait-free 計算を特徴づけた．彩色単体的複体とは，単体的複体の各頂点に主体が割り振られていて，各単体には主体が相異なる頂点たちが属しているようなもののことである．さらに彩色単体的複体の分割とは，彩色単体的複体であり，頂点にはときどき，carrier と呼ばれる先祖の単体が指定されているようなものである．今回提案した論理 K∨ のモデルに現れる fa という関数は，carrier 関数からヒントを得た．単体を状態とみなすと，彩色単体的複体の分割を，情報を失わずに，K∨ のモデルとみなすこともできる．
Saks と Zaharoglou [23] は，wait-free プロトコルの中でも特に完全情報 [28] なものに特化して特徴付けを行った．共有変数でさえもが，代入された値の履歴全体をリストとして保持している．すべての部品の知識が，時間の経過に従って，増えつづけるのである．このことは，wait-free 計算を特徴づけるために，単調に知識が増え続ける，直観主義論理の意味論に登場する主体を用いることが適していることを示唆している．また，Saks と Zaharoglou [23] は，“We believe that it will beworthwhile to explore the connection with the formal theory of distributed knowledge” (我々は，分散知識の形式的理論との関連を探求することにそれなりの価値があろうと信じる) と述べている．
本研究は，wait-free 計算における知識伝達の形式的な取り扱いをすることによって，彼らが示唆した方向の研究の足掛りとなるものである．

4.2

類似の論理

Majer の Relevant Epistemic Logic [18] は，論理結合子の意味が古典論理と異なる論理に知識様相をつけたという点で，本研究の K∨ と類似している．しかし，彼らの論理には知識様相は一種類しか入っていない．つまり，単一の主体しか扱わないので，コミュニケーションを扱えるわけではない．
時相様相と知識様相を両方使う論理はたくさんある．また，Ewald [7] は，時相のついた直観主義
論理を考案している．統語論的にプロセスが現れるが時間が現れない点では，小林・米澤 [14] の体系は K∨ に類似している．しかし統語論的にも，この体系は線形論理をもとにしている点で K∨ と大きく異なり，使い方も論理プログラミングなので，本研究の論理の使い方と異なる．この体系で論理式がプロセスを表すのに対して，K∨ では様相がプロセスを名指す．

5

議論

5.1

レイテンシの分析により適している

今回提案した論理 K∨ が分析に適しているコミュニケーションとは，スループットよりもレイテンシが重要である場面であると考える．なぜならば，論理を単純にする目的から直観主義論理のKripke モデルの半順序を時間の進行と同一視しているために，あらゆる知識が，時間の進行に沿って保たれることを暗黙に仮定しているからである．特に，通信に沿って時間が進むために，通信は，
完全情報 [28] として扱わざるを得ない．完全情報プロトコルから実装可能なプロトコルを抽出する研究は盛んに行われている [8–10, 28]．けれども，今回提案した論理がより向いている状況が，レイ
テンシがスループットに比べてきつい制約になっていて，課題を解くために何通のメッセージが必要か推論するような場面であることに変わりはない．

5.2

逐次一貫性か，整列可能性か

Attiya と Welch [2] は，逐次一貫性 [16] と整列可能性 [12] との定義が類似しているために，よく取り違えられることを指摘した．簡単に，演繹体系 `SC が整列可能性を特徴づけるわけではないことを確認する．整列可能性を定義した Herlihy [12] によると，整列可能性の特徴は局所的な性質である:
つまり，各メモリオブジェクトが整列可能性を満たすときに，それらのメモリオブジェクトを並べて大きなメモリオブジェクトとみなしても，整列可能性を満たすというのだ．しかし，我々の公理型
は，局所的ではない．メモリオブジェクト m と m0 とがあるとする．我々の公理型は，それぞれのメ
モリオブジェクトについて，(Km ϕ ⊃ Km ψ) ∨ (Km ψ ⊃ Km ϕ) と (Km0 ϕ ⊃ Km0 ψ) ∨ (Km0 ψ ⊃ Km0 ϕ)という形の論理式から成る．両方の形の公理型を認めたところで，両方のメモリオブジェクトにまたがる性質 (Km ϕ ⊃ Km0 ψ) ∨ (Km0 ψ ⊃ Km ϕ) を証明することはできない．このことは，`sc が表す
性質が局所的な性質ではなく，特に整列可能性ではないことを示している．

5.3

他の共有メモリ一貫性

Steinke と Nutt [24] は，共有メモリの一貫性たちから成る束を定義した．そのなかには，名前がついているだけでも，逐次一貫性，因果一貫性，プロセッサ一貫性，PRAM 一貫性，キャッシュ一
貫性，遅い一貫性，局所一貫性という一貫性が属する．逐次一貫性以外の一貫性を論理的に特徴づけることは，今後の課題である．

5.4

選言 ∨ を知識様相 K が分配すること

Kripke モデル上で，様相の意味が関数であることから，選言を様相が分配する．小島・五十嵐 [15]は，Kripke モデル上の関数で様相を意味づけることを避けて，選言を様相が分配することを避けている．一方本研究の K∨ では，様相の意味を状態集合上の関数にして，選言を様相に分配させている．彼らの様相の使い方では様相の内側は未来を指すのに対して，本研究の K∨ の使い方では様相の内側が過去を指すという違いによって，この選択の違いがうまれているのであろう．
鈴木 [25] の翻訳によって，K∨ の主体が 1 つだけの場合のモデルは，任意の状態 w について対応する領域が単元集合であるような直観主義述語論理のモデル (Kripke バンドル) に対応する7 ．このことは，K∨ の意味論が，主体が 1 つだけの場合には極めて単純であることを示唆している．できるだけ単純な論理を用いたかったという目的に叶っている．

5.5

著者の以前の研究との関係

著者は，平井 [29] でも論理を定義して，wait-free な知識の伝達を特徴づけることを目標としたが，健全性は示したけれども，いかなる意味でも完全性を示さなかった．そこ [29] で扱った体系は，今回の `sc と目標が似ているが，論理結合子 ⊃ も無いし公理も異なるし古典論理なので，異なる．
謝辞 以前の関連する研究について発表 [29] した際，議論してくださった方々に，謝意を表する．
匿名査読者たちに学ぶべき点は多大である．感謝する．

参考文献[1] N. Alechina, M. Mendler, and V. Paiva. Categorical and Kripke semantics for constructive S4 modal
logic. 2001.
[2] H. Attiya and J.L. Welch. Sequential consistency versus linearizability. ACM Transactions on Computer Systems (TOCS), 12(2):122, 1994.
7
対応するというのは，小野 [19] にある論理 L3 のモデルが定領域の直観主義述語論理のモデルに対応するのと同様に対応するという意味である．

[3] P. Balbiani, A. Baltag, H.V.A.N. Ditmarsch, A. Herzig, T. Hoshi, and T. de Lima. Knowable
known after an announcement . The Review of Symbolic Logic, 1(03):305–334, 2008.

as[4] A. Baltag, B. Coecke, and M. Sadrzadeh. Epistemic actions as resources. Journal of Logic andComputation, 17(3):555, 2007.
[5] P. Bieber and T. Onera-Cert. A logic of communication in hostile environment. In Computer Security
Foundations Workshop III, 1990. Proceedings, pages 14–22, 1990.
[6] V. Costa and M. Benevides. Formalizing Concurrent Common Knowledge as Product of Modal Logics.
Logic Journal of IGPL, 13(6):665, 2005.
[7] W.B. Ewald. Intuitionistic tense and modal logic. The Journal of Symbolic Logic, 51(1):166–179,
1986.
[8] J.Y. Halpern. Using reasoning about knowledge to analyze distributed systems. Annual Review of
Computer Science, 2(1):37–68, 1987.
[9] J.Y. Halpern and R. Fagin. A formal model of knowledge, action, and communication in distributed
systems: preliminary report. In Proceedings of the fourth annual ACM symposium on Principles of
distributed computing, pages 224–236. ACM New York, NY, USA, 1985.
[10] J.Y. Halpern and Y. Moses. Knowledge and common knowledge in a distributed environment. Journalof the ACM (JACM), 37(3):549–587, 1990.
[11] M. Herlihy and N. Shavit. The topological structure of asynchronous computability. Journal of theACM (JACM), 46(6):858–923, 1999.
[12] M. Herlihy and J.M. Wing. Linearizability: A correctness condition for concurrent objects. ACM
Transactions on Programming Languages and Systems (TOPLAS), 12(3):463–492, 1990.
[13] L. Jia and D. Walker. Modal proofs as distributed programs. Lecture notes in computer science, pages
219–233, 2004.
[14] N. Kobayashi and A. Yonezawa. Asynchronous communication model based on linear logic. Formal
Aspects of Computing, 7(2):113–149, 1995.
[15] K. Kojima and A. Igarashi. On constructive linear-time temporal logic. Proc. of IMLA, 8, 2008.
[16] L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess progranm.
IEEE transactions on computers, 100(28):690–691, 1979.
[17] C.J. Liau. Belief, information acquisition, and trust in multi-agent systems―A modal logic formulation. Artiﬁcial Intelligence, 149(1):31–60, 2003.
[18] O. Majer and M. Peliš. Epistemic Logic with Relevant Agents.
[19] H. Ono. On some intuitionistic modal logics. Publ. Res. Inst. Math. Sci., 13(3):687–722, 1977.
[20] D. Peleg. Communication in concurrent dynamic logic. J. COMP. SYST. SCI., 35(1):23–58, 1987.
[21] J. Plaza. Logics of public communications. Synthese, 158(2):165–179, 2007.
[22] G. Plotkin and C Stirling. A framework for intuitionistic modal logics: extended abstract. In TARK
’86: Proceedings of the 1986 conference on Theoretical aspects of reasoning about knowledge, pages
399–406, San Francisco, CA, USA, 1986. Morgan Kaufmann Publishers Inc.
[23] M. Saks and F. Zaharoglou. Wait-free k-set agreement is impossible: The topology of public knowledge.
SIAM journal on computing(Print), 29(5):1449–1483, 2000.
[24] R.C. Steinke and G.J. Nutt. A uniﬁed theory of shared memory consistency. Journal of the ACM(JACM), 51(5):800–849, 2004.
[25] N.Y. Suzuki. Kripke bundles for intermediate predicate logics and Kripke frames for intuitionistic
modal logics. Studia Logica, 49(3):289–306, 1990.
[26] A.S. Troelstra and D. Van Dalen. Constructivism in Mathematics: An Introduction: Vol.: 1. NorthHolland, 1988.
[27] J. van Benthem. The information in intuitionistic logic. Synthese, 167(2):251–270, 2009.
[28] Thomas Y.C. Woo and Simon S. Lam. A lesson on authentication protocol design. SIGOPS Oper.
Syst. Rev., 28(3):24–37, 1994.
[29] 平井洋一. 「分散プログラムを形式的証明から抽出する」. 日本ソフトウェア科学会第 26 回大会, 2009.