Teoría de tipos intuicionistas - Intuitionistic type theory

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 tanto intensionales como extensionales de la teoría y las primeras versiones impredicativas , demostrado ser inconsistente por la paradoja de Girard , dio paso a versiones predicativas . Sin embargo, todas las versiones mantienen el diseño central de la lógica constructiva utilizando tipos dependientes.

Diseño

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". Entonces, cualquier prueba de "existe un primo mayor que 1000" debe identificar un número específico que sea primo y 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 pruebas se convierten en objetos matemáticos que pueden examinarse, compararse y manipularse.

Los constructores de tipos de la teoría intuicionista de tipos se construyeron para seguir una correspondencia uno a uno con los conectivos lógicos. Por ejemplo, el conectivo lógico llamado implicación ( ) corresponde al tipo de función ( ). Esta correspondencia se denomina 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 .

Teoría de tipos

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 basan en una lógica como la de Frege . Entonces, 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 resumen rápido 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 .

0 tipo, 1 tipo y 2 tipo

Hay 3 tipos finitos: El 0 de tipos contiene 0 términos. El tipo 1 contiene 1 término canónico. Y el tipo 2 contiene 2 términos canónicos.

Dado que el tipo 0 contiene 0 términos, también se denomina tipo vacío . Se utiliza para representar cualquier cosa que no pueda existir. También está escrito y representa cualquier cosa indemostrable. (. Es decir, no puede existir una prueba de ello) Como resultado de ello, la negación se define como una función a la misma: .

Asimismo, el tipo 1 contiene 1 término canónico y representa la existencia. También se denomina tipo de unidad . A menudo representa proposiciones que se pueden probar y, por lo tanto, a veces se escribe .

Finalmente, el 2 de tipo 2 contiene términos canónicos. Representa una elección definida entre dos valores. Se utiliza para valores booleanos pero no para proposiciones. Las proposiciones se consideran del tipo 1 y se puede probar que nunca tienen una prueba (el tipo 0 ), o puede que no se prueben de ninguna manera. (La ley del medio excluido no se aplica a las proposiciones en la teoría de tipos intuicionistas).

Σ constructor de tipos

Los tipos Σ contienen pares ordenados. Al igual que con par típico ordenado (o 2-tupla) tipos, un tipo Σ puede describir el producto cartesiano , , de otros dos tipos, y . Lógicamente, un par ordenado de este tipo tendría una prueba de y una prueba de , por lo que uno puede ver un tipo escrito como .

Los tipos Σ son más potentes que los tipos de pares ordenados típicos debido a la tipificación dependiente . En el par ordenado, el tipo del segundo término puede depender del valor del primer término. Por ejemplo, el primer término del par podría ser un número natural y el tipo del segundo término podría ser un vector de longitud igual al primer término. Tal tipo se escribiría:

Utilizando la terminología de la teoría de conjuntos, esto es similar a las uniones disjuntas indexadas de conjuntos. En el caso de pares ordenados habituales, el tipo del segundo término no depende del valor del primer término. Así, el tipo que describe el producto cartesiano se escribe:

Es importante señalar aquí que el valor del primer término ,, no depende del tipo del segundo término ,.

Obviamente, los tipos Σ se pueden usar para construir tuplas más largas de tipo dependiente que se usan en matemáticas y los registros o estructuras que se usan en la mayoría de los lenguajes de programación. Un ejemplo de una 3-tupla de tipo dependiente son dos enteros y una prueba de que el primer entero es más pequeño que el segundo entero, descrito por el tipo:

La tipificación dependiente permite que los tipos Σ desempeñen el papel de cuantificador existencial . La declaración "existe un tipo de , tal que está probado" se convierte en el tipo de pares ordenados donde el primer elemento es el valor del tipo y el segundo elemento es una prueba de . Observe que el tipo del segundo elemento (pruebas de ) depende del valor en la primera parte del par ordenado ( ). Su tipo sería:

Π constructor de tipos

Los tipos Π contienen funciones. Como ocurre con los tipos de funciones típicos, constan de un tipo de entrada y un tipo de salida. Sin embargo, son más potentes que los tipos de función típicos, ya que el tipo de retorno puede depender del valor de entrada. Las funciones en la teoría de tipos son diferentes de la teoría de conjuntos. En la teoría de conjuntos, busca el valor del argumento en un conjunto de pares ordenados. En la teoría de tipos, el argumento se sustituye por un término y luego se aplica el cálculo ("reducción") al término.

Como ejemplo, se escribe el tipo de función que, dado un número natural , devuelve un vector que contiene números reales:

Cuando el tipo de salida no depende del valor de entrada, el tipo de función a menudo se escribe simplemente con un . Así, es el tipo de funciones desde números naturales hasta números reales. Tales tipos Π corresponden a la implicación lógica. La proposición lógica corresponde al tipo , que contiene funciones que toman pruebas de A y devuelven pruebas de B. Este tipo podría escribirse de forma más coherente como:

Los tipos Π también se utilizan en lógica para la cuantificación universal . El enunciado "para cada tipo , está probado" se convierte en una función desde el tipo hasta las pruebas de . Por lo tanto, dado el valor de la función, se genera una prueba que se cumple para ese valor. El tipo sería

= tipo constructor

= -los tipos se crean a partir de dos términos. Dados dos términos como y , puede crear un nuevo tipo . Los términos de ese nuevo tipo representan pruebas de que el par se reduce al mismo término canónico. Por lo tanto, dado que ambos y calculan el término canónico , habrá un término del tipo . En la teoría de tipos intuicionista, hay una forma única de hacer términos de tipos = y es mediante la reflexividad :

Es posible crear tipos =, por ejemplo, donde los términos no se reducen al mismo término canónico, pero no podrá crear términos de ese nuevo tipo. De hecho, si pudiera crear un término de , podría crear un término de . Poner eso en una función generaría una función de tipo . Dado que así es como la teoría de tipos intuicionista define la negación, tendrías o, finalmente ,.

La igualdad de pruebas es un área de investigación activa en la teoría de pruebas y ha llevado al desarrollo de la teoría de tipos de homotopía y otras teorías de tipos.

Tipos inductivos

Los tipos inductivos permiten la creación de tipos complejos y autorreferenciales. Por ejemplo, una lista enlazada de números naturales es una lista vacía o un par de un número natural y otra lista enlazada. Los tipos inductivos se pueden utilizar para definir estructuras matemáticas ilimitadas como árboles, gráficos, etc. De hecho, el tipo de números naturales puede definirse como un tipo inductivo, ya sea como sucesor de otro número natural.

Los tipos inductivos definen nuevas constantes, como cero y la función sucesora . Dado que no tiene una definición y no se puede evaluar mediante sustitución, los términos como y se convierten en términos canónicos de los números naturales.

Las pruebas en tipos inductivos son posibles por inducción . Cada nuevo tipo inductivo viene con su propia regla inductiva. Para probar un predicado para cada número natural, usa la siguiente regla:

Los tipos inductivos en la teoría de tipos intuicionistas se definen en términos de tipos W, el tipo de árboles bien fundamentados . El trabajo posterior en la teoría de tipos generó tipos coinductivos, inducción-recursión e inducción-inducción para trabajar con tipos con tipos más oscuros de autorreferencialidad. Los tipos inductivos superiores permiten definir la igualdad entre términos.

Tipos de universo

Los tipos de universo permiten que se escriban pruebas sobre todos los tipos creados con los otros constructores de tipos. Cada término del tipo de universo se puede asignar a un tipo creado con cualquier combinación de y el constructor de tipo inductivo. Sin embargo, para evitar paradojas, no hay ningún término que corresponda .

Para escribir pruebas sobre todos los "tipos pequeños" y , debe usar , que contiene un término para , pero no para sí mismo . Del mismo modo, para . Existe una jerarquía predicativa de universos, por lo que para cuantificar una prueba sobre cualquier universos constantes fijos , puede usar .

Los tipos de universo son una característica complicada de las teorías de tipos. La teoría de tipos original de Martin-Löf tuvo que cambiarse para dar cuenta de la paradoja de Girard . La investigación posterior cubrió temas como "superuniversos", "universos Mahlo" y universos impredicativos.

Juicios

La definición formal de la teoría de tipos intuicionista se escribe utilizando juicios. Por ejemplo, en la declaración "si es un tipo y es un tipo, entonces es un tipo" hay juicios de "es un tipo", "y", y "si ... entonces ...". La expresión no es un juicio; es el tipo que se está definiendo.

Este segundo nivel de la teoría de tipos puede resultar confuso, sobre todo en lo que respecta a la igualdad. Hay un juicio de igualdad de términos, lo que podría decir . Es una afirmación de que dos términos se reducen al mismo término canónico. También hay un juicio de igualdad de tipos, digamos eso , lo que significa que cada elemento de es un elemento del tipo y viceversa. A nivel de tipo, hay un tipo y contiene términos si hay una prueba de eso y se reduce al mismo valor. (Obviamente, los términos de este tipo se generan usando el juicio de igualdad de términos.) Por último, hay un nivel de igualdad en el idioma inglés, porque usamos la palabra "cuatro" y el símbolo " " para referirnos al término canónico . Martin-Löf denomina sinónimos como estos "iguales en términos de definición".

La descripción de los juicios a continuación se basa en la discusión en Nordström, Petersson y Smith.

La teoría formal trabaja con tipos y objetos .

Un tipo es declarado por:

Un objeto existe y está en un tipo si:

Los objetos pueden ser iguales

y los tipos pueden ser iguales

Se declara un tipo que depende de un objeto de otro tipo

y eliminado por sustitución

  • , reemplazando la variable con el objeto en .

Un objeto que depende de un objeto de otro tipo se puede hacer de dos formas. Si el objeto es "abstraído", entonces está escrito

y eliminado por sustitución

  • , reemplazando la variable con el objeto en .

El objeto dependiente del objeto también se puede declarar como una constante como parte de un tipo recursivo. Un ejemplo de tipo recursivo es:

Aquí, es un objeto constante que depende del objeto. No está asociado con una abstracción. Las constantes como se pueden eliminar definiendo igualdad. Aquí, la relación con la suma se define mediante la igualdad y la coincidencia de patrones para manejar el aspecto recursivo de :

se manipula como una constante opaca; no tiene una estructura interna para la sustitución.

Entonces, los objetos y tipos y estas relaciones se usan para expresar fórmulas en la teoría. Los siguientes estilos de juicios se utilizan para crear nuevos objetos, tipos y relaciones a partir de los existentes:

σ es un tipo bien formado en el contexto Γ.
t es un término bien formado de tipo σ en contexto Γ.
σ y τ son tipos iguales en el contexto Γ.
t y u son iguales judgmentally términos de tipo σ en el contexto Γ.
Γ es un contexto bien formado para escribir suposiciones.

Por convención, hay un tipo que representa todos los demás tipos. Se llama (o ). Dado que es un tipo, sus miembros son objetos. Hay un tipo dependiente que asigna cada objeto a su tipo correspondiente. En la mayoría de los textos nunca se escribe. A partir del contexto de la declaración, un lector casi siempre puede decir si se refiere a un tipo o si se refiere al objeto que corresponde al tipo.

Ésta es la base completa de la teoría. Todo lo demás se deriva.

Para implementar la lógica, a cada proposición se le da su propio tipo. Los objetos de esos tipos representan las diferentes formas posibles de probar la proposición. Obviamente, si no hay prueba para la proposición, entonces el tipo no tiene objetos. Los operadores como "y" y "o" que trabajan en proposiciones introducen nuevos tipos y nuevos objetos. Entonces es un tipo que depende del tipo y el tipo . Los objetos de ese tipo dependiente están definidos para existir para cada par de objetos en y . Obviamente, si o no tiene prueba y es un tipo vacío, entonces el nuevo tipo que representa también está vacío.

Esto se puede hacer para otros tipos (booleanos, números naturales, etc.) y sus operadores.

Modelos categóricos de la teoría de tipos

Utilizando el lenguaje de la teoría de categorías , RAG Seely introdujo la noción de una categoría cerrada localmente cartesiana (LCCC) como el modelo básico de la teoría de tipos. Esto ha sido refinado por Hofmann y Dybjer a Categorías con familias o Categorías con atributos basados ​​en trabajos anteriores de Cartmell.

Una categoría con familias es una categoría C de contextos (en la que los objetos son contextos y los morfismos de contexto son sustituciones), junto con un functor T  : C opFam ( Set ).

Fam ( Set ) es la categoría de familias de conjuntos, en los que los objetos son pares de un "conjunto de índice" A y una función B : XA , y morfismos son pares de funciones f  : AA' y g  : XX ' , tal que B' ° g = f ° B - en otras palabras, f mapea B a con B g ( a ) .

El funtor T asigna a un contexto G un conjunto de tipos y, para cada uno , un conjunto de términos. Los axiomas de un funtor requieren que estos jueguen armoniosamente con la sustitución. Cambio se suele escribir en la forma Af o af , donde A es un tipo en y una es un término en , y f es una sustitución de D a G . Aquí y .

La categoría C debe contener un objeto terminal (el contexto vacío) y un objeto final para una forma de producto llamada comprensión o extensión de contexto, en la que el elemento derecho es un tipo en el contexto del elemento izquierdo. Si G es un contexto, y , entonces debería haber un objeto final entre contextos D con mapeos p  : DG , q  : Tm ( D, Ap ).

Un marco lógico, como el de Martin-Löf, toma la forma de condiciones de cierre sobre los conjuntos de tipos y términos dependientes del contexto: que debería haber un tipo llamado Conjunto, y para cada conjunto un tipo, que los tipos deberían cerrarse bajo formas de suma y producto dependientes, etc.

Una teoría como la de la teoría de conjuntos predicativa expresa condiciones de cierre sobre los tipos de conjuntos y sus elementos: que deben cerrarse bajo operaciones que reflejan suma y producto dependientes, y bajo diversas formas de definición inductiva.

Extensional versus intensional

Una distinción fundamental es la teoría de tipo extensional vs intensional . En la teoría de tipo extensional, la igualdad definicional (es decir, computacional) no se distingue de la igualdad proposicional, que requiere prueba. Como consecuencia, la verificación de tipos se vuelve indecidible en la teoría de tipos extensionales porque los programas en la teoría pueden no terminar. Por ejemplo, tal teoría permite dar un tipo al combinador Y , un ejemplo detallado de esto se puede encontrar en Programación de Nordstöm y Petersson en la teoría de tipos de Martin-Löf . Sin embargo, esto no impide que la teoría de tipos extensionales sea la base de una herramienta práctica, por ejemplo, NuPRL se basa en la teoría de tipos extensionales.

En contraste, en la teoría de tipos intensional, la verificación de tipos es decidible , pero la representación de conceptos matemáticos estándar es algo más engorrosa, ya que el razonamiento intensional requiere el uso de setoides o construcciones similares. Hay muchos objetos matemáticos comunes con los que es difícil trabajar o no se pueden representar sin esto, por ejemplo, números enteros , números racionales y números reales . Los números enteros y racionales se pueden representar sin setoides, pero no es fácil trabajar con esta representación. Los números reales de Cauchy no se pueden representar sin esto.

La teoría de tipos de homotopía trabaja para resolver este problema. Permite definir tipos inductivos superiores , que no sólo definen constructores de primer orden ( valores o puntos ), sino constructores de orden superior, es decir, igualdades entre elementos ( caminos ), igualdades entre igualdades ( homotopías ), ad infinitum .

Implementaciones de la teoría de tipos

Se han implementado diferentes formas de teoría de tipos como sistemas formales subyacentes a varios asistentes de prueba . Si bien muchos se basan en las ideas de Per Martin-Löf, muchos tienen características adicionales, más axiomas o diferentes antecedentes filosóficos. Por ejemplo, el sistema NuPRL se basa en la teoría de tipos computacionales y Coq se basa en el cálculo de construcciones (co) inductivas . Los tipos dependientes también se incluyen en el diseño de lenguajes de programación como ATS , Cayenne , Epigram , Agda e Idris .

Teorías de tipo Martin-Löf

Per Martin-Löf construyó varias teorías tipográficas que se publicaron en diversas épocas, algunas de ellas mucho más tarde que cuando los preprints con su descripción se hicieron accesibles a los especialistas (entre otros Jean-Yves Girard y Giovanni Sambin). La siguiente lista intenta enumerar todas las teorías que se han descrito en forma impresa y esbozar las características clave que las distinguen entre sí. Todas estas teorías tenían productos dependientes, sumas dependientes, uniones disjuntas, tipos finitos y números naturales. Todas las teorías tenían las mismas reglas de reducción que no incluían la reducción η ni para los productos dependientes ni para las sumas dependientes, excepto MLTT79 donde se suma la reducción η para los productos dependientes.

MLTT71 fue la primera de las teorías de tipos creadas por Per Martin-Löf. Apareció en una preimpresión en 1971. Tenía un universo pero este universo tenía un nombre en sí mismo, es decir, era una teoría de tipos con, como se llama hoy, "Type in Type". Jean-Yves Girard ha demostrado que este sistema era inconsistente y la preimpresión nunca se publicó.

MLTT72 se presentó en una versión preliminar de 1972 que ya se ha publicado. Esa teoría tenía un universo V y ningún tipo de identidad. El universo era "predicativo" en el sentido de que el producto dependiente de una familia de objetos de V sobre un objeto que no estaba en V, como, por ejemplo, el propio V, no se suponía que estuviera en V. El universo era a la Russell, es decir, se escribiría directamente "T∈V" y "t∈T" (Martin-Löf usa el signo "∈" en lugar del moderno ":") sin el constructor adicional como "El".

MLTT73 fue la primera definición de una teoría de tipos que publicó Per Martin-Löf (se presentó en el Logic Colloquium 73 y se publicó en 1975). Hay tipos de identidad que él llama "proposiciones", pero como no se introduce una distinción real entre proposiciones y el resto de los tipos, el significado de esto no está claro. Existe lo que más tarde adquiere el nombre de eliminador-J pero aún sin nombre (véanse las págs. 94-95). En esta teoría hay una secuencia infinita de universos V 0 , ..., V n , .... ¡Los universos son predicativos, a la Russell y no acumulativos ! De hecho, el Corolario 3.10 de la p. 115 dice que si A∈V my B∈V n son tales que A y B son convertibles, entonces m  =  n . Esto significa, por ejemplo, que sería difícil formular univalencia en esta teoría: hay tipos contractibles en cada uno de los V i, pero no está claro cómo declararlos iguales, ya que no hay tipos de identidad que conecten V i y V j para ij .

MLTT79 se presentó en 1979 y se publicó en 1982. En este artículo, Martin-Löf introdujo los cuatro tipos básicos de juicio para la teoría de tipos dependientes que desde entonces se ha convertido en fundamental en el estudio de la metateoría de tales sistemas. También introdujo los contextos como un concepto separado en él (ver p. 161). Hay tipos de identidad con el eliminador de J (que ya aparecía en MLTT73 pero no tenía ese nombre allí) pero también con la regla que hace que la teoría sea "extensional" (p. 169). Hay tipos W. Hay una secuencia infinita de universos predicativos que son acumulativos .

Bibliopolis : hay una discusión de una teoría de tipos en el libro de Bibliopolis de 1984, pero es algo abierta y no parece representar un conjunto particular de opciones, por lo que no hay una teoría de tipos específica asociada con ella.

Ver también

Notas

Referencias

Otras lecturas

enlaces externos