Defensa Tesis Licenciatura Luis Francisco Ziliani

• Titulo: Lambda Sigma_gc: Un lambda calculo basado en Lambda Sigma con Garbage Collection
• Alumno: Luis Francisco Ziliani
• Director: Alejandro Rios
• Jurados: Ariel Arbiser y Eduardo Bonelli
• Resumen:

Desde hace unos 20 años que distintos calculos de sustituciones explicitas han dado diferentes resultados en la forma de imitar al Lambda Calculo. Uno de los primeros, Lambda Sigma, ha sido inspiracion para muchos de ellos por su forma de componer sustituciones y por su forma de trabajar los indices de de Bruijn. Sin embargo, ningun calculo derivado de este logra combinar satisfactoriamente todas las buenas propiedades que se esperan de un calculo de sustituciones explicitas: preservacion de la normalizacion fuerte (PSN), simulacion del Lambda Calculo (Sim), metaconfluencia (MC), etc. En un reciente trabajo de D. Kesner se presenta un calculo derivado de Lambda x que tiene todas estas propiedades. Parte fundamental de este calculo es la eliminacion de "basura" - sustituciones que no modifican el termino a sustituir, que al componerse con otras sustituciones terminan generando mas basura, resultando en terminos con derivaciones infinitas que en el Lambda Calculo tradicional son fuertemente normalizantes. En este trabajo presentamos Lambda Sigma GC, un calculo basado en Lambda Sigma, que resulta de agregar una regla que elimina sustituciones "basura", y evita la composicion y/o distribucion de esta basura. Demostramos que este nuevo calculo presenta las mismas propiedades que Lambda Sigma. Ademas, demostramos que Lambda Sigma GC consigue incluir al termino de Mèllies en el conjunto de terminos fuertemente normalizantes, aunque PSN para este calculo sigue siendo una pregunta abierta. En el estudio de algunas propiedades del nuevo calculo hemos desarrollado herramientas logicas originales, que pueden servir a futuras extensiones de Lambda Sigma, y hemos abierto la discusion sobre como evitar la basura en calculos derivados de dicho calculo.