Teoría de tipos

format_list_bulleted Contenido keyboard_arrow_down

ImprimirCitar

En matemáticas, lógica e informática, una teoría de tipos es un sistema formal en el que cada "término" tiene un "tipo". Un "tipo" en la teoría de tipos tiene un papel similar al de un "tipo" en un lenguaje de programación: dicta las operaciones que se pueden realizar en un término y, para las variables, los posibles valores con los que se puede reemplazar.

Algunas teorías de tipos sirven como alternativas a la teoría de conjuntos como fundamento de las matemáticas. Dos teorías de tipos influyentes que se propusieron como fundamentos son el cálculo λ tipado de Alonzo Church y la teoría de tipos intuicionista de Per Martin-Löf. La mayoría de los sistemas computarizados de redacción de pruebas utilizan una teoría de tipos como base. Uno común es el Cálculo de construcciones inductivas de Thierry Coquand.

La teoría de tipos está estrechamente relacionada y, en algunos casos, se superpone con los sistemas de tipos, que son una característica del lenguaje de programación utilizada para reducir errores y facilitar ciertas optimizaciones del compilador. Debido a que la teoría de tipos y los sistemas de tipos pueden superponerse, algunos expertos usan la frase "sistema de tipos" para referirse a un sistema formal específico y la frase "teoría de tipos" para referirse al estudio académico de ellos.

Historia

La teoría de tipos se creó para evitar una paradoja en una base matemática basada en la teoría de conjuntos ingenua y la lógica formal. La paradoja de Russell, que fue descubierta por Bertrand Russell, existía porque un conjunto podía definirse utilizando "todos los conjuntos posibles", que se incluían a sí mismos. Entre 1902 y 1908, Bertrand Russell propuso varias "teorías de tipos" para solucionar el problema. En 1908, Russell llegó a una teoría de tipos "ramificada" junto con un "axioma de reducibilidad", los cuales ocuparon un lugar destacado en Whitehead y Principia Mathematica de Russell.publicado entre 1910 y 1913. Este sistema evitó la paradoja de Russell al crear una jerarquía de tipos y luego asignar cada entidad matemática concreta (y posiblemente otra) a un tipo. Las entidades de un tipo determinado se construyen exclusivamente a partir de entidades de aquellos tipos que están más abajo en su jerarquía, evitando así que una entidad se defina utilizando a sí misma.

Los tipos no siempre se usaron en lógica. Había otras técnicas para evitar la paradoja de Russell. Los tipos ganaron terreno cuando se usaron con una lógica particular, el cálculo lambda de Alonzo Church.

El ejemplo temprano más famoso es el cálculo lambda de tipo simple de Church. La teoría de tipos de Church ayudó al sistema formal a evitar la paradoja de Kleene-Rosser que afectaba al cálculo lambda original sin tipos. Church demostró que podía servir como base de las matemáticas y se denominó lógica de orden superior.

La frase "teoría de tipos" ahora generalmente se refiere a un sistema tipificado basado en el cálculo lambda. Un sistema influyente es la teoría de tipos intuicionista de Per Martin-Löf, que se propuso como base para las matemáticas constructivas. Otro es el cálculo de construcciones de Thierry Coquand, que Coq, Lean y otros "asistentes de prueba" (programas computarizados de redacción de pruebas) utilizan como base. Las teorías de tipos son un área de investigación activa, como lo demuestra la teoría de tipos de homotopía.

Introducción

Hay muchas teorías de tipos, por lo que describirlas todas es difícil. Esta sección cubre las características de muchas de las principales teorías de tipos. Es una introducción para quienes no están familiarizados con la teoría de tipos. Esta sección no pretende ser una categorización completa de las teorías de tipos, ni una descripción exhaustiva de las mismas.

Lo esencial

Términos y tipos

En la teoría de tipos, cada término tiene un tipo. Un término y su tipo a menudo se escriben juntos como " término: tipo ". Un tipo común para incluir en una teoría de tipos son los números naturales, a menudo escritos como " $matemáticas N$ " o "nat". Otro son los valores lógicos booleanos. Entonces, algunos términos muy simples con sus tipos son:

0: nacional
42: nacional
cierto: bool

Los términos se pueden construir a partir de otros términos usando llamadas a funciones. En la teoría de tipos, una llamada de función se denomina "aplicación de función". La aplicación de funciones toma un término de un tipo dado y da como resultado un término de otro tipo dado. La aplicación de función se escribe " argumento de argumento de función...", en lugar de la " función (argumento, argumento, argumento,...)" convencional. Para números naturales, es posible definir una función llamada "suma" que toma dos números naturales. Así, algunos términos más con sus tipos son:

añadir 0 0: natural
suma 2 3: natural
agregar 1 (agregar 1 (agregar 1 0)): nat

En el último término, se agregaron paréntesis para indicar el orden de las operaciones. Técnicamente, la mayoría de las teorías de tipos requieren que los paréntesis estén presentes para cada operación, pero, en la práctica, no están escritos y los autores asumen que los lectores pueden usar la precedencia y la asociatividad para saber dónde están. Para una facilidad similar, es una notación común escribir " $x+y$ " en lugar de "agregar ". Entonces, los términos anteriores podrían reescribirse como: $X$ $y$

0 + 0: natural
2 + 3: natural
1 + (1 + (1 + 0)): natural

Los términos también pueden contener variables. Las variables siempre tienen un tipo. Entonces, asumiendo que "x" e "y" son variables de tipo "nat", los siguientes también son términos válidos:

x: natural
x + 2: natural
x + (x + y): nacional

Hay más tipos además de "nat" y "bool". Ya hemos visto el término "agregar", que no es un "nat", sino una función que, cuando se aplica a dos "nat", calcula un "nat". El tipo de "agregar" se tratará más adelante. Primero, necesitamos describir "computa a".

Cálculo

La teoría de tipos tiene una notación de cálculo incorporada. Los siguientes términos son todos diferentes:

1 + 4: natural
3 + 2: natural
0 + 5: nacional

pero todos computan al término "5: nat". En la teoría de tipos, usamos las palabras "reducción" y "reducir" para referirnos al cálculo. Entonces, decimos que "0 + 5: nat" se reduce a "5: nat". Se puede escribir "0 + 5: nat $doscabezaderechaflecha$ 5: nat". El cálculo es mecánico y se logra reescribiendo la sintaxis del término.

Los términos que contienen variables también se pueden reducir. Entonces el término "x + (1 + 4): nat" se reduce a "x + 5: nat". (Podemos reducir cualquier subtérmino dentro de un término, gracias al teorema de Church-Rosser).

Un término sin variables que no se pueden reducir más es un "término canónico". Todos los términos anteriores se reducen a "5: nat", que es un término canónico. Los términos canónicos de los números naturales son:

0: nacional
1: nacional
2: natural
etc.

Obviamente, los términos que computan al mismo término son iguales. Entonces, asumiendo "x: nat", los términos "x + (1 + 4): nat" y "x + (4 + 1): nat" son iguales porque ambos se reducen a "x + 5: nat". Cuando dos términos son iguales, pueden sustituirse entre sí. La igualdad es un tema complejo en la teoría de tipos y hay muchos tipos de igualdad. Este tipo de igualdad, donde dos términos equivalen al mismo término, se denomina "igualdad de juicio".

Funciones

En la teoría de tipos, las funciones son términos. Las funciones pueden ser términos lambda o definirse "por regla".

Términos lambda

Un término lambda se parece a "(λ variablename: type1. term)" y tiene el tipo " type1 type2 ". El tipo " tipo1 tipo2 " indica que el término lambda es una función que toma un parámetro de tipo " tipo1 " y calcula un término de tipo " tipo2 ". El término dentro del término lambda debe ser un valor de " tipo2 ", asumiendo que la variable tiene el tipo " tipo1 ". $para$ $para$

Un ejemplo de un término lambda es esta función que duplica su argumento:

(λ x: nat. (añadir xx)): nat $para$ nat

El nombre de la variable es "x" y la variable tiene el tipo "nat". El término "(add xx) tiene el tipo "nat", asumiendo "x: nat". Por lo tanto, el término lambda tiene el tipo "nat $para$ nat", lo que significa que si se le da un "nat" como argumento, calculará para un "nat". La reducción (también conocida como cálculo) se define para los términos lambda. Cuando se aplica la función (también conocida como llamada), el argumento se sustituye por el parámetro.

Anteriormente, vimos que la aplicación de la función se escribe colocando el parámetro después del término de la función. Entonces, si queremos llamar a la función anterior con el parámetro "5" de tipo "nat", escribimos:

(λ x: nat. (añadir xx)) 5: nat

El término lambda era de tipo "nat $para$ nat", lo que significaba que dado un "nat" como argumento, produciría un término de tipo "nat". Como le hemos dado el argumento "5", el término anterior tiene el tipo "nat". La reducción funciona sustituyendo el argumento "5" por el parámetro "x" en el término "(sumar xx)", por lo que el término se computa como:

(suma 5 5): natural

que obviamente calcula

10: nacional

Un término lambda a menudo se denomina "función anónima" porque no tiene nombre. A menudo, para facilitar la lectura, se asigna un nombre a un término lambda. Esto es simplemente una notación y no tiene significado matemático. Algunos autores lo llaman "igualdad notacional". Se podría dar un nombre a la función anterior usando la notación:

doble: nat $para$ nat::= (λ x: nat. (añadir xx))

Esta es la misma función que la anterior, solo una forma diferente de escribirla. Así que el término

doble 5: natural

todavía calcula para

10: nacional

Escritura dependiente

La tipificación dependiente es cuando el tipo devuelto por una función depende del valor de su argumento. Por ejemplo, cuando una teoría de tipos tiene una regla que define el tipo "bool", también define la función "if". La función "if" toma 3 argumentos y "if true b c" computa como "b" y "if false b c" computa como "c". Pero, ¿cuál es el tipo de "si ab c"?

Si "b" y "c" tienen el mismo tipo, es obvio: "si ab c" tiene el mismo tipo que "b" y "c". Así, asumiendo "a: bool",

si un 2 4: nat
si es falso verdadero: bool

Pero si "b" y "c" tienen tipos diferentes, entonces el tipo de "si ab c" depende del valor de "a". Usamos el símbolo "Π" para indicar una función que toma un argumento y devuelve un tipo. Suponiendo que tenemos algunos tipos "B" y C" y "a: bool", "b: B" y "c: C", entonces

si abc: (Π a: bool. B $para$ C $para$ si a BC)

Es decir, el tipo del término "si" es el tipo del segundo o tercer argumento, según el valor del primer argumento. En realidad, "si un B C" no se define usando "si", pero eso entra en detalles demasiado complicados para esta introducción.

Debido a que el tipo puede contener computación, la tipificación dependiente es increíblemente poderosa. Cuando los matemáticos dicen "existe un número $X$ tal que $X$ es primo" o "existe un número $X$ tal que se $P(x)$ cumple la propiedad", se puede expresar como un tipo dependiente. Es decir, se prueba la propiedad para el " $X$ " específico y eso es visible en el tipo del resultado.

Hay muchos detalles en la tipificación dependiente. Son demasiado largos y complicados para esta introducción. Consulte el artículo sobre tipificación dependiente y el cubo lambda para obtener más información.

Universos

Los términos Π devuelven un tipo. Entonces, ¿cuál es el tipo de su valor de retorno? Bueno, debe haber un tipo que contenga tipos. Un tipo que contiene otros tipos se denomina "universo". A menudo se escribe con el símbolo $tu$ . A veces hay una jerarquía de universos, con " $tu_{0}$ : $tu_{1}$ ", " $tu_{1}$ : $tu_{2}$ ", etc.

Los universos son complicados. Si un universo se contiene a sí mismo, puede conducir a paradojas como la Paradoja de Girard. Los detalles de los universos son demasiado largos y complicados para esta introducción.

Tipos y términos comunes "por regla"

Las teorías de tipos se definen por sus reglas de inferencia. Hay reglas para un "núcleo funcional", descritas anteriormente, y reglas que crean tipos y términos. A continuación se muestra una lista no exhaustiva de tipos comunes y sus términos asociados.

La lista termina con "tipos inductivos", que es una técnica poderosa que puede construir todos los demás en la lista. Los fundamentos matemáticos utilizados por los asistentes de prueba "Coq" y "Lean" se basan en el "Cálculo para construcciones inductivas", que es el "Cálculo de construcciones" (su "núcleo funcional") con tipos inductivos.

Tipo vacío

El tipo vacío no tiene términos. El tipo generalmente se escribe " $bot$ " o " ${ estilo de visualización mathbb {0}}$ ".

Se utiliza para mostrar que algo no es computable. Si para un tipo "A", puede crear una función de tipo "A ${ estilo de visualización a bot}$ ", sabe que "A" no tiene términos. Un ejemplo para el tipo "A" podría ser "existe un número $X$ tal que $X$ es par y $X$ es impar". (Consulte "Tipo de producto" a continuación para ver cómo se construye el ejemplo "A".) Cuando un tipo no tiene términos, decimos que está "deshabitado".

Tipo de unidad

El tipo de unidad tiene exactamente 1 término canónico. El tipo se escribe " $cima$ " o " ${ estilo de visualización mathbb {1}}$ " y el único término canónico se escribe "*".

El tipo de unidad se usa para mostrar que algo existe o es computable. Si para un tipo "A", puedes crear una función de tipo " ${ estilo de visualización arriba a }$ A", sabes que "A" tiene uno o más términos. Cuando un tipo tiene al menos 1 término, decimos que está "habitado".

Tipo booleano

El tipo booleano tiene exactamente 2 términos canónicos. El tipo suele escribirse "bool" o " ${ estilo de visualización mathbb {B}}$ " o " ${ estilo de visualización mathbb {2}}$ ". Los términos canónicos suelen ser "verdadero" y "falso".

El tipo booleano se define con una función eliminadora "si" tal que:

si es cierto bc $doscabezaderechaflecha$ b
si es falso bc $doscabezaderechaflecha$ c

Tipo de producto

El tipo de producto tiene términos que son pares ordenados. Para los tipos "A" y "B", el tipo de producto se escribe "A $veces$ B". Los términos canónicos son creados por la función constructora "par". Los términos son "par a b", donde "a" es un término de tipo "A" y "b" es un término de tipo "B". El tipo de producto se define con funciones de eliminación "primero" y "segundo" de manera que:

primero (par ab) $doscabezaderechaflecha$ a
segundo (par ab) $doscabezaderechaflecha$ b

Además de los pares ordenados, este tipo se usa para el operador lógico "y", porque contiene una "A" y una "B". También se usa para intersección, porque contiene uno de los dos tipos.

Si una teoría de tipos tiene tipos dependientes, tiene pares dependientes. En un par dependiente, el segundo tipo depende del valor del primer término. Así, el tipo se escribe " $Sigma$ a:A. B(a)" donde "B" tiene tipo "A $para$ U". Es útil cuando se muestra la existencia de un "a" con la propiedad "B(a)".

Tipo de suma

El tipo de suma es una "unión etiquetada". Es decir, para los tipos "A" y "B", el tipo "A + B" contiene un término de tipo "A" o un término de tipo "B" y sabe cuál contiene. El tipo viene con los constructores "injectionLeft" e "injectionRight". La llamada "injectionLeft a" toma "a: A" y devuelve un término canónico de tipo "A + B". De manera similar, injectionRight b" toma "b: B" y devuelve un término canónico de tipo "A + B". El tipo se define con una función eliminadora "match" tal que para un tipo "C" y funciones "f: A $para$ C " y "g: B $para$ C":

partido (inyecciónLeft a) C fg $doscabezaderechaflecha$ (fa)
partido (inyecciónDerecha b) C fg $doscabezaderechaflecha$ (gb)

El tipo de suma se utiliza para la unión lógica o y.

Números naturales

Los números naturales suelen implementarse al estilo de la Aritmética de Peano. Hay un término canónico, "0: nat" para cero. Los valores canónicos mayores que cero usan la función constructora "S: nat $para$ nat". Por lo tanto, "S 0" es uno. "S (S 0)" es dos. "S (S (S 0)))" es tres. Etc. Los números decimales son sólo notacionalmente iguales a esos términos.

1: natural::= S 0
2: natural::= S (S 0)
3: natural::= S (S (S 0))
...

Los números naturales se definen con una función eliminadora "R" que utiliza la recursividad para definir una función para todos los nats. Se necesita una función "P: nat $para$ U" que es el tipo de función a definir. También toma un término "PZ: P 0" que es el valor en cero y una función "PS: P n $para$ P (S n)" que dice cómo transformar el valor en "n" en el valor en "n + 1 ". Por tanto, sus reglas de cálculo son:

RP PZ PS 0 $doscabezaderechaflecha$ PZ
RP PZ PS (S $norte$ ) $doscabezaderechaflecha$ PS (RP PZ PS $norte$ )

La función "añadir", que se utilizó anteriormente, se puede definir mediante "R".

agregar: nat $para$ nat $para$ nat::= R (λ n:nat. nat $para$ nat) (λ n:nat. n) (λ g:nat $para$ nat. (λ m:nat. S (gm)))

Tipo de identidad

El tipo de identidad es el tercer concepto de igualdad en la teoría de tipos. La primera es "igualdad notacional", que es para definiciones como "2: nat::= (S (S 0))" que no tienen significado matemático pero son útiles para los lectores. El segundo es "igualdad de juicio", que es cuando dos términos calculan el mismo término, como "x + (1 + 4)" y "x + (4 + 1)", que ambos calculan "x + 5". Pero la teoría de tipos necesita otra forma de igualdad, conocida como "tipo de identidad" o "igualdad proposicional".

La razón por la que necesita el tipo de identidad es porque algunos términos iguales no se calculan en el mismo término. Suponiendo que "x: nat", los términos "x + 1" y "1 + x" no se computan como el mismo término. Recuerde que "+" es una notación para la función "sumar", que es una notación para la función "R". No podemos calcular en "R" hasta que se especifique el valor de "x" y, hasta que se especifique, dos llamadas diferentes a "R" no calcularán el mismo término.

Un tipo de identidad requiere dos términos "a" y "b" del mismo tipo y se escribe "a = b". Entonces, para "x + 1" y "1 + x", el tipo sería "x+1 = 1+x". Los términos canónicos se crean con el constructor "reflexividad". La llamada "reflexividad a" toma un término "a" y devuelve un término canónico del tipo "a = a".

El cálculo con el tipo de identidad se realiza con la función eliminadora "J". La función "J" permite reescribir un término dependiente de "a", "b" y un término del tipo "a = b" de manera que "b" se reemplaza por "a". Si bien "J" es unidireccional, solo capaz de sustituir "b" por "a", se puede probar que el tipo de identidad es reflexivo, simétrico y transitivo.

Si los términos canónicos son siempre "a=a" y "x+1" no se calcula como el mismo término que "1+x", ¿cómo creamos un término de "x+1 = 1+x"? Usamos la función "R". (Consulte "Números naturales" más arriba). El argumento "P" de la función "R" se define como "(λ x:nat. x+1 = 1+x)". Los otros argumentos actúan como las partes de una prueba de inducción, donde "PZ: P 0" se convierte en el caso base "0+1 = 1+0" y "PS: P n $para$ P (S n)" se convierte en el caso inductivo. Esencialmente, esto dice que cuando "x+1 = 1+x" tiene "x" reemplazada con un valor canónico, la expresión será la misma que "reflexividad (x+1)". Esta aplicación de la función "R" tiene tipo "x: nat $para$ x+1 = 1+x". Podemos usarla y la función "J" para sustituir "1+x" por "x+1" en cualquier término. De esta forma, el tipo identidad es capaz de capturar igualdades que son no es posible con la igualdad de juicio.

Para que quede claro, es posible crear el tipo "0 = 1", pero no habrá forma de crear términos de ese tipo. Sin un término del tipo "0 = 1", no será posible utilizar la función "J" para sustituir "0" por "1" en otro término.

Las complejidades de la igualdad en la teoría de tipos la convierten en un área de investigación activa; consulte la teoría de tipos de homotopía.

Tipos inductivos

Los tipos inductivos son una forma de crear una gran variedad de tipos. De hecho, todos los tipos descritos anteriormente y más se pueden definir usando las reglas de tipos inductivos. Una vez que se especifican los constructores del tipo, las funciones del eliminador y el cálculo se determinan mediante la recursividad estructural.

Existen formas similares y más potentes de crear tipos. Estos incluyen inducción-recursión e inducción-inducción. También hay una forma de crear tipos similares usando solo términos lambda, llamada codificación Scott.

(NOTA: Las teorías de tipos no suelen incluir tipos coductivos. Representan un tipo de datos infinito y la mayoría de las teorías de tipos se limitan a funciones que se puede demostrar que se detienen).

Diferencias con la teoría de conjuntos

La base tradicional de las matemáticas ha sido la teoría de conjuntos combinada con una lógica. La más común citada es la teoría de conjuntos de Zermelo-Fraenkel, conocida como "ZF" o, con el axioma de elección, "ZFC". Las teorías de tipos difieren de esta base en varios aspectos.

La teoría de conjuntos tiene reglas y axiomas, mientras que las teorías de tipos solo tienen reglas. Las teorías de conjuntos se construyen sobre la lógica. Por lo tanto, ZFC se define tanto por las reglas de la lógica de primer orden como por sus propios axiomas. (Un axioma es una declaración lógica aceptada como verdadera sin una derivación lógica.) Las teorías de tipos, en general, no tienen axiomas y se definen por sus reglas de inferencia.
La teoría de conjuntos y la lógica tienen la ley del tercero excluido. Es decir, todo teorema es verdadero o falso. Cuando una teoría de tipos define los conceptos de "y" y "o" como tipos, conduce a la lógica intuicionista, que no tiene la ley del tercero excluido. Sin embargo, la ley puede ser probada para algunos tipos.
En la teoría de conjuntos, un elemento no está restringido a un conjunto. El elemento puede aparecer en subconjuntos y uniones con otros conjuntos. En la teoría de tipos, los términos (generalmente) pertenecen a un solo tipo. Donde se usaría un subconjunto, la teoría de tipos puede usar una función de predicado o usar un tipo de producto de tipo dependiente, donde cada elemento $X$ se empareja con una prueba de que la propiedad del subconjunto se cumple para $X$ . Donde se usaría una unión, la teoría de tipos usa el tipo de suma, que contiene nuevos términos canónicos.
La teoría de tipos tiene una noción incorporada de computación. Por lo tanto, "1+1" y "2" son términos diferentes en la teoría de tipos, pero calculan el mismo valor. Además, las funciones se definen computacionalmente como términos lambda. En la teoría de conjuntos, "1+1=2" significa que "1+1" es solo otra forma de referirse al valor "2". El cálculo de la teoría de tipos requiere un concepto complicado de igualdad.
La teoría de conjuntos generalmente codifica números como conjuntos. (0 es el conjunto vacío, 1 es un conjunto que contiene el conjunto vacío, etc. Consulte la definición teórica de conjuntos de números naturales). La teoría de tipos puede codificar números como funciones utilizando la codificación de Church o, más naturalmente, como tipos inductivos. Los constructores "0" y "S" creados por el tipo inductivo se parecen mucho a los axiomas de Peano.
La teoría de conjuntos tiene notación de constructor de conjuntos. Puede crear cualquier conjunto que se pueda definir. Esto le permite crear conjuntos incontables. Las teorías de tipos son sintácticas, lo que las limita a términos numerables infinitos. Además, la mayoría de las teorías de tipos requieren que la computación siempre se detenga y se limite a términos generables recursivamente. Como resultado, la mayoría de las teorías de tipos no usan los números reales sino los números computables.
En la teoría de conjuntos, el axioma de elección es un axioma y es controvertido, particularmente cuando se aplica a conjuntos incontables. En la teoría de tipos, el enunciado equivalente es un teorema (tipo) y es demostrable (habitado por un término).
En la teoría de tipos, las pruebas son objetos matemáticos. El tipo "x+1 = 1+x" no se puede utilizar a menos que haya un término del tipo. Ese término representa una prueba de que "x+1 = 1+x". Así, la teoría de tipos abre pruebas para ser estudiadas como objetos matemáticos.

Los defensores de la teoría de tipos también señalarán su conexión con las matemáticas constructivas a través de la interpretación BHK, su conexión con la lógica por el isomorfismo de Curry-Howard y sus conexiones con la teoría de categorías.

Detalles técnicos

Una teoría de tipos es una lógica matemática. Es un conjunto de reglas de inferencia que dan como resultado juicios. La mayoría de las lógicas tienen juicios que significan "El término $X$ es verdadero". o "El término $X$ es una fórmula bien formada".. Una teoría de tipos tiene juicios adicionales que definen tipos y relacionan términos con tipos.

Términos

Un término en lógica se define recursivamente como un símbolo constante, una variable o una aplicación de función, donde un término se aplica a otro término. Algunos símbolos constantes serán "0" de los números naturales, "verdadero" de los booleanos y funciones como "S" y "si". Así, algunos términos son "0", "(S 0)", "(S (S x))" y "si es verdadero 0 (S 0)".

Sentencias

La mayoría de las teorías de tipos tienen 4 juicios:

" $T$ es un tipo".
" $t$ es un término de tipo $T$ ".
"El tipo $T_{1}$ es igual al tipo $T_{2}$ ".
"Los términos $t_{1}$ y $t_{2}$ son ambos del tipo $T$ y son iguales".

Los juicios pueden hacerse bajo una suposición. Así, podríamos decir, "asumiendo $X$ que es un término de tipo "bool" y $y$ es un término de tipo "nat", (si xyy) es un término de tipo "nat"". La notación matemática para las suposiciones es una lista separada por comas de " término: tipo " que precede al símbolo del torniquete ' $vdash$ '. Por lo tanto, la declaración de ejemplo se escribe formalmente:

x: bool, y: nat $vdash$ (si xyy): nat

Si no hay suposiciones, no habrá nada a la izquierda del torniquete.

$vdash$ S: natural $para$ natural

La lista de suposiciones se denomina "contexto". Es muy común ver el símbolo ' $Gama$ ' utilizado para representar algunas o todas las suposiciones. Así, la notación formal para los 4 juicios diferentes suele ser:

{ estilo de visualización Gamma vdash T}

Notación formal para sentencias	Descripción
${ estilo de visualización Gamma vdash T}$ Tipo	$T$ es un tipo (bajo suposiciones $Gama$ ).
${ estilo de visualización Gamma vdash t: T}$	$t$ es un término de tipo $T$ (bajo supuestos $Gama$ ).
${displaystyle Gamma vdash T_{1}=T_{2}}$	Tipo $T_{1}$ es igual a tipo $T_{2}$ (bajo suposiciones $Gama$ ).
${ estilo de visualización gamma vdash t_ {1} = t_ {2}: T}$	Los términos $t_{1}$ y $t_{2}$ son ambos del tipo $T$ y son iguales (bajo supuestos $Gama$ ).

(NOTA: El juicio de igualdad de términos es de donde proviene la frase "igualdad de juicio".)

Las sentencias imponen que todo término tiene un tipo. El tipo restringirá qué reglas se pueden aplicar a un término.

Normas

Las reglas de una teoría de tipos dicen qué juicios se pueden hacer, basados en la existencia de otros juicios. Las reglas se expresan usando una línea horizontal, con los juicios de entrada requeridos arriba de la línea y el juicio resultante debajo de la línea. La regla para crear un término lambda es:

{displaystyle {begin{array}{c}Gamma,a:Avdash b:B\hline Gamma vdash (lambda a:Ab):Ato B\end{array} }}

Los juicios necesarios para crear el término lambda van por encima de la línea. En este caso, sólo se requiere una sentencia. Es que existe algún término "b" de algún tipo "B", suponiendo que existe algún término "a" de algún tipo "A" y algunos otros supuestos " $Gama$ ". (Nota: " $Gama$ " "a", "A", "b" y "B" son todas metavariables en la regla). El juicio resultante va debajo de la línea. El juicio resultante de esta regla establece que el nuevo término lambda tiene el tipo " $para$ AB" bajo las otras suposiciones $Gama$ .

Las reglas son sintácticas y funcionan por reescritura. Por lo tanto, las metavariables como " $Gama$ ", "a", "A", etc. en realidad pueden consistir en términos complejos que contienen muchas aplicaciones de funciones, no solo símbolos individuales.

Para generar un juicio particular en la teoría de tipos, debe haber una regla para generarlo. Luego, debe haber reglas para generar todas las entradas requeridas de esa regla. Y luego reglas para todas las entradas de esas reglas. Las reglas aplicadas forman un árbol de prueba. Esto generalmente se dibuja al estilo Gentzen, donde el juicio objetivo (raíz) está en la parte inferior y las reglas que no requieren ninguna entrada (hojas) en la parte superior. (Consulte Deducción natural#Pruebas_y_teoría_de_tipos). Un ejemplo de una regla que no requiere ninguna entrada es una que establece que hay un término "0" de tipo "nat":

{displaystyle {begin{matriz}{c}hline vdash 0:nat\end{matriz}}}

Una teoría de tipos generalmente tiene una serie de reglas, incluidas algunas para:

crear un contexto
agregar una suposición al contexto ("debilitamiento")
reorganizar las suposiciones
usar una suposición para crear una variable
definir la reflexividad, la simetría y la transitividad para la igualdad de juicio
definir la sustitución para la aplicación de términos lambda
todas las interacciones de igualdad, sustitución, etc.
definir universos

Además, para cada tipo "por regla", hay 4 tipos diferentes de reglas

Las reglas de "formación de tipos" dicen cómo crear el tipo.
Las reglas de "introducción de términos" definen los términos canónicos y las funciones constructoras, como "par" y "S".
Las reglas de "eliminación de términos" definen las otras funciones como "primero", "segundo" y "R".
Las reglas de "cálculo" especifican cómo se realiza el cálculo con las funciones específicas del tipo.

Ejemplos de reglas:

Reglas de la teoría intuicionista de tipos de Martin-Löf
Apéndice A.2 del libro de teoría de tipos de homotopía

Propiedades de las teorías de tipos

Los términos suelen pertenecer a un solo tipo. Sin embargo, existen teorías establecidas que definen la "subtipificación".

El cálculo tiene lugar mediante la aplicación repetida de reglas. Muchas teorías de tipos son fuertemente normalizadoras, lo que significa que cualquier orden de aplicación de las reglas siempre terminará en el mismo resultado. Sin embargo, algunos no lo son. En una teoría de tipo de normalización, las reglas de cálculo unidireccionales se denominan "reglas de reducción" y la aplicación de las reglas "reduce" el término. Si una regla no es unidireccional, se denomina "regla de conversión".

Algunas combinaciones de tipos son equivalentes a otras combinaciones de tipos. Cuando las funciones se consideran "exponenciación", las combinaciones de tipos se pueden escribir de manera similar a las identidades algebraicas. Así, ${displaystyle {mathbb {0} }+Acong A}$ , ${displaystyle {mathbb {1} }times Acong A}$ , ${displaystyle {mathbb {1} }+{mathbb {1} }cong {mathbb {2} }}$ , ${displaystyle A^{B+C}cong A^{B}times A^{C}}$ , ${displaystyle A^{Btimes C}cong (A^{B})^{C}}$ .

Axiomas

La mayoría de las teorías de tipos no tienen axiomas. Esto se debe a que una teoría de tipos se define por sus reglas de inferencia. (Ver "Reglas" arriba). Esta es una fuente de confusión para las personas familiarizadas con la teoría de conjuntos, donde una teoría se define tanto por las reglas de inferencia de una lógica (como la lógica de primer orden) como por axiomas sobre conjuntos.

A veces, una teoría de tipos agregará algunos axiomas. Un axioma es un juicio que se acepta sin una derivación usando las reglas de inferencia. A menudo se agregan para garantizar propiedades que no se pueden agregar limpiamente a través de las reglas.

Los axiomas pueden causar problemas si introducen términos sin una forma de calcularlos. Es decir, los axiomas pueden interferir con la propiedad normalizadora de la teoría de tipos.

Algunos axiomas comúnmente encontrados son:

El "Axioma K" asegura la "exclusividad de las pruebas de identidad". Es decir, que todo término de un tipo de identidad es igual a reflexividad.
El "Axioma de Univalencia" sostiene que la equivalencia de tipos es igualdad de tipos. La investigación de esta propiedad condujo a la teoría del tipo cúbico, donde la propiedad se cumple sin necesidad de un axioma.
A menudo se agrega la "Ley del medio excluido" para satisfacer a los usuarios que desean una lógica clásica, en lugar de una lógica intuicionista.

No es necesario agregar el axioma de elección a la teoría de tipos, porque en la mayoría de las teorías de tipos se puede derivar de las reglas de inferencia. Esto se debe a la naturaleza constructiva de la teoría de tipos, donde demostrar que existe un valor requiere un método para calcular el valor. El axioma de elección es menos poderoso en la teoría de tipos que en la mayoría de las teorías de conjuntos, porque las funciones de la teoría de tipos deben ser computables y, al estar impulsadas por la sintaxis, el número de términos en un tipo debe ser contable. (Ver Axioma de elección § En matemáticas constructivas).

Problemas de decisión

Una teoría de tipos se asocia naturalmente con el problema de decisión de la habitación tipo.

Tipo habitacion

El problema de decisión de tipo habitacional (abreviado por ${displaystyle existe e.Gamma vdash e:tau ?}$ ) es:Dado un entorno de tipos $Gama$ y un tipo $tau$ , decida si existe un término al $mi$ que se le pueda asignar el tipo $tau$ en el entorno de tipos $Gama$ .

La paradoja de Girard muestra que la presencia de tipos está fuertemente relacionada con la consistencia de un sistema de tipos con la correspondencia Curry-Howard. Para ser sólido, dicho sistema debe tener tipos deshabitados.

La oposición de términos y tipos también puede ser vista como una de implementación y especificación. Mediante la síntesis de programas (la contrapartida computacional de) la habitación de tipo (ver más abajo) se puede utilizar para construir (todos o partes de) programas a partir de especificaciones dadas en forma de información de tipo.

Tipo de inferencia

Muchos programas que trabajan con la teoría de tipos (p. ej., demostradores de teoremas interactivos) también hacen inferencias de tipos. Les permite seleccionar las reglas que el usuario desea, con menos acciones por parte del usuario.

Áreas de investigación

La teoría del tipo de homotopía difiere de la teoría del tipo intuicionista principalmente por su manejo del tipo de igualdad. En 2016 se propuso la teoría de tipos cúbicos, que es una teoría de tipos de homotopía con normalización.

Interpretaciones

La teoría de tipos tiene conexiones con otras áreas de las matemáticas. Los defensores de la teoría de tipos como base a menudo mencionan estas conexiones como justificación para su uso.

Los tipos son proposiciones; los términos son pruebas

Cuando se usan como base, ciertos tipos se interpretan como proposiciones (enunciados que pueden probarse) y un término del tipo es una prueba de esa proposición. Así, el tipo "Π x:nat. x+1=1+x" representa que, para cualquier "x" de tipo "nat", "x+1" y "1+x" son iguales. Y un término de ese tipo representa su prueba.

Correspondencia de Curry-Howard

La correspondencia de Curry-Howard es la similitud observada entre la lógica y los lenguajes de programación. La implicación en lógica, "A $para$ B" se parece a una función del tipo "A" al tipo "B". Para una variedad de lógicas, las reglas son similares a la expresión en los tipos de un lenguaje de programación. La similitud va más allá, ya que las aplicaciones de las reglas se parecen a los programas en los lenguajes de programación. Por lo tanto, la correspondencia a menudo se resume como "pruebas como programas".

Los operadores lógicos "para todos" y "existe" llevaron a Per Martin-Löf a inventar la teoría de tipos dependientes.

Lógica intuicionista

Cuando algunos tipos se interpretan como proposiciones, existe un conjunto de tipos comunes que se pueden usar para conectarlos y crear una lógica a partir de los tipos. Sin embargo, esa lógica no es la lógica clásica sino la lógica intuicionista. Es decir, no tiene la ley del medio excluido ni la doble negación.

Hay una relación natural de los tipos con las proposiciones lógicas. Si "A" es un tipo que representa una proposición, poder crear una función de tipo " ${ estilo de visualización arriba a }$ A" indica que A tiene una prueba y poder crear la función "A ${ estilo de visualización a bot}$ " indica que A no tiene una prueba. Es decir, se prueban los tipos habitables y se refutan los tipos inhabitables.

ADVERTENCIA: Esta interpretación puede llevar a mucha confusión. Una teoría de tipos puede tener términos "verdadero" y "falso" de tipo "bool", que actúan como una lógica booleana, y al mismo tiempo tienen tipos y para representar "verdadero" (probable) y "falso" (refutado), como parte de una lógica intuicionista para la proposición.

Bajo esta interpretación intuicionista, existen tipos comunes que actúan como operadores lógicos:

Nombre lógico	Notación lógica	Tipo de notación	Escribe un nombre
Verdadero	$cima$	$cima$	Tipo de unidad
Falso	$bot$	$bot$	Tipo vacío
No	$neg A$	${displaystyle Aabot}$	Función a tipo vacío
Implicación	$De la A, a la B$	$De la A, a la B$	Función
Y	$Atierra B$	$Aveces B$	tipo de producto
O	$A o B$	$A + B$	Tipo de suma
Para todos	${displaystyle forall ain A,P(a)}$	Π a: A. Pensilvania)	función dependiente
existe	${displaystyle existe unen A,P(a)}$	Σ a: A. Pensilvania)	Tipo de producto dependiente

Pero bajo esta interpretación, no existe la ley del tercero excluido. Es decir, no existe un término de tipo Π A. A + (A ${ estilo de visualización a bot}$ ).

Asimismo, no hay doble negación. No existe ningún término de tipo Π A. ((A ${ estilo de visualización a bot}$ ) ${ estilo de visualización a bot}$ ) ${ estilo de visualización a }$ R. (Nota: la lógica intuicionista sí permite ${displaystyle lnot lnot lnot Ato lnot A}$ y hay un término de tipo (((A ${ estilo de visualización a bot}$ ) ${ estilo de visualización a bot}$ ) ${ estilo de visualización a bot}$ ) ${ estilo de visualización a }$ (A ${ estilo de visualización a bot}$ ).)

Así, la lógica-de-tipos es una lógica intuicionista. La teoría de tipos se cita a menudo como una implementación de la interpretación de Brouwer-Heyting-Kolmogorov.

Es posible incluir la ley del medio excluido y la doble negación en una teoría de tipos, por regla o suposición. Sin embargo, es posible que los términos no se reduzcan a términos canónicos e interferirán con la capacidad de determinar si dos términos son iguales entre sí desde el punto de vista del juicio.

Matemáticas constructivas

Per Martin-Löf propuso su teoría de tipo intuicionista como base para las matemáticas constructivas. La matemática constructiva requiere que al probar "Existe un $X$ con propiedad P( $X$ )", debe haber un particular $X$ y una prueba de que tiene propiedad "P". En la teoría de tipos, la existencia se logra usando el tipo de producto dependiente y, su demostración, requiere un término de ese tipo. Para el término $t$ , "primero $t$ " producirá el $X$ y "segundo $t$ " producirá la prueba de P( $X$ ).

Un ejemplo de una prueba no constructiva es una "prueba por contradicción". El primer paso es asumir que $X$ no existe y refutarlo por contradicción. La conclusión de ese paso es "no es el caso que $X$ no existe". El último paso es, por doble negación, concluir que $X$ existe. Para ser claros, las matemáticas constructivas todavía permiten "refutar por contradicción". Puede probar que "no es el caso que $X$ no existe". Pero las matemáticas constructivas no permiten el último paso de eliminar la doble negación para concluir que $X$ existe.

Las matemáticas constructivas a menudo han utilizado la lógica intuicionista, como lo demuestra la interpretación de Brouwer-Heyting-Kolmogorov.

La mayoría de las teorías de tipos propuestas como fundamentos son constructivas. Esto incluye la mayoría de los que utilizan los asistentes de pruebas.

Es posible agregar características no constructivas a una teoría de tipos, por regla o suposición. Estos incluyen operadores en continuaciones como llamada con continuación actual. Sin embargo, estos operadores tienden a romper propiedades deseables como la canonicidad y la parametricidad.

Teoría de categorías

Aunque la motivación inicial de la teoría de categorías estaba muy alejada del fundacionalismo, los dos campos resultaron tener profundas conexiones. Como escribe John Lane Bell: "De hecho, las categorías pueden verse como teorías de tipos de cierto tipo; este solo hecho indica que la teoría de tipos está mucho más relacionada con la teoría de categorías que con la teoría de conjuntos". En resumen, una categoría puede verse como una teoría de tipos al considerar sus objetos como tipos (o clases), es decir, "En términos generales, una categoría puede considerarse como una teoría de tipos despojada de su sintaxis". Una serie de resultados significativos siguen de esta manera:

las categorías cerradas cartesianas corresponden al cálculo λ tipado (Lambek, 1970);
Los C-monoides (categorías con productos y exponenciales y un objeto no terminal) corresponden al cálculo λ sin tipo (observado de forma independiente por Lambek y Dana Scott alrededor de 1980);
las categorías cerradas localmente cartesianas corresponden a teorías tipo Martin-Löf (Seely, 1984).

La interacción, conocida como lógica categórica, ha sido objeto de investigación activa desde entonces; ver la monografía de Jacobs (1999) por ejemplo.

La teoría de tipos de homotopía intenta combinar la teoría de tipos y la teoría de categorías. Se centra en las igualdades, especialmente las igualdades entre tipos.

Lista de teorías de tipos

Principal

Cálculo lambda simplemente escrito, que es una lógica de orden superior
teoría de tipos intuicionista
sistema F
LF se usa a menudo para definir otras teorías de tipo
cálculo de construcciones y sus derivados

Menor

autómata
Teoría del tipo ST
UTT (Teoría unificada de tipos dependientes de Luo)
algunas formas de lógica combinatoria
otros definidos en el cubo lambda (también conocidos como sistemas de tipo puro)
otros bajo el nombre de cálculo lambda escrito

Investigación activa

La teoría del tipo de homotopía explora la igualdad de tipos
La teoría de tipos cúbicos es una implementación de la teoría de tipos de homotopía

Aplicaciones

Fundamentos matemáticos

El primer asistente de prueba por computadora, llamado Automath, usó la teoría de tipos para codificar las matemáticas en una computadora. Martin-Löf desarrolló específicamente la teoría de tipos intuicionista para codificar todas las matemáticas para que sirvieran como una nueva base para las matemáticas. Hay una investigación en curso sobre los fundamentos matemáticos que utilizan la teoría del tipo de homotopía.

Los matemáticos que trabajaban en la teoría de categorías ya tenían dificultades para trabajar con la base ampliamente aceptada de la teoría de conjuntos de Zermelo-Fraenkel. Esto condujo a propuestas como la Teoría elemental de la categoría de conjuntos (ETCS) de Lawvere. La teoría de tipos de homotopía continúa en esta línea utilizando la teoría de tipos. Los investigadores están explorando las conexiones entre los tipos dependientes (especialmente el tipo de identidad) y la topología algebraica (específicamente la homotopía).

Asistentes de prueba

Gran parte de la investigación actual sobre la teoría de tipos está impulsada por verificadores de pruebas, asistentes de prueba interactivos y probadores de teoremas automatizados. La mayoría de estos sistemas utilizan una teoría de tipos como base matemática para codificar pruebas, lo cual no es sorprendente, dada la estrecha conexión entre la teoría de tipos y los lenguajes de programación:

LF es utilizado por Twelf, a menudo para definir otras teorías de tipos;
muchas teorías de tipos que caen bajo la lógica de orden superior son utilizadas por la familia de probadores HOL y PVS;
NuPRL utiliza la teoría de tipos computacional;
el cálculo de construcciones y sus derivados son utilizados por Coq, Matita y Lean;
UTT (Teoría unificada de tipos dependientes de Luo) es utilizado por Agda, que es tanto un lenguaje de programación como un asistente de prueba.

Muchas teorías de tipos son compatibles con LEGO e Isabelle. Isabelle también admite fundaciones además de teorías de tipos, como ZFC. Mizar es un ejemplo de un sistema de prueba que solo admite la teoría de conjuntos.

Lenguajes de programación

Existe una amplia superposición e interacción entre los campos de la teoría de tipos y los sistemas de tipos. Los sistemas de tipos son una característica del lenguaje de programación diseñada para identificar errores. Cualquier análisis de programa estático, como los algoritmos de verificación de tipos en la fase de análisis semántico del compilador, tiene una conexión con la teoría de tipos.

Un buen ejemplo es Agda, un lenguaje de programación que utiliza UTT (Teoría unificada de tipos dependientes de Luo) para su sistema de tipos. El lenguaje de programación ML fue desarrollado para manipular teorías de tipos (ver LCF) y su propio sistema de tipos estuvo fuertemente influenciado por ellas.

Lingüística

La teoría de tipos también se usa ampliamente en las teorías formales de la semántica de los lenguajes naturales, especialmente en la gramática de Montague y sus descendientes. En particular, las gramáticas categoriales y las gramáticas pregrupales utilizan mucho los constructores de tipos para definir los tipos (sustantivo, verbo, etc.) de las palabras.

La construcción más común toma los tipos básicos $mi$ y $t$ para individuos y valores de verdad, respectivamente, y define recursivamente el conjunto de tipos de la siguiente manera:

si $un$ y $b$ son tipos, entonces también lo es $langle a,brangle$ ;
nada excepto los tipos básicos, y lo que se puede construir a partir de ellos por medio de la cláusula anterior son tipos.

Un tipo complejo $langle a,brangle$ es el tipo de funciones de entidades de tipo $un$ a entidades de tipo $b$ . Así, uno tiene tipos como $langle e,trangle$ los que se interpretan como elementos del conjunto de funciones de entidades a valores de verdad, es decir, funciones indicadoras de conjuntos de entidades. Una expresión de tipo $langle langle e,trangle,trangle$ es una función de conjuntos de entidades a valores de verdad, es decir, una (función indicadora de un) conjunto de conjuntos. Este último tipo se toma normalmente como el tipo de cuantificadores del lenguaje natural, como todos o nadie (Montague 1973, Barwise y Cooper 1981).

Ciencias Sociales

Gregory Bateson introdujo una teoría de los tipos lógicos en las ciencias sociales; sus nociones de doble vínculo y niveles lógicos se basan en la teoría de los tipos de Russell.

Contenido relacionado

Más resultados...