Teoría de tipos intuicionistas
La teoría de tipos intuicionista (también conocida como teoría de tipos constructiva o teoría de tipos de Martin-Löf ) es una teoría de tipos y una base alternativa de las matemáticas . La teoría de tipos intuicionista fue creada por Per Martin-Löf , un matemático y filósofo sueco , quien la publicó por primera vez en 1972. Hay múltiples versiones de la teoría de tipos: Martin-Löf propuso variantes tanto intensionales como extensionales de la teoría y las primeras versiones impredicativas , demostrado ser inconsistente por la paradoja de Girard , dio paso a predicativasversiones. Sin embargo, todas las versiones mantienen el diseño básico de lógica constructiva utilizando tipos dependientes.
Martin-Löf diseñó la teoría de tipos sobre los principios del constructivismo matemático . El constructivismo requiere que cualquier prueba de existencia contenga un "testigo". Entonces, cualquier prueba de "existe un primo mayor que 1000" debe identificar un número específico que sea primo y mayor que 1000. La teoría de tipos intuicionista logró este objetivo de diseño internalizando la interpretación BHK . Una consecuencia interesante es que las demostraciones se convierten en objetos matemáticos que pueden examinarse, compararse y manipularse.
Los constructores de tipos de la teoría intuicionista de tipos se construyeron para seguir una correspondencia uno a uno con los conectivos lógicos. Por ejemplo, el conectivo lógico llamado implicación ( ) corresponde al tipo de función ( ). Esta correspondencia se denomina isomorfismo de Curry-Howard . Las teorías de tipos anteriores también habían seguido este isomorfismo, pero Martin-Löf fue el primero en extenderlo a la lógica de predicados mediante la introducción de tipos dependientes .
La teoría de tipos intuicionista tiene 3 tipos finitos, que luego se componen utilizando 5 constructores de tipos diferentes. A diferencia de las teorías de conjuntos, las teorías de tipos no se basan en una lógica como la de Frege . Entonces, cada característica de la teoría de tipos cumple una doble función como característica tanto de las matemáticas como de la lógica.
Si no está familiarizado con la teoría de tipos y conoce la teoría de conjuntos, un resumen rápido es: Los tipos contienen términos al igual que los conjuntos contienen elementos. Los términos pertenecen a un solo tipo. Términos como y calcular ("reducir") hasta términos canónicos como 4. Para obtener más información, consulte el artículo sobre la teoría de tipos .
Hay 3 tipos finitos: El 0 de tipos contiene 0 términos. El tipo 1 contiene 1 término canónico. Y el tipo 2 contiene 2 términos canónicos.