La teoría de tipos se creó inicialmente para evitar paradojas en una variedad de lógicas formales y sistemas de reescritura . Posteriormente, la teoría de tipos se refirió a una clase de sistemas formales , algunos de los cuales pueden servir como alternativas a la teoría ingenua de conjuntos como base de todas las matemáticas.
Ha estado vinculado a las matemáticas formales desde Principia Mathematica hasta los asistentes de prueba actuales .
En una carta a Gottlob Frege (1902), Bertrand Russell anunció su descubrimiento de la paradoja en el Begriffsschrift de Frege . [1] Frege respondió rápidamente, reconociendo el problema y proponiendo una solución en una discusión técnica de " niveles ". Para citar a Frege:
Por cierto, me parece que la expresión "un predicado se predica por sí mismo" no es exacta. Un predicado es, por regla general, una función de primer nivel, y esta función requiere un objeto como argumento y no puede tenerse a sí misma como argumento (sujeto). Por lo tanto, preferiría decir "un concepto se predica de su propia extensión". [2]
Continúa mostrando cómo podría funcionar esto, pero parece retroceder. Como consecuencia de lo que se conoce como la paradoja de Russell, tanto Frege como Russell tuvieron que modificar rápidamente los trabajos que tenían en la imprenta. En un Apéndice B que Russell añadió a sus Principios de Matemáticas (1903) se encuentra su teoría "provisional" de tipos. El asunto atormentó a Russell durante unos cinco años. [3]
Willard Quine [4] presenta una sinopsis histórica del origen de la teoría de tipos y de la teoría de tipos "ramificada": tras considerar abandonar la teoría de tipos (1905), Russell propuso a su vez tres teorías:
Quine observa que la introducción por parte de Russell de la noción de "variable aparente" tuvo el siguiente resultado:
la distinción entre 'todos' y 'cualquiera': 'todos' se expresa mediante la variable ligada ('aparente') de cuantificación universal, que abarca un tipo, y 'cualquiera' se expresa mediante la variable libre ('real') que se refiere esquemáticamente a cualquier cosa no especificada independientemente de su tipo.
Quine descarta esta noción de "variable ligada" por considerarla " inútil aparte de cierto aspecto de la teoría de tipos ". [5]
Quine explica la teoría ramificada de la siguiente manera: "Se ha llamado así porque el tipo de una función depende tanto de los tipos de sus argumentos como de los tipos de las variables aparentes contenidas en ella (o en su expresión), en caso de que éstas excedan los tipos de argumentos". [5] Stephen Kleene en su Introducción a las metamatemáticas de 1952 [6] describe la teoría ramificada de tipos de esta manera:
Pero debido a que las estipulaciones de la teoría ramificada resultarían (citando a Quine) "onerosas", Russell en su Lógica matemática de 1908 basada en la teoría de tipos [7] también propondría su axioma de reducibilidad . En 1910, Whitehead y Russell, en sus Principia Mathematica, aumentarían aún más este axioma con la noción de matriz , una especificación totalmente extensional de una función. A partir de su matriz se podría derivar una función mediante el proceso de "generalización" y viceversa, es decir, los dos procesos son reversibles: (i) generalización de una matriz a una función (mediante el uso de variables aparentes) y (ii) el proceso inverso de reducción de tipo mediante sustitución de cursos de valores de argumentos por la variable aparente. Con este método se podría evitar la impredicabilidad. [8]
En 1921, Emil Post desarrollaría una teoría de las "funciones de verdad" y sus tablas de verdad, que reemplazan la noción de variables aparentes versus reales. De su "Introducción" (1921): "Mientras que la teoría completa [de Whitehead y Russell (1910, 1912, 1913)] requiere para la enunciación de sus proposiciones variables reales y aparentes, que representan tanto individuos como funciones proposicionales de diferentes tipos, y como resultado necesita la engorrosa teoría de tipos, esta subteoría utiliza sólo variables reales, y estas variables reales representan sólo un tipo de entidad, que los autores han elegido llamar proposiciones elementales". [9]
Casi al mismo tiempo, Ludwig Wittgenstein desarrolló ideas similares en su obra de 1922 Tractatus Logico-Philosophicus :
3.331 De esta observación obtenemos una visión más amplia: la teoría de tipos de Russell. El error de Russell se demuestra por el hecho de que al elaborar sus reglas simbólicas tiene que hablar de los significados de sus signos.
3.332 Ninguna proposición puede decir nada sobre sí misma, porque el signo proposicional no puede estar contenido en sí mismo (esa es toda la "teoría de los tipos").
3.333 Una función no puede ser su propio argumento, porque el signo funcional ya contiene el prototipo de su propio argumento y no puede contenerse a sí mismo...
Wittgenstein también propuso el método de la tabla de verdad. En sus 4.3 a 5.101, Wittgenstein adopta un trazo de Sheffer ilimitado como su entidad lógica fundamental y luego enumera las 16 funciones de dos variables ( 5.101 ).
La noción de matriz como tabla de verdad aparece todavía en los años 1940-1950 en el trabajo de Tarski, por ejemplo, en sus índices de 1946 "Matrix, ver: Tabla de verdad" [10]
Russell, en su Introducción a la Filosofía Matemática de 1920 , dedica un capítulo entero al "Axioma del infinito y los tipos lógicos" en el que expresa sus preocupaciones: "Ahora bien, la teoría de los tipos enfáticamente no pertenece a la parte terminada y segura de nuestro tema: gran parte de esta teoría es todavía incipiente, confusa y oscura, pero la necesidad de alguna doctrina de tipos es menos dudosa que la forma precisa que debería adoptar la doctrina y en conexión con el axioma del infinito es particularmente fácil ver la necesidad de alguna de esas doctrinas; doctrina". [11]
Russell abandona el axioma de reducibilidad : en la segunda edición de Principia Mathematica (1927) reconoce el argumento de Wittgenstein. [12] Al comienzo de su Introducción declara que "no puede haber duda... de que no hay necesidad de distinguir entre variables reales y aparentes...". [13] Ahora abraza plenamente la noción de matriz y declara "Una función sólo puede aparecer en una matriz a través de sus valores " (pero objeta en una nota al pie: "Ocupa el lugar (no del todo adecuadamente) del axioma de reducibilidad" [14 ] ). Además, introduce una nueva noción (abreviada, generalizada) de "matriz", la de una "matriz lógica... una que no contiene constantes. Por tanto, p | q es una matriz lógica". [15] Así, Russell prácticamente ha abandonado el axioma de reducibilidad, [16] pero en sus últimos párrafos afirma que de "nuestras proposiciones primitivas actuales" no puede derivar "relaciones dedekindianas y relaciones bien ordenadas" y observa que si hay una nuevo axioma para sustituir el axioma de reducibilidad "queda por descubrir". [17]
En la década de 1920, Leon Chwistek [18] y Frank P. Ramsey [19] notaron que, si uno está dispuesto a abandonar el principio del círculo vicioso , la jerarquía de niveles de tipos en la "teoría de tipos ramificada" puede colapsar.
La lógica restringida resultante se denomina teoría de tipos simples [20] o, quizás más comúnmente, teoría de tipos simples. [21] A finales de la década de 1920 y principios de la de 1930, R. Carnap, F. Ramsey, WVO Quine y A. Tarski publicaron formulaciones detalladas de la teoría de tipos simples. En 1940, Alonzo Church lo (re)formuló como un cálculo lambda simplemente mecanografiado . [22] y examinado por Gödel en 1944. Un estudio de estos desarrollos se encuentra en Collins (2012). [23]
Kurt Gödel en su Lógica matemática de Russell de 1944 dio la siguiente definición de "teoría de tipos simples" en una nota a pie de página:
Concluyó que (1) la teoría de tipos simples y (2) la teoría de conjuntos axiomáticos "permiten la derivación de las matemáticas modernas y al mismo tiempo evitan todas las paradojas conocidas" (Gödel 1944:126); además, la teoría de tipos simples "es el sistema de los primeros Principia [ Principia Mathematica ] en una interpretación apropiada... [M]uchos síntomas muestran muy claramente, sin embargo, que los conceptos primitivos necesitan una mayor elucidación" (Gödel 1944 :126).
La correspondencia Curry-Howard es la interpretación de pruebas-como-programas y fórmulas-como-tipos. La idea comenzó en 1934 con Haskell Curry y finalizó en 1969 con William Alvin Howard . Conectó el "componente computacional" de muchas teorías de tipos con las derivaciones en lógica.
Howard demostró que el cálculo lambda tipificado correspondía a la deducción natural intuicionista (es decir, la deducción natural sin la ley del tercero excluido ). La conexión entre tipos y lógica condujo a muchas investigaciones posteriores para encontrar nuevas teorías de tipos para lógicas existentes y nuevas lógicas para teorías de tipos existentes.
Nicolaas Govert de Bruijn creó la teoría de tipos Automath como base matemática para el sistema Automath, que podía verificar la exactitud de las pruebas. El sistema se desarrolló y agregó características con el tiempo a medida que se desarrollaba la teoría de tipos.
Per Martin-Löf encontró una teoría de tipos que correspondía a la lógica de predicados mediante la introducción de tipos dependientes , que se conoció como teoría de tipos intuicionista o teoría de tipos de Martin-Löf.
La teoría de Martin-Löf utiliza tipos inductivos para representar estructuras de datos ilimitadas, como los números naturales.
La presentación de Martin-Löf de su teoría utilizando reglas de inferencia y juicios se convierte en el estándar para presentar teorías futuras.
Thierry Coquand y Gérard Huet crearon el Cálculo de Construcciones , [25] una teoría de tipos dependientes para funciones. Con los tipos inductivos, se llamaría "el Cálculo de Construcciones Inductivas" y se convertiría en la base de Coq y Lean .
El cubo lambda no era una nueva teoría de tipos sino una categorización de las teorías de tipos existentes. Las ocho esquinas del cubo incluían algunas teorías existentes con cálculo lambda simplemente escrito en la esquina inferior y cálculo de construcciones en la superior.
Antes de 1994, muchos teóricos de tipos pensaban que todos los términos del mismo tipo de identidad eran iguales. Es decir, que todo fuera reflexividad. Pero Martin Hofmann y Thomas Streicher demostraron que las reglas del tipo de identidad no exigían esto. En su artículo, "El modelo grupoide refuta la unicidad de las pruebas de identidad", [26] demostraron que los términos de igualdad podían modelarse como un grupo donde el elemento cero era "reflexitividad", la suma era "transitividad" y la negación era "simetría".
Esto abrió una nueva área de investigación, la teoría del tipo de homotopía , donde la teoría de categorías se aplicó al tipo de identidad.