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

• Práctica 1
• Práctica 2
• Práctica 3
• Práctica 4
• Práctica 5

Parciales

• 2023p1
• 2023p2
• 2023r1
• 2023r2

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.