Teoría de tipos

La versión actual de la página aún no ha sido revisada por colaboradores experimentados y puede diferir significativamente de la versión revisada el 6 de diciembre de 2021; las comprobaciones requieren 2 ediciones .

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

Tipo Doctrina

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 .

Teoría de tipos en lógica

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.

Algo de teoría de tipos

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

Teoría de tipos ramificados

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 .

Teoría de tipos simple

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.

Teoría intuicionista de tipos

La Teoría Intuicionista de Tipos ( ITT ) fue construida por Per Martin-Löf .

Sistemas de tipos puros

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]

Teorías de tipos multidimensionales

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

Teoría del tipo de homotopía

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.

Teoría económica de tipos

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

Véase también

Notas

  1. ↑ "Fundamentos de las matemáticas": un libro fundamental de lógica matemática de tres volúmenes (Whitehead, Alfred N. Fundamentos de las matemáticas: en 3 volúmenes / A. N. Whitehead, B. Russell; Editado por G. P. Yarovoy, Yu. N. Radaev. - Samara : Editorial de la Universidad de Samara, 2005-2006 - ISBN 5-86465-359-4 )
  2. ↑ Modern Perspective on Type Theory, 2004 , 2b The Ramified Theory of Types RTT, p. 35.
  3. ↑ Barendregt, "Lambda Calculi with Types", 1992 , 5.2. Sistema de tipo puro, p. 96-114.
  4. ↑ Modern Perspective on Type Theory, 2004 , 4c Pure Type Systems, p. 116.
  5. ↑ Pierce, 2002 , pág. 493.
  6. ↑ Harper, "Teoría de tipos de dimensiones superiores", 2011 .
  7. ↑ Documentos de investigación de Robert Harper (enlace no disponible) . Consultado el 20 de octubre de 2016. Archivado desde el original el 30 de octubre de 2016. 
  8. ↑ Yue Niu, Robert Harper. Teoría del tipo consciente de los costos. - Universidad Carnegie Mellon, 2020. - arXiv : 2011.03660v1 .

Literatura

Enlaces

  Ir al elemento de Wikidata  diccionarios y enciclopedias