Comprender la prueba de una fuerte normalización del cálculo de las construcciones

9

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 T una interpretación [[T]]ξ basado en alguna evaluación de las variables de tipoξ(α) . Y luego construye algún término interpretación(|M|)ρ basado en alguna evaluación de las variables de términoρ(x) y demuestra que para evaluaciones válidas la afirmación(|M|)ρ[[T]]ξ para todosΓM:T sostiene.

Mi problema: para los tipos fáciles (como los tipos del sistema F), la interpretación de tipos [[T]]ξ es realmente un conjunto de términos, por lo que la afirmación(|M|)ρ[[T]]ξ tiene sentido. Pero para los tipos más complejos, la interpretación[[T]]ξ 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(|M|)ρ[[T]]ξ para los tipos más complejoT .

¿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 α:A y las variables de objeto. Una valoración de tipo es válida, si para todos (α:A)Γ con ΓA: entonces ξ(α)ν(A) es válida. Pero ν(A) puede ser un elemento de (SAT) y no solo SAT. 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:

[]:axiom[α:]α:variable introduction[α:]:weaken[](Πα:.):product formation[β:Πα:.]β:(Πα:.)variable introduction

En el último contexto, una evaluación de tipo válida debe satisfacer ξ(β)ν(Πα:.)={f|f:SATSAT} . Para este tipo de evaluación no existe un término válido de evaluación.

helmut
fuente
1
La mitad de las personas que lean esto pensarán que es SAT. Deberías explicar de qué se trata. Además, su derivación parece un poco extraña. La segunda línea no debería mencionar α en su conclusión, debería leer algo como [ α : ] : , ¿no debería? SATα[α:]:
Andrej Bauer el
Estoy usando la notación de Herman Geuvers (que parece ser estándar en este dominio). es el conjunto de todos los conjuntos saturados de expresiones lambda. Para la segunda línea de mi derivación: es la regla de introducción para las variables de un sistema de tipo puro. Esta regla dice Γ T : sSAT dondeses algún tipo. ΓT:sΓ,x:Tx:Ts
helmut
Entiendo cómo obtuviste la segunda línea, pero no es la premisa correcta para la formación de la tercera línea, ¿verdad? Qué regla da la tercera línea.
Andrej Bauer el
La regla de formación de producto de PTS dice . El cálculo de las construcciones tiene la reglar(,,). Esto me permite usar la primera y la segunda línea para derivar la tercera. Sin embargo, tuve un error tipográfico en mi publicación. Faltaba el tipo en la tercera línea que agregué ahora. r(s1,s2,s3;ΓA:s1;Γ,x:AB:s2Γ(Πx:A.B):s3r(,,)
helmut
¿No debería entonces la primera línea leer ? ¿O confundiste y ◻ en alguna parte? La segunda línea no puede ser la segunda premisa de la regla de formación del producto, porque eso significaría que está tratando de formar algo como α : . α en lugar de α : . . []:α:.αα:.
Andrej Bauer el

Respuestas:

6

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 :

ΓM:T  ΓT: or 

Esto significa que mientras [[T]]ξ puedeser una función complicada,si ΓM:T tiene, entonces[[T]]ξ

(|t|)σ[[T]]ξΓt:T:V()P(Term)V()=SAT

SAT

cody
fuente
1
Gracias por la explicación. Eso resuelve mi problema de no entender las funciones utilizadas en la prueba de Geuver. Ya tenía una sospecha al leer y releer el artículo de Geuver, pero lo dejaste muy claro.
helmut