Título: Semántica dinámica de cálculos de sustituciones explícitas a distancia

Directores: Eduardo Bonelli y Delia Kesner.

Jurados:
Dr. Nazareno Aguirre (Universidad de Río Cuarto y CONICET)
Dr. Zena Ariola (University of Oregon)
Dr. Alexandre Miquel (Universidad de la República / Fing / IMERL)

Resumen:
Los cálculos de sustituciones explícitas son variantes del cálculo-lambda en los que la operación de sustitución no se define a nivel del metalenguaje, sino con reglas de reescritura que la implementan. Nuestro principal objeto de estudio es un cálculo de sustituciones explícitas particular, el Linear Substitution Calculus (LSC), definido por Accattoli y Kesner en 2010. Se caracteriza por el hecho de que las reglas de reescritura operan no localmente (a distancia). En esta tesis, en primer lugar, definimos máquinas abstractas que implementan estrategias de evaluación en el LSC: call-by-name para evaluación débil y fuerte, call-by-value y call-by-need. Demostramos que dichas máquinas son correctas y preservan la complejidad temporal. En segundo lugar, definimos una extensión de la estrategia de evaluación call-by-need en el LSC para evaluación fuerte. Demostramos que la estrategia es completa con respecto a call-by-name, usando un sistema de tipos intersección no idempotente, y mostramos cómo extenderla para lidiar con pattern matching y recursión. Por último, estudiamos la teoría de residuos y familias de radicales en el LSC. Para ello definimos una variante del LSC con etiquetas de Lévy, lo que nos permite demostrar que cumple con la propiedad de Finite Family Developments. Aplicamos esta propiedad para obtener resultados de optimalidad, estandarización y normalización de estrategias en el LSC, y generalizamos algunos de estos resultados al marco axiomático de Deterministic Family Structures.