Teoría de tipos intuicionista

La teoría de tipos intuicionista (también conocida como teoría de tipos constructiva o teoría de tipos de Martin-Löf ( MLTT )) 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. Existen múltiples versiones de la teoría de tipos: Martin-Löf propuso variantes intensionales y extensionales de la teoría y las primeras versiones impredicativas , que se demostraron inconsistentes por la paradoja de Girard , dieron paso a versiones predicativas . Sin embargo, todas las versiones mantienen el diseño central de la lógica constructiva utilizando tipos dependientes .

Martin-Löf diseñó la teoría de tipos sobre la base de los principios del constructivismo matemático . El constructivismo exige que cualquier prueba de existencia contenga un "testigo". Por lo tanto, cualquier prueba de "existe un primo mayor que 1000" debe identificar un número específico que sea a la vez primo y mayor que 1000. La teoría de tipos intuicionista logró este objetivo de diseño al internalizar la interpretación de BHK . Una consecuencia útil es que las pruebas se convierten en objetos matemáticos que se pueden examinar, comparar y manipular.

Los constructores de tipos de la teoría de tipos intuicionista se construyeron para seguir una correspondencia uno a uno con los conectores lógicos. Por ejemplo, el conector lógico llamado implicación ( ) corresponde al tipo de una función ( ). Esta correspondencia se llama isomorfismo de Curry-Howard . Las teorías de tipos anteriores también habían seguido este isomorfismo, pero la de Martin-Löf fue la primera en extenderlo a la lógica de predicados introduciendo tipos dependientes. ${\displaystyle A\implica B}$${\displaystyle A\to B}$

La teoría de tipos intuicionista tiene tres tipos finitos, que luego se componen utilizando cinco constructores de tipos diferentes. A diferencia de las teorías de conjuntos , las teorías de tipos no se construyen sobre una lógica como la de Frege . Por lo tanto, cada característica de la teoría de tipos cumple una doble función como característica de las matemáticas y la lógica.

Si no estás familiarizado con la teoría de tipos y conoces la teoría de conjuntos, un breve resumen es el siguiente: los tipos contienen términos, al igual que los conjuntos contienen elementos. Los términos pertenecen a un único tipo. Términos como y se computan ("reducen") hasta convertirse en términos canónicos como 4. Para obtener más información, consulta el artículo sobre teoría de tipos .${\estilo de visualización 2+2}$${\estilo de visualización 2\cdot 2}$

Hay tres tipos finitos: el tipo 0 contiene 0 términos, el tipo 1 contiene 1 término canónico y el tipo 2 contiene 2 términos canónicos.

Debido a que el tipo 0 contiene 0 términos, también se lo denomina tipo vacío . Se utiliza para representar cualquier cosa que no pueda existir. También se escribe y representa cualquier cosa que no se pueda demostrar (es decir, no puede existir una prueba de ello). Como resultado, la negación se define como una función de él: . ${\estilo de visualización \bot}$${\displaystyle \neg A:=A\to \bot }$

De la misma manera, el tipo 1 contiene 1 término canónico y representa la existencia. También se le denomina tipo unidad .

Por último, el tipo 2 contiene 2 términos canónicos. Representa una elección definitiva entre dos valores. Se utiliza para valores booleanos, pero no para proposiciones.

En cambio, las proposiciones se representan mediante tipos particulares. Por ejemplo, una proposición verdadera puede representarse mediante el tipo 1 , mientras que una proposición falsa puede representarse mediante el tipo 0. Pero no podemos afirmar que estas sean las únicas proposiciones, es decir, la ley del tercio excluido no se cumple para las proposiciones en la teoría de tipos intuicionista.

Los tipos Σ contienen pares ordenados. Al igual que los tipos de pares ordenados (o de 2-tuplas) típicos, un tipo Σ puede describir el producto cartesiano , , de otros dos tipos, y . Lógicamente, un par ordenado de este tipo contendría una prueba de y una prueba de , por lo que se puede ver un tipo de este tipo escrito como . ${\displaystyle A\times B}$${\estilo de visualización A}$${\estilo de visualización B}$${\estilo de visualización A}$${\estilo de visualización B}$${\displaystyle A\cuña B}$

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 puede ser un número natural y el tipo del segundo término puede ser una secuencia de números reales de longitud igual al primer término. Un tipo de este tipo se escribiría:

${\displaystyle \sum _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)}$

Utilizando la terminología de la teoría de conjuntos, esto es similar a una unión disjunta indexada de conjuntos. En el caso del producto cartesiano habitual, el tipo del segundo término no depende del valor del primer término. Por lo tanto, el tipo que describe el producto cartesiano se escribe: ${\displaystyle {\mathbb {N}}\times {\mathbb {R}}}$

${\displaystyle \sum_{n{\mathbin {:}}{\mathbb {N}}}{\mathbb {R}}}$

Es importante señalar aquí que el valor del primer término, , no depende del tipo del segundo término, . ${\estilo de visualización n}$${\displaystyle {\mathbb {R} }}$

Los tipos Σ se pueden utilizar para construir tuplas más largas con tipos dependientes que se utilizan en matemáticas y los registros o estructuras que se utilizan en la mayoría de los lenguajes de programación. Un ejemplo de una tupla de 3 tipos con tipos dependientes son dos números enteros y una prueba de que el primer número entero es menor que el segundo, descrito por el tipo:

${\displaystyle \sum _{m{\mathbin {:}}{\mathbb {Z} }}{\sum _{n{\mathbin {:}}{\mathbb {Z} }}((m<n)={\text{True}})}}$

La tipificación dependiente permite que los Σ-tipos cumplan la función de cuantificador existencial . La afirmación "existe un del tipo , tal que se demuestra" 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: ${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle P(n)}$${\displaystyle n}$

${\displaystyle \sum _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

Los tipos Π contienen funciones. Al igual que los tipos de función 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, se busca el valor del argumento en un conjunto de pares ordenados. En la teoría de tipos, el argumento se sustituye en un término y luego se aplica un cálculo ("reducción") al término.

A modo de ejemplo, el tipo de una función que, dado un número natural , devuelve un vector que contiene números reales se escribe: ${\displaystyle n}$${\displaystyle n}$

${\displaystyle \prod _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)}$

Cuando el tipo de salida no depende del valor de entrada, el tipo de función se suele escribir simplemente con un . Por lo tanto, es el tipo de funciones desde números naturales hasta números reales. Estos 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: ${\displaystyle \to }$${\displaystyle {\mathbb {N} }\to {\mathbb {R} }}$${\displaystyle A\implies B}$${\displaystyle A\to B}$

${\displaystyle \prod _{a{\mathbin {:}}A}B}$

Los tipos Π también se utilizan en lógica para cuantificación universal . La afirmación "para cada uno de tipo , se demuestra" se convierte en una función de tipo , para 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 ${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle P(\,\cdot \,)}$

${\displaystyle \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

Los tipos = se crean a partir de dos términos. Dados dos términos como y , puedes 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 tanto y como computan como el término canónico , habrá un término del tipo . En la teoría de tipos intuicionista, hay una única forma de introducir los tipos = y es mediante la reflexividad : ${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\displaystyle 2+2=2\cdot 2}$${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\displaystyle 4}$${\displaystyle 2+2=2\cdot 2}$

${\displaystyle \operatorname {refl} {\mathbin {:}}\prod _{a{\mathbin {:}}A}(a=a).}$

Es posible crear tipos = como cuando 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 . Como es como la teoría de tipos intuicionista define la negación, tendría o, finalmente, . ${\displaystyle 1=2}$${\displaystyle 1=2}$${\displaystyle \bot }$${\displaystyle 1=2\to \bot }$${\displaystyle \ldots \to \bot }$${\displaystyle \neg (1=2)}$${\displaystyle 1\neq 2}$

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.

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 se puede definir como un tipo inductivo, que puede ser o ser el sucesor de otro número natural. ${\displaystyle 0}$

Los tipos inductivos definen nuevas constantes, como el cero y la función sucesora . Como no tiene una definición y no se puede evaluar mediante sustitución, términos como y se convierten en los términos canónicos de los números naturales. ${\displaystyle 0{\mathbin {:}}{\mathbb {N} }}$${\displaystyle S{\mathbin {:}}{\mathbb {N} }\to {\mathbb {N} }}$${\displaystyle S}$${\displaystyle S0}$${\displaystyle SSS0}$

Las demostraciones de tipos inductivos son posibles gracias a la inducción . Cada nuevo tipo inductivo viene con su propia regla inductiva. Para demostrar un predicado para cada número natural, se utiliza la siguiente regla: ${\displaystyle P(\,\cdot \,)}$

${\displaystyle {\operatorname {{\mathbb {N} }-elim} }\,{\mathbin {:}}P(0)\,\to \left(\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)\to P(S(n))\right)\to \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

Los tipos inductivos en la teoría de tipos intuicionista se definen en términos de tipos W, el tipo de árboles bien fundados . Trabajos posteriores en la teoría de tipos generaron tipos coinductivos, inducción-recursión e inducción-inducción para trabajar con tipos con tipos de autorreferencialidad más oscuros. Los tipos inductivos superiores permiten definir la igualdad entre términos.

Los tipos de universo permiten escribir pruebas sobre todos los tipos creados con los demás 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 tipos inductivo. Sin embargo, para evitar paradojas, no hay ningún término en que se asigne a for any . ^[1]${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle 0,1,2,\Sigma ,\Pi ,=,}$${\displaystyle {\mathcal {U}}_{n}}$${\displaystyle {\mathcal {U}}_{n}}$${\displaystyle {\mathcal {n}}\in \mathbb {N} }$

Para escribir pruebas sobre todos los "tipos pequeños" y , debe utilizar , que contiene un término para , pero no para sí mismo . De manera similar, para . Existe una jerarquía predicativa de universos, por lo que para cuantificar una prueba sobre cualquier universo constante fijo , puede utilizar . ${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{2}}$${\displaystyle k}$${\displaystyle {\mathcal {U}}_{k+1}}$

Los tipos de universos son una característica complicada de las teorías de tipos. La teoría de tipos original de Martin-Löf tuvo que modificarse para tener en cuenta la paradoja de Girard . Investigaciones posteriores abordaron temas como los "superuniversos", los " universos de Mahlo " y los universos impredicativos.

La definición formal de la teoría de tipos intuicionista se escribe utilizando juicios. Por ejemplo, en la afirmació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 define. ${\displaystyle A}$${\displaystyle B}$${\displaystyle \textstyle \sum _{a:A}B}$${\displaystyle \textstyle \sum _{a:A}B}$

Este segundo nivel de la teoría de tipos puede ser confuso, particularmente cuando se trata de igualdad. Existe un juicio de igualdad de términos, que podría decir . Es una afirmación de que dos términos se reducen al mismo término canónico. También existe un juicio de igualdad de tipos, digamos que , lo que significa que cada elemento de es un elemento del tipo y viceversa. En el nivel de tipos, hay un tipo y contiene términos si hay una prueba de que y se reducen al mismo valor. (Los términos de este tipo se generan utilizando el juicio de igualdad de términos). Por último, existe un nivel de igualdad en inglés, porque usamos la palabra "cuatro" y el símbolo " " para referirnos al término canónico . Martin-Löf llama a sinónimos como estos "definitivamente iguales". ${\displaystyle 4=2+2}$${\displaystyle A=B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle 4=2+2}$${\displaystyle 4}$${\displaystyle 2+2}$${\displaystyle 4}$${\displaystyle SSSS0}$

La descripción de las sentencias que figuran a continuación se basa en el debate de Nordström, Petersson y Smith.

La teoría formal trabaja con tipos y objetos .

Un tipo se declara mediante:

• ${\displaystyle A\ {\mathsf {Type}}}$

Un objeto existe y es de un tipo si:

• ${\displaystyle a{\mathbin {:}}A}$

Los objetos pueden ser iguales

• ${\displaystyle a=b}$

y los tipos pueden ser iguales

• ${\displaystyle A=B}$

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

• ${\displaystyle (x{\mathbin {:}}A)B}$

y eliminado por sustitución

• ${\displaystyle B[x/a]}$, reemplazando la variable con el objeto en .${\displaystyle x}$${\displaystyle a}$${\displaystyle B}$

Un objeto que depende de un objeto de otro tipo se puede hacer de dos maneras. Si el objeto es "abstraído", entonces se escribe

• ${\displaystyle [x]b}$

y eliminado por sustitución

• ${\displaystyle b[x/a]}$, reemplazando la variable con el objeto en .${\displaystyle x}$${\displaystyle a}$${\displaystyle b}$

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

• ${\displaystyle 0{\mathbin {:}}\mathbb {N} }$
• ${\displaystyle S{\mathbin {:}}\mathbb {N} \to \mathbb {N} }$

Aquí, hay una constante que depende de un objeto. No está asociada a una abstracción. Las constantes como se pueden eliminar definiendo la igualdad. Aquí, la relación con la suma se define utilizando la igualdad y la coincidencia de patrones para manejar el aspecto recursivo de : ${\displaystyle S}$${\displaystyle S}$${\displaystyle S}$

${\displaystyle {\begin{aligned}\operatorname {add} &{\mathbin {:}}\ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}}$

${\displaystyle S}$se manipula como una constante opaca: no tiene estructura interna para la sustitución.

Por lo tanto, los objetos y los tipos y estas relaciones se utilizan 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:

Por convención, existe un tipo que representa a todos los demás tipos. Se denomina (o ). Como es un tipo, sus miembros son objetos. Existe 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 saber si se refiere a un tipo o si se refiere al objeto que corresponde al tipo. ${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {Set} }$${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {El} }$${\displaystyle \operatorname {El} }$${\displaystyle A}$${\displaystyle {\mathcal {U}}}$

Ésta es la base fundamental de la teoría. Todo lo demás es derivado.

Para implementar la lógica, a cada proposición se le asigna su propio tipo. Los objetos en esos tipos representan las diferentes formas posibles de probar la proposición. Si no hay prueba para la proposición, entonces el tipo no tiene objetos en él. Los operadores como "y" y "o" que funcionan en proposiciones introducen nuevos tipos y nuevos objetos. Por lo tanto, es un tipo que depende del tipo y el tipo . Los objetos en ese tipo dependiente están definidos para existir para cada par de objetos en y . Si o no tiene prueba y es un tipo vacío, entonces el nuevo tipo que representa también está vacío. ${\displaystyle A\times B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\times B}$

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

Utilizando el lenguaje de la teoría de categorías , RAG Seely introdujo la noción de categoría cartesiana cerrada localmente (LCCC) como modelo básico de la teoría de tipos. Hofmann y Dybjer la refinaron hasta convertirla en categorías con familias o categorías con atributos, basándose en trabajos anteriores de Cartmell. ^[2]

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 funtor T  : C ^op → Fam ( Set ).

Fam ( Conjunto ) es la categoría de familias de Conjuntos, en la que los objetos son pares ⁠ ⁠${\displaystyle (A,B)}$ de un "conjunto índice" A y una función B : X → A , y los morfismos son pares de funciones f  : A → A' y g  : X → X' , tales que B' _° g = f _° B – en otras palabras, f mapea B _a a B _{g ( a )} .

El funtor T asigna a un contexto G un conjunto de tipos${\displaystyle Ty(G)}$ y, para cada uno ,${\displaystyle A:Ty(G)}$ un conjunto de términos${\displaystyle Tm(G,A)}$ . Los axiomas para un funtor requieren que estos jueguen armoniosamente con la sustitución. La sustitución se escribe usualmente en la forma Af o af , donde A es un tipo en y a${\displaystyle Ty(G)}$ es un término en , y f es una sustitución de D a G . Aquí y .${\displaystyle Tm(G,A)}$${\displaystyle Af:Ty(D)}$${\displaystyle af:Tm(D,Af)}$

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 ⁠ ⁠${\displaystyle A:Ty(G)}$ , entonces debería haber un objeto ⁠ ⁠${\displaystyle (G,A)}$ final entre los contextos D con asignaciones p  : D → G , 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 estar cerrados bajo formas de suma y producto dependientes, y así sucesivamente.

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

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

Por el contrario, en la teoría de tipos intensionales la comprobació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 que 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 esta representación es difícil de trabajar. Los números reales de Cauchy no se pueden representar sin esto. ^[4]

La teoría de tipos de homotopía resuelve este problema, ya que permite definir tipos inductivos superiores que no sólo definen constructores de primer orden ( valores o puntos ), sino también constructores de orden superior, es decir, igualdades entre elementos ( caminos ), igualdades entre igualdades ( homotopías ) , etc.

Se han implementado diferentes formas de teoría de tipos como sistemas formales subyacentes a una serie de asistentes de prueba . Si bien muchas se basan en las ideas de Per Martin-Löf, muchas han agregado características, más axiomas o un trasfondo filosófico diferente. Por ejemplo, el sistema Nuprl se basa en la teoría de tipos computacional [ ^5] y Coq se basa en el cálculo de construcciones (co)inductivas . Los tipos dependientes también aparecen en el diseño de lenguajes de programación como ATS , Cayenne , Epigram , Agda ^[6] e Idris ^[7] .

Per Martin-Löf construyó varias teorías de tipos que se publicaron en diversas épocas, algunas de ellas mucho después de que los preprints con su descripción se hicieran accesibles a los especialistas (entre otros, Jean-Yves Girard y Giovanni Sambin). La lista a continuación 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 productos dependientes ni para sumas dependientes, excepto MLTT79 donde se agrega la η-reducción para productos dependientes.

MLTT71 fue la primera teoría de tipos creada por Per Martin-Löf. Apareció en un preprint 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, "Tipo en Tipo". Jean-Yves Girard ha demostrado que este sistema era inconsistente, y el preprint nunca fue publicado.

MLTT72 fue presentada en una preimpresión de 1972 que ahora ha sido publicada. ^[8] Esa teoría tenía un universo V y ningún tipo de identidad (=-tipos). 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, V mismo, no se suponía que estuviera en V. El universo era à la Principia Mathematica de Russell , es decir, uno escribiría directamente "T∈V" y "t∈T" (Martin-Löf usa el signo "∈" en lugar del moderno ":") sin un constructor agregado como "El".

MLTT73 fue la primera definición de una teoría de tipos que Per Martin-Löf publicó (fue presentada en el Colloquium de Lógica '73 y publicada en 1975 ^[9] ). Hay tipos identidad, que él describe como "proposiciones", pero como no se introduce ninguna distinción real entre proposiciones y el resto de tipos, el significado de esto no está claro. Hay lo que más tarde adquiere el nombre de J-eliminator pero aún sin nombre (ver pp. 94-95). Hay en esta teoría una secuencia infinita de universos V ₀ , ..., V _n , ... . Los universos son predicativos, à la Russell y no acumulativos . De hecho, el Corolario 3.10 en la p. 115 dice que si A∈V _m y B∈V _n son tales que A y B son convertibles entonces m  =  n . Esto significa, por ejemplo, que sería difícil formular un axioma de univalencia en esta teoría: hay tipos contráctiles en cada uno de los V _i , pero no está claro cómo declararlos iguales ya que no hay tipos identidad que conecten V _i y V _j para i ≠ j .

MLTT79 fue presentado en 1979 y publicado en 1982. ^[10] 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 vuelto fundamental en el estudio de la metateoría de tales sistemas. También introdujo los contextos como un concepto separado en ella (ver p. 161). Hay tipos de identidad con el J-eliminador (que ya aparecía en MLTT73 pero no tenía este 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 sobre una teoría de tipos en el libro Bibliopolis de 1984, ^[11] pero es algo abierta y no parece representar un conjunto particular de opciones y por lo tanto no hay una teoría de tipos específica asociada con ella.

• Lógica intuicionista
• Cálculo lambda tipificado

• Martin-Löf, Per ; Sambin, Giovanni (1984). Teoría de tipos intuicionista (PDF) . Nápoles: Bibliópolis. ISBN 978-8870881059.OCLC 12731401  .

• Notas de Per Martin-Löf, registradas por Giovanni Sambin (1980)
• Nordström, Bengt; Petersson, Kent; Smith, enero M. (1990). Programación en la teoría de tipos de Martin-Löf. Prensa de la Universidad de Oxford. ISBN 9780198538141.
• Thompson, Simon (1991). Teoría de tipos y programación funcional. Addison-Wesley. ISBN 0-201-41667-0.
• Granström, Johan G. (2011). Tratado sobre la teoría de tipos intuicionista. Saltador. ISBN 978-94-007-1735-0.

• Proyecto EU Types: Tutoriales: notas de clase y diapositivas de la Escuela de verano de Types 2005
• n-Categorías: esbozo de una definición – carta de John Baez y James Dolan a Ross Street , 29 de noviembre de 1995