Defensa Tesis Licenciatura Ariel Mendelzon

• Tí­tulo: Una curiosa versión de lambda-dB basada en "swappings": aplicación a traducciones entre cálculos de sustituciones explícitas con nombres e índices.
• Directores: Alejandro Ríos, Beta Ziliani.
• Jurados: Eduardo Bonelli, Sergio Mera.
• Resumen:

Desde que Melliès demuestra que el cálculo lambda-sigma no posee la propiedad de preservación de la normalización fuerte (PSN), numerosos cálculos de sustituciones explícitas han visto la luz; el objetivo: solventar dicho inconveniente sin perder, a la vez, el abanico de propiedades que sí posee lambda-sigma, e intentando ganar -- también -- confluencia sobre metatérminos. En 2009, Delia Kesner presenta lambda-ex, formalismo con variables nombradas que posee todas las propiedades esperables de un cálculo de sustituciones explícitas. El objetivo de esta tesis es introducir el cálculo de sustituciones explícitas con índices à la de Bruijn lambda-rex, formalismo que resulta ser isomorfo a lambda-ex y que, por lo tanto, tiene exactamente las mismas propiedades. A su vez, y a diferencia de otros formalismos existentes, lambda-rex exhibe una notación extremadamente sencilla. Todo esto lo convierte en el primer cálculo con índices, sustituciones unarias y notación muy simple en poseer un conjunto completo de propiedades deseables. Junto con lambda-rex, se presentan otros dos cálculos indexados e isomorfos a lambda-x y a lambda-xgc: lambda-re y lambda-regc, respectivamente. Hasta donde sabemos, no se conocían al momento tales isomorfismos.