Título: Estrategias de prueba de normalización fuerte en cálculos lambda tipados
Director: Dr. Alejandro Díaz-Caro
Co-director: Dr. Pablo E. Martínez López
Consejero de estudios: Dr. Juan Pablo Galeotti

Jurados:
– Dra. Mariangiola Dezzani (Università di Torino)
– Dr. Giulio Guerrieri (University of Sussex)
– Dra. Femke van Raamsdonk (Vrije Universiteit Amsterdam)

Transmisión en vivo: https://youtube.com/live/9peCcw_U7FI

Resumen:

La terminación es una propiedad de seguridad deseable en lenguajes de programación. En lenguajes con reglas de ejecución no deterministas, como el λ–cálculo, tenemos dos variantes. Weak normalization (WN): existe un camino de ejecución que llega al resultado. Strong normalization (SN): todos los posibles caminos de ejecución llegan al resultado. Los principales λ–cálculos tipados satisfacen SN, estando sus pruebas entre los resultados más complejos en teoría de tipos.

La primera prueba de SN para el λ–cálculo simplemente tipado (STLC) fue introducida por Luis Elpidio Sanchis, miembro de esta Casa de Estudios, en 1965. Se publicó en 1967, el mismo año en el que William Walker Tait presentó una prueba de WN. Tait introdujo una técnica llamada computabilidad, que mostró tener gran capacidad de adaptación, siendo extendida por Jean-Yves Girard para demostrar SN en 1971, y para demostrar SN del λ–cálculo polimórfico en 1972. Fue renombrada a reducibilidad, y al día de hoy constituye la forma principal de demostrar SN en λ–cálculos. Siendo todo lo potente y concisa que es, también es una técnica abstracta que no aporta mucha intuición sobre por qué la propiedad vale. Aunque la validez de la propiedad ya se conocía, la comunidad científica continuó trabajando en pruebas alternativas. Se escribieron muchos papers analizando reducibilidad, introduciendo formas alternativas de demostrar SN, y haciendo comparaciones detalladas reducibilidad con las pruebas alternativas.

La técnica de medidas decrecientes es una de las principales alternativas para demostrar SN en λ–cálculos tipados. Consiste en asignar elementos de un orden bien fundado a los programas, de manera tal que un paso de computación lleva a decrecer el elemento asignado. La primera medida decreciente para STLC fue introducida por Gandy en 1980, asignando números naturales a términos mediante una interpretación en el dominio de las funciones hereditaria y estrictamente monótonas. En 1987 de Vrijer simplificó la medida de Gandy, usando un dominio similar de funcionales crecientes, proveyendo un refinamiento donde el número asignado es igual a la cantidad de pasos desde el camino de ejecución más largo desde el programa.

En esta tesis presentamos nuevas medidas decrecientes para dos sistemas. Para STLC, presentamos primero una medida basada en un cálculo con memoria que recuerda los argumentos consumidos, de forma tal que nos permite simular la ejecución de manera controlada, y contar la cantidad de argumentos recordados en el resultado. Usando el mismo cálculo con memorias, proveemos otra medida para STLC, en este caso mejorando una medida dada por Turing para una noción restringida de ejecución. La de Turing implica WN, y nosotros la extendimos para que implique SN. La suya está basada en multiset de grados; la nuestra agrega multiconjuntos anidados a cada grado, con información de simulaciones controladas de ciertos caminos de ejecución.

Extendimos la primera medida a tipos intersección idempotente (IIT), un sistema de asignación de tipos que introduce en STLC una forma finitaria de polimorfismo. Proveemos la primera medida nativa para IIT que decrece para cualquier paso de ejecución, dando una prueba directa de SN. Tiene un dominio más simple que las otras, los números naturales. Como la presentación de IIT es en general con tipado extrínseco, y nuestra técnica requiere tipado intrínseco, definimos una variante intrínseca y demostramos correspondencia y simulación con respecto a la versión extrínseca.

En medidas que dan números, el valor asignado a cada programa es una cota superior para la longitud de su camino de ejecución más largo. Una pregunta que surge es si dicho número se corresponde con esa longitud, que no es el caso de nuestra primera medida. Presentamos su refinamiento a exactitud, donde probamos que el número obtenido es una cota superior exacta para la longitud del camino de ejecución más largo. Para eso adaptamos la creación de memorias en el cálculo con memorias, de manera tal que solo los argumentos borrados son recordados. Discutimos el refinamiento a exactitud de la extensión a IIT, que es un trabajo en progreso.