¿Cómo demostrar las relaciones entre "clases" de tipos?

8

Después de leer Efectos como Sesiones, Sesiones como Efectos , me preguntaba cómo podría tener lugar una prueba de equivalencia entre ambos, o incluso, una prueba de que los tipos de Sesiones son un Sistema de Tipo y Efecto.

De una manera más genérica, ¿cómo se puede probar una relación (por ejemplo, equivalencia) entre diferentes "clases" * de tipos? ¿Sería suficiente esa prueba de expresividad realizada por Orchard y Yoshida?

[*]: No sé cómo definirlo correctamente, no quiero usar "tipos de tipos" o "tipos de tipos".

cyberglot
fuente

Respuestas:

6

Un enfoque para tales preguntas es a través de codificaciones .

Digamos que tiene un idioma L1 y un idioma L2 y desea mostrar que de alguna manera son "iguales", puede hacer esto buscando una codificación

[[]]:L1L2

y luego demuestre que para todos los programas cumple lo siguiente:L1M,N

M1Niff[[M1]]2[[M2]]

Aquí es una noción elegida de equivalencia de programa para . Con el fin de hacer esto para lenguajes de tipos, uno mapas normalmente también -Tipos a por medio de una función que se extiende a entornos de escritura, tales que algo así se cumple lo siguiente:L i L 1 L 2iLiL1L2

i

Γ1M:αimpliesΓ2[[M]]:α
Aquí es el juicio de tipeo para . Todo el enfoque se llama abstracción completa .iLi

Con el fin de evitar la "maldición de la universalidad de la Iglesia-Turing", uno típicamente impone condiciones en , por ejemplo, que es compositivo, o cerrado bajo cambio de nombre inyectivo. más condiciones , más fuerte será el resultado de la abstracción completa.[[[]][[]]

Esto también es lo que intentan hacer Orchard y Yoshida (Teoremas 1 a 5), ​​aunque no lo logran.

Martin Berger
fuente