Agregando polimorfismo a una lógica que identifica proposiciones isomorfas

Título:

Agregando polimorfismo a una lógica que identifica proposiciones isomorfas

Autor:

Sottile, Cristian

Otros autores / Colaboradores:

 Díaz Caro, Alejandro; [ Director/a]  Pons, Claudia Fabiana; [ Codirector/a] 

Temas:

CÁLCULO LAMBDA; POLIMORFISMO; 

URL:

http://sedici.unlp.edu.ar/handle/10915/118544,

Palabras clave:

teoría de tipos, 

Nota de tesis:

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

Extensión:

1 archivo (3,1 MB)

Resumen:

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 AaB y BaA, 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 dichas proposiciones son equivalentes. 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. En este trabajo proponemos una extensión de Sistema I hacia polimorfismo, añadiendo al sistema de tipos el cuantificador universal y sus isomorfismos relacionados.

Puede solicitar más fácilmente el ejemplar con: TES 20/72

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