Formalización de Fundaciones de la Matemática y Compiladores Correctos por Construcción
Resumen
El desarrollo de las teorías fundacionales de la Matemática aparecidas en el siglo XX ha dado lugar a numerosos avances científicos en lógica y en ciencias de la computación. La teoría de conjuntos propuesta inicialmente por Georg Cantor a finales del siglo XIX y luego axiomatizada por Zermelo y Fraenkel para evitar paradojas constituye una de las teorías fundacionales más estudiadas y aceptadas por la comunidad científica. Paralelamente a ésta se desarrolló la teoría de tipos a partir de las primeras propuestas realizadas por Bertrand Russell, luego con el cálculo lambda simplemente tipado de Alonzo Church y más adelante con Per Martin-Löf, entre otros. La teoría de tipos abrió el camino a una prolífica área de estudio en ciencias de la computación: por un lado los lenguajes de programación pueden expresar propiedades de corrección en el tipado de los programas, y por otro permiten escribir formalmente resultados matemáticos que pueden chequearse automáticamente, lo que se conoce como formalización de matemática.
En el transcurso de este doctorado hemos estudiado la teoría de tipos y su aplicación para desarrollar programas correctos por construcción, en particular compiladores. Mediante el uso de tipos dependientes se puede especificar en el tipo de un compilador la propiedad de corrección con respecto a las semánticas de los lenguajes; presentamos en la tesis una metodología que muestra los alcances y límites de esta propuesta. La teoría subyacente surge de considerar a los lenguajes como álgebras de términos de una signatura, lo cual nos llevó a estudiar álgebras heterogéneas y traducciones entre álgebras de distintas signaturas. El siguiente aporte de nuestro trabajo es la formalización en el lenguaje Agda de una librería con los principales conceptos de álgebra universal, incluyendo un sistema deductivo para la lógica de cuasi identidades y las nociones de morfismos entre signaturas y álgebras reducto asociadas a dichos morfismos.
Finalmente hemos estudiado uno de los problemas más famosos en teoría de conjuntos: la independencia de la hipótesis del continuo. La misma afirma que con la axiomatización de Zermelo y Fraenkel (ZF) no se puede probar ni refutar que existan conjuntos con cardinalidad mayor estricta a la de los números naturales y menor estricta a la de los números reales. Este resultado fue obtenido gracias a los aportes de Kurt Gödel en 1940 (quien probó que la hipótesis del continuo es consistente con ZF) y luego completado por Paul Cohen veinte años más tarde, quien introdujo la técnica de forcing para probar que la negación de la hipótesis del continuo también es consistente con ZF. El desarrollo matemático implicado en estos resultados conlleva un interés particular para realizarlo formalmente en un asistente de pruebas, y no existe hasta el momento una formalización completa. Lawrence Paulson realizó una importante contribución en el asistente de pruebas Isabelle hasta obtener una prueba formal del resultado de Gödel. En la última parte de esta tesis, presentamos los primeros pasos hacia una formalización de forcing iiitomando como punto de partida el trabajo de Paulson. En particular, definimos la extensión genérica de modelos transitivos contables y probamos la validez de algunos de los axiomas de ZF en ella.
Código fuente
En cada link se encuentra disponible el código fuente de las implementaciones desarrolladas en la tesis. Instrucciones sobre instalación y versiones en las que el código fue testeado se encuentran en los archivos README correspondientes.
* Un enfoque internalista para compiladores correctos