Динамическая логика (модальная логика)
В логике , философии и информатике теоретической динамическая логика является расширением модальной логики, способной кодировать свойства компьютерных программ .
Простой пример утверждения в динамической логике:
![{\displaystyle {\text{Земля сухая}}\to [{\text{Идет дождь}}] {\text{Земля мокрая}},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de80b1ce7d120cf005841519eb247fe816933c81)
в котором говорится, что если земля сейчас сухая и идет дождь, то потом земля будет влажной.
Синтаксис динамической логики содержит язык предложений (например, «земля сухая») и язык действий (например, «идет дождь»). Основными модальными конструкциями являются , в котором говорится, что после выполнения действия a предложение p должно выполняться, и , в котором говорится, что после выполнения действия a возможно выполнение p .Язык действий поддерживает операции (выполнение одного действия, за которым следует другое), (выполнение того или иного действия) и итерация (выполнение одного действия ноль или более раз). Язык предложений поддерживает логические операции (и, или, и нет). Логика действий достаточно выразительна для кодирования программ. Для произвольной программы , предварительное условие , и постусловие , оператор динамической логики кодирует корректность программы, делая динамическую логику более общей, чем логика Хоара .
![{\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)
Помимо использования в формальной верификации программ, динамическая логика применяется для описания сложного поведения, возникающего в лингвистике , философии , искусственном интеллекте и других областях.
Язык [ править ]
Модальная логика характеризуется модальными операторами (блок p), утверждая, что это обязательно так, и (ромб p), утверждая, что возможно, это так. Динамическая логика расширяет это, связывая с каждым действием модальные операторы и , тем самым делая его мультимодальной логикой . Значение заключается в том, что после совершения действия это обязательно так, что держится, то есть должен вызвать . Значение это после выступления возможно, что держится, то есть может вызвать . Эти операторы двойственны друг другу, что означает, что они связаны соотношением и , аналогично отношению между универсальными ( ) и экзистенциальный ( ) кванторы.
![{\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)
Динамическая логика позволяет выполнять сложные действия, состоящие из более мелких действий. Хотя для этой цели можно использовать базовые управляющие операторы любого языка программирования, Клини операторы регулярных выражений хорошо подходят для модальной логики. Данные действия и , сложное действие , выбор , также написано или , выполняется путем выполнения одного из или . Комплексное действие , последовательность , выполняется путем выполнения сначала а потом . Комплексное действие , итерация , выполняется путем выполнения ноль или более раз последовательно. Постоянное действие или BLOCK ничего не делает и не завершается, тогда как постоянное действие или SKIP или NOP , определяемые как , ничего не делает, но завершает работу.
Аксиомы [ править ]
Эти операторы могут быть аксиоматизированы в динамической логике следующим образом, принимая за уже заданную подходящую аксиоматизацию модальной логики , включая такие аксиомы для модальных операторов, как вышеупомянутая аксиома и два правила вывода modus ponens ( и подразумевает ) и необходимость ( подразумевает ).
![{\displaystyle \vdash [a]p\,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2e29082f88fc448e5cd1c39baaf08ac42c55162c)
А1.
![{\displaystyle [0]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2243a8da2a7d9c6ac5fd5a27d57a1638e440a72f)
А2.
![{\displaystyle [1]p\leftrightarrow p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/05d2121433a49fdebbe6a438b47b610777e28880)
А3.
![{\displaystyle [a\cup b]p\leftrightarrow [a]p\land [b]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cec2af744b28f7391c56c7642a3adbcd7700b945)
A4.
![{\displaystyle [a\mathbin {;} b]p\leftrightarrow [a][b]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2bf59d82a76d12d6f470e1ba7862205b6adb6fd1)
А5.
![{\displaystyle [a*]p\leftrightarrow p\land [a][a*]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/dde210e320a21a65135afb9b38cab0c8b981b4c2)
А6.
\to [a*]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/596a5affc1e9f43a0389e75c7aea2479d05fd014)
Аксиома А1 дает пустое обещание, что когда BLOCK завершится, выдержит, даже если является ли предложение ложным . (Таким образом, БЛОК абстрагирует суть действия замерзающего ада.)
А2 говорит, что NOP действует как тождественная функция предложений, то есть преобразует в себя.
А3 говорит, что если выполнить одно из или должен вызвать , затем должен вызвать и аналогично для , и наоборот.
А4 говорит, что если делать а потом должен вызвать , затем должно создать ситуацию, в которой должен вызвать .
A5 является очевидным результатом применения A2, A3 и A4 к уравнению Клини алгебры .
А6 утверждает, что если сохраняется сейчас, и независимо от того, как часто мы выполняем остается фактом, что истина после этого выступления влечет за собой свою истинность после еще одного исполнения , затем должно оставаться верным независимо от того, как часто мы выполняем . A6 можно узнать как математическую индукцию с действием n := n+1 приращения n, обобщенным на произвольные действия. .
Производные [ править ]
Аксиома модальной логики позволяет вывести следующие шесть теорем, соответствующих приведенным выше:
Т1.
Т2.
Т3.
Т4.
Т5.
Т6.
T1 утверждает невозможность чего-либо добиться, выполнив BLOCK .
T2 снова отмечает, что NOP ничего не меняет, имея в виду, что NOP является одновременно детерминированным и завершающим, откуда и иметь одинаковую силу.
Т3 говорит, что если выбор или может вызвать , то либо или в одиночку могло бы вызвать .
Т4 похож на А4.
T5 поясняется так же, как и A5.
Т6 утверждает, что если возможно добиться выполняя достаточно часто, то либо верно сейчас или можно выполнить неоднократно, чтобы создать ситуацию, в которой (все еще) ложь, но еще одно представление может вызвать .
![{\displaystyle [1]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/76fdef3b81c82f740f94bda91755a8ee95bea6f1)
Коробка и ромб совершенно симметричны относительно того, что принято считать примитивным. Альтернативной аксиоматизацией было бы принять теоремы T1–T6 в качестве аксиом, из которых мы могли бы затем вывести A1–A6 как теоремы.
Разница между импликацией и умозаключением в динамической логике такая же, как и в любой другой логике: тогда как импликация утверждает, что если это правда, тогда так и есть , вывод утверждает, что если действительно, тогда так и есть . Однако динамическая природа динамической логики выводит это различие из области абстрактной аксиоматики в обыденный опыт постоянно меняющихся ситуаций. Правило вывода например, является правильным, поскольку его предпосылка утверждает, что держится всегда, откуда бы ни было может взять нас, там будет верно. Значение однако недействителен, поскольку истина в настоящий момент нет гарантии ее истинности после выполнения . Например, будет верным в любой ситуации, когда является ложным, или в любой ситуации, когда верно, но утверждение ложно в любой ситуации, когда имеет значение 1 и поэтому недействителен.
![{\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)
Производные правила вывода [ править ]
Что касается модальной логики, то правила вывода modus ponens и необходимости достаточны и для динамической логики как единственные примитивные правила, которые ей нужны, как отмечалось выше. Однако, как это обычно бывает в логике, из них можно вывести гораздо больше правил с помощью аксиом. Примером такого производного правила в динамической логике является то, что если удар по сломанному телевизору один раз не сможет его починить, то повторные удары по нему тоже не смогут его починить. Письмо за то, что пнул телевизор, и Для утверждения о том, что телевизор сломан, динамическая логика выражает этот вывод как , имея в качестве предпосылки и в качестве заключения . Значение заключается в том, что после удара ногой телевизор гарантированно сломается. Отсюда предпосылка означает, что если телевизор сломан, то после одного удара ногой он все равно будет сломан. обозначает действие, когда телевизор пинают ноль или более раз. Отсюда вывод означает, что если телевизор сломан, то после ноля и более ударов ногой он все равно будет сломан. В противном случае, после предпоследнего пинка телевизор окажется в состоянии, в котором повторный пинок его исправит, чего, как утверждает посылка, никогда не произойдет ни при каких обстоятельствах.
![{\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 (б\к [к]б)\к (б\к [к*]б)\,\!}](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)
Примером допустимой импликации является предложение . Это говорит о том, что если больше или равно 3, то после увеличения , должно быть больше или равно 4. В случае детерминированных действий которые гарантированно завершаются, например , должно и может иметь одинаковую силу, то есть, и имеют то же значение. Следовательно, приведенное выше предложение эквивалентно утверждая, что если больше или равно 3, то после выполнения , может быть больше или равно 4.
\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/bc161d9b9d88878ef16af585a731fb107f67f63b)
Назначение [ править ]
Общая форма оператора присваивания: где является переменной и — это выражение, построенное из констант и переменных с использованием любых операций, предусмотренных языком, таких как сложение и умножение. Аксиома Хоара для присваивания представлена не как отдельная аксиома, а скорее как схема аксиом.
A7.
![{\displaystyle [x:=e]\Phi (x)\leftrightarrow \Phi (e)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4165ffa60cf13e329cf352f0ba2fe6e95822230f)
Это схема в том смысле, что может быть создан с помощью любой формулы содержащий ноль или более экземпляров переменной . Значение является с такими явлениями которые происходят бесплатно в , то есть не связан каким-либо квантором, как в , заменен на . Например, мы можем создать экземпляр A7 с помощью или с . Такая схема аксиом позволяет записать бесконечное количество аксиом, имеющих общую форму, в виде конечного выражения, обозначающего эту форму.
\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)
Экземпляр А7 позволяет механически вычислить, что пример встречавшийся несколько абзацев назад эквивалентен , что, в свою очередь, эквивалентно по элементарной алгебре .
\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)
Пример, иллюстрирующий присваивание в сочетании с это предложение . Это утверждает, что это возможно, увеличивая достаточно часто, чтобы сделать равно 7. Это, конечно, не всегда верно, например, если изначально равно 8, или 6,5, следовательно, это предложение не является теоремой динамической логики. Если однако имеет целочисленный тип, то это утверждение верно тогда и только тогда, когда для начала не более 7, то есть это всего лишь окольный способ сказать .
Математическая индукция может быть получена как пример А6, в котором предложение создается как , действие как , и как . Первые два из этих трех экземпляров просты: они преобразуют A6 в . Однако, казалось бы, простая замена для не так просто, поскольку выявляет так называемую референциальную непрозрачность модальной логики в случае, когда модальность может мешать замене.
\to [n:=n+1]\Phi (n)))\to [(n :=n+1)*]\You (n)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/387b4dd2f085e5a8f4a98bcd89bca88811a94cf8)
Когда мы заменили для , мы думали о символе предложения как жесткий указатель по отношению к модальности , что означает, что это то же самое предложение после приращения как и прежде, хотя и увеличивается может повлиять на его истинность. Аналогично, действие это все то же действие после увеличения , хотя и увеличивается приведет к его выполнению в другой среде. Однако, само по себе не является жестким обозначением модальности. ; если он обозначает 3 перед увеличением , это обозначает 4 после. Поэтому мы не можем просто заменить для везде в А6.
![{\displaystyle [n:=n+1]\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/044fb0d8c92e5e7228efb8f16bf07edf10216353)
Один из способов справиться с непрозрачностью модальностей — устранить их. Для этого разверните как бесконечное соединение , то есть союз над всеми из . Теперь примените А4, чтобы повернуть в , имея модальности. Затем примените аксиому Хоара раз для этого, чтобы произвести , затем упростите эту бесконечную конъюнкцию до . Все это сокращение должно быть применено к обоим экземплярам в А6, что дает . Оставшуюся модальность теперь можно устранить, еще раз применив аксиому Хоара, чтобы получить .
![{\displaystyle [(n:=n+1)*]\Phi (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}]\Phi (n)\land \ldots \,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/04e959dd47b2fdde55833b0755833bd0deefe611)
![{\displaystyle [(n:=n+1)^{i}]\Phi (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 +я)\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/64af1426c5434142818e7aea3a0fa53e25aec648)
Теперь, когда непрозрачные модальности устранены, мы можем смело заменить для обычным способом логики первого порядка, чтобы получить . знаменитую аксиому Пеано , а именно математическая индукция.
Одна тонкость, которую мы здесь умолчали, заключается в том, что следует понимать как диапазон натуральных чисел, где это верхний индекс в разложении как союз по всем натуральным числам . Важность сохранения ясности этой печатной информации становится очевидной, если имел тип целочисленного или даже вещественного типа , для любого из которых А6 вполне допустим как аксиома. В качестве примера, если является действительной переменной и это предикат — натуральное число , то аксиома А6 после первых двух подстановок, т. е. , столь же действителен, то есть истинен в каждом состоянии, независимо от значения в таком состоянии, как когда имеет тип натурального числа . Если в данном состоянии — натуральное число, то имеет место антецедент основного импликации A6, но тогда также является натуральным числом, поэтому справедливо и следствие. Если не является натуральным числом, то антецедент ложен, и поэтому A6 остается истинным независимо от истинности консеквента. Мы могли бы усилить A6 до эквивалентности не влияя ни на что из этого, другое направление доказуемо из А5, откуда мы видим, что если антецедент А6 где-то окажется ложным, то и консеквент должен быть ложным.
\leftrightarrow [a*]p\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8a1257d316eecefc8cb32db6fb0e4aaca34c4f19)
Тест [ править ]
Динамическая логика связана с каждым предложением действие называется тестом. Когда держится, тест действует как NOP , ничего не меняя, но позволяя действию двигаться дальше. Когда ложно, действует как БЛОК . Тесты можно аксиоматизировать следующим образом.
А8.
![{\ displaystyle [p?] q \ leftrightarrow (p \ to q) \, \!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0d3bd6998d5aacd0db40c16709918c446a6f3d1e)
Соответствующая теорема для является:
Вопрос 8.
Конструкция if p then a else b реализуется в динамической логике как . Это действие выражает осторожный выбор: если тогда держится эквивалентно , тогда как эквивалентно BLOCK, и эквивалентно . Следовательно, когда верно, исполнитель действия может пойти только по левой ветке, и когда ложное право.
Конструкция while p do a реализуется как . Это выполняет ноль или более раз, а затем выполняет . Пока остается верным, в конце блокирует исполнителя от преждевременного завершения итерации, но как только она становится ложной, дальнейшие итерации тела блокируются, и тогда исполнителю не остается другого выбора, кроме как выйти через тест. .
оценка как случайное распределение Количественная
Оператор случайного присваивания обозначает недетерминированное действие установки до произвольного значения. потом говорит, что держится независимо от того, что вы установили чтобы, пока говорит, что можно установить до значения, которое делает истинный. таким образом, имеет то же значение, что и квантор всеобщности , пока аналогично соответствует квантору существования . То есть логику первого порядка можно понимать как динамическую логику программ вида .
![{\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)
Дейкстра утверждал, что показал невозможность программы, устанавливающей значение переменной. к произвольному положительному целому числу. [1] Однако в динамической логике с присваиванием и оператором * может быть установлено произвольное положительное целое число с помощью программы динамической логики . Следовательно, мы должны либо отвергнуть аргумент Дейкстры, либо признать, что оператор * неэффективен.
возможного Семантика мира
Модальную логику чаще всего интерпретируют с точки зрения возможной семантики мира или структур Крипке. Эта семантика естественным образом переносится в динамическую логику путем интерпретации миров как состояний компьютера в приложениях для проверки программ или состояний нашей среды в приложениях к лингвистике, искусственному интеллекту и т. д. Одна из функций возможной семантики мира заключается в формализации интуитивных представлений о истинность и достоверность, которые, в свою очередь, позволяют определить понятия обоснованности и полноты для систем аксиом. Правило вывода является правильным, когда истинность его посылок подразумевает обоснованность его вывода. Система аксиом надежна, когда все ее аксиомы действительны и правила вывода верны. Система аксиом является полной, когда каждая действительная формула выводится как теорема этой системы. Эти концепции применимы ко всем логическим системам, включая динамическую логику.
Пропозициональная динамическая логика (PDL) [ править ]
Обычная логика или логика первого порядка имеет два типа терминов: утверждения и данные соответственно. Как видно из приведенных выше примеров, динамическая логика добавляет третий тип терминов, обозначающих действия. Утверждение динамической логики содержит все три типа: , , и являются данными, это действие, и и являются утверждениями. Логика высказываний выводится из логики первого порядка путем исключения терминов данных и причин только в отношении абстрактных предложений, которые могут быть простыми пропозициональными переменными или атомами или составными предложениями, построенными с помощью таких логических связок, как и , или , и not .
\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7c7fcfa23d464f4776e68d47af0f174364ea6173)
Пропозициональная динамическая логика, или PDL, была выведена из динамической логики в 1977 году Майклом Дж. Фишером и Ричардом Ладнером . PDL сочетает в себе идеи, лежащие в основе логики высказываний и динамической логики, добавляя действия, опуская данные; следовательно, терминами PDL являются действия и предложения. Приведенный выше пример телевидения выражен в PDL, тогда как следующий пример, включающий находится в динамической логике первого порядка. PDL относится к динамической логике (первого порядка) так же, как логика высказываний относится к логике первого порядка.
Фишер и Ладнер показали в своей статье 1977 года, что выполнимость PDL имеет вычислительную сложность в большинстве случаев недетерминированное экспоненциальное время и, по крайней мере, детерминированное экспоненциальное время в худшем случае . Этот пробел был закрыт в 1978 году Воаном Праттом , который показал, что PDL разрешима в детерминированном экспоненциальном времени. В 1977 году Кристер Сегерберг предложил полную аксиоматизацию PDL, а именно любую полную аксиоматизацию модальной логики K вместе с аксиомами A1 – A6, как указано выше. Доказательства полноты аксиом Сегерберга были найдены Габбаем (неопубликованная заметка), Парихом (1978), Праттом (1979), Козеном и Парихом (1981).
История [ править ]
Динамическая логика была разработана Воаном Праттом в 1974 году в примечаниях к классу по верификации программ как подход к приданию смысла логике Хоара путем выражения формулы Хоара. как . Позже этот подход был опубликован в 1976 году как логическая система отдельная . Система параллельна Анджея Салвицкого. Система алгоритмической логики [2] и Эдсгера Дейкстры о преобразователе предикатов со слабым предусловием. понятие , с соответствующий Дейкстре , самая слабая либеральная предпосылка. Однако эта логика не имела никакой связи ни с модальной логикой, ни с семантикой Крипке, ни с регулярными выражениями, ни с исчислением бинарных отношений. Таким образом, динамическую логику можно рассматривать как усовершенствование алгоритмической логики и преобразователей предикатов , которое связывает их с аксиоматикой и семантикой Крипке модальной логики, а также с исчислением бинарных отношений и регулярными выражениями.
![{\displaystyle p\to [a]q\,\!}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d8e1788859ff60725bc56a43ac4d5ecc072ea6b4)
Проблема параллелизма [ править ]
Логика Хоара, алгоритмическая логика, слабейшие предусловия и динамическая логика хорошо подходят для рассуждений и рассуждений о последовательном поведении. Однако распространение этой логики на параллельное поведение оказалось проблематичным. Существуют различные подходы, но всем им не хватает элегантности последовательного случая. Напротив, Амира Пнуэли 1977 года система темпоральной логики , еще один вариант модальной логики, имеющий много общих черт с динамической логикой, отличается от всех вышеупомянутых логик тем, что Пнуэли охарактеризовал как «эндогенную» логику, а остальные — «экзогенная» логика. Под этим Пнуэли имел в виду, что утверждения темпоральной логики интерпретируются в рамках универсальной поведенческой структуры, в которой одна глобальная ситуация меняется с течением времени, тогда как утверждения других логик делаются вне множества действий, о которых они говорят. Преимущество эндогенного подхода заключается в том, что он не делает фундаментальных предположений о том, что является причиной того, что окружающая среда меняется со временем. Вместо этого формула темпоральной логики может говорить о двух несвязанных частях системы, которые, поскольку они не связаны между собой, молчаливо развиваются параллельно. По сути, обычное логическое соединение темпоральных утверждений является параллельным оператором композиции темпоральной логики. Простота этого подхода к параллелизму привела к тому, что темпоральная логика стала предпочтительной модальной логикой для рассуждений о параллельных системах с их аспектами синхронизации, взаимодействия, независимости и т. д. тупик , активная блокировка , справедливость и т. д.
См. также [ править ]
Дальнейшее чтение [ править ]
- Дэвид Харел , Декстер Козен и Ежи Тюрин, «Динамическая логика». MIT Press, 2000 (450 стр.).
- Николя Трокар и Филипп Бальбиани, «Пропозициональная динамическая логика». Стэнфордская энциклопедия философии , 2007.
Сноски [ править ]
- ^ Дейкстра, EW (1976). Дисциплина программирования . Энглвуд Клиффс: Prentice-Hall Inc., стр. 221 . ISBN 013215871X .
- ^ Мирковская, Гражина; Салвицкий А. (1987). Алгоритмическая логика (PDF) . Варшава и Бостон: PWN & D. Reidel Publ. стр. 372. ISBN 8301068590 .
Ссылки [ править ]
- Воган Пратт , «Семантические соображения по логике Флойда-Хора», Proc. 17-й ежегодный симпозиум IEEE по основам информатики , 1976, 109–121.
- Дэвид Харел , «Динамическая логика», Д. Габбай и Ф. Гентнер, редакторы, «Справочник по философской логике», том II: Расширения классической логики, глава 10, страницы 497–604. Райдель, Дордрехт, 1984 г.
- Дэвид Харел , Декстер Козен и Ежи Тюрин, «Динамическая логика», В Д. Габбае и Ф. Гюнтенере, редакторах, «Справочник по философской логике», том 4: страницы 99–217. Клювер, 2-е издание, 2002 г.
Внешние ссылки [ править ]
- Семантические соображения по логике Флойда-Хора (оригинальная статья по динамической логике)
- Глава 6: Логика и действие на Logic In Action сайте
- Конспект лекций по динамической логике Андре Платцера