Tengo dificultades para comprender la prueba de una fuerte normalización para el cálculo de las construcciones. Trato de seguir la prueba en el documento de Herman Geuvers "Una prueba corta y flexible de Normalización Fuerte para el Cálculo de Construcciones".
Puedo seguir bien la línea principal de razonamiento. Geuvers construye para cada tipo una interpretación basado en alguna evaluación de las variables de tipo . Y luego construye algún término interpretación basado en alguna evaluación de las variables de término y demuestra que para evaluaciones válidas la afirmación para todos sostiene.
Mi problema: para los tipos fáciles (como los tipos del sistema F), la interpretación de tipos es realmente un conjunto de términos, por lo que la afirmación tiene sentido. Pero para los tipos más complejos, la interpretación no es un conjunto de términos, sino un conjunto de funciones de algún espacio de funciones apropiado. Creo que casi entiendo la construcción de los espacios de funciones, sin embargo, no puede asignar ningún significado a para los tipos más complejo .
¿Alguien puede explicar o dar enlaces a algunas presentaciones más comprensibles de la prueba?
Editar: Déjame intentar aclarar la pregunta. Un contexto tiene declaraciones para las variables de tipo y las variables de objeto. Una valoración de tipo es válida, si para todos con entonces es válida. Pero puede ser un elemento de y no solo . Por lo tanto, no se puede definir un término válido de evaluación para . debe ser un término y no una función de un espacio de funciones.
Edición 2: ejemplo que no funciona
Hagamos la siguiente derivación válida:
En el último contexto, una evaluación de tipo válida debe satisfacer . Para este tipo de evaluación no existe un término válido de evaluación.
Respuestas:
Desafortunadamente, no estoy seguro de que haya más recursos amigables para principiantes que la cuenta de Geuvers. Puede probar esta nota de Chris Casinghino que da cuenta de varias pruebas con detalles insoportables.
No estoy seguro de comprender la esencia de su confusión, pero creo que una cosa importante a tener en cuenta es el siguiente lema (Corolario 5.2.14), probado en el texto clásico de Barendregt :
Esto significa que mientras[[T]]ξ puedeser una función complicada,si Γ⊢M:T tiene, entonces[[T]]ξ
fuente