Razonamiento sobre bucles de terminación no determinista

10

Aquí hay una pregunta de "pista B" si alguna vez hubo una. Resumen: lo primero en lo que pienso cuando intento dar una semántica a los programas no deterministas resulta en una semántica donde no puedo probar cosas sobre los bucles que solo terminan de manera no determinista. Seguramente alguien ha resuelto qué hacer en esta situación, o al menos señaló que es difícil, pero no sé cómo buscarlo (de ahí la etiqueta de "solicitud de referencia").

Antecedentes

Quiero modelar un lenguaje while con no determinismo. Creo que esta es la forma obvia (o al menos ingenua) de modelar un lenguaje de este tipo con un dominio de poder Smyth, pero corrígeme si me equivoco. Modelaremos el significado de un comando en este lenguaje como una función cuyo dominio es el conjunto de estados y cuyo codominio es el conjunto P ( S ) = { } P ( S ) , donde es un elemento mínimo representando la no terminación y P ( S ) es el conjunto de poder de los estados.SP(S)={}P(S)P(S)

Interpretamos los comandos como mapas de los estados al evento de no terminación o a conjuntos de estados { σ 1 , σ 2 , ... } que representan posibles resultados. P Q es una elección no determinista.σ{σ1,σ2,}PQ

  • skipσ={σ}
  • x:=Eσ={σ[(Eσ)/x]}
  • abortσ=
  • siE sigma = t r u e , de lo contrarioQ sigmaif E then P else Qσ=PσEσ=trueQσ
  • siP sigma = oQ sigma = , de lo contrarioP sigma Q sigmaPQσ=Pσ=Qσ=PσQσ
  • siP sigma = oQ tau = para algunos tau P sigma , de lo contrariotau P sigmaQ tauP;Qσ=Pσ=Qτ=τPστPσQτ

Hay un orden parcial completo dirigido , donde S para cualquier S P ( S ) y S 1S 2 si S 1 y S 2 son conjuntos adecuados y S 1S 2 , y podemos extender esto a las funciones f de S a P ( S ) puntual: f 1f 2SSP(S)S1S2S1S2S1S2fSP(S)f1f2si para cada σ , y f es la función que asigna cada estado a .f1(σ)f2(σ)σf

El significado de un bucle es es el extremo superior de la cadena f f ( f ) f ( f ( f ) ) ... , donde f ( g ) ( σ ) = { σ } si E ( σ ) = f un lwhile E do Pσff(f)f(f(f))f(g)(σ)={σ} , de lo contrario siP sigma = o g ( τ ) = para algunos τ P sigma , de lo contrarioτ P sigma g ( τ ) . (Esta definición supone que la f que acabo de definir es Scott continua, pero creo que es seguro dejar eso de lado).E(σ)=falsePσ=g(τ)=τPστPσg(τ)f

Pregunta

Considere este programa:

b : = t r u e ; w h i l e b d ox:=0;
b:=true;
while b do
x:=x+2;
b:=falseb:=true

Intuitivamente, este es un bucle que puede devolver cualquier número par positivo o no terminar, y eso corresponde a lo que podemos probar sobre este bucle utilizando la precondición liberal más débil (es posible mostrar que es un bucle invariante). Sin embargo, debido a que el ciclo tiene la capacidad de no terminar (podemos refinar la elección no determinista del programa que siempre toma la rama derecha), el significado de este programa dado cualquier estado inicial es . (Menos informalmente: la función que mapea cualquier estado donde b es falso para sí mismo y cualquier estado donde b es verdadero para es un punto fijo de la fn.x=2nbbf usado para definir el bucle.)

Esto significa que la semántica ingenua que propuse no corresponde en la forma en que espero poder razonar sobre los programas. Culpo a mi semántica, pero no sé cómo solucionarlos.

Rob Simmons
fuente
44
Creo que al usar como codominio del significado de un programa, efectivamente ha renunciado a razonar cualquier cosa sobre un programa que pueda divergir. Un pensamiento ingenuo es usar P ( S { } ) , pero no sé si eso introducirá otro problema. {}P(S)P(S{})
Tsuyoshi Ito
Sí, tiene toda la razón en que mirando el conjunto ya es evidente que la esperanza se pierde incluso antes de llegar al ejemplo. Tu sugerencia también se me ocurrió, pero creo que terminas con el mismo problema en este ejemplo, siempre y cuando la posible no terminación sea modelada por S { } no { } , y si elegimos este último, interferiría con nuestra capacidad de dar sentido a un bucle como un punto menos fijo de la forma habitual. {}P(S)S{}{}
Rob Simmons
¿Has mirado en Dynamic Logic? La semántica se da en términos de relaciones de estados a estados, y puede usar la lógica para razonar sobre la corrección parcial y total, es decir, las propiedades de los cálculos que terminan y que todos los cálculos terminan con una propiedad dada.
Dave Clarke
No he pensado en la lógica dinámica en este entorno, pero veo cómo podría ser relevante: veré qué piensan Platzer y sus estudiantes cuando regrese a Pittsburgh.
Rob Simmons

Respuestas:

10

En [dB80], se ha demostrado que el análisis de Hitchcock y Park de las propiedades de terminación de la recursión corresponde a un análisis semántico basado en la llamada interpretación de las relaciones de Egli-Milner [Egl75, Plo76], que expresa el no determinismo errático . Esta noción captura que una unión de relaciones no determinista es correcta si genera al menos un cálculo que conduce a un resultado deseado (incluso en presencia de un cálculo no determinante). Esto parece corresponder a lo que está tratando de hacer.

A continuación, caracterice el significado de una declaración como una función f S que asigna cada estado inicial σ a un conjunto de estados no vacío, que posiblemente contenga , de modo que f S sea ​​estricto en el sentido de que f S ( ) = { } . La elección no determinista entre las declaraciones S 1 y S 2 se describe mediante el mapeo de funciones de cada estado inicial σ a la unión de los resultados individuales f S 1 ( σ ) SfSσfSfS()={}S1S2σ . Por lo tanto, siempre que S 1 o S 2 tengan la posibilidad no determinista de producir un resultado indeseable, también lo hará su elección no determinista. Como conjuntos resultantes de estados finales, se obtiene en este análisis el llamado conjunto de estados de Egli-Milner:fS1(σ)fS2(σ)S1S2

es finito y no vacío, o contiene}PE--M(S)={ sS | s}

¿Por qué los subconjuntos infinitos de no se consideran conjuntos posibles de estados finales en este modelo? Bajo el supuesto de que todos los bloques de construcción básicos de términos relacionales producen solo conjuntos finitos y no vacíos de posibles estados finales, un conjunto infinito de posibles estados finales solo puede generarse cuando es posible un cálculo infinito. Esto se puede ver de la siguiente manera. Estructura el conjunto de todos los cálculos posibles que comienzan en un estado dado σ 0 como un árbol con raíz σ 0 y estados como nodos. El conjunto de hojas es entonces exactamente el conjunto de posibles estados finales accesible desde σ 0 , a excepción de Sσ0σ0σ0, que puede faltar entre las hojas pero se representa en el conjunto de estados finales por el hecho de que hay un camino infinito en el árbol. Por el supuesto anterior, y dado que solo hay opciones finitas no deterministas disponibles, este árbol se ramifica finitamente. Por lo tanto, solo hay un número finito de hojas en cualquier profundidad finita. En consecuencia, un número infinito de estados finales posibles solo puede generarse en presencia de un cálculo infinito (una aplicación del lema de König [Kön32]).

es un poset para E - M definido por: para s , t P E - M ( S ) ,(PE--M(S),E--M)E--Ms,tPE--M(S)

sE--Mt=(ss{}t)(ss=t) .

Aquí, puede verse como un marcador de posición a través del cual se pueden generar E-M -conjuntos más grandes insertando más estados en lugar de . Por lo tanto, { } es el elemento menos importante deE--M{} . Además, el poset ( P E - M ( S ) , E - M ) posee lubricantes para ω -cadenas. Del mismo modo, las funciones estrictas de S { } a P(PE--M(S),E--M)(PE--M(S),E--M)ωS{}están parcialmente ordenado por la extensión puntual deE - M . Además, la función de menor importancia esλσ. También existen{}y lub's deω-cadenas de tales funciones.PE--M(S)E--Mλσ.{}ω

[dB80] JW de Bakker. Teoría matemática de la corrección del programa . Prentice Hall, 1980.

[Egl75] H Egli. Un modelo matemático para cálculos no deterministas. Informe técnico, ETH Zürich, 1975.

[Kön32] D König. Theorie der endlichen und unendlichen Graphen. Informe técnico, Leipzig, 1932.

[Plo76] GD Plotkin. Una construcción de powerdomain. SIAM Journal on Computation , 5 (3): 452-487, 1976.

Descargo de responsabilidad: esto se toma casi al pie de la letra de un libro que una vez escribí en colaboración:

WP de Roever y K Engelhardt. Refinamiento de datos: métodos de prueba orientados a modelos y su comparación . Cambridge University Press, 1998.

Kai
fuente
44
La frase "esto se toma casi al pie de la letra de un libro que una vez escribí en colaboración" probablemente debería tener como prefijo "Extra Awesomeness:" no "Disclaimer:" :-D. Gracias, esto es muy útil.
Rob Simmons
Una forma de ver el no determinismo (y la forma en que quiero verlo) es que es una forma de subespecificación : un programa con una opción no determinista es refinado por el programa que siempre toma la primera opción, siempre toma la segunda opción, o (vea el extenso trabajo de McIver y Morgan en esta área en particular) el programa que toma una opción u otra con probabilidad .5 . Entonces, el ciclo que no termina de manera determinista se refina por el ciclo que nunca termina, y también por su ciclo de lanzamiento de moneda que termina (con probabilidad 1)
Rob Simmons