論理学 、 哲学 、 理論計算機科学 において 、 動的論理は、 計算機プログラム の特性を符号化できる 様相論理 の拡張である 。
動的論理におけるステートメントの簡単な例は次の通りである。
地面は乾いている
→ [
雨が降る
]
地面が濡れている
、
{\displaystyle {\text{地面は乾いている}}\to [{\text{雨が降る}}]{\text{地面は濡れている}},}
これは、地面が現在乾燥していて雨が降った場合、その後地面は濡れていることを示しています。
動的ロジックの構文には、命題 の言語 (「地面は乾いている」など) と アクション の言語(「雨が降る」など) が含まれます。中核となる様相構造は、アクション a を 実行した後、 命題 p が 成り立つはずであると述べる と、アクション a を 実行した後、命題 p が 成り立つ可能性があると述べる です 。アクション言語は、演算 (あるアクションの後に別のアクションを実行する)、 (いずれかのアクションを実行する)、および反復 (1 つのアクションを 0 回以上実行する) をサポートします。命題言語は、 ブール演算 (and、or、not) をサポートします。アクション ロジックは、プログラムをエンコードするのに十分な表現力を持っています。任意のプログラム 、 前提条件 、および 事後条件 に対して、動的ロジック ステートメントはプログラムの正しさをエンコードするため、動的ロジックは Hoare ロジック よりも汎用的です 。
[ 1つの ] p
{\displaystyle [a]p}
⟨ 1つの ⟩ p
{\displaystyle \langle a\rangle p}
1つの
;
b
{\displaystyle a\mathbin {;} b}
1つの ∪ b
{\displaystyle a\cup b}
1つの
∗
{\displaystyle a{*}}
ポ
{\displaystyle P}
φ
{\displaystyle \varphi}
φ ′
{\displaystyle \varphi '}
φ → [ ポ ]
φ ′
{\displaystyle \varphi \to [P]\varphi '}
動的論理は、プログラムの形式検証 での使用を超えて、 言語学 、 哲学 、 AI 、およびその他の分野
で生じる複雑な動作を記述するために適用されてきました。
言語 様相論理は、 必然的にそうなると主張する 様相演算子 (ボックス p)と、 おそらくそうなると 主張する (ダイヤモンド p) ことによって特徴付けられます。動的論理は、あらゆる動作に 様相演算子 およびを関連付けることでこれを拡張し、それによって 多様相論理 にします 。 の意味は 、動作を実行した後、 必然的に が 成り立つ、つまり をもたらす必要があるということです 。 の意味は 、 を実行した後、が 成り立つ、つまり をもたらす 可能性があるということです 。これらの演算子は 互いに 双対であり 、つまり、普遍 ( ) 量指定子と存在 ( ) 量指定子
の関係と同様に、 それらは および によって関連付けられます。
◻ p
{\displaystyle \Box p}
p
{\displaystyle p\,\!}
◊ p
{\displaystyle \Diamond p}
p
{\displaystyle p\,\!}
1つの
{\displaystyle a\,\!}
[ 1つの ]
{\displaystyle [a]\,\!}
⟨ 1つの ⟩
{\displaystyle \langle a\rangle \,\!}
[ 1つの ] p
{\displaystyle [a]p\,\!}
1つの
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
1つの
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
⟨ 1つの ⟩ p
{\displaystyle \langle a\rangle p\,\!}
1つの
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
1つの
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
[ 1つの ] p ↔ ¬ ⟨ 1つの ⟩ ¬ p
{\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}
⟨ 1つの ⟩ p ↔ ¬ [ 1つの ] ¬ p
{\displaystyle \langle a\rangle p\leftrightarrow \neg [a]\neg p\,\!}
∀
{\displaystyle \forall \,\!}
∃
{\displaystyle \exists \,\!}
動的ロジックでは、 より小さなアクションから構築された複合アクションが許可されます。任意のプログラミング言語の基本的な制御演算子をこの目的に使用できますが、 クリーネ の 正規表現 演算子は様相ロジックに適しています。アクション および が与えられた場合 、複合アクション choice ( または とも表記 ) は、 または のいずれかを実行することによって実行されます 。複合アクション sequence は 、最初に を実行し てからを実行することによって実行されます 。複合アクション iteration は 、を 0 回以上順番に 実行することによって実行されます。定数 アクション BLOCK は 何も行わず、終了しませんが、定数アクション SKIP または NOP は として定義でき 、何も行いませんが終了します。
1つの
{\displaystyle a\,\!}
b
{\displaystyle b\,\!}
1つの ∪ b
{\displaystyle a\cup b\,\!}
1つの + b
{\displaystyle a+b\,\!}
1つの
|
b
{\displaystyle a|b\,\!}
1つの
{\displaystyle a\,\!}
b
{\displaystyle b\,\!}
1つの
;
b
{\displaystyle a{\mathbin {;}}b\,\!}
1つの
{\displaystyle a\,\!}
b
{\displaystyle b\,\!}
1つの
∗
{\displaystyle a{*}\,\!}
1つの
{\displaystyle a\,\!}
0
{\displaystyle 0\,\!}
1
{\displaystyle 1\,\!}
0
∗
{\displaystyle 0{*}\,\!}
公理 これらの演算子は、前述の 公理 や、2 つの推論規則 modus ponens ( および が 意味する ) と necessitation (が 意味する) などの様相演算子の公理を含む様相論理の適切な公理化を既に与えたものとして、次のように 動的論理 で公理化できます。
[ 1つの ] p ↔ ¬ ⟨ 1つの ⟩ ¬ p
{\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}
⊢ p
{\displaystyle \vdash p}
⊢ p → q
{\displaystyle \vdash p\to q}
⊢
q
{\displaystyle \vdash q\,}
⊢
p
{\displaystyle \vdash p}
⊢
[
a
]
p
{\displaystyle \vdash [a]p\,}
A1.
[
0
]
p
{\displaystyle [0]p\,\!}
A2.
[
1
]
p
↔
p
{\displaystyle [1]p\leftrightarrow p\,\!}
A3.
[
a
∪
b
]
p
↔
[
a
]
p
∧
[
b
]
p
{\displaystyle [a\cup b]p\leftrightarrow [a]p\land [b]p\,\!}
A4.
[
a
;
b
]
p
↔
[
a
]
[
b
]
p
{\displaystyle [a\mathbin {;} b]p\leftrightarrow [a][b]p\,\!}
A5.
[
a
∗
]
p
↔
p
∧
[
a
]
[
a
∗
]
p
{\displaystyle [a*]p\leftrightarrow p\land [a][a*]p\,\!}
A6.
p
∧
[
a
∗
]
(
p
→
[
a
]
p
)
→
[
a
∗
]
p
{\displaystyle p\land [a*](p\to [a]p)\to [a*]p\,\!}
公理 A1 は、 BLOCK が 終了したときに、 命題 が 偽 で あっても が成り立つ という空約束をします 。(したがって、 BLOCK は 地獄が凍りつくという動作の本質を抽象化します。)
A2 は、 NOP が 命題に対する恒等関数として動作する、つまり、それ 自体に変換すると述べています。A3は、 または
のいずれかを実行すると が 生じる場合 、が 生じる必要があり 、 についても同様に 、またその逆が成り立つと述べています。A4
は、および を実行すると が生じる場合 、 が 生じる必要がある 場合、 が をもたらす必要がある 状況が生じると述べています 。A5は、A2、A3、および A4 を クリーネ代数 の
方程式に適用した明らかな結果です 。A6
は、現在が 成り立ち、何度実行しても、 その実行後の の真理が をもう一度実行した後も の真理を含意する という事実が変わらない場合 、を 何度実行しても真のままであると主張しています。A6 は、 n を増分する 動作 n := n+1 を 任意の動作 に一般化した 数学的帰納法 として認識できます 。
p
{\displaystyle p\,\!}
p
{\displaystyle p\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
b
{\displaystyle b\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
b
{\displaystyle b\,\!}
a
{\displaystyle a\,\!}
b
{\displaystyle b\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
b
{\displaystyle b\,\!}
p
{\displaystyle p\,\!}
a
∗
=
1
∪
a
;
a
∗
{\displaystyle a{*}=1\cup a{\mathbin {;}}a{*}\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
a
{\displaystyle a\,\!}
派生語 様相論理公理により、 上記に対応する次の 6 つの定理を導出できます。
[
a
]
p
↔
¬
⟨
a
⟩
¬
p
{\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}
T1.
¬
⟨
0
⟩
p
{\displaystyle \neg \langle 0\rangle p\,\!}
T2.
⟨
1
⟩
p
↔
p
{\displaystyle \langle 1\rangle p\leftrightarrow p\,\!}
T3.
⟨
a
∪
b
⟩
p
↔
⟨
a
⟩
p
∨
⟨
b
⟩
p
{\displaystyle \langle a\cup b\rangle p\leftrightarrow \langle a\rangle p\lor \langle b\rangle p\,\!}
T4.
⟨
a
;
b
⟩
p
↔
⟨
a
⟩
⟨
b
⟩
p
{\displaystyle \langle a\mathbin {;} b\rangle p\leftrightarrow \langle a\rangle \langle b\rangle p\,\!}
T5.
⟨
a
∗
⟩
p
↔
p
∨
⟨
a
⟩
⟨
a
∗
⟩
p
{\displaystyle \langle a*\rangle p\leftrightarrow p\lor \langle a\rangle \langle a*\rangle p\,\!}
T6.
⟨
a
∗
⟩
p
→
p
∨
⟨
a
∗
⟩
(
¬
p
∧
⟨
a
⟩
p
)
{\displaystyle \langle a*\rangle p\to p\lor \langle a*\rangle (\neg p\land \langle a\rangle p)\,\!}
T1 は、 BLOCK を 実行しても何も起こらないと主張しています 。T2は、 NOP は 決定論的であり、 と が 同じ力を持つ場合に終了する ことを念頭に置いて、NOP は何も変更しないこと
を 再度 指摘しています。T3 は、または
の選択が を引き起こす可能性がある場合 、 または のいずれ か 単独で を引き起こす可能性があると述べています 。T4
は A4 とまったく同じです。T5
は A5 の場合と同様に説明されています。T6は、十分な頻度 で実行することによって
を引き起こす可能性がある場合 、 が現在真であるか、または を 繰り返し実行して が（依然として）偽である状況を引き起こすこと が可能である が、 をもう 1 回実行すると を引き起こす可能性があると主張しています 。
[
1
]
{\displaystyle [1]\,\!}
⟨
1
⟩
{\displaystyle \langle 1\rangle \,\!}
a
{\displaystyle a\,\!}
b
{\displaystyle b\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
b
{\displaystyle b\,\!}
p
{\displaystyle p\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
ボックスとダイヤモンドは、どちらを原始的なものとしてとるかに関して完全に対称です。別の公理化としては、定理 T1 ～ T6 を公理としてとり、そこから定理 A1 ～ A6 を導出するという方法があります。
含意と推論の違いは、動的論理でも他の論理と同じです。つまり、含意は、 が真であれば も真である と主張します が、推論は、 が有効であれば も真である と主張します 。ただし、動的論理の動的な性質により、この区別は抽象的な公理の領域から、変化する状況の常識的な経験へと移されます。 たとえば、推論規則 は、その前提が が 常に成り立つと主張しているため、 がどこに 導こうとも、 そこでは が真であるため、妥当です。ただし、含意は 有効ではありません。なぜなら、 現時点で が真実だからといって、 を実行した後も が真実であるという保証はないからです 。たとえば、 は、が偽 である状況 や が真である状況では真になりますが、 の値が 1 である状況では 主張は偽で あるため、 は有効ではありません。
p
→
q
{\displaystyle p\to q\,\!}
p
{\displaystyle p\,\!}
q
{\displaystyle q\,\!}
p
⊢
q
{\displaystyle p\vdash q\,\!}
p
{\displaystyle p\,\!}
q
{\displaystyle q\,\!}
p
⊢
[
a
]
p
{\displaystyle p\vdash [a]p\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
p
→
[
a
]
p
{\displaystyle p\to [a]p\,\!}
p
{\displaystyle p\,\!}
a
{\displaystyle a\,\!}
p
→
[
a
]
p
{\displaystyle p\to [a]p\,\!}
p
{\displaystyle p\,\!}
[
a
]
p
{\displaystyle [a]p\,\!}
(
x
=
1
)
→
[
x
:=
x
+
1
]
(
x
=
1
)
{\displaystyle (x=1)\to [x:=x+1](x=1)\,\!}
x
{\displaystyle x\,\!}
推論の導出規則 様相論理に関しては、上で述べたように、推論規則の 様相ポネンス と 必然性は 、動的論理にも必要な唯一の基本規則として十分です。しかし、論理ではよくあることですが、公理の助けを借りて、これらからさらに多くの規則を導き出すことができます。動的論理におけるそのような導出規則の例は、壊れたテレビを一度蹴っても絶対に直らないのであれば、何度も蹴っても絶対に直らない、というものです。 テレビを蹴るという動作と、 テレビが壊れているという命題について書くと、動的論理ではこの推論を 、前提 、結論 を持つ と表現します 。 の意味は 、テレビを蹴った後は、必ずテレビが壊れているということです。したがって前提 は、 テレビが壊れている場合は、一度蹴った後もまだ壊れていることを意味します。 は、テレビを 0 回以上蹴る動作を表します。したがって結論 は、テレビ が壊れている場合は、0 回以上蹴った後もまだ壊れていることを意味します。そうでなければ、最後から2番目の蹴りの後、テレビはもう一度蹴れば直る状態になりますが、これはいかなる状況でも決して起こり得ないことを前提としています。
k
{\displaystyle k\,\!}
b
{\displaystyle b\,\!}
b
→
[
k
]
b
⊢
b
→
[
k
∗
]
b
{\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}
b
→
[
k
]
b
{\displaystyle b\to [k]b\,\!}
b
→
[
k
∗
]
b
{\displaystyle b\to [k*]b\,\!}
[
k
]
b
{\displaystyle [k]b\,\!}
b
→
[
k
]
b
{\displaystyle b\to [k]b\,\!}
k
∗
{\displaystyle k{*}\,\!}
b
→
[
k
∗
]
b
{\displaystyle b\to [k*]b\,\!}
推論 は正しい。しかし、含意は正しくない。なぜなら、 成り立つが 成り立たない 状況は簡単に見つかるからである。そのような反例の状況では、 必ず成り立つが 偽でなければならないが、しかしながら は真でなければならない。しかし、これはテレビが壊れているが二回蹴れば復活できるような状況ならどこでも起こり得る。含意は、その 成立を今のみ必要とするので失敗（正しくない）であるが、推論は、その 成立を現在の状況だけでなくあらゆる状況で必要とするので成功（正しい）である。
b
→
[
k
]
b
⊢
b
→
[
k
∗
]
b
{\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}
(
b
→
[
k
]
b
)
→
(
b
→
[
k
∗
]
b
)
{\displaystyle (b\to [k]b)\to (b\to [k*]b)\,\!}
b
→
[
k
]
b
{\displaystyle b\to [k]b\,\!}
b
→
[
k
∗
]
b
{\displaystyle b\to [k*]b\,\!}
b
{\displaystyle b\,\!}
[
k
∗
]
b
{\displaystyle [k*]b\,\!}
[
k
]
b
{\displaystyle [k]b\,\!}
b
→
[
k
]
b
{\displaystyle b\to [k]b\,\!}
b
→
[
k
]
b
{\displaystyle b\to [k]b\,\!}
有効な含意の例は、命題 です 。これは、 が 3 以上の場合、 を増分した後 、は 4 以上でなければならない、というものです。 などの確実に終了する 決定論的アクションの場合 、 と は 同じ効力を持つ 必要が あり、 同じ意味を持つ 可能性があります 。したがって、上記の命題は、が 3 以上の 場合、 を実行した後 、 は 4 以上になる可能性がある、
という主張と同等です。
(
x
≥
3
)
→
[
x
:=
x
+
1
]
(
x
≥
4
)
{\displaystyle (x\geq 3)\to [x:=x+1](x\geq 4)\,\!}
x
{\displaystyle x\,\!}
x
{\displaystyle x\,\!}
x
{\displaystyle x\,\!}
a
{\displaystyle a\,\!}
x
:=
x
+
1
{\displaystyle x:=x+1\,\!}
[
a
]
{\displaystyle [a]\,\!}
⟨
a
⟩
{\displaystyle \langle a\rangle \,\!}
(
x
≥
3
)
→
⟨
x
:=
x
+
1
⟩
(
x
≥
4
)
{\displaystyle (x\geq 3)\to \langle x:=x+1\rangle (x\geq 4)\,\!}
x
{\displaystyle x\,\!}
x
:=
x
+
1
{\displaystyle x:=x+1\,\!}
x
{\displaystyle x\,\!}
割り当て 代入ステートメントの一般的な形式は、 です。 ここで 、 は変数であり、 は 定数と変数から構築された式で、加算や乗算など、言語によって提供される演算が使用されます。代入に関する Hoare 公理は、単一の公理としてではなく、公理スキーマとして与えられます。
x
:=
e
{\displaystyle x:=e\,\!}
x
{\displaystyle x\,\!}
e
{\displaystyle e\,\!}
A7.
[
x
:=
e
]
Φ
(
x
)
↔
Φ
(
e
)
{\displaystyle [x:=e]\Phi (x)\leftrightarrow \Phi (e)\,\!}
これは、変数 のゼロ個以上のインスタンスを含む 任意の式でインスタンス化できるという 意味でのスキーマです 。 の意味は、 内 で自由に出現する 、つまり のように何らかの量指定子によって束縛されない の出現を に 置き換えたものに なります。たとえば、 A7 を 、または でインスタンス化できます 。このような公理スキーマにより、共通の形式を持つ無限の数の公理を、その形式を暗示する有限式として記述できます。
Φ
(
x
)
{\displaystyle \Phi (x)\,\!}
Φ
{\displaystyle \Phi \,\!}
x
{\displaystyle x\,\!}
Φ
(
e
)
{\displaystyle \Phi (e)\,\!}
Φ
{\displaystyle \Phi \,\!}
x
{\displaystyle x\,\!}
Φ
{\displaystyle \Phi \,\!}
∀
x
{\displaystyle \forall x\,\!}
e
{\displaystyle e\,\!}
[
x
:=
e
]
(
x
=
y
2
)
↔
e
=
y
2
{\displaystyle [x:=e](x=y^{2})\leftrightarrow e=y^{2}\,\!}
[
x
:=
e
]
(
b
=
c
+
x
)
↔
b
=
c
+
e
{\displaystyle [x:=e](b=c+x)\leftrightarrow b=c+e\,\!}
A7 の例により、 数段落前に遭遇した 例が に等しいことが機械的に計算でき 、これは 初等代数 によりに等しいことがわかります 。
[
x
:=
x
+
1
]
(
x
≥
4
)
↔
x
+
1
≥
4
{\displaystyle [x:=x+1](x\geq 4)\leftrightarrow x+1\geq 4\,\!}
[
x
:=
x
+
1
]
x
≥
4
{\displaystyle [x:=x+1]x\geq 4\,\!}
x
+
1
≥
4
{\displaystyle x+1\geq 4\,\!}
x
≥
3
{\displaystyle x\geq 3\,\!}
との組み合わせによる代入の例は、 命題 です 。これは、 十分な頻度で増分することで、 を 7 に等しくすることが可能であることを主張しています 。もちろん、 が最初から 8 であったり、 6.5 であったりする場合は常に真であるとは限りません。その場合、この命題は動的論理の定理ではありません。 ただし、 が整数型の場合、 が最初から最大で 7 である場合に限り、この命題は真です。 つまり、 を遠回しに言っているだけです 。
∗
{\displaystyle *\,\!}
⟨
(
x
:=
x
+
1
)
∗
⟩
x
=
7
{\displaystyle \langle (x:=x+1)*\rangle x=7\,\!}
x
{\displaystyle x\,\!}
x
{\displaystyle x\,\!}
x
{\displaystyle x\,\!}
x
{\displaystyle x\,\!}
x
{\displaystyle x\,\!}
x
≤
7
{\displaystyle x\leq 7\,\!}
数学的帰納法は 、命題が、アクション が 、 として インスタンス化された A6 のインスタンスとして取得できます 。これらの 3 つのインスタンス化の最初の 2 つは簡単で、A6 を に変換します。ただし、 を に 置き換えるという一見単純な方法は 、様相が置き換えに干渉する可能性がある場合に様相論理のいわゆる参照の
不透明性 を引き起こすため、それほど単純ではありません。
p
{\displaystyle p\,\!}
Φ
(
n
)
{\displaystyle \Phi (n)\,\!}
a
{\displaystyle a\,\!}
n
:=
n
+
1
{\displaystyle n:=n+1\,\!}
n
{\displaystyle n\,\!}
0
{\displaystyle 0\,\!}
(
Φ
(
n
)
∧
[
(
n
:=
n
+
1
)
∗
]
(
Φ
(
n
)
→
[
n
:=
n
+
1
]
Φ
(
n
)
)
)
→
[
(
n
:=
n
+
1
)
∗
]
Φ
(
n
)
{\displaystyle (\Phi (n)\land [(n:=n+1)*](\Phi (n)\to [n:=n+1]\Phi (n)))\to [(n:=n+1)*]\Phi (n)\,\!}
0
{\displaystyle 0\,\!}
n
{\displaystyle n\,\!}
を 代入したとき 、命題記号を 様相 に関する 固定指定子 として考えていました 。つまり、 を増分すると命題の真偽が変わる可能性がありますが、 を増分した後も以前と同じ命題であるということです。同様に、 を増分すると 別の環境で実行されることになります が、を増分した後も アクションは 同じアクションです。ただし、 自体は様相 に関する固定指定子ではありません 。 を増分する前は 3 を示していたとしても、 を増分した後は 4 を示します。したがって、 A6 のどこでも を
に 代入することはできません。
Φ
(
n
)
{\displaystyle \Phi (n)\,\!}
p
{\displaystyle p\,\!}
p
{\displaystyle p\,\!}
[
n
:=
n
+
1
]
{\displaystyle [n:=n+1]\,\!}
n
{\displaystyle n\,\!}
n
{\displaystyle n\,\!}
a
{\displaystyle a\,\!}
n
{\displaystyle n\,\!}
n
{\displaystyle n\,\!}
n
{\displaystyle n\,\!}
[
n
:=
n
+
1
]
{\displaystyle [n:=n+1]\,\!}
n
{\displaystyle n\,\!}
0
{\displaystyle 0\,\!}
n
{\displaystyle n\,\!}
様相の不透明性に対処する 1 つの方法は、様相を除去することです。このためには、 無限連言 、つまり 全体にわたる連言 として展開します。ここで A4 を適用し て に 変換し 、 様相を持ちます。次に、 これに Hoare の公理を 回適用して を生成し 、この無限連言を に簡略化します。この簡約全体を A6 の の両方のインスタンスに適用して を生成します 。残りの様相は、Hoare の公理をもう 1 回使用して を生成することで除去できます 。
[
(
n
:=
n
+
1
)
∗
]
Φ
(
n
)
{\displaystyle [(n:=n+1)*]\Phi (n)\,\!}
[
(
n
:=
n
+
1
)
0
]
Φ
(
n
)
∧
[
(
n
:=
n
+
1
)
1
]
Φ
(
n
)
∧
[
(
n
:=
n
+
1
)
2
]
Φ
(
n
)
∧
…
{\displaystyle [(n:=n+1)^{0}]\Phi (n)\land [(n:=n+1)^{1}]\Phi (n)\land [(n:=n+1)^{2}]\Phi (n)\land \ldots \,\!}
i
{\displaystyle i\,\!}
[
(
n
:=
n
+
1
)
i
]
Φ
(
n
)
{\displaystyle [(n:=n+1)^{i}]\Phi (n)\,\!}
[
(
n
:=
n
+
1
)
i
]
Φ
(
n
)
{\displaystyle [(n:=n+1)^{i}]\Phi (n)\,\!}
[
n
:=
n
+
1
]
[
n
:=
n
+
1
]
…
Φ
(
n
)
{\displaystyle [n:=n+1][n:=n+1]\ldots \Phi (n)\,\!}
i
{\displaystyle i\,\!}
i
{\displaystyle i\,\!}
Φ
(
n
+
i
)
{\displaystyle \Phi (n+i)\,\!}
∀
i
Φ
(
n
+
i
)
{\displaystyle \forall i\Phi (n+i)\,\!}
[
(
n
:=
n
+
1
)
∗
]
{\displaystyle [(n:=n+1)*]\,\!}
(
Φ
(
n
)
∧
∀
i
(
Φ
(
n
+
i
)
→
[
n
:=
n
+
1
]
Φ
(
n
+
i
)
)
)
→
∀
i
Φ
(
n
+
i
)
{\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to [n:=n+1]\Phi (n+i)))\to \forall i\Phi (n+i)\,\!}
(
Φ
(
n
)
∧
∀
i
(
Φ
(
n
+
i
)
→
Φ
(
n
+
i
+
1
)
)
)
→
∀
i
Φ
(
n
+
i
)
{\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}
不透明な様相がなくなったので、 通常の 一階述語論理 の方法でを安全に置き換えて、 ペアノ の有名な公理、つまり数学的帰納法 を得ることができます 。
0
{\displaystyle 0\,\!}
n
{\displaystyle n\,\!}
(
Φ
(
0
)
∧
∀
i
(
Φ
(
i
)
→
Φ
(
i
+
1
)
)
)
→
∀
i
Φ
(
i
)
{\displaystyle (\Phi (0)\land \forall i(\Phi (i)\to \Phi (i+1)))\to \forall i\Phi (i)\,\!}
ここで簡単に触れた微妙な点は、 は自然数 にわたるものとして理解されるべきであるということです。ここで、 は 、 の展開における上付き文字であり、 すべての自然数 上の の 和集合です 。この型指定情報をきちんと保持することの重要性は、 が 整数 型 、または 実数 型 であった場合に明らかになります 。これらのいずれに対しても、A6 は公理として完全に有効です。好例を挙げると、 が 実数変数で、 述語が 自然数 で ある場合、最初の 2 つの置換後の公理 A6、つまり は、が 自然数 型である場合 と同じように有効、つまり、 その状態での の値に関係なく、すべての状態で真です 。特定の状態で が 自然数である場合、A6 の主な含意の前提は成り立ちますが、 も自然数であるため、結論も成り立ちます。 が 自然数でない場合、前提は偽であるため、結論が真であるかどうかに関係なく、A6 は真のままです。 A6 を同等に強化しても 、このいずれにも影響はありません。他の方向は A5 から証明可能であり、A6 の前提がどこかで誤っている場合は、結論も 必ず 誤っていることがわかります。
∀
i
{\displaystyle \forall i\,\!}
i
{\displaystyle i\,\!}
a
∗
{\displaystyle a{*}\,\!}
a
i
{\displaystyle a^{i}\,\!}
i
{\displaystyle i\,\!}
n
{\displaystyle n\,\!}
n
{\displaystyle n\,\!}
Φ
(
n
)
{\displaystyle \Phi (n)\,\!}
n
{\displaystyle n\,\!}
(
Φ
(
n
)
∧
∀
i
(
Φ
(
n
+
i
)
→
Φ
(
n
+
i
+
1
)
)
)
→
∀
i
Φ
(
n
+
i
)
{\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}
n
{\displaystyle n\,\!}
n
{\displaystyle n\,\!}
n
{\displaystyle n\,\!}
n
+
i
{\displaystyle n+i\,\!}
n
{\displaystyle n\,\!}
p
∧
[
a
∗
]
(
p
→
[
a
]
p
)
↔
[
a
∗
]
p
{\displaystyle p\land [a*](p\to [a]p)\leftrightarrow [a*]p\,\!}
テスト 動的ロジックは、すべての命題に テストと呼ばれる アクションを関連付けます。 が成立する場合、テストは NOP として機能し 、アクションを続行しながら何も変更しません。 が偽の場合、 BLOCK として機能します 。テストは次のように公理化できます。
p
{\displaystyle p\,\!}
p
?
{\displaystyle p?\,\!}
p
{\displaystyle p\,\!}
p
?
{\displaystyle p?\,\!}
p
{\displaystyle p\,\!}
p
?
{\displaystyle p?\,\!}
A8.
[
p
?
]
q
↔
(
p
→
q
)
{\displaystyle [p?]q\leftrightarrow (p\to q)\,\!}
対応する定理は次のとおり です。
⟨
p
?
⟩
{\displaystyle \langle p?\rangle \,\!}
T8.
⟨
p
?
⟩
q
↔
p
∧
q
{\displaystyle \langle p?\rangle q\leftrightarrow p\land q\,\!}
構造 if p then a else b は、 動的ロジックでは として実現されます 。このアクションは保護された選択を表します。 が 成り立つ場合、 は と同等です が、 は BLOCK と同等で、 は と同等です 。したがって、 が真の場合はアクションの実行者は左の分岐のみを取ることができ、 が 偽の場合は右の分岐のみを取ることができます。
(
p
?
;
a
)
∪
(
¬
p
?
;
b
)
{\displaystyle (p?\mathbin {;} a)\cup (\neg p?\mathbin {;} b)\,\!}
p
{\displaystyle p\,\!}
p
?
;
a
{\displaystyle p?\mathbin {;} a\,\!}
a
{\displaystyle a\,\!}
¬
p
?
;
b
{\displaystyle \neg p?\mathbin {;} b\,\!}
a
∪
0
{\displaystyle a\cup 0\,\!}
a
{\displaystyle a\,\!}
p
{\displaystyle p\,\!}
p
{\displaystyle p\,\!}
while p do a という構文は として実現されます 。これは 0 回以上実行されてから を実行します 。 が true である限り 、 最後の は実行者が反復を途中で終了するのをブロックしますが、 が false になるとすぐに、本体のそれ以上の反復 がブロックされ、実行者はテスト を介して終了するしか選択肢がなくなります 。
(
p
?
;
a
)
∗
;
¬
p
?
{\displaystyle ({p?\mathbin {;} a)*}\mathbin {;} \neg p?\,\!}
p
?
;
a
{\displaystyle p?\mathbin {;} a\,\!}
¬
p
?
{\displaystyle \neg p?\,\!}
p
{\displaystyle p\,\!}
¬
p
?
{\displaystyle \neg p?\,\!}
p
{\displaystyle p\,\!}
¬
p
?
{\displaystyle \neg p?\,\!}
ランダム割り当てとしての定量化 ランダム割り当てステートメントは、を 任意の値に 設定する非決定的なアクションを表します。 は、 を何に設定しても が成り立つことを示し 、 は、 true となる値に 設定できることを示します 。 したがって、 は全称量指定子 と同じ意味を持ち 、 は 同様に存在量指定子 に対応します 。 つまり、一階述語論理は、 という形式のプログラムの動的論理として理解できます 。
x
:=
?
{\displaystyle x\mathbin {:=} {?}\,\!}
x
{\displaystyle x\,\!}
[
x
:=
?
]
p
{\displaystyle [x\mathbin {:=} {?}]p\,\!}
p
{\displaystyle p\,\!}
x
{\displaystyle x\,\!}
⟨
x
:=
?
⟩
p
{\displaystyle \langle x\mathbin {:=} {?}\rangle p\,\!}
x
{\displaystyle x\,\!}
p
{\displaystyle p\,\!}
[
x
:=
?
]
{\displaystyle [x\mathbin {:=} {?}]\,\!}
∀
x
{\displaystyle \forall x\,\!}
⟨
x
:=
?
⟩
{\displaystyle \langle x\mathbin {:=} {?}\rangle \,\!}
∃
x
{\displaystyle \exists x\,\!}
x
:=
?
{\displaystyle x:=?\,\!}
ダイクストラは 、変数の値を 任意の正の整数に設定するプログラムの不可能性を示したと主張しました。 [1] しかし、代入と*演算子を含む動的論理では、 動的論理プログラムを使用して変数を任意の正の整数に設定できます 。したがって、ダイクストラの議論を拒否するか、*演算子が有効ではないと主張する必要があります。
x
{\displaystyle x}
x
{\displaystyle x}
(
x
:=
0
)
;
(
x
:=
x
+
1
)
∗
{\displaystyle (x\mathbin {:=} 0)\mathbin {;} (x:=x+1){*}}
可能世界意味論 様相論理は、可能世界 意味論またはクリプキ構造の観点から最も一般的に解釈されます 。この意味論は、世界をプログラム検証への応用ではコンピュータの状態として、言語学、AI などへの応用では環境の状態として解釈することにより、動的論理に自然に引き継がれます。可能世界意味論の役割の 1 つは、真理と妥当性の直感的な概念を形式化することです。これにより、公理系に対して健全性と完全性の概念を定義できるようになります。推論規則が健全であるのは、その前提の妥当性が結論の妥当性を意味する場合です。公理系が健全であるのは、そのすべての公理が有効で、推論規則が健全である場合です。公理系が完全であるのは、すべての有効な式がその系の定理として導出可能である場合です。これらの概念は、 動的論理を含む
すべての 論理系に適用されます。
命題動的論理 (PDL) 通常または 一階論理には 、アサーションとデータの 2 種類の用語があります。上記の例からわかるように、動的論理では、アクションを表す 3 つ目の種類の用語が追加されます。動的論理のアサーションには 、3 種類すべてが含まれます。 、、 は データ、 はアクション、および は アサーションです。 命題論理は 、データ用語を省略して一階論理から派生し、抽象的な命題についてのみ推論します。抽象的な命題は、単純な 命題変数またはアトム、または and 、 または 、 not など の論理接続子で構築された複合命題である可能性があります 。
[
x
:=
x
+
1
]
(
x
≥
4
)
{\displaystyle [x:=x+1](x\geq 4)\,\!}
x
{\displaystyle x\,\!}
x
+
1
{\displaystyle x+1\,\!}
4
{\displaystyle 4\,\!}
x
:=
x
+
1
{\displaystyle x:=x+1\,\!}
x
≥
4
{\displaystyle x\geq 4\,\!}
[
x
:=
x
+
1
]
(
x
≥
4
)
{\displaystyle [x:=x+1](x\geq 4)\,\!}
命題動的論理 (PDL) は、1977 年に Michael J. Fischer と Richard Ladner によって動的論理から派生しました。PDL は、アクションを追加しデータを省略することで、命題論理と動的論理の背後にあるアイデアを融合します。したがって、PDL の用語はアクションと命題です。上記の TV の例は PDL で表現されていますが、次の例は 1 階動的論理で表現されています。PDL は (1 階) 動的論理に対して、命題論理は 1 階論理に対してです。
x
:=
x
+
1
{\displaystyle x:=x+1\,\!}
フィッシャーとラドナーは 1977 年の論文で、PDL の充足可能性の 計算複雑度 はせいぜい非 決定的指数時間 、最悪の場合でも少なくとも 決定的指数時間であることを示した。このギャップは 1978 年に ヴォーン・プラット によって埋められ、 プラットは PDL が決定的指数時間で決定可能であることを示しました。1977 年、クリスター・セガーバーグは PDL の完全な公理化、つまり上記の公理 A1 ～ A6 と組み合わせた様相論理 K の任意の完全な公理化を提案しました。セガーバーグの公理の完全性証明は、 ガベイ (未発表メモ)、 パリク (1978)、プラット (1979)、および コーゼン とパリク (1981) によってなされました。
歴史 動的論理は、 1974年にプログラム検証の授業のノートの中で、 ホーア論理 に意味を割り当てる方法として、ホーアの公式 を と表現するアプローチとして、 ヴォーン・プラット によって開発されました。このアプローチは、後に1976年に それ自体の 論理システムとして発表されました。このシステムは、アンドレイ・サルウィッキの アルゴリズム論理システム [2] や エドガー・ダイクストラ の最弱前提条件述語変換器 の概念に類似しており 、 は ダイクストラの 最弱自由主義前提条件 に対応しています。ただし、これらの論理は、様相論理、クリプキ意味論、正規表現、二項関係の計算とは関係がありません。したがって、動的論理は、アルゴリズム論理と 述語変換器を 、様相論理の公理とクリプキ意味論、および二項関係と正規表現の計算に結び付ける改良版と見なすことができます。
p
{
a
}
q
{\displaystyle p\{a\}q\,\!}
p
→
[
a
]
q
{\displaystyle p\to [a]q\,\!}
wp
(
a
,
p
)
{\displaystyle \operatorname {wp} (a,p)\,\!}
[
a
]
p
{\displaystyle [a]p\,\!}
wlp
(
a
,
p
)
{\displaystyle \operatorname {wlp} (a,p)\,\!}
同時実行の課題 ホーア論理、アルゴリズム論理、最弱前提条件、動的論理はすべて、順次動作についての議論や推論に適しています。ただし、これらの論理を並行動作に拡張すると、問題が生じることが判明しています。さまざまなアプローチがありますが、いずれも順次動作の場合のようなエレガントさを欠いています。対照的に、 アミール・プヌエリ の 1977 年の 時相論理 システムは、動的論理と多くの共通点を持つ様相論理の別の変種であり、プヌエリが「内生的」論理と特徴付けたものであり、他の論理は「外生的」論理である点で、上記のすべての論理とは異なります。これによりプヌエリは、時相論理の主張は、単一のグローバル状況が時間の経過とともに変化する普遍的な動作フレームワーク内で解釈されるのに対し、他の論理の主張は、それらが語る複数の動作の外部で行われるということを意味しました。内生的アプローチの利点は、環境が時間とともに変化するときに何が何を引き起こすかについて基本的な仮定を行わないことです。代わりに、時相論理式は、システムの無関係な 2 つの部分について話すことができます。これらの部分は無関係であるため、暗黙的に並行して進化します。実際、時相アサーションの通常の論理結合は、時相論理の並行合成演算子です。並行性に対するこのアプローチの単純さにより、同期、干渉、独立性、 デッドロック 、 ライブロック 、公平性などの側面を持つ並行システムについて推論するための様相論理として、時相論理が選ばれるようになりました。
参照
さらに読む Nicolas Troquard と Philippe Balbiani、「命題動的論理」。 スタンフォード哲学百科事典 、2007 年。
^ Dijkstra, EW (1976). プログラミングの規律。Englewood Cliffs: Prentice-Hall Inc. pp. 221. ISBN 013215871X 。 ^ ミルコフスカ、グラジナ;サルウィッキー A. (1987)。アルゴリズム ロジック (PDF) 。ワルシャワとボストン: PWN & D. Reidel Publ. p. 372.ISBN 8301068590 。
参考文献
外部リンク フロイド・ホーア論理に関する意味論的考察（動的論理に関する原著論文） 第 6 章 : ロジックとアクション (Logic In Action サイト) アンドレ・プラッツァーによるダイナミックロジックの講義ノート 
![{\displaystyle {\text{地面は乾いている}}\to [{\text{雨が降る}}]{\text{地面は濡れている}},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de80b1ce7d120cf005841519eb247fe816933c81)
![{\displaystyle [a]p}](https://wikimedia.org/api/rest_v1/media/math/render/svg/10d66303d69dcf8270cb4eef1ecb9a7cef7fee32)
![{\displaystyle \varphi \to [P]\varphi '}](https://wikimedia.org/api/rest_v1/media/math/render/svg/81a2668587746277088662177d1de5ed9d1ca57c)
![{\displaystyle [a]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a1fb5b3d73ccbb07fc5a491131c0322f70356187)
![{\displaystyle [a]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/62ca72b8b7c76d167780fd376152ae5edd1aa688)
![{\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/afbad750e3a6b697376e2c6e6b1408e5d03afdce)
![{\displaystyle \langle a\rangle p\leftrightarrow \neg [a]\neg p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/580ea5b61ba30003e61688b3bbb2da75a0fbe1c4)
![{\displaystyle \vdash [a]p\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2e29082f88fc448e5cd1c39baaf08ac42c55162c)
![{\displaystyle [0]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2243a8da2a7d9c6ac5fd5a27d57a1638e440a72f)
![{\displaystyle [1]p\leftrightarrow p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/05d2121433a49fdebbe6a438b47b610777e28880)
![{\displaystyle [a\cup b]p\leftrightarrow [a]p\land [b]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cec2af744b28f7391c56c7642a3adbcd7700b945)
![{\displaystyle [a\mathbin {;} b]p\leftrightarrow [a][b]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2bf59d82a76d12d6f470e1ba7862205b6adb6fd1)
![{\displaystyle [a*]p\leftrightarrow p\land [a][a*]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dde210e320a21a65135afb9b38cab0c8b981b4c2)
\to [a*]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/596a5affc1e9f43a0389e75c7aea2479d05fd014)
![{\displaystyle [1]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/76fdef3b81c82f740f94bda91755a8ee95bea6f1)
![{\displaystyle p\vdash [a]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1e3d4111e86ea26cccf17376fb9595d1ac982313)
![{\displaystyle p\to [a]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/25333da70b990f4a843fafa918b10a0287fbcbd5)
\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f06f0d0b572bdd220c15a0f12238a08496299518)
![{\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/62d0f1dce56bcad6e2fed130d59b49aec18e728a)
![{\displaystyle b\to [k]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a80357a9742d2223221e74a92ae1f4e1e8ba445e)
![{\displaystyle b\to [k*]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e656caffdc43024ca5be23536741ff4946214517)
![{\displaystyle [k]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d4f9fa4da5dcef257a7a39cb7fc502044c1993d8)
![{\displaystyle (b\to [k]b)\to (b\to [k*]b)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c1e1a37706b4e0882227d6b43de44df679cb1aef)
![{\displaystyle [k*]b\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4f183003713ca95bab7f66b8a8e0d9f39df156ee)
\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bc161d9b9d88878ef16af585a731fb107f67f63b)
![{\displaystyle [x:=e]\ファイ (x)\leftrightarrow \ファイ (e)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4165ffa60cf13e329cf352f0ba2fe6e95822230f)
\leftrightarrow e=y^{2}\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/91cb75040a38f2ab230cbf5208dd8ab16b3df477)
\leftrightarrow b=c+e\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e9158c1b2ecd540ddbdb386bfb33a3c0a1381dfc)
\leftrightarrow x+1\geq 4\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7278650454eea62477c767e7aa4a95f1567680db)
![{\displaystyle [x:=x+1]x\geq 4\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7f65816abeab4b4d94fe1d648e60f32d76fb9d47)
\to [n:=n+1]\Phi (n)))\to [(n :=n+1)*]\ファイ (n)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/387b4dd2f085e5a8f4a98bcd89bca88811a94cf8)
![{\displaystyle [n:=n+1]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/044fb0d8c92e5e7228efb8f16bf07edf10216353)
![{\displaystyle [(n:=n+1)*]\ファイ (n)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/87f13127d75cee89f7e659c3807d4fe801583058)
![{\displaystyle [(n:=n+1)^{0}]\Phi (n)\land [(n:=n+1)^{1}]\Phi (n)\land [(n:= n+1)^{2}]\ファイ (n)\land \ldots \,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/04e959dd47b2fdde55833b0755833bd0deefe611)
![{\displaystyle [(n:=n+1)^{i}]\ファイ (n)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/59da810a92ad42e14b5c4b17a69aa35c93e2cca2)
![{\displaystyle [n:=n+1][n:=n+1]\ldots \Phi (n)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7caacf5aab8e5b04d1f275a84143f124cde2132f)
![{\displaystyle [(n:=n+1)*]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b3e0a9d62923411630e49bdac5651338095541a7)
![{\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to [n:=n+1]\Phi (n+i)))\to \forall i\Phi (n+i)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/64af1426c5434142818e7aea3a0fa53e25aec648)
\leftrightarrow [a*]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8a1257d316eecefc8cb32db6fb0e4aaca34c4f19)
![{\displaystyle [p?]q\leftrightarrow (p\to q)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0d3bd6998d5aacd0db40c16709918c446a6f3d1e)
![{\displaystyle [x\mathbin {:=} {?}]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4915db0b49441ae835afeab4809c7528b0cab8cb)
![{\displaystyle [x\mathbin {:=} {?}]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/498f12aa1cfa7e1ff50f2be7a5bc73e6d5ac4774)
\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7c7fcfa23d464f4776e68d47af0f174364ea6173)
![{\displaystyle p\to [a]q\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8e1788859ff60725bc56a43ac4d5ecc072ea6b4)
