Динамическая логика (модальная логика)

В логике , философии и теоретической информатике динамическая логика является расширением модальной логики, способным кодировать свойства компьютерных программ .

Простой пример утверждения в динамической логике:

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

который гласит, что если сейчас земля сухая и идет дождь, то после этого земля станет мокрой.

Синтаксис динамической логики содержит язык предложений ( например, «земля сухая») и язык действий (например, «идет дождь»). Основными модальными конструкциями являются , который утверждает, что после выполнения действия a должно выполняться предложение p , и , который утверждает, что после выполнения действия a возможно выполнение p . Язык действий поддерживает операции (выполнение одного действия, за которым следует другое), (выполнение одного действия или другого) и итерацию (выполнение одного действия ноль или более раз). Язык предложений поддерживает булевы операции (и, или, и не). Логика действий достаточно выразительна, чтобы кодировать программы. Для произвольной программы , предусловия и постусловия , оператор динамической логики кодирует правильность программы, делая динамическую логику более общей, чем логика Хоара . ${\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 '}$

Помимо использования в формальной проверке программ, динамическая логика применяется для описания сложного поведения, возникающего в лингвистике , философии , искусственном интеллекте и других областях.

Язык

Модальная логика характеризуется модальными операторами (box p), утверждающими, что это обязательно так, и (diamond 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 \,\!}$

Динамическая логика допускает составные действия, составленные из более мелких действий. В то время как для этой цели можно использовать основные операторы управления любого языка программирования, операторы регулярных выражений Клини хорошо подходят для модальной логики. При наличии действий и составное действие выбор , также записываемое как или , выполняется путем выполнения одного из или . Составное действие последовательность , выполняется путем выполнения сначала и затем . Составное действие итерация , выполняется путем выполнения ноль или более раз последовательно. Постоянное действие или 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{*}\,\!}$

Аксиомы

Эти операторы могут быть аксиоматизированы в динамической логике следующим образом, принимая в качестве уже данной подходящую аксиоматизацию модальной логики, включающую такие аксиомы для модальных операторов, как вышеупомянутая аксиома и два правила вывода modus ponens ( и подразумевает ) и необходимость ( подразумевает ). ${\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\,}$

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

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

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

А4. ${\displaystyle [a\mathbin {;} b]p\leftrightarrow [a][b]p\,\!}$

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

А6. ${\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+1 приращения n , обобщенным на произвольные действия . ${\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\,\!}$

Производные

Аксиома модальной логики позволяет вывести следующие шесть теорем, соответствующих вышеизложенным: ${\displaystyle [a]p\leftrightarrow \neg \langle a\rangle \neg p\,\!}$

Т1. ${\displaystyle \neg \langle 0\rangle p\,\!}$

Т2. ${\displaystyle \langle 1\rangle p\leftrightarrow p\,\!}$

Т3. ${\displaystyle \langle a\cup b\rangle p\leftrightarrow \langle a\rangle p\lor \langle b\rangle p\,\!}$

Т4. ${\displaystyle \langle a\mathbin {;} b\rangle p\leftrightarrow \langle a\rangle \langle b\rangle p\,\!}$

Т5. ${\displaystyle \langle a*\rangle p\leftrightarrow p\lor \langle a\rangle \langle a*\rangle p\,\!}$

Т6. ${\displaystyle \langle a*\rangle p\to p\lor \langle a*\rangle (\neg p\land \langle a\rangle p)\,\!}$

T1 утверждает невозможность вызвать что-либо, выполнив BLOCK .
T2 снова отмечает, что NOP ничего не меняет, имея в виду, что NOP является как детерминированным, так и завершающим wherece и имеет одинаковую силу. T3 говорит, что если выбор или может вызвать , то либо или по отдельности может вызвать . T4 точно так же, как A4. T5 объясняется так же, как и для A5. T6 утверждает, что если возможно вызвать , выполняя достаточно часто, то либо истинно сейчас, либо возможно выполнять повторно, чтобы вызвать ситуацию, в которой (все еще) ложно, но еще одно выполнение может вызвать . ${\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\,\!}$

Производные правила вывода

Что касается модальной логики, то правил вывода modus ponens и necessitation достаточно и для динамической логики в качестве единственных примитивных правил, которые ей нужны, как отмечено выше. Однако, как обычно в логике, из них можно вывести гораздо больше правил с помощью аксиом. Примером такого производного правила в динамической логике является то, что если пнуть сломанный телевизор один раз, то его невозможно починить, то и многократное его пинание тоже не может его починить. Записывая действие пнуть телевизор и предложение о том, что телевизор сломан, динамическая логика выражает этот вывод как , имея в качестве предпосылки и в качестве заключения . Значение заключается в том, что гарантированно после пинка телевизора он сломается. Следовательно, предпосылка означает, что если телевизор сломан, то после пинка его один раз он все равно будет сломан. обозначает действие пнуть телевизор ноль или более раз. Следовательно, заключение означает, что если телевизор сломан, то после пинка его ноль или более раз он все равно будет сломан. В противном случае после предпоследнего удара телевизор окажется в состоянии, в котором повторный удар его исправит, а это, согласно посылке, не может произойти ни при каких обстоятельствах. ${\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\,\!}$

Вывод обоснован. Однако импликация недействительна, потому что мы можем легко найти ситуации, в которых выполняется, но не выполняется. В любой такой ситуации контрпримера должно выполняться, но должно быть ложным, в то время как however должно быть истинным. Но это может произойти в любой ситуации, когда телевизор сломан, но его можно оживить двумя ударами. Импликация недействительна (недействительна), потому что она требует выполнения этого условия только сейчас, тогда как вывод успешен (является обоснованным), потому что он требует выполнения этого условия во всех ситуациях, а не только в настоящей. ${\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\,\!}$

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

Это схема в том смысле, что она может быть инстанциирована с помощью любой формулы , содержащей ноль или более экземпляров переменной . Значение заключается в тех вхождениях , которые встречаются свободно в , т.е. не связаны каким-либо квантификатором, как в , замененным на . Например, мы можем инстанцировать 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, откуда это предложение не является теоремой динамической логики. Однако если имеет тип integer, то это предложение истинно тогда и только тогда, когда изначально равно не более 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, в котором предложение инстанциируется как , действие как и как . Первые два из этих трех инстанциаций являются простыми, преобразуя 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)\,\!}$

Одна тонкость, которую мы здесь упустили, заключается в том, что следует понимать как охватывающий натуральные числа, где — верхний индекс в расширении как объединение по всем натуральным числам . Важность сохранения этой типизированной информации становится очевидной, если бы имел тип integer или даже real , для любого из которых A6 совершенно допустима как аксиома. В качестве примера, если — вещественная переменная и — предикат — натуральное число , то аксиома A6 после первых двух подстановок, то есть , так же допустима, то есть истинна в любом состоянии независимо от значения в этом состоянии, как и когда имеет тип natural number . Если в данном состоянии — натуральное число, то антецедент основного следствия 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?\,\!}$

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

Соответствующая теорема для имеет вид: ${\displaystyle \langle p?\rangle \,\!}$

Т8. ${\displaystyle \langle p?\rangle q\leftrightarrow p\land q\,\!}$

Конструкция if p then a else b реализуется в динамической логике как . Это действие выражает защищенный выбор: if hold then эквивалентно , тогда как эквивалентно 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 реализуется как . Она выполняется ноль или более раз, а затем выполняется . Пока остается истинным, в конце блокирует исполнителя от преждевременного завершения итерации, но как только становится ложным, дальнейшие итерации тела блокируются, и у исполнителя не остается иного выбора, кроме как выйти через тест . ${\displaystyle ({p?\mathbin {;} a)*}\mathbin {;} \neg p?\,\!}$ ${\displaystyle p?\mathbin {;} a\,\!}$ ${\displaystyle \neg p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle \neg p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle \neg p?\,\!}$

Количественная оценка как случайное распределение

Оператор случайного назначения обозначает недетерминированное действие установки произвольного значения. then говорит, что выполняется независимо от того, что вы устанавливаете , в то время как говорит, что возможно установить значение, которое делает истинным. таким образом, имеет то же значение, что и квантор всеобщности , в то время как аналогично соответствует квантору существования . То есть, логику первого порядка можно понимать как динамическую логику программ вида . ${\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){*}}$

Семантика возможного мира

Модальная логика чаще всего интерпретируется в терминах семантики возможных миров или структур Крипке. Эта семантика естественным образом переносится в динамическую логику, интерпретируя миры как состояния компьютера в приложении к проверке программ или состояния нашей среды в приложениях к лингвистике, ИИ и т. д. Одна из ролей семантики возможных миров заключается в формализации интуитивных понятий истины и действительности, которые, в свою очередь, позволяют определить понятия обоснованности и полноты для систем аксиом. Правило вывода обосновано, когда обоснованность его предпосылок подразумевает обоснованность его заключения. Система аксиом обоснована, когда все ее аксиомы обоснованы и ее правила вывода обоснованы. Система аксиом завершена, когда каждая допустимая формула выводится как теорема этой системы. Эти понятия применимы ко всем системам логики, включая динамическую логику.

Пропозициональная динамическая логика (PDL)

Обычная или первопорядковая логика имеет два типа терминов, соответственно утверждения и данные. Как видно из приведенных выше примеров, динамическая логика добавляет третий тип термина, обозначающего действия. Утверждение динамической логики содержит все три типа: , , и являются данными, является действием и и являются утверждениями. Пропозициональная логика выводится из первопорядковой логики путем опускания терминов данных и рассуждает только об абстрактных предложениях, которые могут быть простыми пропозициональными переменными или атомами или составными предложениями, построенными с помощью таких логических связок, как и , или , и не . ${\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 году Майклом Дж. Фишером и Ричардом Ладнером . PDL смешивает идеи, лежащие в основе пропозициональной логики и динамической логики, добавляя действия и опуская данные; следовательно, терминами PDL являются действия и предложения. Приведенный выше пример TV выражен в PDL, тогда как следующий пример, включающий динамическую логику первого порядка. PDL относится к динамической логике (первого порядка), как пропозициональная логика относится к логике первого порядка. ${\displaystyle x:=x+1\,\!}$

Фишер и Ладнер показали в своей статье 1977 года, что выполнимость PDL имеет вычислительную сложность в лучшем случае недетерминированное экспоненциальное время и, по крайней мере, детерминированное экспоненциальное время в худшем случае. Этот пробел был закрыт в 1978 году Воаном Праттом , который показал, что PDL разрешима за детерминированное экспоненциальное время. В 1977 году Кристер Сегерберг предложил полную аксиоматизацию PDL, а именно любую полную аксиоматизацию модальной логики K вместе с аксиомами A1–A6, как указано выше. Доказательства полноты для аксиом Сегерберга были найдены Габбеем (неопубликованная заметка), Парихом (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 года , другой вариант модальной логики, разделяющий много общих черт с динамической логикой, отличается от всех вышеупомянутых логик тем, что является тем, что Пнуэли охарактеризовал как «эндогенную» логику, другие являются «экзогенными» логиками. Под этим Пнуэли подразумевал, что утверждения темпоральной логики интерпретируются в рамках универсальной поведенческой структуры, в которой одна глобальная ситуация изменяется с течением времени, тогда как утверждения других логик делаются внешне по отношению к множественным действиям, о которых они говорят. Преимущество эндогенного подхода заключается в том, что он не делает фундаментальных предположений о том, что вызывает что, поскольку окружающая среда изменяется с течением времени. Вместо этого временная логическая формула может говорить о двух несвязанных частях системы, которые, поскольку они не связаны, молчаливо развиваются параллельно. По сути, обычное логическое соединение временных утверждений является параллельным оператором композиции временной логики. Простота этого подхода к параллелизму привела к тому, что временная логика стала модальной логикой выбора для рассуждений о параллельных системах с ее аспектами синхронизации, помех, независимости, тупика , динамической блокировки , справедливости и т. д.

Смотрите также

• Логика Хоара
• алгебра Клини
• Временная логика
• Временная логика в конечно-уровневой верификации
• Временная логика действий
• Модальное μ-исчисление

Дальнейшее чтение

• Дэвид Харел , Декстер Козен и Ежи Тюрин, «Динамическая логика». MIT Press, 2000 (450 стр.).

• Николя Трокар и Филипп Бальбиани, «Пропозициональная динамическая логика». Стэнфордская энциклопедия философии , 2007.

Сноски

1. Дейкстра, Э. У. (1976). Дисциплина программирования. Englewood Cliffs: Prentice-Hall Inc. стр. 221. ISBN 013215871X.
2. Мирковская, Гражина; Салвицкий А. (1987). Алгоритмическая логика (PDF) . Варшава и Бостон: PWN & D. Reidel Publ. п. 372. ИСБН 8301068590.

Ссылки

• Воан Пратт , «Семантические соображения о логике Флойда-Хоара», Труды 17-го ежегодного симпозиума IEEE по основам компьютерной науки , 1976, 109-121.
• Дэвид Харел , «Динамическая логика», в книге Д. Габбея и Ф. Гюнтнера, редакторов, Справочник по философской логике, том II: Расширения классической логики, глава 10, страницы 497-604. Рейдель, Дордрехт, 1984.
• Дэвид Харел , Декстер Козен и Ежи Тюрин, «Динамическая логика», в книге Д. Габбея и Ф. Гюнтнера, редакторов, Справочник по философской логике, том 4: страницы 99-217. Kluwer, 2-е издание, 2002.

Внешние ссылки

• Семантические соображения о логике Флойда-Хоара (оригинальная статья по динамической логике)
• Глава 6: Логика и действие на сайте Logic In Action
• Конспект лекций по динамической логике Андре Платцера