Cristian Fabián Sottile expuso la tesina de grado “Agregando polimorfismo a una lógica que identifica proposiciones isomorfas”
En marzo de 2020, Cristian Fabián Sottile expuso la tesina de grado “Agregando polimorfismo a una lógica que identifica proposiciones isomorfas”, con la que obtuvo la Licenciatura en Informática.
Este trabajo de grado, que contó con la dirección de Alejandro Díaz-Caro y la codirección de Claudia Pons, propone una extensión de Sistema I hacia polimorfismo, incorporando el cuantificador universal y sus isomorfismos relacionados al sistema de tipos .
Tanto los sistemas de tipos como los sistemas de pruebas distinguen elementos que tienen diferente forma aunque tengan el mismo significado, como pueden ser las pruebas de las conjunciones AB y BA, por lo cual una prueba de una no constituye una prueba de la otra, a pesar de que se puede demostrar, mediante la existencia de un isomorfismo, que las proposiciones son equivalentes.
Es importante tener en cuenta que, sistema I es un cálculo lambda simplemente tipado con pares, extendido con una teoría ecuacional obtenida a partir de los isomorfismos de tipos existentes entre los tipos simples con pares, de forma tal que las proposiciones con mismo significado son equivalentes.
Para alcanzar los objetivos de la tesina Cristian, en una primera instancia, analizó el trabajo ya realizado en torno a la familia de sistemas módulo isomorfismos, en particular Sistema I, y revisó las técnicas que se aplicaron en su desarrollo. Luego, propuso una extensión a este sistema con polimorfismo, llamado Sistema I Polimórfico. Además describió las diferentes características particulares del mismo: el conjunto de isomorfismos a identificar, y las consecuencias en la relación de tipado, reducción y equivalencia entre tipos y términos. Expuso los motivos de las decisiones de inclusión y exclusión de isomorfismos y de equivalencias entre tipos y términos y, finalmente, probó la correctitud del cálculo mediante la propiedad de preservación de tipos, que debido a la cantidad de isomorfismos internalizados no resulta trivial.
Como trabajo a futuro Cristian propone:
– Adicionar conectivas, por ejemplo un elemento neutro para la conjunción ⊤.
– Realizar una prueba de terminación, aplicando la técnica utilizada para demostrar normalización fuerte en Sistema I.
– Realiza una prueba de progresión mediante la incorporación de la K-expansión, entre otras reglas.
– Extender la implementación existente de Sistema I siguiendo el diseño de Sistema I Polimórfico.
– Desarrollar bibliotecas o extensiones para lenguajes como Haskell, Coq o Agda.