Agregando polimorfismo a una lógica que identifica proposiciones isomorfas

Abstract

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 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.