Agregando polimorfismo a una lógica que identifica proposiciones isomorfas

Tesina (Licenciatura en Informática) - Universidad Nacional de La Plata. Facultad de Informática, 2020.

I Introducción y preliminares -- 1 Introducción -- 1.1 Motivación -- 1.2 El cálculo lambda como método de estudio -- 1.3 Nuestro aporte: una extensión polimórfica de Sistema I -- 1.4 Estructura del trabajo -- 2 Introducción al cálculo lambda -- 2.1 Orígenes -- 2.2 Definición -- 2.3 Computación -- 2.3.1 Sistemas de reescritura -- 2.3.2 Reescritura en el calculo lambda -- 2.3.3 Estrategias de reducción -- 3 Cálculo lambda y sistemas de tipos -- 3.1 Sistemas de tipos -- 3.2 Cálculo lambda simplemente tipado -- 3.2.1 El conjunto de los tipos -- 3.2.2 El conjunto de los términos -- 3.2.3 Reglas de tipado -- 3.2.4 Derivaciones de tipos -- 3.2.5 Propiedades de interés -- 3.3 Sistema F -- 3.3.1 Tipos y términos -- 3.3.2 Funciones relevantes -- 3.3.3 Reglas de tipado -- 3.3.4 Reglas de reducción -- 3.3.5 Ejemplos -- 3.4 Extensión con pares -- 4 Computación y Lógica: la correspondencia Curry-Howard -- 4.1 Deducción Natural -- 4.1.1 Definición -- 4.1.2 Construcción de pruebas -- 4.1.3 Simplificación de pruebas -- 4.2 Correspondencia Curry-Howard -- 4.2.1 Definición -- 4.2.2 Simplificación de pruebas y evaluación de programas -- 4.3 Conclusiones -- II Estado del arte -- 5 Isomorfismos en la programación y en la lógica -- 5.1 Definición -- 5.2 Caracterización -- 5.2.1 Cálculo lambda simplemente tipado con pares -- 5.2.2 Sistema F con pares -- 6 Conjunto I: sistemas módulo isomorfismos -- 6.1 Motivación -- 6.1.1 La perspectiva de la programación -- 6.1.2 La perspectiva de la lógica -- 6.2 Internacionalización de isomorfismos -- 6.2.1 Equivalencia entre tipos -- 6.2.2 Reglas de tipado -- 6.2.3 Equivalencia entre términos -- 6.2.4 Relación de reducción -- 6.3 Sistema I -- 6.3.1 Definición -- 6.3.2 Ejemplos -- III Nuestro aporte: Sistema I Polimórfico -- 7 Sistema I Polimórfico -- 7.1 Introducción -- 7.2 Definición -- 7.2.1 Funciones relevantes -- 7.2.2 Equivalencia entre tipos -- 7.2.3 Reglas de tipado -- 7.2.4 Equivalencia entre términos -- 7.2.5 Relación de reducción -- 7.3 Ejemplos -- 7.4 Propiedades -- 8 Conclusiones y trabajo futuro -- 8.1 Conclusiones -- 8.2 Trabajo futuro -- 8.2.1 Adición de conectivas -- 8.2.2 Terminación -- 8.2.3 Eta-expansión rule -- 8.2.4 Implementación y punto fijo