Defensa Tesis Licenciatura Lucas Rafael Romero
19 marzo, 2020 @ 11:00 am - 12:00 pm
Titulo: Una extensión polimórfica para los λ-cálculos cuánticos λρ y λρ°
Director: Alejandro Díaz-Caro
Jurados: Hernán Melgratti – Andrés Viso
Resumen:
En 2017 Díaz-Caro presentó dos extensiones al cálculo lambda simplemente tipado que modelaban el cómputo cuántico, llamadas λρ y λρ°. La novedad de estos cálculos radica en que representan los sistemas cuánticos mediante sus matrices de densidad asociadas haciendo que el cálculo esté más cercano a su semántica. El paper original contiene las demostraciones de las propiedades de subject reduction y progreso. En 2019 Borgna demostró en su tesis de licenciatura la normalización fuerte de los cálculos mediante una traducción al cálculo cuántico λq de Selinger y Valiron.
Este trabajo apunta a extender ambos cálculos con un sistema de tipado polimórfico a la Curry, extensión de System F, y contextos de tipado un poco más permisivos. Sobre estas extensiones demostramos que se mantienen subject reduction y presentamos una demostración de normalización fuerte mediante candidatos de reducibilidad. También probamos que λρ° es confluente, y utilizando la noción de confluencia probabilística definida por Martínez en 2018, presentamos las dificultades y posibles enfoques para lograr la confluencia de λρ.
