Lógica dinámica (lógica modal)

En lógica , filosofía y ciencia informática teórica , la lógica dinámica es una extensión de la lógica modal capaz de codificar propiedades de programas informáticos .

Un ejemplo sencillo de una afirmación en lógica dinámica es

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

que establece que si actualmente el suelo está seco y llueve, después el suelo estará mojado.

La sintaxis de la lógica dinámica contiene un lenguaje de proposiciones (como "el suelo está seco") y un lenguaje de acciones (como "llueve"). Las construcciones modales básicas son , que establece que después de realizar la acción a, la proposición p debería cumplirse, y , que establece que después de realizar la acción a, es posible que p se cumpla. El lenguaje de acción admite operaciones (realizar una acción seguida de otra), (realizar una acción u otra) e iteración (realizar una acción cero o más veces). El lenguaje de proposiciones admite operaciones booleanas (y, o, y no). La lógica de acción es lo suficientemente expresiva como para codificar programas. Para un programa arbitrario , una condición previa y una condición posterior , la declaración de lógica dinámica codifica la corrección del programa, lo que hace que la lógica dinámica sea más general que la lógica de Hoare . ${\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 '}$

Más allá de su uso en la verificación formal de programas, la lógica dinámica se ha aplicado para describir comportamientos complejos que surgen en la lingüística , la filosofía , la IA y otros campos.

Idioma

La lógica modal se caracteriza por los operadores modales (caja p) que afirman que es necesariamente el caso, y (rombo p) que afirma que es posiblemente el caso. La lógica dinámica extiende esto al asociar a cada acción los operadores modales y , convirtiéndola así en una lógica multimodal . El significado de es que después de realizar la acción es necesariamente el caso que se cumple, es decir, debe producir . El significado de es que después de realizar es posible que se cumple, es decir, podría producir . Estos operadores son duales entre sí, lo que significa que están relacionados por y , análogamente a la relación entre los cuantificadores universales ( ) y existenciales ( ). ${\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 \,\!}$

La lógica dinámica permite acciones compuestas formadas a partir de acciones más pequeñas. Si bien los operadores de control básicos de cualquier lenguaje de programación se pueden utilizar para este propósito, los operadores de expresión regular de Kleene son una buena opción para la lógica modal. Dadas las acciones y , la acción compuesta choice , también escrita or , se realiza ejecutando una de o . La acción compuesta sequence , se realiza ejecutando first y then . La acción compuesta iteration , se realiza ejecutando cero o más veces, secuencialmente. La acción constante o BLOCK no hace nada y no termina, mientras que la acción constante o SKIP o NOP , definible como , no hace nada pero termina. ${\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{*}\,\!}$

Axiomas

Estos operadores pueden axiomatizarse en lógica dinámica de la siguiente manera, tomando como ya dada una axiomatización adecuada de la lógica modal que incluye axiomas para operadores modales como el axioma mencionado anteriormente y las dos reglas de inferencia modus ponens ( e implica ) y necesidad ( implica ). ${\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\,\!}$

El axioma A1 hace la promesa vacía de que cuando BLOQUE termina, se cumplirá, incluso si es falsa la proposición . (De este modo, BLOQUE abstrae la esencia de la acción de congelar el infierno.) A2 dice que NOP actúa como la función identidad en proposiciones, es decir, se transforma en sí misma. A3 dice que si al hacer una de o debe producir , entonces debe producir y lo mismo para , y a la inversa. A4 dice que si al hacer y entonces debe producir , entonces debe producir una situación en la que debe producir . A5 es el resultado evidente de aplicar A2, A3 y A4 a la ecuación del álgebra de Kleene . A6 afirma que si se cumple ahora, y no importa con qué frecuencia realicemos sigue siendo el caso de que la verdad de después de esa ejecución implica su verdad después de una ejecución más de , entonces debe seguir siendo verdadera sin importar con qué frecuencia realicemos . A6 es reconocible como inducción matemática con la acción n := n+1 de incrementar n generalizada a acciones arbitrarias . ${\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\,\!}$

Derivaciones

El axioma de la lógica modal permite la derivación de los siguientes seis teoremas correspondientes a lo anterior: ${\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 afirma la imposibilidad de lograr algo ejecutando BLOCK .
T2 observa nuevamente que NOP no cambia nada, teniendo en cuenta que NOP es determinista y terminante de donde y tienen la misma fuerza. T3 dice que si la elección de o podría lograr , entonces o bien o bien por sí solo podría lograr . T4 es igual que A4. T5 se explica como para A5. T6 afirma que si es posible lograrlo ejecutando con suficiente frecuencia, entonces o bien es cierto ahora o bien es posible ejecutar repetidamente para lograr una situación donde es (todavía) falso pero una ejecución más de podría lograr . ${\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\,\!}$

La caja y el rombo son completamente simétricos respecto de cuál de ellos se tome como primitivo. Una axiomatización alternativa habría sido tomar los teoremas T1–T6 como axiomas, de los cuales podríamos haber derivado A1–A6 como teoremas.

La diferencia entre implicación e inferencia es la misma en la lógica dinámica que en cualquier otra lógica: mientras que la implicación afirma que si es verdadero entonces también lo es , la inferencia afirma que si es válido entonces también lo es . Sin embargo, la naturaleza dinámica de la lógica dinámica saca esta distinción del ámbito de la axiomática abstracta y la lleva a la experiencia de sentido común de situaciones en cambio. La regla de inferencia , por ejemplo, es válida porque su premisa afirma que se cumple en todo momento, por lo que no importa a dónde nos lleve, será verdadera allí. Sin embargo, la implicación no es válida porque la verdad de en el momento presente no es garantía de su verdad después de realizar . Por ejemplo, será verdadera en cualquier situación donde sea falsa, o en cualquier situación donde sea verdadera, pero la afirmación es falsa en cualquier situación donde tenga valor 1 y, por lo tanto, no es válida. ${\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\,\!}$

Reglas de inferencia derivadas

En cuanto a la lógica modal, las reglas de inferencia modus ponens y necesidad son suficientes también para la lógica dinámica como las únicas reglas primitivas que necesita, como se señaló anteriormente. Sin embargo, como es habitual en lógica, se pueden derivar muchas más reglas de estas con la ayuda de los axiomas. Un ejemplo de una regla derivada de este tipo en lógica dinámica es que si patear un televisor roto una vez no puede arreglarlo, patearlo repetidamente tampoco puede arreglarlo. Escribiendo para la acción de patear el televisor y para la proposición de que el televisor está roto, la lógica dinámica expresa esta inferencia como , que tiene como premisa y como conclusión . El significado de es que está garantizado que después de patear el televisor, está roto. Por lo tanto, la premisa significa que si el televisor está roto, luego de patearlo una vez seguirá roto. denota la acción de patear el televisor cero o más veces. Por lo tanto, la conclusión significa que si el televisor está roto, luego de patearlo cero o más veces seguirá roto. De lo contrario, después de la penúltima patada, el televisor estaría en un estado en el que patearlo una vez más lo arreglaría, lo que la premisa afirma que nunca puede suceder bajo ninguna circunstancia. ${\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\,\!}$

La inferencia es válida. Sin embargo, la implicación no es válida porque podemos encontrar fácilmente situaciones en las que se cumple pero no se cumple. En cualquier situación de contraejemplo, debe cumplirse pero debe ser falso, mientras que sin embargo debe ser verdadero. Pero esto podría suceder en cualquier situación en la que el televisor esté roto pero se pueda revivir con dos patadas. La implicación falla (no es válida) porque solo requiere que se cumpla ahora, mientras que la inferencia tiene éxito (es válida) porque requiere que se cumpla en todas las situaciones, no solo en la actual. ${\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\,\!}$

Un ejemplo de implicación válida es la proposición . Esta dice que si es mayor o igual a 3, entonces después de incrementar , debe ser mayor o igual a 4. En el caso de acciones deterministas que tienen una terminación garantizada, como , deben y podrían tener la misma fuerza, es decir, y tienen el mismo significado. Por lo tanto, la proposición anterior es equivalente a afirmar que si es mayor o igual a 3, entonces después de realizar , podría ser mayor o igual a 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\,\!}$

Asignación

La forma general de una declaración de asignación es donde es una variable y es una expresión construida a partir de constantes y variables con cualquier operación provista por el lenguaje, como la suma y la multiplicación. El axioma de Hoare para la asignación no se da como un único axioma sino como un esquema axiomático. ${\displaystyle x:=e\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle e\,\!}$

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

Este es un esquema en el sentido de que se puede instanciar con cualquier fórmula que contenga cero o más instancias de una variable . El significado de es con aquellas ocurrencias de que ocurren libres en , es decir, no limitadas por algún cuantificador como en , reemplazadas por . Por ejemplo, podemos instanciar A7 con , o con . Un esquema de axioma de este tipo permite que infinitos axiomas que tienen una forma común se escriban como una expresión finita que connota esa forma. ${\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\,\!}$

La instancia de A7 nos permite calcular mecánicamente que el ejemplo encontrado hace unos párrafos es equivalente a , que a su vez es equivalente a por álgebra elemental . ${\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\,\!}$

Un ejemplo que ilustra la asignación en combinación con es la proposición . Esta afirma que es posible, incrementando con la suficiente frecuencia, hacer que sea igual a 7. Por supuesto, esto no siempre es cierto, por ejemplo, si es 8 para empezar, o 6,5, por lo que esta proposición no es un teorema de lógica dinámica. Sin embargo, si es de tipo entero, entonces esta proposición es verdadera si y solo si es como máximo 7 para empezar, es decir, es solo una forma indirecta de decir . ${\displaystyle *\,\!}$ ${\displaystyle \langle (x:=x+1)*\rangle x=7\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\,\!}$ ${\displaystyle x\leq 7\,\!}$

La inducción matemática se puede obtener como la instancia de A6 en la que la proposición se instancia como , la acción como , y como . Las primeras dos de estas tres instancias son sencillas, convirtiendo A6 en . Sin embargo, la sustitución aparentemente simple de por no es tan simple como para poner de manifiesto la llamada opacidad referencial de la lógica modal en el caso en que una modalidad puede interferir con una sustitución. ${\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\,\!}$

Cuando sustituimos por , estábamos pensando en el símbolo de proposición como un designador rígido con respecto a la modalidad , lo que significa que es la misma proposición después de incrementar que antes, aunque incrementar puede afectar su verdad. Del mismo modo, la acción sigue siendo la misma acción después de incrementar , aunque incrementar dará como resultado su ejecución en un entorno diferente. Sin embargo, en sí mismo no es un designador rígido con respecto a la modalidad ; si denota 3 antes de incrementar , denota 4 después. Por lo tanto, no podemos simplemente sustituir por en todas partes en 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\,\!}$

Una forma de lidiar con la opacidad de las modalidades es eliminarlas. Para ello, expanda como la conjunción infinita , es decir, la conjunción sobre todos los . Ahora aplique A4 para convertir en , que tiene modalidades. Luego aplique el axioma de Hoare a esto para producir , luego simplifique esta conjunción infinita a . Toda esta reducción debe aplicarse a ambas instancias de en A6, produciendo . La modalidad restante ahora puede eliminarse con un uso más del axioma de Hoare para dar . ${\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)\,\!}$

Ahora que ya no somos responsables de las modalidades opacas, podemos sustituir con seguridad la fórmula de la manera habitual de la lógica de primer orden para obtener el célebre axioma de Peano , es decir, la inducción matemática. ${\displaystyle 0\,\!}$ ${\displaystyle n\,\!}$ ${\displaystyle (\Phi (0)\land \forall i(\Phi (i)\to \Phi (i+1)))\to \forall i\Phi (i)\,\!}$

Una sutileza que pasamos por alto aquí es que debe entenderse como que abarca los números naturales, donde es el superíndice en la expansión de como la unión de sobre todos los números naturales . La importancia de mantener esta información de tipificación directa se hace evidente si había sido de tipo entero , o incluso real , para cualquiera de los cuales A6 es perfectamente válido como axioma. Como ejemplo, si es una variable real y es el predicado es un número natural , entonces el axioma A6 después de las dos primeras sustituciones, es decir, , es tan válido, es decir, verdadero en cada estado independientemente del valor de en ese estado, como cuando es de tipo número natural . Si en un estado dado es un número natural, entonces el antecedente de la implicación principal de A6 se cumple, pero entonces también es un número natural, por lo que el consecuente también se cumple. Si no es un número natural, entonces el antecedente es falso y, por lo tanto, A6 sigue siendo verdadero independientemente de la verdad del consecuente. Podríamos fortalecer A6 a una equivalencia sin impactar nada de esto, la otra dirección siendo demostrable a partir de A5, de donde vemos que si el antecedente de A6 resulta ser falso en alguna parte, entonces el consecuente debe ser falso. ${\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\,\!}$

Prueba

La lógica dinámica asocia a cada proposición una acción llamada prueba. Cuando se cumple, la prueba actúa como una NOP , sin cambiar nada y permitiendo que la acción continúe. Cuando es falsa, actúa como BLOCK . Las pruebas se pueden axiomatizar de la siguiente manera. ${\displaystyle p\,\!}$ ${\displaystyle p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle p?\,\!}$

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

El teorema correspondiente es: ${\displaystyle \langle p?\rangle \,\!}$

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

El constructo si p entonces a sino b se realiza en lógica dinámica como . Esta acción expresa una elección cautelosa: si se cumple entonces es equivalente a , mientras que es equivalente a BLOQUEAR, y es equivalente a . Por lo tanto, cuando es verdadero el ejecutante de la acción solo puede tomar la rama izquierda, y cuando es falso la derecha. ${\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\,\!}$

El constructo while p do a se realiza como . Esto se ejecuta cero o más veces y luego ejecuta . Mientras siga siendo verdadero, el al final impide que el ejecutante finalice la iteración prematuramente, pero tan pronto como se vuelve falso, se bloquean las iteraciones posteriores del cuerpo y el ejecutante no tiene otra opción que salir a través de la prueba . ${\displaystyle ({p?\mathbin {;} a)*}\mathbin {;} \neg p?\,\!}$ ${\displaystyle p?\mathbin {;} a\,\!}$ ${\displaystyle \neg p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle \neg p?\,\!}$ ${\displaystyle p\,\!}$ ${\displaystyle \neg p?\,\!}$

Cuantificación como asignación aleatoria

La declaración de asignación aleatoria denota la acción no determinista de establecer un valor arbitrario. then dice que se cumple sin importar lo que establezca , mientras que dice que es posible establecer un valor que haga verdadero. por lo tanto tiene el mismo significado que el cuantificador universal , mientras que corresponde de manera similar al cuantificador existencial . Es decir, la lógica de primer orden puede entenderse como la lógica dinámica de programas de la forma . ${\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:=?\,\!}$

Dijkstra afirmó haber demostrado la imposibilidad de un programa que establezca el valor de variable en un entero positivo arbitrario. ^[1] Sin embargo, en lógica dinámica con asignación y el operador *, se puede establecer en un entero positivo arbitrario con el programa de lógica dinámica . Por lo tanto, debemos rechazar el argumento de Dijkstra o sostener que el operador * no es efectivo. ${\displaystyle x}$ ${\displaystyle x}$ ${\displaystyle (x\mathbin {:=} 0)\mathbin {;} (x:=x+1){*}}$

Semántica del mundo posible

La lógica modal se interpreta más comúnmente en términos de semántica de mundos posibles o estructuras de Kripke. Esta semántica se traslada naturalmente a la lógica dinámica al interpretar mundos como estados de una computadora en la aplicación a la verificación de programas, o estados de nuestro entorno en aplicaciones a la lingüística, la inteligencia artificial, etc. Una función de la semántica de mundos posibles es formalizar las nociones intuitivas de verdad y validez, que a su vez permiten definir las nociones de solidez y completitud para los sistemas axiomáticos. Una regla de inferencia es válida cuando la validez de sus premisas implica la validez de su conclusión. Un sistema axiomático es válido cuando todos sus axiomas son válidos y sus reglas de inferencia son válidas. Un sistema axiomático es completo cuando cada fórmula válida es derivable como un teorema de ese sistema. Estos conceptos se aplican a todos los sistemas de lógica, incluida la lógica dinámica.

Lógica dinámica proposicional (LDP)

La lógica ordinaria o de primer orden tiene dos tipos de términos, respectivamente aserciones y datos. Como se puede ver en los ejemplos anteriores, la lógica dinámica agrega un tercer tipo de término que denota acciones. La aserción de la lógica dinámica contiene los tres tipos: , , y son datos, es una acción y y son aserciones. La lógica proposicional se deriva de la lógica de primer orden omitiendo los términos de datos y razonando solo sobre proposiciones abstractas, que pueden ser variables proposicionales simples o átomos o proposiciones compuestas construidas con conectores lógicos tales como y , o , y no . ${\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)\,\!}$

La lógica dinámica proposicional, o PDL, fue derivada de la lógica dinámica en 1977 por Michael J. Fischer y Richard Ladner . La PDL combina las ideas detrás de la lógica proposicional y la lógica dinámica agregando acciones y omitiendo datos; por lo tanto, los términos de la PDL son acciones y proposiciones. El ejemplo de TV anterior se expresa en PDL, mientras que el siguiente ejemplo que involucra es en lógica dinámica de primer orden. La PDL es a la lógica dinámica (de primer orden) lo que la lógica proposicional es a la lógica de primer orden. ${\displaystyle x:=x+1\,\!}$

Fischer y Ladner demostraron en su artículo de 1977 que la satisfacibilidad de PDL era de complejidad computacional en el tiempo exponencial no determinista como máximo , y al menos en el tiempo exponencial determinista en el peor de los casos. Esta brecha fue cerrada en 1978 por Vaughan Pratt , quien demostró que PDL era decidible en tiempo exponencial determinista. En 1977, Krister Segerberg propuso una axiomatización completa de PDL, es decir, cualquier axiomatización completa de la lógica modal K junto con los axiomas A1–A6 como se indicó anteriormente. Gabbay (nota no publicada), Parikh (1978), Pratt (1979) y Kozen y Parikh (1981) encontraron pruebas de completitud para los axiomas de Segerberg .

Historia

La lógica dinámica fue desarrollada por Vaughan Pratt en 1974 en notas para una clase sobre verificación de programas como un enfoque para asignar significado a la lógica de Hoare expresando la fórmula de Hoare como . El enfoque se publicó más tarde en 1976 como un sistema lógico por derecho propio. El sistema es paralelo al sistema de lógica algorítmica de Andrzej Salwicki ^[2] y la noción de transformador de predicado de precondición más débil de Edsger Dijkstra , con correspondiente a la precondición liberal más débil de Dijkstra . Sin embargo, esas lógicas no hicieron conexión ni con la lógica modal, la semántica de Kripke, las expresiones regulares o el cálculo de relaciones binarias. Por lo tanto, la lógica dinámica puede verse como un refinamiento de la lógica algorítmica y los transformadores de predicados que los conecta con la axiomática y la semántica de Kripke de la lógica modal, así como con los cálculos de relaciones binarias y expresiones regulares. ${\displaystyle p\{a\}q\,\!}$ ${\displaystyle p\to [a]q\,\!}$ ${\displaystyle \operatorname {wp} (a,p)\,\!}$ ${\displaystyle [a]p\,\!}$ ${\displaystyle \operatorname {wlp} (a,p)\,\!}$

El desafío de la concurrencia

La lógica de Hoare, la lógica algorítmica, las precondiciones más débiles y la lógica dinámica son todas ellas adecuadas para el discurso y el razonamiento sobre el comportamiento secuencial. Sin embargo, la extensión de estas lógicas al comportamiento concurrente ha resultado problemática. Hay varios enfoques, pero todos ellos carecen de la elegancia del caso secuencial. En contraste, el sistema de lógica temporal de Amir Pnueli de 1977 , otra variante de la lógica modal que comparte muchas características comunes con la lógica dinámica, difiere de todas las lógicas mencionadas anteriormente al ser lo que Pnueli ha caracterizado como una lógica "endógena", siendo las otras lógicas "exógenas". Con esto Pnueli quiso decir que las afirmaciones de la lógica temporal se interpretan dentro de un marco de comportamiento universal en el que una única situación global cambia con el paso del tiempo, mientras que las afirmaciones de las otras lógicas se hacen externamente a las múltiples acciones sobre las que hablan. La ventaja del enfoque endógeno es que no hace suposiciones fundamentales sobre qué causa qué a medida que el entorno cambia con el tiempo. En cambio, una fórmula de lógica temporal puede hablar de dos partes no relacionadas de un sistema, que, por no estar relacionadas, evolucionan tácitamente en paralelo. En efecto, la conjunción lógica ordinaria de aserciones temporales es el operador de composición concurrente de la lógica temporal. La simplicidad de este enfoque de la concurrencia ha dado como resultado que la lógica temporal sea la lógica modal de elección para razonar sobre sistemas concurrentes con sus aspectos de sincronización, interferencia, independencia, interbloqueo , interbloqueo activo , equidad, etc.

Véase también

• Lógica antigua
• Álgebra de Kleene
• Lógica temporal
• Lógica temporal en la verificación de estados finitos
• Lógica temporal de las acciones
• Cálculo μ modal

Lectura adicional

• David Harel , Dexter Kozen y Jerzy Tiuryn, "Lógica dinámica". MIT Press, 2000 (450 págs.).

• Nicolas Troquard y Philippe Balbiani, "Lógica dinámica proposicional". Enciclopedia de filosofía de Stanford , 2007.

Notas al pie

1. Dijkstra, EW (1976). Una disciplina de programación. Englewood Cliffs: Prentice-Hall Inc., págs. 221. ISBN 013215871X.
2. Mirkowska, Grażyna; Salwicki A. (1987). Lógica algorítmica (PDF) . Varsovia y Boston: PWN y D. Reidel Publ. pag. 372.ISBN​ 8301068590.

Referencias

• Vaughan Pratt , "Consideraciones semánticas sobre la lógica Floyd-Hoare", Proc. 17º Simposio Anual IEEE sobre Fundamentos de la Ciencia de la Computación , 1976, 109-121.
• David Harel , "Lógica dinámica", en D. Gabbay y F. Guenthner, editores, Handbook of Philosophical Logic, volumen II: Extensions of Classical Logic, capítulo 10, páginas 497-604. Reidel, Dordrecht, 1984.
• David Harel , Dexter Kozen y Jerzy Tiuryn, "Lógica dinámica", en D. Gabbay y F. Guenthner, editores, Handbook of Philosophical Logic, volumen 4: páginas 99-217. Kluwer, 2.ª edición, 2002.

Enlaces externos

• Consideraciones semánticas sobre la lógica Floyd-Hoare (artículo original sobre lógica dinámica)
• Capítulo 6: Lógica y acción en el sitio Logic In Action
• Apuntes de la lección de lógica dinámica de André Platzer