La teoría de tipos es cualquier sistema formal , que es una alternativa a la teoría de conjuntos ingenua , acompañada de una clasificación de los elementos de dicho sistema utilizando tipos que forman una cierta jerarquía. La teoría de tipos también se entiende como el estudio de tales formalismos.
La teoría de tipos es una base matemáticamente formalizada para diseñar, analizar y estudiar sistemas de tipos de datos en la teoría de los lenguajes de programación (sección de informática ). Muchos programadores usan este término para referirse a cualquier trabajo analítico que estudie sistemas de tipos en lenguajes de programación. En los círculos científicos, la teoría de tipos se entiende con mayor frecuencia como una rama más estrecha de las matemáticas discretas , en particular , el cálculo λ con tipos.
La teoría de tipos moderna se desarrolló en parte en el proceso de resolución de la paradoja de Russell y se basa en gran medida en el trabajo de Bertrand Russell y Alfred Whitehead " Principia mathematica " [1] .
La doctrina de los tipos se remonta a B. Russell, según la cual cualquier tipo se considera como un rango de significación de una función proposicional (proposicional). Además, se cree que cada función tiene un tipo (su dominio, alcance). En la doctrina de los tipos se respeta la factibilidad del principio de sustitución de un tipo (proposición) por un tipo (proposición) definicionalmente equivalente .
Esta teoría se basa en el principio de jerarquía. Esto significa que los conceptos lógicos ( enunciados , individuos, funciones proposicionales) están ordenados en una jerarquía de tipos. Es esencial que una función arbitraria tenga como argumentos sólo aquellos conceptos que la preceden en la jerarquía.
Una determinada teoría de tipos suele entenderse como lógica aplicada de órdenes superiores, en la que existe un tipo N de números naturales y en la que se satisfacen los axiomas de la aritmética de Peano . .
Históricamente, la primera teoría de tipos propuesta (el período de 1902 a 1913) es la Teoría Ramificada de Tipos ( RTT ) , construida por Whitehead y Russell, y finalmente formulada en la obra fundamental Principia Mathematica . Esta teoría se basa en el principio de limitar el número de casos cuando los objetos pertenecen a un solo tipo. Ocho de estos casos se declaran explícitamente y se distinguen dos jerarquías de tipos: (simplemente) "tipos" y "órdenes". Al mismo tiempo, la notación de "tipo" en sí no está definida, y hay una serie de otras imprecisiones, ya que la intención principal era declarar tipos desiguales de funciones a partir de un número diferente de argumentos o de argumentos de diferentes tipos [2] . Una parte integral de la teoría es el axioma de reducibilidad .
En la década de 1920, Chwistek y Ramsey propusieron una teoría de tipos no ramificados, ahora conocida como "Teoría de tipos simple" o Teoría de tipos simple , que colapsa la jerarquía de tipos, eliminando la necesidad del axioma de reducibilidad.
La Teoría Intuicionista de Tipos ( ITT ) fue construida por Per Martin-Löf .
La teoría de los sistemas de tipos puros ( eng. sistemas de tipos puros , PTS ) generaliza todos los cálculos de cubo lambda y formula reglas que permiten calcularlos como casos especiales. Fue construido independientemente por Berardi y Terlouw . Los sistemas de tipos puros operan solo con el concepto de un tipo, considerando todos los conceptos de otros cálculos solo en forma de tipos, por eso se les llama " puros ". No hay separación entre términos y tipos, entre diferentes capas (es decir , los géneros de tipos también se denominan tipos, solo que están relacionados con otro universo), e incluso las capas mismas no se denominan variedades , sino tipos (más precisamente, universos de tipos) . En general, un sistema de tipo puro se define por la noción de una especificación, cinco reglas estrictas y dos flexibles (que varían de un sistema a otro). La especificación de un sistema de tipo puro es un triple (S, A, R), donde esS el conjunto de géneros ( S orts), Aes el conjunto de axiomas ( A xioms) sobre estos géneros, y Res el conjunto de reglas ( Rules ). [3] [4] [5]
Las teorías de tipos de dimensiones superiores o simplemente las teorías de tipos superiores ( HTT ) generalizan las teorías de tipos tradicionales , lo que permite establecer relaciones de equivalencia no triviales entre tipos . Por ejemplo, si uno toma un conjunto de pares ( productos cartesianos ) de números naturales y un conjunto de funciones que devuelven un número natural , entonces no se puede decir que los elementos de estos conjuntos son pares iguales, pero se puede decir que estos conjuntos son equivalente. Se estudian los isomorfismos entre tipos y en bidimensionales, tridimensionales, etc. teorías tipo. Girard-Reynolds sentó todas las bases necesarias para la formulación de estas teorías , pero las teorías mismas se formularon mucho más tarde. [6] [7]nat × natnat -> nat
La teoría de tipos de homotopía ( ing. Homotopia type theory , HoTT ) generaliza teorías multidimensionales, estableciendo la igualdad de tipos a nivel de topologías . En las teorías multidimensionales, los conceptos de "equivalencia de tipos" e "igualdad de tipos" se consideran diferentes. Una innovación radical de la teoría de la homotopía es el axioma de univalencia , que postula que si los tipos son topológicamente equivalentes, entonces son topológicamente iguales.
La Teoría de Tipos Conscientes de los Costos ( CATT ) , formulada en 2020 , amplía los tipos funcionales con la información más simple sobre la complejidad algorítmica (la cantidad de pasos computacionales necesarios para obtener un resultado), lo que le permite verificar los programas no solo para la corrección semántica, sino también para la imposición. Restricciones de complejidad de tiempo. [8] Esto se hace a través del constructor de tipos de funciones dependientes . La formalización de la teoría requiere, entre otras cosas, tener en cuenta el problema de la detención , para lo cual las reglas de tipeo exigen que la llamada recursiva sea estrictamente menos compleja que la llamada con el valor actual del argumento. CATT permite distinguir una prueba entre "costo abstracto" que involucra pasos matemáticos (como una llamada recursiva) y "costo de máquina" teniendo en cuenta la eficiencia de las instrucciones implementadas físicamente (por ejemplo, que las operaciones aritméticas de suma y producto toman el mismo tiempo en la mayoría de los procesadores), y también tener en cuenta el paralelismo . funtime
![]() |
---|