動的論理（様相論理）

Extension of modal logic

論理学、哲学、理論コンピュータサイエンスにおいて、動的論理はコンピュータプログラムの特性をエンコードできる様相論理の拡張です。

動的論理におけるステートメントの簡単な例は次の通りである。

${\displaystyle {\text{The ground is dry}}\to [{\text{It rains}}]{\text{The ground is wet}},}$

これは、地面が現在乾燥していて雨が降った場合、その後地面は濡れていることを示しています。

動的論理の構文には、命題の言語（「地面は乾いている」など）とアクションの言語（「雨が降る」など）が含まれます。 中核となる様相構造は、アクションaを実行した後、命題pが成り立つはずであると述べる と、アクションaを実行した後、命題pが成り立つ可能性があると述べる です。アクション言語は、演算（あるアクションの後に別のアクションを実行する）、（いずれかのアクションを実行する）、および反復（1 つのアクションを 0 回以上実行する）をサポートします。命題言語はブール演算（and、or、not）をサポートします。アクション ロジックは、プログラムをエンコードするのに十分な表現力を持っています。任意のプログラム、前提条件、および事後条件に対して、動的論理ステートメントはプログラムの正しさをエンコードするため、動的論理はホーア論理よりも汎用的です。 ${\displaystyle [a]p}$ ${\displaystyle \langle a\rangle p}$ ${\displaystyle a\mathbin {;} b}$ ${\displaystyle a\cup b}$ ${\displaystyle a{*}}$ ${\displaystyle P}$ ${\displaystyle \varphi }$ ${\displaystyle \varphi '}$ ${\displaystyle \varphi \to [P]\varphi '}$

動的論理は、プログラムの形式検証での使用以外にも、言語学、哲学、AI、その他の分野で生じる複雑な動作を記述するために適用されてきました。

言語

様相論理は、必然的に が成り立つと主張する様相演算子 (ボックス p)と、おそらく が成り立つと主張する (ダイヤモンド p)ことによって特徴付けられます。動的論理は、あらゆる動作に様相演算子およびを関連付けることでこれを拡張し、それによって多様相論理にします。 の意味は、動作を実行した後、必然的に が成り立つ、つまり をもたらす必要があるということです。 の意味は、 を実行した後、が成り立つ可能性がある、つまり をもたらす可能性があるということです。これらの演算子は互いに双対であり、つまり、全称 ( ) 量指定子と存在 ( ) 量指定子の関係と同様に、および によって関連付けられています。 ${\displaystyle \Box p}$ ${\displaystyle p\,\!}$ ${\displaystyle \Diamond p}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle [a]\,\!}$ ${\displaystyle \langle a\rangle \,\!}$ ${\displaystyle [a]p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle \langle a\rangle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}$ ${\displaystyle \langle a\rangle p\leftrightarrow \neg [a]\neg p\,\!}$ ${\displaystyle \forall \,\!}$ ${\displaystyle \exists \,\!}$

動的ロジックでは、小さなアクションを積み重ねて複合アクションを作成できます。任意のプログラミング言語の基本的な制御演算子をこの目的に使用できますが、クリーネの正規表現演算子は様相ロジックに適しています。アクション および が与えられた場合、複合アクションchoice (または とも表記) は、またはのいずれかを実行することによって実行されます。複合アクションsequenceは、最初に を実行し、次にを実行することによって実行されます。複合アクションiterationは、 を 0 回以上、順番に実行することによって実行されます。定数アクションBLOCKは何も実行せず、終了しませんが、定数アクションSKIPまたはNOP はとして定義でき、何も実行しませんが、終了します。 ${\displaystyle a\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle a\cup b\,\!}$ ${\displaystyle a+b\,\!}$ ${\displaystyle a|b\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle a{\mathbin {;}}b\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle a{*}\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle 0\,\!}$ ${\displaystyle 1\,\!}$ ${\displaystyle 0{*}\,\!}$

公理

これらの演算子は、前述の公理や、可能性（および を意味する）と必然性（を意味する）という2 つの推論規則などの様相演算子の公理を含む様相論理の適切な公理化をすでに与えているものとして、次のように動的論理で公理化できます。 ${\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}$ ${\displaystyle \vdash p}$ ${\displaystyle \vdash p\to q}$ ${\displaystyle \vdash q\,}$ ${\displaystyle \vdash p}$ ${\displaystyle \vdash [a]p\,}$

A1. ${\displaystyle [0]p\,\!}$

A2. ${\displaystyle [1]p\leftrightarrow p\,\!}$

A3. ${\displaystyle [a\cup b]p\leftrightarrow [a]p\land [b]p\,\!}$

A4です。 ${\displaystyle [a\mathbin {;} b]p\leftrightarrow [a][b]p\,\!}$

A5. ${\displaystyle [a*]p\leftrightarrow p\land [a][a*]p\,\!}$

A6. ${\displaystyle p\land [a*](p\to [a]p)\to [a*]p\,\!}$

公理 A1 は、 BLOCK が終了したときに、命題 が偽 であっても が成り立つという空約束をします。 (したがって、BLOCK は地獄が凍りつくという動作の本質を抽象化します。) A2 は、NOP が命題に対して恒等関数として働く、つまりそれ自体に変化する、と述べています。A3は、またはの 1 つを行うとが必ず生じる場合、 が必ず生じ、についても同様に起こり、その逆も同様であるとしています。A4は、および を行うと が必ず生じる場合、 が必ず生じる状況が生じなければならない、が必ず生じる、と述べています。A5は、A2、A3、および A4 をクリーネ代数の方程式に適用した明らかな結果です。A6は、現在が成り立ち、また、何度実行しても、の真実性がを 1 回実行した後もその真実性を必然的に伴うという事実が変わらない場合、を何度実行しても真実であり続ける、と主張しています。A6 は、 nを増分する動作n := n+1を任意の動作 に一般化した数学的帰納法として認識できます。 ${\displaystyle p\,\!}$ ${\displaystyle p\,\!}$
${\displaystyle p\,\!}$
${\displaystyle a\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle b\,\!}$
${\displaystyle a\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle p\,\!}$
${\displaystyle a{*}=1\cup a{\mathbin {;}}a{*}\,\!}$
${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle a\,\!}$

派生

様相論理公理により、上記に対応する次の 6 つの定理を導出できます。 ${\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}$

T1。 ${\displaystyle \neg \langle 0\rangle p\,\!}$

T2。 ${\displaystyle \langle 1\rangle p\leftrightarrow p\,\!}$

T3。 ${\displaystyle \langle a\cup b\rangle p\leftrightarrow \langle a\rangle p\lor \langle b\rangle p\,\!}$

T4。 ${\displaystyle \langle a\mathbin {;} b\rangle p\leftrightarrow \langle a\rangle \langle b\rangle p\,\!}$

T5。 ${\displaystyle \langle a*\rangle p\leftrightarrow p\lor \langle a\rangle \langle a*\rangle p\,\!}$

T6。 ${\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 回実行すると をもたらす可能性があると主張しています。 ${\displaystyle [1]\,\!}$ ${\displaystyle \langle 1\rangle \,\!}$
${\displaystyle a\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle p\,\!}$


${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$

箱とひし形は、どちらを原始的なものとするかに関して完全に対称である。別の公理化としては、定理T1～T6を公理とし、そこから定理A1～A6を導出することもできただろう。

含意と推論の違いは、動的論理においても他の論理と同様です。含意は、が真であれば も であると主張しますが、推論は、が有効であれば も であると主張します。しかし、動的論理の動的な性質により、この区別は抽象的な公理の領域から、変化する状況における常識的な経験へと移されます。たとえば、推論規則 は、その前提が が常に成り立つと主張しているため、 が私たちをどこに導くとしても、そこで が真となるため、妥当です。ただし、含意は有効ではありません。なぜなら、現時点で が真実だからといって、を実行した後も が真実であるという保証はないからです。たとえば、 は、が偽であるどのような状況でも、または が真であるどのような状況でも真になりますが、 の値が 1であるどのような状況でも主張は偽であるため、 は有効ではありません。 ${\displaystyle p\to q\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle q\,\!}$ ${\displaystyle p\vdash q\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle q\,\!}$ ${\displaystyle p\vdash [a]p\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle p\to [a]p\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\to [a]p\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle [a]p\,\!}$ ${\displaystyle (x=1)\to [x:=x+1](x=1)\,\!}$ ${\displaystyle x\,\!}$

推論の導出規則

様相論理に関しては、前述のように、動的論理にとっても推論規則の様相と必然性は必要な唯一の基本規則として十分です。しかし、論理学ではよくあるように、公理の助けを借りて、これらからさらに多くの規則を導出できます。動的論理におけるそのような導出規則の例としては、壊れたテレビを一度蹴っても直らないのであれば、繰り返し蹴っても直らない可能性がある、というものがあります。テレビを蹴るという動作と、テレビが壊れているという命題について書くと、動的論理ではこの推論を と表現し、前提 を、結論 を持ちます。 の意味は、テレビを蹴った後、テレビが壊れていることが保証されているということです。したがって前提は、テレビが壊れている場合は、一度蹴った後もまだ壊れていることを意味します。は、テレビを 0 回以上蹴る動作を表します。したがって結論は、テレビが壊れている場合は、 0 回以上蹴った後もまだ壊れていることを意味します。そうでない場合、最後から2番目の蹴りの後、テレビはもう一度蹴れば直る状態になりますが、これはいかなる状況でも決して起こり得ないことを前提としています。 ${\displaystyle k\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}$ ${\displaystyle b\to [k]b\,\!}$ ${\displaystyle b\to [k*]b\,\!}$ ${\displaystyle [k]b\,\!}$ ${\displaystyle b\to [k]b\,\!}$ ${\displaystyle k{*}\,\!}$ ${\displaystyle b\to [k*]b\,\!}$

推論は正しい。しかし、含意は妥当ではない。なぜなら、成立するが成立しない状況は容易に見つけられるからだ。このような反例の状況では、必ず成立するが偽である必要があり、しかしながら真である必要がある。しかし、これはテレビが壊れているが二回蹴れば復活できるような状況であればどこでも起こり得る。含意は、その成立を今のみ必要とするため失敗（妥当ではない）する。一方、推論は、その成立を今の状況だけでなくあらゆる状況で必要とするため成功（妥当）する。 ${\displaystyle b\to [k]b\vdash b\to [k*]b\,\!}$ ${\displaystyle (b\to [k]b)\to (b\to [k*]b)\,\!}$ ${\displaystyle b\to [k]b\,\!}$ ${\displaystyle b\to [k*]b\,\!}$ ${\displaystyle b\,\!}$ ${\displaystyle [k*]b\,\!}$ ${\displaystyle [k]b\,\!}$ ${\displaystyle b\to [k]b\,\!}$ ${\displaystyle b\to [k]b\,\!}$

有効な含意の例としては、命題 が挙げられます。これは、が 3 以上の場合、 を増分した後、は 4 以上になる必要がある、というものです。 のように、必ず終了することが保証されている決定論的なアクションの場合、と は同じ効力を持つ可能性があり、つまり、と は同じ意味を持つ可能性があります。したがって、上記の命題は、 が 3 以上の場合、 を実行した後、は 4 以上になる可能性がある、という主張と同等です。 ${\displaystyle (x\geq 3)\to [x:=x+1](x\geq 4)\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle x:=x+1\,\!}$ ${\displaystyle [a]\,\!}$ ${\displaystyle \langle a\rangle \,\!}$ ${\displaystyle (x\geq 3)\to \langle x:=x+1\rangle (x\geq 4)\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x:=x+1\,\!}$ ${\displaystyle x\,\!}$

割り当て

代入文の一般的な形式は、 です。ここでは変数であり、は定数と変数から構築された式であり、言語で提供される加算や乗算などの演算が用いられます。代入に関するホーア公理は、単一の公理としてではなく、公理スキームとして与えられます。 ${\displaystyle x:=e\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle e\,\!}$

A7. ${\displaystyle [x:=e]\Phi (x)\leftrightarrow \Phi (e)\,\!}$

これは、変数 のインスタンスを 0 個以上含む任意の式でインスタンス化できるという意味で、スキーマです。 の意味は、内で自由に出現する （つまり、 のように何らかの量指定子に束縛されていない ） を に置き換えたものです。例えば、A7 を、 、または でインスタンス化できます。このような公理スキーマにより、共通の形式を持つ無限個の公理を、その形式を包含する有限式として記述することができます。 ${\displaystyle \Phi (x)\,\!}$ ${\displaystyle \Phi \,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle \Phi (e)\,\!}$ ${\displaystyle \Phi \,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle \Phi \,\!}$ ${\displaystyle \forall x\,\!}$ ${\displaystyle e\,\!}$ ${\displaystyle [x:=e](x=y^{2})\leftrightarrow e=y^{2}\,\!}$ ${\displaystyle [x:=e](b=c+x)\leftrightarrow b=c+e\,\!}$

A7 のインスタンスにより、数段落前に遭遇した例が と同等であることが機械的に計算でき、これは初等代数によりと同等になります。 ${\displaystyle [x:=x+1](x\geq 4)\leftrightarrow x+1\geq 4\,\!}$ ${\displaystyle [x:=x+1]x\geq 4\,\!}$ ${\displaystyle x+1\geq 4\,\!}$ ${\displaystyle x\geq 3\,\!}$

との組み合わせによる代入の例は、命題 です。これは、十分な頻度で増分することで を 7 に等しくすることが可能であることを主張しています。もちろん、これは常に真であるとは限りません。例えば、 が最初から 8 であったり、 6.5 であったりする場合は、この命題は動的論理の定理ではありません。しかし、 が整数型の場合、この命題が真となるのは、 が最初から最大で 7 である場合のみです。つまり、これは を遠回しに表現しただけです。 ${\displaystyle *\,\!}$ ${\displaystyle \langle (x:=x+1)*\rangle x=7\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\leq 7\,\!}$

数学的帰納法は、命題を、動作を、そしてとして具体化したA6 のインスタンスとして得られる。これらの3つの具体化のうち最初の2つは単純で、A6 を に変換する。しかし、を に置き換えるという一見単純な置換は、様相が置換に干渉する場合に様相論理のいわゆる指示的不透明性を露呈させるため、それほど単純ではない。 ${\displaystyle p\,\!}$ ${\displaystyle \Phi (n)\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle n:=n+1\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle 0\,\!}$ ${\displaystyle (\Phi (n)\land [(n:=n+1)*](\Phi (n)\to [n:=n+1]\Phi (n)))\to [(n:=n+1)*]\Phi (n)\,\!}$ ${\displaystyle 0\,\!}$ ${\displaystyle n\,\!}$

を に代入したとき、命題記号 を様相 に関して厳密な指示子として考えていました。つまり、 を増分しても命題は以前と同じままですが、増分によってその真理値が変化する可能性があります。同様に、 を増分しても動作は変わりませんが、増分によって異なる環境で実行されます。しかし、自体は様相 に関して厳密な指示子ではありません。 を増分する前は 3 を示していましたが、増分後は 4 を示します。したがって、A6 のどこでも をに代入することはできません。 ${\displaystyle \Phi (n)\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle [n:=n+1]\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle [n:=n+1]\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle 0\,\!}$ ${\displaystyle n\,\!}$

様相の不透明性に対処する方法の一つは、それらを除去することです。そのためには、無限連言、つまり 全体にわたる連言として展開します。ここで A4 を適用してを に変換し、様相を持ちます。次に、これにホーアの公理 を回適用して を生成し、この無限連言を に簡約します。この簡約全体をA6の の両方のインスタンスに適用して を生成します。残りの様相は、ホーアの公理をもう一度使用して を除去することで実現できます。 ${\displaystyle [(n:=n+1)*]\Phi (n)\,\!}$ ${\displaystyle [(n:=n+1)^{0}]\Phi (n)\land [(n:=n+1)^{1}]\Phi (n)\land [(n:=n+1)^{2}]\Phi (n)\land \ldots \,\!}$ ${\displaystyle i\,\!}$ ${\displaystyle [(n:=n+1)^{i}]\Phi (n)\,\!}$ ${\displaystyle [(n:=n+1)^{i}]\Phi (n)\,\!}$ ${\displaystyle [n:=n+1][n:=n+1]\ldots \Phi (n)\,\!}$ ${\displaystyle i\,\!}$ ${\displaystyle i\,\!}$ ${\displaystyle \Phi (n+i)\,\!}$ ${\displaystyle \forall i\Phi (n+i)\,\!}$ ${\displaystyle [(n:=n+1)*]\,\!}$ ${\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to [n:=n+1]\Phi (n+i)))\to \forall i\Phi (n+i)\,\!}$ ${\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}$

不透明な様相がなくなったので、通常の第一階論理のやり方でを安全に置き換えて、ペアノの有名な公理、つまり数学的帰納法を得ることができます。 ${\displaystyle 0\,\!}$ ${\displaystyle n\,\!}$ ${\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 の前提がどこかで誤っている場合は、結論も必ず誤りであることが分かります。 ${\displaystyle \forall i\,\!}$ ${\displaystyle i\,\!}$ ${\displaystyle a{*}\,\!}$ ${\displaystyle a^{i}\,\!}$ ${\displaystyle i\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle \Phi (n)\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle (\Phi (n)\land \forall i(\Phi (n+i)\to \Phi (n+i+1)))\to \forall i\Phi (n+i)\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle n+i\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle p\land [a*](p\to [a]p)\leftrightarrow [a*]p\,\!}$

テスト

動的論理は、すべての命題にテストと呼ばれる動作を関連付けます。が成立する場合、テストはNOPとして動作し、何も変更せずに動作を続行します。が偽の場合、BLOCKとして動作します。テストは以下のように公理化できます。 ${\displaystyle p\,\!}$ ${\displaystyle p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle p?\,\!}$

A8. ${\displaystyle [p?]q\leftrightarrow (p\to q)\,\!}$

に対応する定理は次のとおりです。 ${\displaystyle \langle p?\rangle \,\!}$

T8。 ${\displaystyle \langle p?\rangle q\leftrightarrow p\land q\,\!}$

動的論理では、if p then a else bという構文はとして実現されます。このアクションは保護された選択を表します。が成立する場合、 はと同等であり、は BLOCK と同等であり、 は と同等です。したがって、が真の場合はアクションの実行者は左の分岐のみを、 が偽の場合は右の分岐のみを取ることができます。 ${\displaystyle (p?\mathbin {;} a)\cup (\neg p?\mathbin {;} b)\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle p?\mathbin {;} a\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle \neg p?\mathbin {;} b\,\!}$ ${\displaystyle a\cup 0\,\!}$ ${\displaystyle a\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle p\,\!}$

while p do a という構文は として実現されます。これは を0回以上実行した後、 を実行します。 が真である限り、最後の は実行者が反復処理を途中で終了するのを阻止しますが、 が偽になると、本体の以降の反復処理は阻止され、実行者はテスト を介して終了するしかなくなります。 ${\displaystyle ({p?\mathbin {;} a)*}\mathbin {;} \neg p?\,\!}$ ${\displaystyle p?\mathbin {;} a\,\!}$ ${\displaystyle \neg p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle \neg p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle \neg p?\,\!}$

ランダム割り当てとしての定量化

ランダム代入文は、任意の値を設定するという非決定的な動作を表します。は、 に何を設定するかに関係なく が成り立つことを表します。一方、 は、 trueとなる値を設定することが可能であることを表します。したがって、 は全称量指定子 と同じ意味を持ち、同様に は存在量指定子 に対応します。つまり、一階述語論理は、 という形式のプログラムの動的論理として理解できます。 ${\displaystyle x\mathbin {:=} {?}\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle [x\mathbin {:=} {?}]p\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle \langle x\mathbin {:=} {?}\rangle p\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle [x\mathbin {:=} {?}]\,\!}$ ${\displaystyle \forall x\,\!}$ ${\displaystyle \langle x\mathbin {:=} {?}\rangle \,\!}$ ${\displaystyle \exists x\,\!}$ ${\displaystyle x:=?\,\!}$

ダイクストラは、変数の値を任意の正の整数に設定するプログラムの不可能性を示したと主張した。^[1]しかし、代入と*演算子を用いた動的論理では、動的論理プログラムによって変数を任意の正の整数に設定することができる。したがって、ダイクストラの主張を却下するか、*演算子は有効ではないと判断する必要がある。 ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle (x\mathbin {:=} 0)\mathbin {;} (x:=x+1){*}}$

可能世界意味論

様相論理は、可能世界意味論またはクリプキ構造の観点から解釈されるのが最も一般的です。この意味論は、プログラム検証への応用においては世界をコンピュータの状態として、言語学やAIなどへの応用においては環境の状態として解釈することで、動的論理に自然に引き継がれます。可能世界意味論の役割の一つは、真理と妥当性という直感的な概念を形式化し、それによって公理系における健全性と完全性の概念を定義できるようにすることです。推論規則は、前提の妥当性が結論の妥当性を意味する場合、健全です。公理系は、そのすべての公理が有効であり、かつ推論規則が健全である場合、健全です。公理系は、すべての有効な式がその系の定理として導出可能である場合、完全です。これらの概念は、動的論理を含む すべての論理系に当てはまります。

命題動的論理（PDL）

通常論理、すなわち一階論理には、アサーションとデータという2種類の用語があります。上記の例からわかるように、動的論理では、アクションを表す3つ目の用語が追加されます。動的論理のアサーションには、これら3種類すべてが含まれます。、、はデータ、はアクション、およびはアサーションです。命題論理は、一階論理からデータ項を省略し、単純な命題変数、またはアトム、あるいはand、or、notなどの論理接続詞で構成された複合命題など、抽象的な命題についてのみ推論することで派生します。 ${\displaystyle [x:=x+1](x\geq 4)\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x+1\,\!}$ ${\displaystyle 4\,\!}$ ${\displaystyle x:=x+1\,\!}$ ${\displaystyle x\geq 4\,\!}$ ${\displaystyle [x:=x+1](x\geq 4)\,\!}$

命題動的論理（PDL）は、1977年にマイケル・J・フィッシャーとリチャード・ラドナーによって動的論理から派生しました。PDLは、データを省略しアクションを追加することで、命題論理と動的論理の背後にある考え方を融合させています。したがって、PDLの用語はアクションと命題です。上記のTVの例はPDLで表現されていますが、次の例は一階動的論理で表現されています。PDLと（一階）動的論理の関係は、命題論理と一階論理の関係と同じです。 ${\displaystyle x:=x+1\,\!}$

フィッシャーとラドナーは1977年の論文で、PDLの充足可能性は計算量が最大でも非決定性指数時間、最悪の場合でも少なくとも決定性指数時間であることを示した。このギャップは1978年にヴォーン・プラットによって埋められ、プラットはPDLが決定性指数時間で決定可能であることを示した。1977年、クリスター・ゼーゲルバーグはPDLの完全な公理化、すなわち上記に示した公理A1～A6を伴う様相論理Kの任意の完全な公理化を提案した。ゼーゲルバーグの公理の完全性証明は、ガベイ（未発表メモ）、パリク（1978年）、プラット（1979年）、コーゼンとパリク（1981年）によってなされた。

歴史

動的論理は、1974 年にプログラム検証の授業のノートの中で、ホーア論理に意味を割り当てる方法として、ヴォーン プラットによって開発されました。これは、ホーア論理の公式を と表現することによって行われました。このアプローチは、後に 1976 年にそれ自体の論理システムとして発表されました。このシステムは、アンドレイ サルウィッキのアルゴリズム論理システム^[2] やエドガー ダイクストラの最弱前提条件述語変換器 の概念に類似しており、 はダイクストラの最弱自由前提条件 に対応しています。ただし、これらの論理は、様相論理、クリプキ意味論、正規表現、または二項関係の計算とは関係がありません。したがって、動的論理は、アルゴリズム論理と述語変換器を、様相論理の公理とクリプキ意味論、および二項関係と正規表現の計算に結び付けた改良版と見なすことができます。 ${\displaystyle p\{a\}q\,\!}$ ${\displaystyle p\to [a]q\,\!}$ ${\displaystyle \operatorname {wp} (a,p)\,\!}$ ${\displaystyle [a]p\,\!}$ ${\displaystyle \operatorname {wlp} (a,p)\,\!}$

同時実行の課題

ホーア論理、アルゴリズミック論理、最弱前提条件、そして動的論理は、いずれも逐次的行動に関する議論や推論に適しています。しかしながら、これらの論理を並行行動に拡張することは困難であることが判明しています。様々なアプローチがありますが、いずれも逐次的行動の場合のような簡潔さを欠いています。対照的に、アミール・プヌエリの1977年の時相論理体系は、動的論理と多くの共通点を持つ様相論理の別の変種であり、プヌエリが「内生的」論理と特徴づけた点において、上記のすべての論理とは異なります。他の論理は「外生的」論理です。プヌエリがここで意味したのは、時相論理の主張は、単一の全体的状況が時間の経過と共に変化するという普遍的な行動枠組みの中で解釈されるのに対し、他の論理の主張は、それらが論じる複数の行動の外部でなされるということです。内生的アプローチの利点は、環境が時間と共に変化する際に、何が何を引き起こすのかという根本的な仮定を置かないことです。代わりに、時相論理式はシステム内の無関係な2つの部分について論じることができます。これらの部分は無関係であるため、暗黙のうちに並行して進化します。実際、時相アサーションの通常の論理積は、時相論理の並行合成演算子です。この並行性へのアプローチの単純さから、時相論理は、同期、干渉、独立性、デッドロック、ライブロック、公平性などの側面を持つ並行システムの推論において、様相論理として最適に選ばれています。

参照

• ホーア論理
• クリーネ代数
• 時相論理
• 有限状態検証における時相論理
• 行動の時間的論理
• 様相μ計算

さらに読む

• デイヴィッド・ハレル、デクスター・コーゼン、イェジー・ティウリン、「ダイナミック・ロジック」、MITプレス、2000年（450ページ）。

• ニコラ・トロカードとフィリップ・バルビアーニ、「命題動的論理」スタンフォード哲学百科事典、2007年。

脚注

1. ダイクストラ, EW (1976). 『プログラミングの規律』 エングルウッド・クリフス: プレンティス・ホール社. pp. 221. ISBN 013215871X。
2. ミルコフスカ、グラジナ;サルウィッキー A. (1987)。アルゴリズム ロジック(PDF)。ワルシャワとボストン: PWN & D. Reidel Publ. p. 372.ISBN​ 8301068590。

参考文献

• Vaughan Pratt、「Floyd-Hoare 論理に関する意味論的考察」、第 17 回 IEEEコンピュータ サイエンスの基礎に関するシンポジウム論文集、1976 年、109-121 ページ。
• デイヴィッド・ハレル「動的論理」、D. ギャベイとF. ゲントナー編『哲学論理ハンドブック』第2巻：古典論理の拡張、第10章、497-604ページ。ライデル社、ドルドレヒト、1984年。
• David Harel、Dexter Kozen、Jerzy Tiuryn、「Dynamic Logic」、D. GabbayとF. Guenthner編『Handbook of Philosophical Logic』第4巻、99-217ページ。Kluwer、第2版、2002年。

外部リンク

• フロイド・ホーア論理に関する意味論的考察（動的論理に関する原著論文）
• 第6章 ロジックとアクション（Logic In Actionサイト）
• アンドレ・プラッツァーによる動的論理に関する講義ノート

Retrieved from "https://en.wikipedia.org/w/index.php?title=Dynamic_logic_(modal_logic)&oldid=1322459605"