¿Cuáles son las diferencias entre relaciones lógicas y simulaciones?

29

Soy un principiante trabajando en métodos que prueban la equivalencia del programa. He leído algunos artículos sobre la definición de relaciones lógicas o simulaciones para demostrar que dos programas son equivalentes. Pero estoy bastante confundido acerca de estas dos técnicas.

Solo sé que las relaciones lógicas se definen inductivamente mientras que las simulaciones se basan en la coinducción. ¿Por qué se definen de esa manera? ¿Cuáles son sus pros y sus contras respectivamente? ¿Cuál debo elegir en diferentes situaciones?

Hongjin Liang
fuente
1
Es posible que desee proporcionar enlaces a estos documentos que ha leído. Esto aclararía qué ejemplos específicos te confunden.
Marc Hamann
1
Para las relaciones lógicas, he leído el reciente artículo de Hur y Dreyer "Una relación lógica de Kripke entre ML y ensamblaje" (POPL'11). También he leído los capítulos clásicos en el libro de Pierce "Temas avanzados en tipos y lenguajes de programación". Creo que las relaciones lógicas se definen inductivamente en la estructura de tipos del lenguaje, pero ¿qué sucede si el lenguaje no tiene una estructura de tipos (como C)? (Parece otra pregunta, supongo.)
Hongjin Liang
1
Para simulaciones, he leído el documento original "Leyes algebraicas para el no determinismo y concurrencia" de Hennessy y Milner. Koutavas and Wand's "Small bisimulations for razonamiento sobre programas imperativos de orden superior" (POPL'06) es incomprensible para mí y no estoy seguro de por qué llamaron a su método "bisimulación".
Hongjin Liang
3
Sería mejor si incluye la información que ha proporcionado en los comentarios en la publicación. Puede editar su pregunta haciendo clic en el enlace de edición debajo de la pregunta.
Kaveh
1
@HongjinLiang: si no tiene una estructura de tipos (o si tiene tipos recursivos), puede usar relaciones lógicas indexadas por pasos; con las relaciones lógicas, use la inducción en los tipos, con la indexación por pasos, haga la inducción en los pasos de observación. Encontrará sugerencias en la declaración de investigación de Amal Ahmed: ccs.neu.edu/home/amal/ahmed-research.pdf . (Otra descripción general de la investigación sobre relaciones lógicas es esta charla de Derek Dreyer y en su declaración de investigación: mpi-sws.org/~dreyer/research.pdf ).
Blaisorblade

Respuestas:

20

Tengo una respuesta a esta pregunta que posiblemente sea nueva. De hecho, todavía lo estoy pensando durante los últimos 6 meses más o menos, y aún no se ha escrito en los periódicos.

La tesis general es que los principios de razonamiento relacional como "relaciones lógicas", "simulaciones" e incluso "invariantes" son manifestaciones de abstracción de datos u ocultamiento de información. Dondequiera que haya información oculta, estos principios surgen.

Las primeras personas en descubrirlo fueron los teóricos de los autómatas. Los autómatas tienen estado oculto. Por lo tanto, necesita un razonamiento relacional para hablar sobre su equivalencia. Los teóricos de los autómatas lucharon con los homomorfismos durante un tiempo, se rindieron y se les ocurrió una noción llamada "cobertura relacional", que es una forma de relaciones de simulación.

Milner recogió la idea en un artículo poco conocido pero muy fundamental llamado " Una noción algebraica de simulación entre programas " en 1971. Hoare lo sabía y lo usó para elaborar la " Prueba de corrección de las representaciones de datos " en 1972 (pero utilizó la abstracción funciona en lugar de las relaciones porque pensaba que eran "más simples"). Más tarde se retractó de la afirmación de simplicidad y volvió a usar las relaciones en " Refinamiento de datos refinado ". Reynolds utilizó el razonamiento relacional en " Craft of Programming"", Capítulo 5 (1981). Pensó que las relaciones eran más naturales y generales que las funciones de abstracción. Si regresa y lee este capítulo, encontrará ideas de paramétrica relacional que acechan, esperando ser descubiertas. Efectivamente, dos años después, Reynolds publicó "Tipos, abstracción y polimorfismo paramétrico" (1983).

Parece que todas estas ideas no tienen nada que ver con los tipos, pero realmente lo tienen. Los lenguajes y modelos con estado tienen abstracción de datos incorporada . No necesita definir un "tipo de datos abstractos" para ocultar la información. Simplemente declara una variable local y la oculta. Podemos enseñarlo a estudiantes de primer año en clases de Java en las primeras semanas. Sin sudar.

Los lenguajes y modelos funcionales, por otro lado, tienen que ocultar su información mediante tipos . Los modelos funcionales no tienen abstracción de datos incorporada. Tenemos que agregarlo explícitamente, usando o . Entonces, si traduce un lenguaje con estado a un lenguaje funcional, notará que todo el estado local se traduce en variables de tipo. Para una descripción explícita de cómo funciona esto, vea mi artículo " Objetos y clases en lenguajes similares a Algol ", pero las ideas realmente provienen de Reynolds 1981 ("La esencia de Algol"). Estamos entendiendo mejor esas ideas clásicas ahora.

Tome dos máquinas y M que quiera probar equivalentes. Milner 1971 dice, define una relación entre los estados de M y M ' y muestra que las dos máquinas preservan la relación. La parametricidad de Reynolds dice: piense en los estados de las máquinas como pertenecientes a los tipos X y X ' . Defina una relación R entre ellos. Si las máquinas son de tipo F ( X ) y F ( X ' ) , parametrizadas por los tipos de sus estados, compruebe que las dos máquinas están relacionadas por la relación FMETROMETROMETROMETROXXRF(X)F(X) . F(R)

Entonces, las simulaciones y la parametricidad relacional son esencialmente la misma idea . No es simplemente un parecido superficial. El primero está hecho para lenguajes con estado donde hay abstracción de datos incorporada. Este último está hecho para lenguajes sin estado donde la abstracción de datos se obtiene a través de variables de tipo.

¿Qué pasa con las relaciones lógicas entonces? En la superficie, las relaciones lógicas parecen ser una idea más general. Mientras que la parametricidad habla sobre cómo relacionar las variables de tipo dentro del mismo modelo, las relaciones lógicas parecen relacionar tipos en diferentes modelos. (Dave Clarke escribió una exposición brillante de esto antes). Pero mi sensación es (y aún debe demostrarse) que esta es una instancia de alguna forma de parametricidad de tipo superior que aún no se ha formulado. Estén atentos para más progreso en ese frente.


[Nota agregada] La conexión entre las relaciones lógicas y las simulaciones se discute en nuestro artículo reciente Relaciones lógicas y paramétrica: Un programa de Reynolds para teoría de categorías y lenguajes de programación .

Uday Reddy
fuente
Me preguntaba si sería cierto decir que la relación mencionada anteriormente es la llamada elevación de relación de R dado que F describe la máquina. F(R)Rfunctor F
Dave Clarke
@DaveClarke Sí, es la misma idea. En el estilo de definición de Reynolds, cada constructor de tipo viene equipado con una acción de relación que asocia, a cada relación R : X X , una relación correspondiente F ( R ) : F ( X ) F ( X ) que satisface algunos axiomas En algunas otras comunidades, les gustaría derivar F ( R ) de otros principios, de donde los llaman levantamientos de relaciones . El F (FR:XXF(R):F(X)F(X)F(R) que producen por este proceso sería una acción de relación en el sentido de Reynolds. F(R)
Uday Reddy
14

Una de las diferencias clave es que las relaciones lógicas se usan como una técnica para mostrar que una clase de programas (por ejemplo, entrada a un compilador) corresponde a otra clase de programas (por ejemplo, la salida del compilador), mientras que las relaciones de simulación se usan para mostrar la correspondencia entre dos programas.

La similitud entre las dos nociones es que ambas definen una relación utilizada para mostrar la correspondencia entre dos entidades diferentes. En cierto sentido, uno puede pensar en una relación lógica como una relación de simulación que se define inductivamente en la sintaxis de los tipos. Pero existen diferentes tipos de relaciones de simulación.

Las relaciones lógicas se pueden usar para mostrar la correspondencia entre un lenguaje como ML y su traducción al lenguaje ensamblador, como en el documento que lee. Una relación lógica se define inductivamente en la estructura de tipo. Una relación lógica proporciona un medio compositivo para mostrar, por ejemplo, que una traducción es correcta, al mostrar que la traducción es correcta para cada tipo de constructor. En los tipos de función, la condición de condición de corrección diría algo así como, la traducción de esta función toma una entrada bien traducida a una salida bien traducida.

Las relaciones lógicas son una técnica versátil para lenguajes basados ​​en el cálculo lambda. Otras aplicaciones de relaciones lógicas incluyen (a partir de aquí ): caracterizar la definibilidad lambda, relacionar definiciones semánticas denotacionales, caracterizar polimorfismo paramétrico, modelar interpretación abstracta, verificar representaciones de datos, definir semántica completamente abstracta y modelar estado local en lenguajes de orden superior.

Las relaciones de simulación se usan generalmente para mostrar la equivalencia de dos programas. Típicamente, estos programas producen algún tipo de observación, como enviar mensajes por canales. Un programa P simula otra Q si P puede hacer todo lo que Q puede hacer, aunque quizás más.

La bisimulación, aproximadamente, es dos relaciones de simulación juntas. Muestra que el programa P y simula el programa Q y que el programa Q puede simular el programa P y tiene una bisimulación, aunque generalmente existen condiciones adicionales. La entrada de Wikipedia sobre la bisimulación es un buen punto de partida (más preciso). Existen miles de variantes de la idea, pero es una idea fundamental que se ha reinventado en más o menos la misma forma informática, lógica modal y teoría de modelos. El artículo de Sangiorgi da una historia maravillosa de la idea.

Un artículo que establece una relación entre las dos nociones es una nota sobre las relaciones lógicas entre semántica y sintaxis, de Andy Pitts, que utiliza relaciones lógicas, en última instancia, una noción semántica definida sintácticamente, para demostrar una cierta propiedad sobre la bisimulación aplicativa , que es una noción puramente sintáctica.

Dave Clarke
fuente
Muchas gracias por tu explicación detallada! Leeré sus referencias e intentaré descubrir conexiones / diferencias profundas entre los dos.
Hongjin Liang
¿está seguro de la afirmación "Muestra que el programa P y simula el programa Q y que el programa Q puede simular el programa P y tiene una bisimulación"? Sea A = (a. (B + c)) + (a.b + ac) y B = a.b + ac cuando, por lo que puedo decir, A es similar a B, B es similar a A, pero A y B no son bisimilares.
András Salamon
@ András: Tienes razón. Mi declaración no es lo suficientemente precisa. La diferencia se abstrae con la frase "Algunas condiciones adicionales pueden estar presentes".
Dave Clarke
Hennessy y Milner definieron tres tipos de relaciones de equivalencia en su artículo original para la bisimulación y dieron algunos ejemplos para ilustrar sus diferencias. Su declaración original es en realidad la mediana en su documento, que es más débil que la bisimulación y más fuerte que la traza de equivalencia. No estoy seguro de qué equivalencia es mejor. Tal vez depende del uso práctico.
Hongjin Liang
La simulación también se utiliza como una técnica de prueba para establecer el refinamiento de datos entre dos tipos de datos. Cada una de esas pruebas de simulación relaciona clases enteras de programas. Ver, por ejemplo, [1] para más detalles. Esto sugiere que la distinción entre los dos conceptos es aún más borrosa. [1]: CAR Hoare, He J y JW Sanders. Preespecificación en refinamiento de datos. Cartas de procesamiento de información , 25: 71-76, 1987.
Kai
8

Los dos tipos de relaciones parecen usarse en diferentes contextos. Simulaciones lógicas para lenguajes mecanografiados y relaciones de simulación cuando se trata de cálculos de procesos o lógicas modales interpretadas sobre sistemas de transición. Dave Clarke ha proporcionado una explicación muy intuitiva, por lo que solo agregaré algunos consejos que pueden ayudar.

Se ha trabajado en caracterizar ambas nociones utilizando la interpretación abstracta. Puede que no sea lo que desea, pero al menos ambas nociones se tratan en el mismo marco matemático.

Samson Abramsky usó relaciones lógicas para probar la solidez y la terminación del análisis de rigurosidad para el cálculo perezoso de Lambda ( Interpretación abstracta, Relaciones lógicas y Extensiones Kan ). También demostró que las relaciones lógicas definen funciones de abstracción en el sentido de conexión de Galois de interpretación abstracta. Más recientemente, Backhouse y Backhouse mostraron cómo construir conexiones de Galois para tipos de orden superior a partir de conexiones de Galois para tipos base y que estas construcciones se pueden describir de manera equivalente utilizando relaciones lógicas ( Relaciones lógicas y Conexiones de Galois ). Por lo tanto, en el contexto específico de los lenguajes funcionales mecanografiados, las dos nociones son equivalentes.

Las relaciones de simulación caracterizan la preservación de la propiedad entre las estructuras de Kripke para varias lógicas modales y temporales. En lugar de tipos, tenemos modalidades en una lógica. Las relaciones de simulación también definen las conexiones de Galois y, por lo tanto, las abstracciones. Uno puede preguntar si estas abstracciones tienen propiedades especiales. La respuesta es que las abstracciones estándar son sólidas y las abstracciones basadas en relaciones de simulación están completas. La noción de integridad es con respecto a las conexiones de Galois, que pueden no coincidir con las interpretaciones intuitivas. Esta línea de trabajo ha sido desarrollada por David Schmidt ( Relaciones binarias que preservan la estructura para la abstracción del programa ), y Francesco Ranzato y Francesco Tapparo ( Preservación fuerte generalizada por interpretación abstracta ).

Vijay D
fuente
Su respuesta es muy útil para conectar los conceptos con la interpretación abstracta. ¡Gracias!
Hongjin Liang
Una pregunta sincera: no soy un experto, pero ¿Reynolds (1983, "Tipos, abstracción y polimorfismo paramétrico") ya no define relaciones lógicas que son conexiones de Galois (Sec. 6)? Las únicas diferencias que noto: no dice el término "conexión de Galois", sino solo los "functores adjuntos equivalentes entre órdenes parciales considerados como categorías", y se limita a los dominios. OTOH, Backhouse y Backhouse citan a Reynolds pero no discuten este reclamo, de una forma u otra.
Blaisorblade
6

Yo diría que los dos conceptos son algo vagos. Ambos tratan sobre relaciones binarias de mecanismos computacionales que de alguna manera encarnan una noción de igualdad. Las relaciones lógicas se definen por la inducción de la estructura tipográfica, mientras que las simulaciones se pueden definir como se desee, pero el término alude a la coinducción.

Es engañoso decir que las relaciones lógicas están restringidas a cálculos lambda o lenguajes secuenciales, aunque ahí es donde se originaron las relaciones lógicas. Por ejemplo, en nuestro trabajo sobre modelos completamente abstractos para el Sistema Fπ

Martin Berger
fuente
Su referencia es realmente buena! No he escuchado relaciones lógicas para programas concurrentes antes. ¡Gracias! Supongo que la dificultad de definir una relación lógica es encontrar la estructura tipográfica. Con la misma estructura de tipo, se puede definir una relación lógica entre diferentes lenguajes de programación. Por otro lado, una simulación requiere programas de modelado por un sistema de transición de estado, lo que podría ser incómodo si los programas se escriben para diferentes modelos de estado.
Hongjin Liang
¡Hola! Sí, encontrar una estructura tipográfica adecuada no siempre es fácil. Puede definir simulaciones utilizando diferentes sistemas de transición para los dos cálculos que desea comparar. Se podría argumentar que la definición de simulación débil hace exactamente eso. Todo lo que realmente necesita para definir simulaciones es una relación para comparar etiquetas de transición.
Martin Berger