Reescritura, Cálculo-Lambda y Tipos
Teóricas (cronograma)
- Reescritura abstracta, nociones de confluencia y normalización y sus relaciones, inducción bien fundada, lema de König, resultados abstractos.
- Sistemas de reescritura de cadenas y de términos. Ortogonalidad y teorema de pares críticos.
- Órdenes de reducción. Órdenes lexicográficos y de multiconjuntos. Interpretaciones polinomiales. Lema de Newman revisitado.
- Path orderings (LPOs y RPOs). Algoritmo de compleción de Knuth--Bendix. Posiblemente: otras técnicas para probar terminación.
- Cálculo-lambda sin tipos. Alfa, beta y eta-conversión. Expresividad. Relación con la lógica combinatoria. Nociones de residuo y development. Casos de creación de redexes.
- Confluencia del cálculo-lambda. Postponement de la eta-reducción. Normalización de la estrategia head. Solubilidad y árboles de Böhm.
- Deducción natural proposicional. Cálculo-lambda simplemente tipado y su relación. Terminación débil vía argumento de Turing.
- System F. Codificaciones. Terminación a través de candidatos de reducibilidad.
- Sistemas de tipos con intersección y caracterización de la normalización.
- Sustituciones explícitas. Preservación de la normalización fuerte. Máquinas abstractas. Evaluación big-step.
Guías de ejercicios
Parciales
Bibliografía
- F. Baader, T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
- Terese. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, 2003.
- H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North Holland, 1984.
- M. H. Sørensen, P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Studies in Logic and the Foundations of Mathematics, vol. 149. Elsevier, 2006.