¿Para qué idiomas ya existe una teoría de equivalencia observacional?

Para una prueba de corrección, estoy buscando una noción utilizable de equivalencia de programa para los sistemas de tipo puro (PTS) de Barendregt; falta eso, para suficientes sistemas de tipos específicos. Mi objetivo es simplemente usar la noción, no investigarla por sí misma. $\cong$

Esta noción debería ser " extensional ", en particular, para demostrar que , debería ser suficiente para demostrar que $t_1 \cong t_2$ para todos los valores del tipo apropiado. $t_1\; v \cong t_2\; v$ $v$

Equivalencia denotacional

La equivalencia denotacional satisface fácilmente todos los lemas correctos, pero una semántica denotacional para PTS arbitrario parece bastante desafiante: ya parece difícil para el Sistema F.

Equivalencia contextual / observacional

La alternativa obvia son las diversas formas de equivalencia contextual (dos términos son equivalentes si ningún contexto básico puede distinguirlos), pero su definición no se puede utilizar de inmediato; los diversos lemas no son triviales de probar. ¿Han sido probados para PTS? Alternativamente, ¿sería la teoría una "extensión obvia", o hay alguna razón para creer que la teoría sería significativamente diferente?

EDITAR: No dije lo que es difícil arriba.

Parte fácil: la definición

Definir la equivalencia no es demasiado difícil, y la definición aparece en muchos artículos (comenzando al menos desde el estudio de PCF de Plotkin 1975, si no antes, la fuente podría ser la tesis doctoral de Morris de 1968). We si para todos los contextos básicos , , es decir, y dan el mismo resultado $t_1 \cong t_2$ $C$ $C[t_1] \simeq C[t_2]$ $C[t_1]$ $C[t_2]$ $a \simeq b$ $a$ $b$

Parte difícil: las pruebas

Sin embargo, esos documentos a menudo no explican lo difícil que es realmente usar esta definición. Todas las referencias a continuación muestran cómo lidiar con este problema, pero la teoría necesaria es más difícil de lo que uno piensa. ¿Cómo demostramos que ? ¿Realmente hacemos análisis de casos e inducción en contextos? No quieres hacer eso. $t_1 \cong t_2$

Como señala Martin Berger, desea utilizar, en su lugar, bisimulación (como lo hizo Pitts) o una relación de equivalencia lógica (que Harper simplemente llama "equivalencia lógica").

Finalmente, ¿cómo se prueba la extensionalidad como se definió anteriormente?

Harper resuelve estas preguntas en 10 páginas para el Sistema T, a través de una considerable inteligencia y relaciones lógicas. Pitts toma más. Algunos idiomas son aún más complejos.

Como lidiar con esto

De hecho, estoy tentado de hacer mis pruebas condicionalmente en una teoría de equivalencia conjeturada para PTS, pero las teorías reales requieren argumentos no triviales, por lo que no estoy seguro de la probabilidad de que tal conjetura sea válida.

Soy consciente (aunque no en detalle) de los siguientes trabajos:

Andrew Pitts (por ejemplo, en ATTAPL para un Sistema F extendido, y en algunos documentos, como las "Teorías de equivalencia de programas de 58 páginas basadas en operaciones").
Fundamentos prácticos de los lenguajes de programación (capítulos 47-48), que está inspirado en Pitts (pero afirma tener pruebas más simples).
Un estudio lógico de equivalencia del programa . No puedo encontrar un resumen en inglés, pero parece gastar mucho esfuerzo para los efectos secundarios (referencias), lo que parece una complicación ortogonal.

pl.programming-languages type-theory operational-semantics Blaisorblade
fuente

⇓

$\Downarrow$

P ≅ Q

$P \cong Q$

C [\cdot]

$C[\cdot]$

C [P] ⇓

$C[P] \Downarrow$

C [Q] ⇓

$C[Q] \Downarrow$

@MartinBerger: esa es la idea que estoy insinuando, pero probarlo directamente es sorprendentemente difícil, porque necesitas hacer pruebas para todo C (lo explicaré mejor en la pregunta). Además, si todos los programas terminan, la definición que utiliza, como se indica, identifica todos los programas.

Blaisorblade

β η

$\beta\eta$

C [P] ⇓ t r u e

$C[P] \Downarrow true$

C [Q] ⇓ t r u e

$C[Q] \Downarrow true$

≅

$\cong$ y (2) fácil de manejar, por ejemplo, alguna noción de bisimilaridad o relación lógica. Depende de la aplicación.

Martin Berger

@Blaisorblade Probablemente. Los teóricos de la concurrencia han estado haciendo esto de manera intensiva durante mucho tiempo, porque con los procesos concurrentes es mucho menos claro qué noción de equivalencia utilizar. Esto ha llevado a una división del trabajo: use una semántica basada en la reducción con cuantificación sobre los contextos para definir la noción de equivalencia y luego use bisimulaciones o trazas sobre transiciones etiquetadas para probar la equivalencia (o la ausencia de la misma). Una gran pregunta de investigación abierta en la teoría de la concurrencia es cómo pasar de lo primero a lo último algorítmicamente.

Martin Berger

Respuestas:

$[\![ {-} ]\!]$

[[t_{1}]] = [[t_{2}]] ⟹ t_{1} ≅ t_{2} .

$[\![ t_1 ]\!] = [\![ t_2 ]\!] \implies t_1 \cong t_2.$

Andrej Bauer
fuente

≅

$\cong$

Gracias por la respuesta, pero -1: aunque estoy de acuerdo, la pregunta menciona sistemas de tipo puro: AFAICS, una semántica denotativa para sistemas de tipo puro es un problema abierto, por lo que creo que una respuesta debería apuntar a alguna semántica denotacional. (De hecho, si tuviera una semántica denotacional, prescindiría por completo de la operativa, como se menciona en la pregunta). (Pero perdón por la pregunta demasiado larga).

Blaisorblade

@ MartinBerger, no entiendo tu crítica. El OP pide métodos para mostrar equivalencia observacional, menciono uno común, y luego objetas que existen otras formas que evitan el método.

Andrej Bauer

@Blaisorblade, bueno, entonces solo tendrás que inventar una semántica denotacional para sistemas de tipo puro, ¿no? :-) Pero más en serio, le preguntaré a Alex Simpson, él sabría mejor sobre semántica denotacional para tales cosas.

Andrej Bauer

@AndrejBauer No pretendía ser una crítica, sino más bien una adición.

Martin Berger

$\eta$

cody
fuente

No creo que el doctorado de Streicher sea sobre PTS. Se trata de la semántica del cálculo de construcciones y los resultados de independencia a través de la semántica de confiabilidad. Ver aquí .

Martin Berger

¡Gracias por la aclaración! Sin embargo, me temo que el enlace está roto (y es difícil de solucionar con el enlace minimizado).

cody

El enlace fue a la tabla de contenido del libro aquí . Espero que este funcione mejor.

Martin Berger

λ^{*}

$\lambda^*$

@ MartinBerger: ¿te refieres a la semántica de realizabilidad?

Dominique Devriese

Esta respuesta sugiere un enfoque del problema. (Comentarios son bienvenidos).

El capítulo 49 de PFPL discute, a la vez, las nociones equivalentes de equivalencia observacional y equivalencia lógica. La equivalencia lógica es la misma relación utilizada para establecer la parametricidad, por lo que el núcleo del capítulo es una prueba de la parametricidad para el Sistema F.

El trabajo sobre parametricidad para PTS, AFAICT, no discute la relación con la equivalencia observacional. De hecho, incluso para definir la equivalencia observacional, a menos que tenga no terminación, necesita algún tipo de suelo positivo (naturales, booleanos) para usar en las observaciones.

Sin embargo, el teorema clave (PFPL 47.6, 48.3, 49.2) para relacionar las dos relaciones se demuestra independientemente del lenguaje específico:

La equivalencia observacional es la congruencia más gruesa y consistente en las expresiones.

Entonces, para mostrar que la equivalencia lógica implica equivalencia observacional, uno solo necesita demostrar que la equivalencia lógica es una congruencia consistente. Sin embargo, la otra dirección requiere más trabajo: en particular, para demostrar que la equivalencia lógica es una congruencia, se procede por inducción en contextos.

n + 1 = 1 + nVecN nnVecNVecN $n + 1 = 1 + n$ Vec (n + 1)Vec (1 + n)n + 11 + n

Blaisorblade
fuente