Teoría de tipos intuicionista
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 intensionales y extensionales de la teoría y versiones impredicativas tempranas, demostrado ser inconsistente por la paradoja de Girard , dio paso a predicativoversiones. Sin embargo, todas las versiones mantienen el diseño central de la 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". Por lo tanto, cualquier prueba de que "existe un número primo mayor que 1000" debe identificar un número específico que sea tanto primo como mayor que 1000. La teoría de tipos intuicionista logró este objetivo de diseño al internalizar la interpretación BHK . Una consecuencia interesante es que las demostraciones se convierten en objetos matemáticos que se pueden examinar, comparar y manipular.
Los constructores de tipos de la teoría intuicionista de tipos se construyeron para seguir una correspondencia uno a uno con conectores lógicos. Por ejemplo, el conectivo lógico llamado implicación ( ) corresponde al tipo de una función ( ). Esta correspondencia se llama 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 construyen sobre una lógica como la de Frege . Por lo tanto, 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 breve resumen 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 tipo 0 contiene 0 términos. El tipo 1 contiene 1 término canónico. Y el tipo 2 contiene 2 términos canónicos.