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):
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 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?
¿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?
lambda-calculus
type-theory
logic
Gilles 'SO- deja de ser malvado'
fuente
fuente
Respuestas:
En el primer sistema, lo que llama subtipo son estas dos reglas:
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:∨ → ⊥
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)Ω:A→A ⊥E
Pensamientos aleatorios: (quizás valga la pena preguntar esto en TCS)
Esto me lleva a conjeturar que las propiedades relacionadas son algo así como:
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→⊥)
fuente
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:M2 M1→M2 M1
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ónMNN 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.xx S,T1,…
Es por eso que no creo que haya una caracterización fácil sobre la normalización para los tipos de unión.
fuente