Tipos Dependientes y Demostradores Interactivos

Teóricas (cronograma)

• Juicios y proposiciones. Funciones y funciones dependientes. Pares y pares dependientes. Tipos unitario y vacío. Universos. Introducción a la teoría de tipos de Martin-Löf y lógica en Agda.
• Igualdad definicional vs. proposicional. Inducción en caminos. Recursión e inducción sobre números naturales. Razonamiento ecuacional.
• Propiedades de la igualdad: estructura de infinito-grupoide. Transporte. Recursión e inducción sobre números naturales (continuación).
• Propiedades del transporte (transportconst, apd, transporte vía una familia de caminos). Homotopía. Equivalencia de tipos. Recursión e inducción sobre tipos de datos inductivos.
• Axioma de univalencia. Estructura de groupoide de orden superior de los constructores de tipos. Predicados definidos inductivamente. Equivalencia de tipos.
• Tipos contráctiles, proposiciones, conjuntos, grupoides, etc. Lógica clásica. Equivalencia entre principios de razonamiento clásicos. Demostración de algunas equivalencias de tipos.
• Metateoría: Cálculo-lambda sin tipos. Alfa y beta-equivalencia. Confluencia. Ejemplos de formalización de tipos abstractos de datos y algoritmos.
• Metateoría: Punto de vista de Curry-Howard y normalización del cálculo-lambda simplemente tipado. Ejemplos de formalización de matemática y estructuras algebraicas.
• Metateoría: Sistema F. Formalización del cálculo-lambda simplemente tipado.
• Metateoría: Lógica de orden superior (HOL). Codificación de la igualdad a la Leibniz y el existencial en HOL. Pure type systems, cálculo de construcciones y cubo de Barendregt.
• Implementación de un asistente de demostración minimalista usando chequeo de tipos bidireccional.
• Tipos de datos inductivos: F-álgebras y unicidad de la F-álgebra inicial. Restricciones de positividad y paradojas asociadas. Tipos de datos coinductivos: F-coálgebras.
• Tipos inductivos de orden superior (HITs).

Material de las clases

• Clase 01: introducción a MLTT en Agda.
• Clase 02: inducción en naturales.
• Clase 03: ejemplo de recursión no primitiva.
• Clase 04: demostración de algunas equivalencias de tipos.
• Clase 05: preservación del invariante de árbol binario de búsqueda por inserción.
• Clase 06: interderivabilidad de principios de razonamiento clásicos.
• Clase 07: corrección del algoritmo de ordenamiento por inserción.
• Clase 08: teorema fundamental del cálculo en geometría sintética diferencial.
• Clase 09: formalización cálculo-lambda simplemente tipado.
• Clase 10: ejemplos de usos de tácticas básicas en Rocq.
• Clase 11: código fuente en Haskell de un asistente de demostración minimalista usando chequeo de tipos bidireccional.
• Clase 12: tipos de datos coinductivos.
• Clase 13: tipos inductivos de orden superior.

Guías de ejercicios

• Práctica 1: productos y sumas.
• Práctica 2: naturales e igualdad.
• Práctica 3: estructura de infinito-grupoide del tipo identidad y operador de transporte.
• Práctica 4: inducción y razonamiento ecuacional.
• Práctica 5: programas correctos por construcción.

Trabajos

• Parcial: equivalencia de expresiones regulares.
• TP 1A: corrección de la deducción natural clásica con respecto a la semántica bivaluada.
• TP 1B: semántica de lenguajes imperativos con triplas de Hoare.
• Ideas para TP2:
  1. Formalizar algún algoritmo y demostrar que es correcto con respecto a su especificación:
     1. Algoritmos de sorting; devuelven una permutación ordenada de la lista de entrada.
     2. Algoritmo de Euclides para el máximo común divisor.
     3. SAT solver: determinar si una fórmula es satisfactible en lógica proposicional clásica.
  2. Formalizar alguna estructura de datos y demostrar que las operaciones preservan el invariante:
     1. Árboles balanceados (AVLs, Red-Black Trees).
     2. Heaps binarios.
     3. Disjoint sets (union-find).
  3. Formalizar algún teorema matemático:
     1. Existen infinitos números primos.
     2. Definición de coeficientes binomiales y sus propiedades.
     3. Todo entero se puede escribir como un producto de números primos.
     4. Propiedades de cardinales (p. ej. argumento diagonal de Cantor; teorema de Cantor-Schröder-Bernstein).
     5. Teoremas de isomorfismo de grupos.
  4. Formalizar algún teorema de HoTT:
     1. Demostrar la equivalencia entre distintas nociones de equivalencia de tipos (Capítulo 4 de HoTT).

Objetivos

El curso se propone dar los fundamentos teóricos que subyacen a los asistentes de demostración interactiva de teoremas, y en particular a aquellos basados en teorías de tipos dependientes. Desde el punto de vista práctico, el curso se propone introducir a los estudiantes al uso de demostradores interactivos para la verificación de programas y la formalización de teoremas matemáticos.

Se espera que, después de haber aprobado el curso, los estudiantes:

• Entiendan los fundamentos de la correspondencia entre proposiciones y tipos, y en particular la importancia de los teoremas de preservación de tipos y normalización, tanto desde el punto de vista lógico-filosófico como desde el punto de vista lógico-matemático.
• Conozcan las principales teorías en las que se basan los asistentes de demostración y los principios lógicos que usan: lógica clásica vs. intuicionista, teoría de conjuntos vs. teoría de tipos, igualdad extensional vs. intensional, predicatividad vs. impredicatividad, relevancia vs. irrelevancia de demostraciones, axioma K y principio de univalencia.
• Se familiaricen con los conceptos teóricos necesarios para usar demostradores interactivos, y especialmente con las nociones de producto y suma dependiente, el tipo identidad, la noción de equivalencia de tipos y algunas nociones provenientes de la teoría homotópica de tipos (n-types y principio de univalencia).
• Adquieran experiencia práctica a través de la formalización de problemas de pequeña o mediana escala.

Bibliografía

• The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Disponible electrónicamente. Institute for Advanced Study, 2013.
• Philip Wadler, Wen Kokke y Jeremy G. Siek. Programming Language Foundations in Agda. Disponible electrónicamente. 2022.
• Benjamin C. Pierce y otros. Software Foundations series, volume 1: Logical Foundations, versión 6.7. Disponible electrónicamente. Electronic textbook, 2024.
• Morte Heine Sørensen y Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. Elsevier, 2006.