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 , o MLTT ) es una teoría de tipos y un fundamento alternativo de las matemáticas . Fue creada por Per Martin-Löf , 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 , y las primeras versiones impredicativas , cuya inconsistencia fue demostrada por la paradoja de Girard , dieron paso a versiones predicativas . Sin embargo, todas las versiones conservan el diseño central de la lógica constructiva mediante tipos dependientes .

Diseño

Martin-Löf diseñó la teoría de tipos basándose en los principios del constructivismo matemático . El constructivismo exige que toda prueba de existencia contenga un «testigo». Por lo tanto, cualquier prueba de «existe un número 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 útil es que las pruebas se convierten en objetos matemáticos que pueden examinarse, compararse y manipularse.

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 ( $A\implies B$ ) corresponde al tipo de una función ( $A\to B$ Esta correspondencia se denomina 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 mediante la introducción de tipos dependientes.

teoría de tipos

Una teoría de tipos es una ontología matemática , o fundamento , que describe los objetos fundamentales que existen. En el fundamento estándar, la teoría de conjuntos combinada con la lógica matemática , el objeto fundamental es el conjunto, que es un contenedor de elementos. En la teoría de tipos, el objeto fundamental es el término, cada uno de los cuales pertenece a un único tipo.

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 basan en una lógica como la de Frege . Por lo tanto, cada característica de la teoría de tipos cumple una doble función, sirviendo tanto para las matemáticas como para la lógica.

tipo 0, tipo 1 y tipo 2

Hay tres tipos finitos: El tipo 0 no contiene términos. El tipo 1 contiene un término canónico. El tipo 2 contiene dos términos canónicos.

Debido a que el tipo 0 no contiene términos, también se le llama tipo vacío . Se utiliza para representar cualquier cosa que no pueda existir. También se escribe $\bot$ y representa todo aquello que no se puede demostrar (es decir, no puede existir una prueba de ello). En consecuencia, la negación se define como una función de ello: $\neg A:=A\to \bot$ .

Asimismo, el tipo 1 contiene un término canónico y representa la existencia. También se le llama tipo de unidad .

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

En cambio, las proposiciones se representan mediante tipos específicos. Por ejemplo, una proposición verdadera puede representarse con el tipo 1 , mientras que una proposición falsa puede representarse con el tipo 0. Sin embargo, no podemos afirmar que estas sean las únicas proposiciones; es decir, el principio del tercero excluido no se aplica a las proposiciones en la teoría de tipos intuicionista.

Constructor de tipo Σ

Los tipos Σ contienen pares ordenados. Al igual que con los tipos de pares ordenados (o 2-tuplas) típicos, un tipo Σ puede describir el producto cartesiano , $A\times B$ , de otros dos tipos, $A$ y $B$ Lógicamente, tal par ordenado contendría una prueba de $A$ y una prueba de $B$ , por lo que se puede ver un tipo de escritura como $A\wedge B$ .

Los tipos Σ son más potentes que los tipos de pares ordenados típicos debido a la dependencia de tipos. 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 una secuencia de números reales de longitud igual a la del primer término. Dicho tipo se escribiría:

$\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 usual, el tipo del segundo término no depende del valor del primer término. Por lo tanto, el tipo que describe el producto cartesiano ${\mathbb {N} }\times {\mathbb {R} }$ está escrito:

$\sum _{n{\mathbin {:}}{\mathbb {N} }}{\mathbb {R} }$

El valor del primer término, $n$ , no depende del tipo del segundo término, ${\mathbb {R} }$ .

Los tipos Σ se pueden usar para construir tuplas dependientes más largas 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 dependiente son dos enteros y una prueba de que el primer entero es menor que el segundo, descrita por el tipo:

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

La tipificación dependiente permite que los tipos Σ sirvan como cuantificador existencial . La afirmación "existe un $n$ de tipo ${\mathbb {N} }$ , de tal manera que $P(n)$ "se demuestra" se convierte en el tipo de pares ordenados donde el primer elemento es el valor $n$ de tipo ${\mathbb {N} }$ y el segundo elemento es una prueba de $P(n)$ . Observe que el tipo del segundo elemento (pruebas de $P(n)$ ) depende del valor en la primera parte del par ordenado ( $n$ ). Su tipo sería:

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

constructor de tipo Π

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 difieren 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") a dicho término.

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

$\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 a menudo se escribe simplemente con un $\to$ . De este modo, ${\mathbb {N} }\to {\mathbb {R} }$ es el tipo de funciones de números naturales a números reales. Dichos tipos Π corresponden a la implicación lógica. La proposición lógica $A\implies B$ corresponde al tipo $A\to B$ , que contiene funciones que toman pruebas de A y devuelven pruebas de B. Este tipo podría escribirse de forma más consistente como:

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

Los tipos Π también se utilizan en lógica para la cuantificación universal . La afirmación "para cada $n$ de tipo ${\mathbb {N} }$ , $P(n)$ "se demuestra" se convierte en una función de $n$ de tipo ${\mathbb {N} }$ a pruebas de $P(n)$ . Por lo tanto, dado el valor de $n$ La función genera una prueba de que $P(\,\cdot \,)$ se mantiene para ese valor. El tipo sería

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

= constructor de tipo

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

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

Es posible crear tipos = como $1=2$ 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 $1=2$ , podrías crear un término de $\bot$ . Poner eso en una función generaría una función de tipo $1=2\to \bot$ . Desde $\ldots \to \bot$ es como la teoría de tipos intuicionista define la negación, tendrías $\neg (1=2)$ o, finalmente, $1\neq 2$ .

La igualdad de las pruebas es un área de investigación activa en la teoría de la demostración y ha llevado al desarrollo de la teoría de tipos homotópicos 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 formado por un número natural y otra lista enlazada. Los tipos inductivos se pueden utilizar para definir estructuras matemáticas no acotadas como árboles , grafos , etc. De hecho, el tipo de números naturales puede definirse como un tipo inductivo, ya sea siendo $0$ o el sucesor de otro número natural.

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

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

${\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)$

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

Tipos de universo

Los tipos de universo permiten escribir demostraciones sobre todos los tipos creados con los demás constructores de tipos. Cada término en el tipo de universo ${\mathcal {U}}_{0}$ se puede asignar a un tipo creado con cualquier combinación de $0,1,2,\Sigma,\Pi,=,$ y el constructor de tipos inductivo. Sin embargo, para evitar paradojas, no hay ningún término en ${\mathcal {U}}_{n}$ que se corresponde con ${\mathcal {U}}_{n}$ para cualquier ${\mathcal {n}}\in \mathbb {N}$ . ^{[ 1 ]}

Escribir demostraciones sobre todos los "tipos pequeños" y ${\mathcal {U}}_{0}$ , debes usar ${\mathcal {U}}_{1}$ , que sí contiene un término para ${\mathcal {U}}_{0}$ pero no por sí mismo ${\mathcal {U}}_{1}$ . De manera similar, para ${\mathcal {U}}_{2}$ . Existe una jerarquía predicativa de universos, por lo que para cuantificar una prueba sobre cualquier constante fija $k$ universos, puedes usar ${\mathcal {U}}_{k+1}$ .

Los tipos de universo son un aspecto complejo de las teorías de tipos. La teoría de tipos original de Martin-Löf tuvo que modificarse para dar cuenta de la paradoja de Girard . Investigaciones posteriores abarcaron temas como los "superuniversos", los " universos de Mahlo " y los universos impredicativos.

Sentencias

La definición formal de la teoría de tipos intuicionista se escribe utilizando juicios. Por ejemplo, en la afirmación "si $A$ es un tipo y $B$ entonces es un tipo $\textstyle \sum _ {a:A}B$ es un tipo" hay juicios de "es un tipo", "y" y "si... entonces...". La expresión $\textstyle \sum _ {a:A}B$ No es un juicio; es el tipo que se está definiendo.

Este segundo nivel de la teoría de tipos puede ser confuso, particularmente en lo que respecta a la igualdad. Hay un juicio de igualdad de términos, que podría decir $4=2+2$ . 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 que $A=B$ , lo que significa cada elemento de $A$ es un elemento del tipo $B$ y viceversa. A nivel de tipo, hay un tipo $4=2+2$ y contiene términos si hay una prueba de que $4$ y $2+2$ reducir al mismo valor. (Los términos de este tipo se generan utilizando el juicio de igualdad de términos). Por último, hay un nivel de igualdad en lengua inglesa, porque usamos la palabra "cuatro" y el símbolo " $4$ " para referirse al término canónico $SSSS0$ Martin-Löf denomina a sinónimos como estos "definitivamente equivalentes".

La descripción de los juicios que figura a continuación se basa en el análisis realizado en Nordström, Petersson y Smith.

La teoría formal trabaja con tipos y objetos .

Un tipo se declara mediante:

$A\ {\mathsf {Tipo}}$

Un objeto existe y pertenece a un tipo si:

$a{\mathbin {:}}A$

Los objetos pueden ser iguales

$a=b$

y los tipos pueden ser iguales

$A=B$

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

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

y eliminado por sustitución

$B[x/a]$ , reemplazando la variable $x$ con el objeto $a$ en $B$ .

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

$[x]b$

y eliminado por sustitución

$b[x/a]$ , reemplazando la variable $x$ con el objeto $a$ en $b$ .

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

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

Aquí, $S$ es un objeto constante que depende de otro objeto. No está asociado a una abstracción. Constantes como $S$ se puede eliminar definiendo la igualdad. Aquí la relación con la suma se define usando la igualdad y usando la coincidencia de patrones para manejar el aspecto recursivo de $S$ :

{\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}}

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

Así pues, los objetos, los tipos y estas relaciones se utilizan para expresar fórmulas en la teoría. Los siguientes estilos de juicio 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 llama ${\mathcal {U}}$ (o $\operatorname {Set}$ ). Desde ${\mathcal {U}}$ es un tipo, sus miembros son objetos. Hay un tipo dependiente. $\operatorname {El}$ que asigna cada objeto a su tipo correspondiente. En la mayoría de los textos $\operatorname {El}$ nunca está escrito. A partir del contexto de la declaración, un lector casi siempre puede saber si $A$ se refiere a un tipo, o si se refiere al objeto en ${\mathcal {U}}$ que corresponde al tipo.

Esta es la base completa de la teoría. Todo lo demás es derivado.

Para implementar la lógica, a cada proposición se le asigna un tipo propio. Los objetos de esos tipos representan las diferentes maneras posibles de demostrar la proposición. Si no hay demostración para la proposición, entonces el tipo no contiene objetos. Los operadores como "y" y "o", que funcionan con proposiciones, introducen nuevos tipos y nuevos objetos. Por lo tanto, $A\times B$ es un tipo que depende del tipo $A$ y el tipo $B$ . Los objetos de ese tipo dependiente se definen para existir para cada par de objetos en $A$ y $B$ . Si alguno $A$ o $B$ no tiene prueba y es un tipo vacío, entonces el nuevo tipo que representa $A\times B$ 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 categoría cerrada localmente cartesiana (LCCC) como modelo básico de la teoría de tipos. Esta noción fue refinada por Hofmann y Dybjer a Categorías con Familias o Categorías con Atributos, basándose en trabajos previos de Cartmell. ^{[ 2 ]}

Extensional versus intensional

Una distinción fundamental radica en la teoría de tipos extensional frente a la intensional . En la teoría de tipos extensional, la igualdad definicional (es decir, computacional) no se distingue de la igualdad proposicional, que requiere demostración. En consecuencia, la verificación de tipos se vuelve indecidible en la teoría de tipos extensional porque los programas en dicha teoría podrían no terminar. Por ejemplo, esta teoría permite asignar un tipo al combinador Y ; un ejemplo detallado de esto se puede encontrar en el artículo de Nordstöm y Petersson, «Programming in Martin-Löf's Type Theory» ^{[ 3 ]} . Sin embargo, esto no impide que la teoría de tipos extensional sirva de base para una herramienta práctica; por ejemplo, Nuprl se basa en la teoría de tipos extensional.

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 que no se pueden representar sin esto, por ejemplo, los números enteros , los números racionales y los números reales . Los enteros y los números racionales se pueden representar sin setoides, pero esta representación es difícil de manejar. Los números reales de Cauchy no se pueden representar sin esto. ^{[ 4 ]}

La teoría de tipos homotópicos trabaja para resolver este problema. Permite definir tipos inductivos superiores , que no solo 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 ), 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 demostración . Si bien muchos se basan en las ideas de Per Martin-Löf, otros han añadido 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 Rocq en el cálculo de construcciones (co)inductivas . ^Los tipos dependientes también se utilizan en el diseño de lenguajes de programación como ATS , Cayenne , Epigram , Agda [ ⁶^] e Idris ^[⁷^] .

Teorías del tipo Martin-Löf

Per Martin-Löf construyó varias teorías de tipos que se publicaron en distintos momentos, algunas mucho después de que las preimpresiones con su descripción se volvieran accesibles a los especialistas (entre ellos 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 productos dependientes ni para sumas dependientes, excepto MLTT79, donde se añade la η-reducción para productos dependientes.

MLTT71 fue la primera teoría de tipos creada por Per Martin-Löf. Apareció en una prepublicación en 1971. Constaba de un único universo, pero este universo tenía nombre propio; es decir, era una teoría de tipos con, como se denomina hoy en día, "tipo dentro de tipo". Jean-Yves Girard demostró que este sistema era inconsistente, y la prepublicación nunca se publicó.

MLTT72 se presentó en una preimpresión de 1972 que ahora se ha publicado. ^{[ 8 ]} Esa teoría tenía un universo V y ningún tipo 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 el propio V, no se asumía que estuviera en V. El universo era a la manera de los Principia Mathematica de Russell , es decir, se escribiría directamente "T∈V" y "t∈T" (Martin-Löf usa el signo "∈" en lugar del moderno ":") sin un constructor añadido como "El".

MLTT73 fue la primera definición de una teoría de tipos que publicó Per Martin-Löf (fue presentada en el Logic Colloquium '73 y publicada en 1975 ^{[ 9 ]} ). Hay tipos identidad, que él describe como "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. Hay lo que más tarde adquiere el nombre de J-eliminador 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, a 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 .

MLTT79 se presentó en 1979 y se publicó 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 él (ver pág. 161). Hay tipos de identidad con el J-eliminador (que ya apareció en MLTT73 pero no tenía este nombre allí) pero también con la regla que hace que la teoría sea "extensional" (pág. 169). Hay tipos W. Hay una secuencia infinita de universos predicativos que son acumulativos .

Bibliopolis : en el libro Bibliopolis de 1984 se discute una teoría de tipos , ^{[ 11 ]} 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 a ella.

Véase también

Notas

↑ Bertot, Yves; Castéran, Pierre (2004). Demostración interactiva de teoremas y desarrollo de programas: Coq'Art: el cálculo de construcciones inductivas . Textos de informática teórica. Berlín Heidelberg: Springer. ISBN 978-3-540-20854-9.
↑ Clairambault, Pierre; Dybjer, Peter (2014). "La biequivalencia de categorías cerradas localmente cartesianas y teorías de tipo Martin-Löf" . Mathematical Structures in Computer Science . 24 (6). arXiv : 1112.3456 . doi : 10.1017/S0960129513000881 . ISSN 0960-1295 . S2CID 416274 .
↑ Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programación en la teoría de tipos de Martin-Löf . Prensa de la Universidad de Oxford, pág. 90.
↑ Altenkirch, Thorsten; Anberrée, Thomas; Li, Nuo. Cocientes definibles en la teoría de tipos (PDF) (Informe). Archivado del original (PDF) el 19 de abril de 2024.
↑ Allen, SF; Bickford, M.; Constable, RL; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. (2006). "Innovaciones en la teoría de tipos computacional usando Nuprl" . Journal of Applied Logic . 4 (4): 428– 469. doi : 10.1016/j.jal.2005.10.005 .
↑ Norell, Ulf (2009). "Programación con tipos dependientes en Agda". Actas del 4.º taller internacional sobre tipos en el diseño e implementación de lenguajes . TLDI '09. Nueva York, NY, EE. UU.: ACM. págs. 1–2 . CiteSeerX 10.1.1.163.7149 . doi : 10.1145/1481861.1481862 . ISBN 9781605584201. S2CID 1777213 .
↑ Brady, Edwin (2013). "Idris, un lenguaje de programación de propósito general con tipado dependiente: diseño e implementación" . Journal of Functional Programming . 23 (5): 552– 593. doi : 10.1017/S095679681300018X . ISSN 0956-7968 . S2CID 19895964 .
↑ Martin-Löf, Per (1998). Una teoría intuicionista de los tipos, Veinticinco años de teoría constructiva de tipos (Venecia, 1995) . Oxford Logic Guides. Vol. 36. Nueva York: Oxford University Press. pp. 127–172 .
↑ Martin-Löf, Per (1975). «Una teoría intuicionista de los tipos: parte predicativa». Estudios en lógica y fundamentos de las matemáticas . Coloquio de lógica '73 (Bristol, 1973). Vol. 80. Ámsterdam: North-Holland. págs. 73–118 .
↑ Martin-Löf, Per (1982). «Matemáticas constructivas y programación informática». Estudios de lógica y fundamentos de las matemáticas . Lógica, metodología y filosofía de la ciencia, VI (Hannover, 1979). Vol. 104. Ámsterdam: North-Holland. pp. 153–175 .
↑ Martin-Löf, Per (1984). Teoría de tipos intuicionista, Estudios en teoría de la demostración (notas de clase de Giovanni Sambin) . Vol. 1. Bibliopolis. pp. iv, 91.

Referencias

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

Lecturas adicionales

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 teoría de tipos intuicionista . Saltador. ISBN 978-94-007-1735-0.

Enlaces externos

Proyecto Tipos de la UE: Tutoriales – apuntes y diapositivas de la Escuela de Verano Tipos 2005
n-Categorías - Esbozo de una definición – carta de John Baez y James Dolan a Ross Street , 29 de noviembre de 1995

[1] Bertot, Yves; Castéran, Pierre (2004). Demostración interactiva de teoremas y desarrollo de programas: Coq'Art: el cálculo de construcciones inductivas . Textos de informática teórica. Berlín Heidelberg: Springer. ISBN 978-3-540-20854-9.

[2] Clairambault, Pierre; Dybjer, Peter (2014). "La biequivalencia de categorías cerradas localmente cartesianas y teorías de tipo Martin-Löf" . Mathematical Structures in Computer Science . 24 (6). arXiv : 1112.3456 . doi : 10.1017/S0960129513000881 . ISSN 0960-1295 . S2CID 416274 .

[3] Bengt Nordström; Kent Petersson; Jan M. Smith (1990). Programación en la teoría de tipos de Martin-Löf . Prensa de la Universidad de Oxford, pág. 90.

[4] Altenkirch, Thorsten; Anberrée, Thomas; Li, Nuo. Cocientes definibles en la teoría de tipos (PDF) (Informe). Archivado del original (PDF) el 19 de abril de 2024.

[5] Allen, SF; Bickford, M.; Constable, RL; Eaton, R.; Kreitz, C.; Lorigo, L.; Moran, E. (2006). "Innovaciones en la teoría de tipos computacional usando Nuprl" . Journal of Applied Logic . 4 (4): 428– 469. doi : 10.1016/j.jal.2005.10.005 .

[6] Norell, Ulf (2009). "Programación con tipos dependientes en Agda". Actas del 4.º taller internacional sobre tipos en el diseño e implementación de lenguajes . TLDI '09. Nueva York, NY, EE. UU.: ACM. págs. 1–2 . CiteSeerX 10.1.1.163.7149 . doi : 10.1145/1481861.1481862 . ISBN 9781605584201. S2CID 1777213 .

[7] Brady, Edwin (2013). "Idris, un lenguaje de programación de propósito general con tipado dependiente: diseño e implementación" . Journal of Functional Programming . 23 (5): 552– 593. doi : 10.1017/S095679681300018X . ISSN 0956-7968 . S2CID 19895964 .

[8] Martin-Löf, Per (1998). Una teoría intuicionista de los tipos, Veinticinco años de teoría constructiva de tipos (Venecia, 1995) . Oxford Logic Guides. Vol. 36. Nueva York: Oxford University Press. pp. 127–172 .

[9] Martin-Löf, Per (1975). «Una teoría intuicionista de los tipos: parte predicativa». Estudios en lógica y fundamentos de las matemáticas . Coloquio de lógica '73 (Bristol, 1973). Vol. 80. Ámsterdam: North-Holland. págs. 73–118 .

[10] Martin-Löf, Per (1982). «Matemáticas constructivas y programación informática». Estudios de lógica y fundamentos de las matemáticas . Lógica, metodología y filosofía de la ciencia, VI (Hannover, 1979). Vol. 104. Ámsterdam: North-Holland. pp. 153–175 .

[MartinLöf1984-11] Martin-Löf, Per (1984). Teoría de tipos intuicionista, Estudios en teoría de la demostración (notas de clase de Giovanni Sambin) . Vol. 1. Bibliopolis. pp. iv, 91.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

Los

6

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]