Título: Un estudio semántico sobre extensiones avanzadas del λ-cálculo: patrones y operadores de control
Director: Eduardo Bonelli
Jurados:
– Pablo Castro (Universidad Nacional de Río Cuarto, Argentina)
– Alejandro Díaz-Caro (Universidad Nacional de Quilmes e ICC, FCEN-UBA, Argentina)
– Miguel Pagano (FAMAF, Universidad Nacional de Córdoba, Argentina)

Dónde: Zoom, pero se transmitirá por streaming (el link se enviará un rato antes del comienzo de la defensa).

Resumen:
El siguiente trabajo presenta distintos análisis semánticos sobre fundamentos de lenguajes de programación funcional. En particular, se establece como objeto de estudio el λ-cálculo para luego focalizar especialmente en dos de sus extensiones, a saber: el Pure Pattern Calculus (PPC) y el λμ-cálculo de Parigot.
En un primer lugar se estudian estrategias de evaluación para λ-cálculo por medio del sistema de tipos intersección (no idempotente) V. El mismo es capaz de caracterizar (exactamente) los términos normalizantes. Esta herramienta permite establecer una igualdad observacional entre la conocida estrategia call-by-need –noción puramente sintáctica– y el concepto semántico de needed redexes.
Más precisamente, se introduce la reducción weak-head needed y se muestra que el sistema V identifica sintácticamente todos los redexes weak-head needed de un término.
PPC, introducido por Kesner y Jay, es una extensión del λ-cálculo con patrones dinámicos y pattern matching que permite abstraer virtualmente cualquier término. Esto dio lugar a dos nuevas formas de polimorfirmo: path polymorphism y pattern polymorphism. El primero se refiere a la definición de funciones que se aplican uniformemente a estructuras de datos arbitrarias, definidas de manera inductiva. Su escencia recae sobre patrones de la forma x y (i.e. la aplicación de dos variables), lo que permite descomponer una estructura de datos en sus diferentes partes. Este trabajo se enfoca en path polymorphism restringiendo el análisis al Calculus of Applicative Patterns (CAP), un nuevo formalismo que puede ser visto como el fragmento estático de PPC, lo que descarta la forma de pattern polymorphism. Se desarrolla un sistema de tipos estático para CAP, capaz de capturar path polymorphism mediante una combinación adecuada de
herramientas de tipado como: tipos constantes, aplicativos, unión y recursivos.
Las propiedades fundamentales de subject reduction y progress se satisfacen en el sistema propuesto, lo que garantiza el buen comportamiento dinámico del cálculo. Esto recae crucialmente en una novedosa noción de compatibilidad de patrones. A su vez, se desarrolla un algoritmo de type-checking eficiente median-
te la formulación de una variante dirigida por sintaxis del sistema de tipos. Esto involucra algoritmos de chequeo de equivalencia de tipos y subtipado, ambos basados en caracterizaciones coinductivas de estas relaciones.
En una tercera línea de investigación, se consideran programas con operadores de control. El objetivo es identificar aquellos programas con tales constructores cuyas semánticas de reducción se corresponden de manera exacta. Esto se logra introduciendo una relación ≃, definida sobre una presentación alternativa del λμ-cálculo con operadores explícitos llamada ΛM . El resultado se basa en dos ingredientes fundamentales: (1) la factorización de la reducción del λμ-cálculo en pasos multiplicativos y exponenciales mediante el uso de los nuevos
operadores explícitos introducidos; y (2) la traducción de los términos de ΛM en las Polarized Proof-Nets (PPN) de Laurent, de modo que cut-elimination en las PPN simula la reducción en ΛM. La relación ≃ propuesta caracteriza la equivalencia estructural de las PPN. Más aún, ≃ resulta ser una bisimulación fuerte con respecto a la reducción en ΛM , i.e. dos térmidos ≃-equivalentes tienen exactamente la misma semántica de reducción, un resultado que falla tanto para la σ-equivalencia de Regnier en el λ-cálculo como para la σ-equivalencia de Laurent en el λμ-cálculo.