Caracterización de términos lambda que tienen tipos de unión

29

Muchos libros de texto cubren los tipos de intersección en el cálculo lambda. Las reglas de tipeo para la intersección se pueden definir de la siguiente manera (además del cálculo lambda simplemente tipado con subtipado):

ΓM:T1ΓM:T2ΓM:T1T2(I)ΓM:(I)

Los tipos de intersección tienen propiedades interesantes con respecto a la normalización:

  • Un término lambda se puede escribir sin usar la regla I si se está normalizando fuertemente.
  • Un término lambda admite un tipo que no contiene si tiene una forma normal.

¿Qué pasa si en lugar de agregar intersecciones, agregamos uniones?

ΓM:T1ΓM:T1T2(I1)ΓM:T2ΓM:T1T2(I2)

¿El cálculo lambda con tipos simples, subtipos y uniones tiene alguna propiedad similar interesante? ¿Cómo pueden caracterizarse los términos tipificables con unión?

Gilles 'SO- deja de ser malvado'
fuente
Interesante pregunta. ¿Podría decir que las interfaces de OOP corresponden a esto?
Raphael
Quizás te pueda interesar este cs.cmu.edu/~rwh/courses/refinements/papers/Barbaneraetal95/…
Fabio F.

Respuestas:

11

En el primer sistema, lo que llama subtipo son estas dos reglas:

Γ,x:T1M:SΓ,x:T1T2M:S(E1)Γ,x:T2M:SΓ,x:T1T2M:S(E2)

Corresponden a reglas de eliminación para ; sin ellos, el conectivo es más o menos inútil.

En el segundo sistema (con las conectivas y , a las que también podríamos agregar un ), las reglas de subtipo anteriores son irrelevantes, y creo que las reglas que tenía en mente son las siguientes:

Γ,x:T1M:SΓ,x:T2M:SΓ,x:T1T2M:S(E)Γ,x:M:S(E)

Por lo que vale, este sistema permite escribir (usando la regla ), que no se puede escribir solo con tipos simples, que tiene una forma normal, pero no se normaliza fuertemente .(λx.I)Ω:AAE


Pensamientos aleatorios: (quizás valga la pena preguntar esto en TCS)

Esto me lleva a conjeturar que las propiedades relacionadas son algo así como:

  • un término λ admite un tipo que no contiene si tiene una forma normal para todo que tiene una forma normal. ( falla ambas pruebas, pero el término λ anterior las pasa)MMNNδ
  • Se puede escribir un término λ sin utilizar la regla si f se normaliza fuertemente para todos los fuertemente normalizadores .MEMNN

Ejercicio: prueba que estoy equivocado.

También parece ser un caso degenerado, tal vez deberíamos considerar agregar a este tipo en la imagen. Por lo que recuerdo, ¿permitiría obtener ?A(A)

Stéphane Gimenez
fuente
Un buen punto sobre las reglas de subtipo, muestran que los tipos de unión no son tan naturales como las intersecciones (que se escriben ortogonalmente a flechas). Sobre la segunda parte, necesito pensar un poco más.
Gilles 'SO- deja de ser malvado'
Creo que responde el ejercicio, si estás hablando de tipos de unión. M=(λx.xx)(λy.y)
jmad
Acerca de call / cc: necesita más que solo términos lambda (como términos lambda-mu u otro marco), pero los sistemas de tipos son sistemas lógicos más complejos, en los que los tipos de unión pueden ser irrelevantes.
jmad
@jmad: De hecho, se necesitan tipos de intersección para escribir este término :-( ¿Quizás sería interesante considerar uniones e intersecciones juntas?
Stéphane Gimenez
Me interesaría un término λ que se pueda escribir con tipos de unión (rs. Con tipos de intersección) pero no con tipos simples (rs. Con tipos de intersección).
jmad
16

Solo quiero explicar por qué los tipos de intersección son adecuados para caracterizar clases de normalización (fuerte, cabeza o débil), mientras que otros sistemas de tipos no pueden. (de tipo simple o sistema F).

La diferencia clave es que debe decir: "si puedo escribir y entonces puedo escribir ". Esto a menudo no es cierto en los tipos sin intersección porque un término puede duplicarse:M2M1M2M1

(λx.Mxx)NMNN

y luego escribir significa que puede escribir ambas apariciones de pero no con el mismo tipo, por ejemplo Con los tipos de intersección puede transformar esto en: y el paso crucial ahora es realmente fácil: so puede con tipos de intersecciónMNNN

M:T1T2T3N:T1N:T2
M:T1T2T1T2T3N:T1T2
(λx.Mxx):T1T2T3N:T1T2
(λx.Mxx)N

Ahora sobre los tipos de unión: suponga que puede escribir con algún tipo de unión, luego también puede escribir y luego obtener algunos tipos Pero todavía tienes que demostrar que por cada , que parece imposible, incluso si es un tipo de unión.(λx.xx)(λy.y)λx.xxS,T1,

x:T1T2Tnxx:S
ix:Tixx:SS

Es por eso que no creo que haya una caracterización fácil sobre la normalización para los tipos de unión.

jmad
fuente