Teoría Del Tipo Intuicionista

Tabla de contenido:

Teoría Del Tipo Intuicionista
Teoría Del Tipo Intuicionista

Vídeo: Teoría Del Tipo Intuicionista

Vídeo: Teoría Del Tipo Intuicionista
Vídeo: Logicismo vs Intuicionismo vs Formalismo vs Realismo | Filosofía de las matemáticas. 2024, Marzo
Anonim

Navegación de entrada

  • Contenido de entrada
  • Bibliografía
  • Herramientas académicas
  • Vista previa de PDF de amigos
  • Información de autor y cita
  • Volver arriba

Teoría del tipo intuicionista

Publicado por primera vez el viernes 12 de febrero de 2016; revisión sustantiva lun 8 de junio de 2020

La teoría de tipos intuitiva (también teoría de tipos constructiva o teoría de tipos de Martin-Löf) es un sistema lógico formal y una base filosófica para las matemáticas constructivas. Es un sistema a gran escala cuyo objetivo es desempeñar un papel similar para las matemáticas constructivas como lo hace la teoría de conjuntos de Zermelo-Fraenkel para las matemáticas clásicas. Se basa en el principio de proposiciones como tipos y aclara la interpretación de Brouwer-Heyting-Kolmogorov de la lógica intuicionista. Extiende esta interpretación al entorno más general de la teoría del tipo intuicionista y, por lo tanto, proporciona una concepción general no solo de lo que es una prueba constructiva, sino también de lo que es un objeto matemático constructivo. La idea principal es que los conceptos matemáticos como elementos, conjuntos y funciones se explican en términos de conceptos de programación como estructuras de datos,tipos de datos y programas. Este artículo describe el sistema formal de la teoría del tipo intuicionista y sus fundamentos semánticos.

En esta entrada, primero damos una visión general de los aspectos más importantes de la teoría del tipo intuicionista, una especie de "resumen extendido". Está destinado a un lector que ya está algo familiarizado con la teoría. La Sección 2, por otro lado, está destinada a un lector que es nuevo en la teoría del tipo intuicionista pero familiarizado con la lógica tradicional, incluida la lógica proposicional y predicada, la aritmética y la teoría de conjuntos. Aquí presentamos informalmente varios aspectos que distinguen la teoría del tipo intuicionista de estas teorías tradicionales. En la Sección 3 presentamos una versión básica de la teoría, cercana a la primera versión publicada de Martin-Löf de 1972. El lector que estaba intrigado por la informalidad de la Sección 2 ahora verá en detalle cómo se desarrolla la teoría. La sección 4 presenta una serie de extensiones importantes de la teoría básica. En particular,enfatiza el papel central de las definiciones inductivas (e inductivas-recursivas). La sección 5 presenta las ideas filosóficas subyacentes, incluida la teoría del significado desarrollada por Martin-Löf. Mientras que la Sección 5 trata sobre filosofía y fundamentos, la Sección 6 ofrece una visión general de los modelos matemáticos de la teoría. Finalmente, en la Sección 7, describimos varias variaciones importantes de la teoría "intensional" central de Martin-Löf descrita en las Secciones 3 y 4.describimos varias variaciones importantes de la teoría "intensional" central de Martin-Löf descrita en las secciones 3 y 4.describimos varias variaciones importantes de la teoría "intensional" central de Martin-Löf descrita en las secciones 3 y 4.

  • 1. Información general
  • 2. Propuestas como tipos

    • 2.1 Teoría del tipo intuicionista: ¿una nueva forma de ver la lógica?
    • 2.2 La correspondencia de Curry-Howard
    • 2.3 Conjuntos de objetos de prueba
    • 2.4 Tipos dependientes
    • 2.5 Propuestas como tipos en teoría de tipo intuicionista
  • 3. Teoría básica del tipo intuicionista

    • 3.1 Juicios
    • 3.2 Formularios de juicio
    • 3.3 Reglas de inferencia
    • 3.4 Lógica de predicados intuitiva
    • 3.5 Números naturales
    • 3.6 El universo de los tipos pequeños
    • 3.7 Identidad proposicional
    • 3.8 El axioma de elección es un teorema
  • 4. Extensiones

    • 4.1 El marco lógico
    • 4.2 Un tipo de identidad general anterior
    • 4.3 Árboles bien fundados
    • 4.4 Conjuntos iterativos y CZF
    • 4.5 Definiciones inductivas
    • 4.6 Definiciones inductivas-recursivas
  • 5. Explicaciones de significado

    • 5.1 Cálculo a la forma canónica
    • 5.2 El significado de los juicios categóricos
    • 5.3 El significado de los juicios hipotéticos
  • 6. Modelos matemáticos

    • 6.1 Modelos categóricos
    • 6.2 Modelo teórico de conjuntos
    • 6.3 Modelos de realizabilidad
    • 6.4 Modelo de formularios normales y verificación de tipo
  • 7. Variantes de la teoría.

    • 7.1 Teoría del tipo extensivo
    • 7.2 Fundamentos univalentes y teoría del tipo de homotopía
    • 7.3 Teoría del tipo parcial y no estándar
    • 7.4 Teoría del tipo impredecible
    • 7.5 Asistentes de prueba
  • Bibliografía
  • Herramientas académicas
  • Otros recursos de internet
  • Entradas relacionadas

1. Información general

Comenzamos con una vista panorámica de algunos aspectos importantes de la teoría del tipo intuicionista. Los lectores que no estén familiarizados con la teoría pueden preferir omitirla en una primera lectura.

Los orígenes de la teoría del tipo intuicionista son el intuicionismo de Brouwer y la teoría del tipo de Russell. Al igual que la teoría clásica simple de los tipos de Church, se basa en el cálculo lambda con tipos, pero difiere de él en que se basa en el principio de proposiciones como tipos, descubierto por Curry (1958) para la lógica proposicional y extendido a la lógica de predicados por Howard (1980) y de Bruijn (1970). Esta extensión fue posible gracias a la introducción de familias indexadas de tipos (tipos dependientes) para representar los predicados de la lógica de predicados. De esta manera, todos los conectivos lógicos y cuantificadores pueden ser interpretados por formadores de tipos. En la teoría del tipo intuicionista se añaden otros tipos, como un tipo de números naturales, un tipo de tipos pequeños (un universo) y un tipo de árboles bien fundados. La teoría resultante contiene la teoría intuitiva de números (aritmética de Heyting) y mucho más.

La teoría se formula en la deducción natural, donde las reglas para cada tipo de formador se clasifican como reglas de formación, introducción, eliminación e igualdad. Estas reglas exhiben ciertas simetrías entre las reglas de introducción y eliminación después del tratamiento de la deducción natural de Gentzen y Prawitz, como se explica en la entrada sobre semántica de la teoría de la prueba.

Los elementos de las proposiciones, cuando se interpretan como tipos, se denominan objetos de prueba. Cuando se agregan objetos de prueba al cálculo de deducción natural, se convierte en un cálculo lambda mecanografiado con tipos dependientes, lo que extiende el cálculo lambda mecanografiado original de Church. Las reglas de igualdad son reglas de cálculo para los términos de este cálculo. Cada función definible en la teoría es total y computable. La teoría de tipo intuicionista es, por lo tanto, un lenguaje de programación funcional tipado con la propiedad inusual de que todos los programas terminan.

La teoría del tipo intuicionista no es solo un sistema lógico formal sino que también proporciona un marco filosófico integral para el intuicionismo. Es un lenguaje interpretado, donde la distinción entre la demostración de un juicio y la prueba de una proposición juega un papel fundamental (Sundholm 2012). El marco aclara la interpretación de Brouwer-Heyting-Kolmogorov de la lógica intuicionista y la extiende al entorno más general de la teoría del tipo intuicionista. Al hacerlo, proporciona una concepción general no solo de lo que es una prueba constructiva, sino también de lo que es un objeto matemático constructivo. El significado de los juicios de la teoría intuitiva de tipos se explica en términos de cálculos de las formas canónicas de tipos y términos. Estos informales,Las explicaciones intuitivas del significado son "prematemáticas" y deben contrastarse con los modelos matemáticos formales desarrollados dentro de un marco matemático estándar como la teoría de conjuntos.

Esta teoría del significado también justifica una variedad de definiciones inductivas, recursivas e inductivas-recursivas. Aunque las nociones teóricamente fuertes de la prueba pueden justificarse, como los análogos de ciertos cardenales grandes, el sistema se considera predicativo. Las definiciones impredecibles del tipo que se encuentran en la lógica de orden superior, la teoría de conjuntos intuitiva y la teoría de topos no son parte de la teoría. Tampoco es el principio de Markov, y por lo tanto la teoría es distinta del constructivismo ruso.

Un sistema lógico formal alternativo para las matemáticas constructivas predicativas es la teoría de conjuntos constructiva de Zermelo-Fraenkel (CZF) de Myhill y Aczel. Esta teoría, que se basa en la lógica predicativa intuitiva de primer orden y debilita algunos de los axiomas de la teoría clásica de conjuntos de Zermelo-Fraenkel, tiene una interpretación natural en la teoría del tipo intuicionista. Las explicaciones de significado de Martin-Löf también forman indirectamente una base para CZF.

Las variantes de la teoría del tipo intuicionista subyacen a varios asistentes de pruebas ampliamente utilizados, incluidos NuPRL, Coq y Agda. Estos asistentes de pruebas son sistemas informáticos que se han utilizado para formalizar pruebas grandes y complejas de teoremas matemáticos, como el Teorema de los cuatro colores en la teoría de grafos y el Teorema de Feit-Thompson en la teoría de grupos finitos. También se han utilizado para demostrar la exactitud de un compilador de C realista (Leroy 2009) y otro software de computadora.

Filosófica y prácticamente, la teoría del tipo intuicionista es un marco fundamental donde las matemáticas constructivas y la programación de computadoras son, en un sentido profundo, lo mismo. Este punto ha sido enfatizado por (Gonthier 2008) en el documento en el que describe su prueba del Teorema de los cuatro colores:

El enfoque que resultó exitoso para esta prueba fue convertir casi todos los conceptos matemáticos en una estructura de datos o un programa en el sistema Coq, convirtiendo así a toda la empresa en una de verificación de programas.

2. Propuestas como tipos

2.1 Teoría del tipo intuicionista: ¿una nueva forma de ver la lógica?

La teoría del tipo intuicionista ofrece una nueva forma de analizar la lógica, principalmente a través de su introducción de objetos de prueba explícitos. Esto proporciona una interpretación computacional directa de la lógica, ya que existen reglas de cálculo para los objetos de prueba. Con respecto al poder expresivo, la teoría del tipo intuicionista puede considerarse como una extensión de la lógica de primer orden, tanto como la lógica de orden superior, pero predicativa.

2.1.1 Una teoría del tipo

Russell desarrolló la teoría de tipos en respuesta a su descubrimiento de una paradoja en la ingenua teoría de conjuntos. En su teoría de los tipos ramificados, los objetos matemáticos se clasifican según sus tipos: el tipo de proposiciones, el tipo de objetos, el tipo de propiedades de los objetos, etc. Cuando Church desarrolló su teoría simple de los tipos sobre la base de una versión mecanografiada de su cálculo lambda agregó la regla de que hay un tipo de funciones entre dos tipos de teoría. La teoría de tipos intuitiva amplía aún más el cálculo lambda simplemente tipado con tipos dependientes, es decir, familias de tipos indexadas. Un ejemplo es la familia de tipos de (n) - tuplas indexadas por (n).

Los tipos han sido ampliamente utilizados en la programación durante mucho tiempo. Los primeros lenguajes de programación de alto nivel introdujeron tipos de enteros y números de coma flotante. Los lenguajes de programación modernos a menudo tienen sistemas de tipo rico con muchas construcciones para formar nuevos tipos. La teoría de tipos intuitiva es un lenguaje de programación funcional donde el sistema de tipos es tan rico que prácticamente cualquier propiedad concebible de un programa puede expresarse como un tipo. Por lo tanto, los tipos pueden usarse como especificaciones de la tarea de un programa.

2.1.2 Una lógica intuitiva con objetos de prueba

El análisis de la lógica de Brouwer lo condujo a una lógica intuicionista que rechaza la ley del medio excluido y la ley de la doble negación. Estas leyes no son válidas en la teoría del tipo intuicionista. Por lo tanto, no contiene aritmética clásica (Peano) sino solo aritmética intuicionista (Heyting). (Otra cuestión es que la aritmética de Peano se puede interpretar en aritmética de Heyting por la interpretación de doble negación, ver la entrada sobre lógica intuicionista).

Considere un teorema de aritmética intuicionista, como el teorema de división

) para todos m, n. m> 0 / supset / existe q, r. mq + r = n / cuña m> r)

Una prueba formal (en el sentido habitual) de este teorema es una secuencia (o árbol) de fórmulas, donde la última fórmula (raíz) es el teorema y cada fórmula en la secuencia es un axioma (una hoja) o el resultado de aplicando una regla de inferencia a algunas fórmulas anteriores (superiores).

Cuando se prueba el teorema de división en la teoría del tipo intuicionista, no solo construimos una prueba formal en el sentido habitual sino también una construcción (u objeto de prueba) "(divi)" que es testigo de la verdad del teorema. Nosotros escribimos

) divi: / forall m, n {:} N. \, m> 0 / supset / existe q, r {:} N. \, mq + r = n / wedge m> r)

para expresar que (divi) es un objeto de prueba para el teorema de división, es decir, un elemento del tipo que representa el teorema de división. Cuando las proposiciones se representan como tipos, el cuantificador (forall) - se identifica con el espacio de función dependiente anterior (o producto cartesiano general) (Pi), el cuantificador (exist) con los pares dependientes tipo anterior (o suma global disjunta) (Sigma), conjunción (cuña) con producto cartesiano (veces), la relación de identidad = con el tipo anterior (I) de objetos de prueba de identidades, y la relación mayor que (>) con el tipo anterior (GT) de objetos de prueba de declaraciones mayores que. Usando "notación de tipo" escribimos así

) divi: / Pi m, n {:} N. \, / GT (m, 0) rightarrow / Sigma q, r {:} N. \, / I (N, mq + r, n) veces / GT (m, r))

para expresar que el objeto de prueba "(divi)" es una función que asigna dos números (m) y (n) y un objeto de prueba (p) que atestigua que (m> 0) a un cuádruple ((q, (r, (s, t)))), donde (q) es el cociente y (r) es el resto obtenido al dividir (n) por (metro). El tercer componente (s) es un objeto de prueba que es testigo del hecho de que (mq + r = n) y el cuarto componente (t) es un objeto de prueba que es testigo de (m> r).

Crucialmente, (divi) no es solo una función en el sentido clásico; también es una función en el sentido intuicionista, es decir, un programa que calcula la salida ((q, (r, (s, t)))) cuando se le da (m), (n), (p) como entradas. Este programa es un término en un cálculo lambda con constantes especiales, es decir, un programa en un lenguaje de programación funcional.

2.1.3 Una extensión de la lógica de predicados de primer orden

La teoría del tipo intuicionista puede considerarse como una extensión de la lógica de primer orden, al igual que la lógica de orden superior es una extensión de la lógica de primer orden. En la lógica de orden superior, encontramos algunos dominios individuales que pueden interpretarse como cualquier conjunto que nos guste. Si hay constantes relacionales en la firma, estas pueden interpretarse como cualquier relación entre los conjuntos que interpretan los dominios individuales. Además de eso, podemos cuantificar las relaciones y las relaciones de relaciones, etc. Podemos pensar en la lógica de orden superior como lógica de primer orden equipada con una forma de introducir nuevos dominios de cuantificación: if (S_1, / ldots, S_n) son dominios de cuantificación, entonces ((S_1, / ldots, S_n)) es un nuevo dominio de cuantificación que consiste en todas las relaciones n-arias entre los dominios (S_1, / ldots, S_n). La lógica de orden superior tiene una interpretación directa de la teoría de conjuntos donde ((S_1, / ldots, S_n)) se interpreta como el conjunto de potencia (P (A_1 / times / cdots / times A_n)) donde (A_i) es la interpretación de (S_i), para (i = 1, / ldots, n). Este es el tipo de lógica de orden superior o teoría simple de tipos que introdujeron Ramsey, Church y otros.

La teoría del tipo intuicionista se puede ver de una manera similar, solo que aquí las posibilidades de introducir dominios de cuantificación son más ricas, se puede usar (Sigma, / Pi, +, / I) para construir nuevos a partir de los antiguos. (Sección 3.1; Martin-Löf 1998 [1972]). La teoría de tipo intuicionista también tiene una interpretación directa de la teoría de conjuntos, donde (Sigma), (Pi), etc., se interpretan como las construcciones teóricas de conjuntos correspondientes; vea abajo. Podemos agregar a la teoría de tipo intuicionista dominios individuales no especificados como en HOL. Estos se interpretan como conjuntos como para HOL. Ahora exhibimos una diferencia con HOL: en la teoría del tipo intuicionista podemos introducir símbolos familiares no especificados. Podemos introducir (T) como una familia de tipos sobre el dominio individual (S):

[T (x); { rm type}; (x {:} S).)

Si (S) se interpreta como (A), (T) se puede interpretar como cualquier familia de conjuntos indexados por (A). Como un ejemplo no matemático, podemos representar la relación binaria entre los miembros de un dominio individual de personas de la siguiente manera. Introducir la familia binaria Loves sobre el dominio People

[{ rm Loves} (x, y); { rm type}; (x {:} { rm People}, y {:} { rm People}).)

La interpretación puede ser cualquier familia de conjuntos (B_ {x, y}) ((x {:} A), (y {:} A)). ¿Cómo cubre esto la noción estándar de relación? Supongamos que tenemos una relación binaria (R) en (A) en el sentido familiar de la teoría de conjuntos. Podemos hacer una familia binaria correspondiente a esto de la siguiente manera

[B_ {x, y} = / begin {cases} {0 } & / text {if} R (x, y) text {hold} / \ varnothing & / text {if} R (x, y) text {es falso.} end {cases})

Ahora claramente (B_ {x, y}) no está vacío si y solo si (R (x, y)) se mantiene. (Podríamos haber elegido cualquier otro elemento de nuestro universo teórico establecido que no sea 0 para indicar la verdad.) Por lo tanto, a partir de cualquier relación podemos construir una familia cuya verdad de (x, y) sea equivalente a (B_ {x, y}) no estar vacío. Tenga en cuenta que a esta interpretación no le importa cuál es la prueba de (R (x, y)), solo que es válida. Recuerde que la teoría intuitiva de tipos interpreta las proposiciones como tipos, entonces (p {:} { rm Loves} ({ rm John}, { rm Mary})) significa que ({ rm Loves} ({ rm John}, { rm Mary})) es cierto.

La interpretación de las relaciones como familias permite realizar un seguimiento de las pruebas o pruebas que (R (x, y)) posee, pero también podemos optar por ignorarlo.

En la semántica de Montague, la lógica de orden superior se usa para dar semántica del lenguaje natural (y ejemplos como los anteriores). Ranta (1994) introdujo la idea de emplear la teoría del tipo intuicionista para capturar mejor la estructura de la oración con la ayuda de los tipos dependientes.

En contraste, ¿cómo se manejaría la relación matemática (>) entre números naturales en la teoría de tipo intuicionista? En primer lugar, necesitamos un tipo de números (N). En principio, podríamos introducir un dominio individual no especificado (N), y luego agregar axiomas tal como lo hacemos en la lógica de primer orden cuando configuramos el sistema de axiomas para la aritmética de Peano. Sin embargo, esto no nos daría la interpretación computacional deseable. Entonces, como se explica a continuación, establecemos reglas de introducción para construir nuevos números naturales en (N) y reglas de eliminación y cálculo para definir funciones en (N) (por recursión). La relación de orden estándar (>) debe satisfacer

) mbox {(x> y) si existe (z {:} N) tal que (y + z + 1 = x)}.)

La mano derecha se representa como (Sigma z {:} N. \, / I (N, y + z + 1, x)) en la teoría del tipo intuicionista, y tomamos esto como definición de relación (>). ((+) se define mediante ecuaciones recursivas, (I) es la construcción del tipo de identidad). Ahora todas las propiedades de (>) están determinadas por la introducción y las reglas de eliminación y cálculo mencionadas para (N).

2.1.4 Una lógica con varias formas de juicio

El sistema de tipos de la teoría de tipos intuicionista es muy expresivo. Como consecuencia, la buena forma de un tipo ya no es una simple cuestión de análisis, es algo que necesita ser probado. La buena formación de un tipo es una forma de juicio de la teoría del tipo intuicionista. La buena tipificación de un término con respecto a un tipo es otra. Además, hay juicios de igualdad para tipos y términos. Esta es otra forma en la que la teoría del tipo intuicionista difiere de la lógica ordinaria de primer orden con su enfoque en el juicio único que expresa la verdad de una proposición.

2.1.5 Semántica

Mientras que una presentación estándar de la lógica de primer orden seguiría a Tarski en la definición de la noción de modelo, la teoría del tipo intuicionista sigue la tradición de la teoría del significado brouweriana desarrollada por Heyting y Kolmogorov, la llamada interpretación BHK de la lógica. El punto clave es que la prueba de una implicación (A / supset B) es un método que transforma una prueba de (A) en una prueba de (B). En la teoría de tipo intuicionista, este método está representado formalmente por el programa (f {:} A / supset B) o (f {:} A / rightarrow B): el tipo de pruebas de una implicación (A / supset B) es el tipo de funciones que asigna pruebas de (A) a pruebas de (B).

Además, mientras que la semántica de Tarski generalmente se presenta metamatemáticamente y supone la teoría de conjuntos, la teoría del significado de Martin-Löf de la teoría del tipo intuicionista debe entenderse directamente y "prematemáticamente", es decir, sin asumir un metalenguaje como la teoría de conjuntos.

2.1.6 Un lenguaje de programación funcional

Los lectores con experiencia en el cálculo lambda y la programación funcional pueden obtener una primera aproximación alternativa de la teoría del tipo intuicionista al pensar en ella como un lenguaje de programación funcional tipeado al estilo de Haskell o uno de los dialectos de ML. Sin embargo, difiere de estos en dos aspectos cruciales: (i) tiene tipos dependientes (ver más abajo) y (ii) todos los programas que se pueden escribir terminan. (Tenga en cuenta que la teoría del tipo intuicionista ha influido en las extensiones recientes de Haskell con tipos de datos algebraicos generalizados que a veces pueden desempeñar un papel similar al de los tipos dependientes definidos inductivamente).

2.2 La correspondencia de Curry-Howard

Como ya se mencionó, el principio de que

una proposición es el tipo de sus pruebas.

es fundamental para la teoría del tipo intuicionista. Este principio también se conoce como la correspondencia de Curry-Howard o incluso el isomorfismo de Curry-Howard. Curry descubrió una correspondencia entre el fragmento de implicación de la lógica intuicionista y el cálculo lambda simplemente tipado. Howard extendió esta correspondencia a la lógica de predicados de primer orden. En la teoría intuitiva de tipos, esta correspondencia se convierte en una identificación de proposiciones y tipos, que se ha extendido para incluir la cuantificación sobre tipos superiores y más.

2.3 Conjuntos de objetos de prueba

Entonces, ¿cómo son estos objetos de prueba? No deben considerarse como derivaciones lógicas, sino más bien como una evidencia simbólica (estructurada) de que algo es cierto. Otro término para tal evidencia es "hacedor de verdad".

Es instructivo, como una primera aproximación algo cruda, reemplazar los tipos por conjuntos ordinarios en esta correspondencia. Defina un conjunto (E_ {m, n}), dependiendo de (m, n / in {{ mathbb N}}), por:

) E_ {m, n} = / left { begin {array} {ll} {0 } & / mbox {if (m = n)} / \ varnothing & / mbox {if (m / ne n).} end {array} right.)

Entonces (E_ {m, n}) no está vacío exactamente cuando (m = n). El conjunto (E_ {m, n}) corresponde a la proposición (m = n), y el número (0) es un objeto de prueba (creador de verdad) que habita los conjuntos (E_ {m, m}).

Considere la proposición de que (m) es un número par expresado como la fórmula (exist n / in {{ mathbb N}}. M = 2n). Podemos construir un conjunto de objetos de prueba correspondientes a esta fórmula utilizando la operación general de suma teórica de conjuntos. Suponga que (A_n) ((n / in {{ mathbb N}})) es una familia de conjuntos. Entonces su suma disjunta viene dada por el conjunto de pares

[(Sigma n / in {{ mathbb N}}) A_n = {(n, a): n / in {{ mathbb N}}, a / in A_n }.)

Si aplicamos esta construcción a la familia (A_n = / E_ {m, 2n}), vemos que ((Sigma n / in {{ mathbb N}}) E_ {m, 2n}) es no vacío exactamente cuando hay un (n / en {{ mathbb N}}) con (m = 2n). Usando la operación general del producto teórico de conjuntos ((Pi n / in {{ mathbb N}}) A_n) podemos obtener de manera similar un conjunto correspondiente a una proposición universalmente cuantificada.

2.4 Tipos dependientes

En la teoría del tipo intuicionista hay formadores de tipos primitivos (Sigma) y (Pi) para sumas y productos generales, y (I) para tipos de identidad, análogos a las construcciones teóricas de conjuntos descritas anteriormente. El tipo de identidad (I (N, m, n)) correspondiente al conjunto (E_ {m, n}) es un ejemplo de un tipo dependiente ya que depende de (m) y (norte). También se llama una familia de tipos indexados, ya que es una familia de tipos indexados por (m) y (n). Del mismo modo, podemos formar la suma disjunta general (Sigma x {:} A. \, B) y el producto cartesiano general (Pi x {:} A. \, B) de dicha familia de tipos (B) indexado por (x {:} A), correspondiente a la suma teórica establecida y las operaciones del producto anteriores.

Los tipos dependientes también se pueden definir por recursividad primitiva. Un ejemplo es el tipo de (n) - tuplas (A ^ n) de elementos de tipo (A) e indexados por (n {:} N) definidos por las ecuaciones

) begin {align *} A ^ 0 & = 1 \\ A ^ {n + 1} & = A / times A ^ n / end {align *})

donde (1) es un tipo de un elemento y (times) denota el producto cartesiano de dos tipos. Observamos que los tipos dependientes introducen el cálculo en tipos: las reglas de definición anteriores son reglas de cálculo. Por ejemplo, el resultado de calcular (A ^ 3) es (A / times (A / times (A / times 1))).

2.5 Propuestas como tipos en teoría de tipo intuicionista

Con proposiciones como tipos, los predicados se convierten en tipos dependientes. Por ejemplo, el predicado (mathrm {Prime} (x)) se convierte en el tipo de pruebas de que (x) es primo. Este tipo depende de (x). Del mismo modo, (x <y) es el tipo de pruebas de que (x) es menor que (y).

Según la interpretación de Curry-Howard de las proposiciones como tipos, las constantes lógicas se interpretan como formadores de tipos:

) begin {align *} bot & = / varnothing \\ / top & = 1 \\ A / vee B & = A + B \\ A / wedge B & = A / times B \\ A / supset B & = A / rightarrow B \\ / existe x {:} A. \, B & = / Sigma x {:} A. \, B \\ / forall x {:} A. \, B & = / Pi x {:} A. \, B / end {align *})

donde (Sigma x {:} A. \, B) es la suma disjunta de la familia indexada (A) de los tipos (B) y (Pi x {:} A. \, B) es su producto cartesiano. Los elementos canónicos de (Sigma x {:} A. \, B) son pares ((a, b)) tales que (a {:} A) y (b {:} B [x: = a]) (el tipo obtenido al sustituir todas las apariciones libres de (x) en (B) por (a)). Los elementos de (Pi x {:} A. \, B) son funciones (computables) (f) tales que (f \, a {:} B [x: = a]), siempre que (a {:} A).

Por ejemplo, considere la proposición

) begin {ecation} forall m {:} N. \, / exist n {:} N. \, m / lt n / wedge / mathrm {Prime} (n) tag {1} label {prop1} end {ecuación})

expresando que hay primos arbitrariamente grandes. Según la interpretación de Curry-Howard, esto se convierte en el tipo (Pi m {:} N. \, / Sigma n {:} N. \, m / lt n / times / mathrm {Prime} (n)) de funciones que asignan un número (m) a un triple ((n, (p, q))), donde (n) es un número, (p) es una prueba de que (m / lt n) y (q) es una prueba de que (n) es primo. Este es el principio de las pruebas como programas: una prueba constructiva de que hay primos arbitrariamente grandes se convierte en un programa que, dado cualquier número, produce un primo mayor junto con pruebas de que realmente es mayor y de hecho es primo.

Tenga en cuenta que la prueba que deriva una contradicción de la suposición de que hay un primo más grande no es constructiva, ya que no proporciona explícitamente una forma de calcular un primo aún mayor. Para convertir esta prueba en constructiva, tenemos que mostrar explícitamente cómo construir el primo más grande. (Dado que la proposición (ref {prop1}) anterior es una fórmula (Pi ^ 0_2), por ejemplo, podemos usar la traducción A de Friedman para convertir dicha prueba en aritmética clásica en una prueba en aritmética intuicionista y, por lo tanto, en una prueba en la teoría del tipo intuicionista.)

3. Teoría básica del tipo intuicionista

Ahora presentamos una versión central de la teoría del tipo intuicionista, estrechamente relacionada con la primera versión de la teoría presentada por Martin-Löf en 1972 (Martin-Löf 1998 [1972]). Además de los formadores de tipos necesarios para la interpretación de Curry-Howard de la lógica de predicados intuicionista tipada enumerados anteriormente, tenemos dos tipos: el tipo (N) de números naturales y el tipo (U) de tipos pequeños.

Se puede demostrar que la teoría resultante contiene la teoría intuitiva de números (HA) (aritmética de Heyting), el Sistema de Gödel (T) de funciones recursivas primitivas de tipo superior y la teoría (HA ^ / omega) de aritmética de Heyting de tipo superior.

Esta teoría básica del tipo intuicionista no es solo la original, sino quizás la versión mínima que exhibe las características esenciales de la teoría. Las extensiones posteriores con tipos de identidad primitivos, tipos de árboles bien fundados, jerarquías universales y nociones generales de definiciones inductivas e inductivas-recursivas han aumentado la fuerza teórica de la teoría y también la han hecho más conveniente para la programación y formalización de las matemáticas. Por ejemplo, con la adición de árboles bien fundados podemos interpretar la teoría constructiva de conjuntos Zermelo-Fraenkel (CZF) de Aczel (1978 [1977]). Sin embargo, esperaremos hasta la próxima sección para describir esas extensiones.

3.1 Juicios

En Martin-Löf (1996) se presenta una filosofía general de la lógica donde la noción tradicional de juicio se expande y se le da una posición central. Un juicio ya no es solo una afirmación o negación de una proposición, sino un acto general de conocimiento. Cuando razonamos matemáticamente, hacemos juicios sobre objetos matemáticos. Una forma de juicio es afirmar que alguna afirmación matemática es verdadera. Otra forma de juicio es afirmar que algo es un objeto matemático, por ejemplo, un conjunto. Las reglas lógicas dan métodos para producir juicios correctos a partir de juicios anteriores. Los juicios obtenidos por tales reglas pueden presentarse en forma de árbol.

) infer [r_4] {J_8} { infer [r_1] {J_3} {J_1 & J_2} & / infer [r_3] {J_7} { infer [r_5] {J_5} {J_4} & J_6}}]

o en forma secuencial

  • (1) (J_1 / quad / text {axiom})
  • (2) (J_2 / quad / text {axiom})
  • (3) (J_3 / quad / text {por regla (r_1) de (1) y (2)})
  • (4) (J_4 / quad / text {axiom})
  • (5) (J_5 / quad / text {por regla (r_2) de (4)})
  • (6) (J_6 / quad / text {axiom})
  • (7) (J_7 / quad / text {por regla (r_3) de (5) y (6)})
  • (8) (J_8 / quad / text {por regla (r_4) de (3) y (7)})

La última forma es común en argumentos matemáticos. Tal secuencia o árbol formado por reglas lógicas a partir de axiomas es una derivación o demostración de un juicio.

El razonamiento de primer orden puede presentarse usando un solo tipo de juicio:

la proposición (B) es verdadera bajo la hipótesis de que las proposiciones (A_1, / ldots, A_n) son todas verdaderas.

Escribimos este juicio hipotético como el llamado secuenciante Gentzen

[A_1, / ldots, A_n { vdash} B.)

Tenga en cuenta que este es un juicio único que no debe confundirse con la derivación del juicio ({ vdash} B) de los juicios ({ vdash} A_1, / ldots, { vdash} A_n). Cuando (n = 0), entonces el juicio categórico ({ vdash} B) establece que (B) es verdadero sin ningún supuesto. Con la notación posterior, la regla familiar para la introducción conjuntiva se convierte en

) infer [(land I)] {A_1, / ldots, A_n { vdash} B / land C} {A_1, / ldots, A_n { vdash} B & A_1, / ldots, A_n { vdash} C}.)

3.2 Formularios de juicio

La teoría de tipo Martin-Löf tiene cuatro formas básicas de juicio y es un sistema considerablemente más complicado que la lógica de primer orden. Una razón es que se lleva más información en las derivaciones debido a la identificación de proposiciones y tipos. Otra razón es que la sintaxis está más involucrada. Por ejemplo, las fórmulas (tipos) bien formadas deben generarse simultáneamente con las fórmulas probadamente verdaderas (tipos habitados).

Las cuatro formas de juicio categórico son

  • (vdash A \; { rm type}), lo que significa que (A) es un tipo bien formado,
  • (vdash a {:} A), lo que significa que (a) tiene el tipo (A),
  • (vdash A = A '), lo que significa que (A) y (A') son tipos iguales,
  • (vdash a = a '{:} A), lo que significa que (a) y (a') son elementos iguales de tipo (A).

En general, un juicio es hipotético, es decir, se realiza en un contexto (Gamma), es decir, una lista (x_1 {:} A_1, / ldots, x_n {:} A_n) de variables que puede ocurrir libre en el juicio junto con sus respectivos tipos. Tenga en cuenta que los tipos en un contexto pueden depender de variables de tipos anteriores. Por ejemplo, (A_n) puede depender de (x_1 {:} A_1, / ldots, x_ {n-1} {:} A_ {n-1}). Las cuatro formas de juicios hipotéticos son

  • (Gamma / vdash A \; { rm type}), lo que significa que (A) es un tipo bien formado en el contexto (Gamma),
  • (Gamma / vdash a {:} A), lo que significa que (a) tiene el tipo (A) en contexto (Gamma),
  • (Gamma / vdash A = A '), lo que significa que (A) y (A') son tipos iguales en el contexto (Gamma),
  • (Gamma / vdash a = a '{:} A), lo que significa que (a) y (a') son elementos iguales de tipo (A) en el contexto (Gamma).

Bajo la proposición como interpretación de tipos

) tag {2} label {analytic} vdash a {:} A)

puede entenderse como el juicio de que (a) es un objeto de prueba para la proposición (A). Al suprimir este objeto, obtenemos un juicio correspondiente al de la lógica ordinaria de primer orden (ver arriba):

) tag {3} label {sintético} vdash A \; { rm verdadero}.)

Observación 3.1. Martin-Löf (1994) argumenta que el juicio analítico de Kant a priori y el juicio sintético a priori pueden ejemplificarse, en el ámbito de la lógica, por ([analítico]) y ([sintético]) respectivamente. En el juicio analítico ([analítico]) todo lo que se necesita para hacer evidente el juicio es explícito. Para su versión sintética ([sintético]) es necesario proporcionar una construcción de prueba posiblemente complicada (a) para que sea evidente. Esta comprensión de la analiticidad y la sintética tiene la sorprendente consecuencia de que "las leyes lógicas en su formulación habitual son todas sintéticas". Martin-Löf (1994: 95). Su análisis además da:

"[…] la lógica de los juicios analíticos, es decir, la lógica para derivar juicios de las dos formas analíticas, es completa y decidible, mientras que la lógica de los juicios sintéticos es incompleta e indecidible, como lo demostró Gödel". Martin-Löf (1994: 97).

La capacidad de decisión de los dos juicios analíticos ((vdash a {:} A) y (vdash a = b {:} A)) depende de las propiedades metamatemáticas de la teoría de tipos: fuerte normalización y verificación de tipos decidible.

A veces también las siguientes formas se consideran explícitamente como juicios de la teoría:

  • (Gamma \; { rm context}), lo que significa que (Gamma) es un contexto bien formado.
  • (Gamma = / Gamma '), lo que significa que (Gamma) y (Gamma') son contextos iguales.

A continuación, abreviaremos el juicio (Gamma / vdash A \; { rm type}) como (Gamma / vdash A) y (Gamma \; { rm context}) como (Gamma / vdash.)

3.3 Reglas de inferencia

Al establecer las reglas usaremos la letra (Gamma) como una meta-variable que se extiende sobre contextos, (A, B, / ldots) como meta-variables que se extienden sobre tipos, y (a, b, c, d, e, f, / ldots) como metavariables que varían en términos.

El primer grupo de reglas de inferencia son reglas generales que incluyen reglas de suposición, sustitución y formación de contexto. También hay reglas que expresan que las igualdades son relaciones de equivalencia. Existen numerosas reglas de este tipo, y solo mostramos la regla particularmente importante de la igualdad de tipos que es crucial para el cálculo en tipos:

) frac { Gamma / vdash a {:} A / hspace {2em} Gamma / vdash A = B} { Gamma / vdash a {:} B})

Las reglas restantes son específicas de los formadores de tipo. Estos se clasifican como reglas de formación, introducción, eliminación e igualdad.

3.4 Lógica de predicados intuitiva

Solo damos las reglas para (Pi). Existen reglas análogas para los otros formadores de tipos correspondientes a las constantes lógicas de la lógica de predicados tipados.

A continuación, (B [x: = a]) significa el término obtenido al sustituir el término (a) por cada aparición libre de la variable (x) en (B) (evitando la captura de variables).

(Pi) - formación.) frac { Gamma / vdash A / hspace {2em} Gamma, x {:} A / vdash B} { Gamma / vdash / Pi x {:} A. B}) (Pi) -Introducción.) frac { Gamma, x {:} A / vdash b {:} B} { Gamma / vdash / lambda x. b {:} Pi x {:} A. B}) (Pi) - eliminación.) frac { Gamma / vdash f {:} Pi x {:} AB / hspace {2em} Gamma / vdash a {:} A} { Gamma / vdash f \, a {:} B [x: = a]}) (Pi) - igualdad.) frac { Gamma, x {:} A / vdash b {:} B / hspace {2em} Gamma / vdash a {:} A} { Gamma / vdash (lambda xb), a = b [x: = a] {:} B [x: = a]}) Esta es la regla de (beta) - conversión. También podemos agregar la regla de (eta) - conversión:) frac { Gamma / vdash f {:} Pi x {:} A. B} { Gamma / vdash / lambda x. f \, x = f {:} Pi x {:} A. B}.)

Además, hay reglas de congruencia que expresan que las operaciones introducidas por las reglas de formación, introducción y eliminación preservan la igualdad. Por ejemplo, la regla de congruencia para (Pi) es

) frac { Gamma / vdash A = A '\ hspace {2em} Gamma, x {:} A / vdash B = B'} { Gamma / vdash / Pi x {:} A. B = / Pi x {:} A '. SI'}.)

3.5 Números naturales

Como en la aritmética de Peano, los números naturales son generados por 0 y la operación sucesora (s). La regla de eliminación establece que estas son las únicas formas posibles de generar un número natural.

Escribimos (f (c) = / R (c, d, xy.e)) para la función que se define por recursividad primitiva en el número natural (c) con el caso base (d) y el paso función (xy.e) (o alternativamente (lambda xy.e)) que asigna el valor (y) para el número anterior (x {:} N) al valor para (s (x)). Tenga en cuenta que (R) es un nuevo operador de enlace de variables: las variables (x) y (y) se enlazan en (e).

(N) - formación.) Gamma / vdash / N) (N) - introducción.) Gamma / vdash 0 {:} N / hspace {2em} frac { Gamma / vdash a {:} N} { Gamma / vdash s (a) {:} N}) (N) - eliminación.) frac { Gamma, x {:} N / vdash C / hspace {1em} Gamma / vdash c {:} N / hspace {1em} Gamma / vdash d {:} C [x: = 0] hspace {1em} Gamma, y {:} N, z {:} C [x: = y] vdash e {:} C [x: = s (y)]} { Gamma / vdash / R (c, d, yz.e) {:} C [x: = c]}) (N) - igualdad (bajo premisas apropiadas).) begin {align *} R (0, d, yz.e) & = d {:} C [x: = 0] / \ R (s (a), d, yz.e) & = e [y: = a, z: = / R (a, d, yz.e)] {:} C [x: = s (a)] end {align *})

La regla de (N): la eliminación expresa simultáneamente el tipo de función definida por la recursividad primitiva y, según la interpretación de Curry-Howard, la regla de la inducción matemática: probamos la propiedad (C) de un número natural (x) por inducción en (x).

El Sistema de Gödel (T) es esencialmente una teoría de tipo intuicionista con solo los formadores de tipo (N) y (A / rightarrow B) (el tipo de funciones de (A) a (B), que es el caso especial de ((Pi x {:} A) B) donde (B) no depende de (x {:} A)). Como no hay tipos dependientes en System (T), las reglas pueden simplificarse.

3.6 El universo de los tipos pequeños

La primera versión de Martin-Löf de la teoría de tipos (Martin-Löf 1971a) tenía un axioma que decía que hay un tipo de todos los tipos. Girard demostró que esto era inconsistente y descubrió que la paradoja de Burali-Forti podía codificarse en esta teoría.

Para superar esta impredicatividad patológica, pero aún conservando algo de su expresividad, Martin-Löf introdujo en 1972 un universo (U) de tipos pequeños cerrado bajo todos los tipos de formadores de la teoría, excepto que no se contiene a sí mismo (Martin- Löf 1998 [1972]). Las reglas son:

(U) - formación.) Gamma / vdash / U) (U) - introducción.) Gamma / vdash / varnothing {:} U / hspace {3em} Gamma / vdash 1 {:} U)) frac { Gamma / vdash A {:} U / hspace {2em} Gamma / vdash B {:} U} { Gamma / vdash A + B {:} U} hspace {3em} frac { Gamma / vdash A {:} U / hspace {2em} Gamma / vdash B {:} U} { Gamma / vdash A / times B {:} U})) frac { Gamma / vdash A {:} U / hspace {2em} Gamma / vdash B {:} U} { Gamma / vdash A / rightarrow B {:} U})) frac { Gamma / vdash A {:} U / hspace {2em} Gamma, x {:} A / vdash B {:} U} { Gamma / vdash / Sigma x {:} A. \, B {:} U} hspace {3em} frac { Gamma / vdash A {:} U / hspace {2em} Gamma, x {:} A / vdash B {:} U} { Gamma / vdash / Pi x {:} A. \, B {:} U})) Gamma / vdash / N {:} U) (U) - eliminación.) frac { Gamma / vdash A {:} U} { Gamma / vdash A})

Como (U) es un tipo, podemos usar (N) - eliminación para definir tipos pequeños por recursividad primitiva. Por ejemplo, si (A: / U), podemos definir el tipo de (n) - tuplas de elementos en (A) de la siguiente manera:

[A ^ n = / R (n, 1, xy. A / times y) {:} U)

Este universo teórico de tipos (U) es análogo a un universo de Grothendieck en la teoría de conjuntos, que es un conjunto de conjuntos cerrados en todas las formas en que los conjuntos se pueden construir en la teoría de conjuntos de Zermelo-Fraenkel. La existencia de un universo Grothendieck no puede probarse a partir de los axiomas habituales de la teoría de conjuntos de Zermelo-Fraenkel, pero necesita un nuevo axioma.

En Martin-Löf (1975) el universo se extiende a una jerarquía contable de universos

) U_0: / U_1: / U_2: / cdots.)

De esta manera, cada tipo tiene un tipo, no solo cada tipo pequeño.

3.7 Identidad proposicional

Arriba, presentamos el juicio de igualdad

) tag {4} label {defeq} Gamma / vdash a = a '{:} A.)

Esto generalmente se llama "igualdad de definición" porque se puede decidir normalizando los términos (a) y (a ') y verificando si las formas normales son idénticas. Sin embargo, esta igualdad es un juicio y no una proposición (tipo) y por lo tanto no podemos probar tales igualdades de juicio por inducción. Por esta razón, necesitamos introducir tipos de identidad proposicionales. Por ejemplo, el tipo de identidad para números naturales (I (N, m, n)) se puede definir mediante (U) - recursividad primitiva valorada. Entonces podemos expresar y probar los axiomas de Peano. Además, la igualdad extensional de las funciones se puede definir por

) I (N / rightarrow / N, f, f ') = / Pi x {:} N. / I (N, f \, x, f '\, x).)

3.8 El axioma de elección es un teorema

La siguiente forma del axioma de elección es una consecuencia inmediata de la interpretación BHK de los cuantificadores intuicionistas, y se prueba fácilmente en la teoría del tipo intuicionista:

[(Pi x {:} A. / Sigma y {:} B. C) rightarrow / Sigma f {:} (Pi x {:} A. B). C [y: = f \, x])

La razón es que (Pi x {:} A. / Sigma y {:} B. C) es el tipo de funciones que asignan elementos (x {:} A) a pares ((y, z)) con (y {:} B) y (z {:} C). La función de elección (f) se obtiene al devolver el primer componente (y {:} B) de este par.

Quizás sea sorprendente que la teoría del tipo intuicionista valide directamente un axioma de elección, ya que este axioma a menudo se considera problemático desde un punto de vista constructivo. Una posible explicación para este estado de cosas es que lo anterior es un axioma de elección para los tipos, y que los tipos no son, en general, aproximaciones constructivas apropiadas de conjuntos en el sentido clásico. Por ejemplo, podemos representar un número real como una secuencia de Cauchy en la teoría del tipo intuicionista, pero el conjunto de números reales no es el tipo de secuencias de Cauchy, sino el tipo de secuencias de Cauchy hasta la convergencia de la equiconvergencia. En términos más generales, un conjunto de matemáticas constructivas de Bishop está representado por un tipo (comúnmente llamado "preestablecido") junto con una relación de equivalencia.

Si (A) y (B) están equipados con relaciones de equivalencia, por supuesto, no hay garantía de que la función de elección, (f) anterior, sea extensional en el sentido de que asigna elementos equivalentes a elementos equivalentes. Este es el fracaso del axioma extensional de elección, ver Martin-Löf (2009) para un análisis.

4. Extensiones

4.1 El marco lógico

Lo anterior completa la descripción de una versión central de la teoría del tipo intuicionista cercana a la de (Martin-Löf 1998 [1972]).

En 1986 Martin-Löf propuso una reformulación de la teoría del tipo intuicionista; ver Nordström, Peterson y Smith (1990) para una exposición. El propósito era dar una formulación más compacta, donde (lambda) y (Pi) son las únicas operaciones de enlace variable. Hoy en día se considera la versión principal de la teoría. También es la base del asistente de prueba Agda. La teoría de 1986 tiene dos partes:

  • la teoría de los tipos (el marco lógico);
  • La teoría de conjuntos (tipos pequeños).

Observación 4.1. Tenga en cuenta que la palabra "conjunto" en el marco lógico no coincide con la forma en que se utiliza en las matemáticas constructivas de Bishop. Para evitar esta confusión, los tipos junto con las relaciones de equivalencia generalmente se denominan "setoides" o "conjuntos extensionales" en la teoría del tipo intuicionista.

El marco lógico tiene solo dos tipos de formadores: (Pi x {:} A. B) (generalmente escrito ((x {:} A) B) o ((x {:} A) rightarrow B) en la formulación del marco lógico) y (U) (generalmente llamado (Set)). Las reglas para (Pi x {:} A. B) (((x {:} A) rightarrow B)) son las mismas que las indicadas anteriormente (incluyendo (eta) - conversión). Las reglas para (U) ((Set)) también son las mismas, excepto que el marco lógico solo estipula el cierre bajo la formación de tipo (Pi).

Los otros formadores de tipo pequeño ("formadores de conjuntos") se introducen en la teoría de conjuntos. En la formulación del marco lógico, cada regla de formación, introducción y eliminación puede expresarse como la tipificación de una nueva constante. Por ejemplo, las reglas para los números naturales se convierten

) begin {align *} N &: / Set, \\ 0 &: / N, \\ / s &: / N / rightarrow / N, \\ / R &: (C {:} N / rightarrow / Set) rightarrow C \, 0 / rightarrow ((x {:} N) rightarrow C \, x / rightarrow C \, (s \, x)) rightarrow (c {:} N) rightarrow C \, c. / end {align *})

donde hemos omitido el contexto común (Gamma), ya que los tipos de estas constantes están cerrados. Tenga en cuenta que el operador de recursión (R) tiene un primer argumento (C {:} N / rightarrow / Set) a diferencia de la formulación original.

Además, las reglas de igualdad pueden expresarse como ecuaciones

) begin {align *} R \, C \, d \, e \, 0 & = d {:} C \, 0 \\ / R \, C \, d \, e \, (s \, a) & = e \, a \, (R \, C \, d \, e \, a) {:} C \, (s \, a) end {align *})

bajo supuestos adecuados.

En la secuela presentaremos varias extensiones de la teoría de tipos. Sin embargo, para mantener la presentación uniforme, no utilizaremos la presentación del marco lógico de la teoría de tipos, sino que utilizaremos la misma notación que en la sección 2.

4.2 Un tipo de identidad general anterior

Como mencionamos anteriormente, la identidad en los números naturales se puede definir por recursividad primitiva. Las relaciones de identidad en otros tipos también se pueden definir en la versión básica de la teoría del tipo intuicionista presentada en la sección 2.

Sin embargo, Martin-Löf (1975) extendió la teoría del tipo intuicionista con un tipo de identidad primitiva uniforme anterior (I) para todos los tipos. Las reglas para (I) expresan que la relación de identidad es generada inductivamente por la prueba de reflexividad, una constante canónica llamada (r). (Tenga en cuenta que (r) fue codificado por el número 0 en la presentación introductoria de objetos de prueba en 2.3. La regla de eliminación para el tipo de identidad es una generalización de la eliminación de identidad en la lógica de predicados e introduce una constante de eliminación (J). Aquí mostramos la formulación debida a Paulin-Mohring (1993) en lugar de la formulación original de Martin-Löf (1975). Las reglas de inferencia son las siguientes.

(I) - formación.) frac { Gamma / vdash A / hspace {1em} Gamma / vdash a {:} A / hspace {1em} Gamma / vdash a '{:} A} { Gamma / vdash / I (A, Automóvil club británico')})

(I. Introducción.) frac { Gamma / vdash A / hspace {1em} Gamma / vdash a {:} A} { Gamma / vdash / r {:} I (A, a, a)})

(I) - eliminación.

) frac { Gamma, x {:} A, y {:} I (A, a, x) vdash C / hspace {1em} Gamma / vdash b {:} A / hspace {1em} Gamma / vdash c {:} I (A, a, b) hspace {1em} Gamma / vdash d {:} C [x: = a, y: = r]} { Gamma / vdash / J (c, d) {:} C [x: = b, y: = c]})

(I) - igualdad (bajo los supuestos apropiados).

) begin {align *} J (r, d) & = d / end {align *})

Tenga en cuenta que si (C) solo depende de (x: A) y no de la prueba (y: / I (A, a, x)) (y también suprimimos los objetos de prueba) en la regla de (I) - eliminación recuperamos la regla de eliminación de identidad en la lógica de predicados.

Al construir un modelo de teoría de tipos donde los tipos se interpretan como grupoides (categorías donde todas las flechas son isomorfismos) Hofmann y Streicher (1998) demostraron que no se puede probar en la teoría de tipos intuitiva que todas las pruebas de (I (A, a, b)) Son identicos. Esto puede parecer una incompletitud de la teoría y Streicher sugirió un nuevo axioma (K) del cual se deduce que todas las pruebas de (I (A, a, b)) son idénticas a (r)

El tipo (I) - a menudo se denomina tipo de identidad intensional, ya que no satisface el principio de extensionalidad de la función. La teoría del tipo intuicionista con el tipo de identidad intensional también se denomina a menudo teoría del tipo intuicionista intensional para distinguirla de la teoría del tipo intuicionista extensional que se presentará en la sección 7.1.

4.3 Árboles bien fundados

Un tipo de árboles bien fundados de la forma (W x {:} A. B) se introdujo en Martin-Löf 1982 (y en una forma más restringida por Scott 1970). Los elementos de (W x {:} A. B) son árboles de ramificación variable y arbitraria: variable, porque el tipo de ramificación (B) está indexado por (x {:} A) y arbitrario porque (B) puede ser arbitrario. El tipo viene dado por una definición inductiva generalizada ya que los árboles bien fundados pueden ramificarse infinitamente. Podemos pensar en (W x {:} A. B) como el término libre de álgebra, donde cada (a {:} A) representa un término constructor (sup \, a) con (posiblemente infinito) arity (B [x: = a]).

(W) - formación.) frac { Gamma / vdash A / hspace {2em} Gamma, x {:} A / vdash B} { Gamma / vdash / W x {:} A. B}) (W) -Introducción.) frac { Gamma / vdash a {:} A / hspace {2em} Gamma, y {:} B [x: = a] vdash b: Wx {:} A. B} { Gamma / vdash / sup (a, yb): / W x {:} A. B})

Omitimos las reglas de (W) - eliminación y (W) - igualdad.

Agregar árboles bien fundados a la teoría del tipo intuicionista aumenta significativamente su fuerza teórica de prueba (Setzer (1998)).

4.4 Conjuntos iterativos y CZF

Una aplicación importante de los árboles bien fundados es la construcción de Aczel (1978) de un modelo de teoría de tipos de la teoría de conjuntos constructivos de Zermelo Fraenkel. Para este fin, define el tipo de conjuntos iterativos como

) V = / W x {:} U. X.)

Sea (A {:} U) un tipo pequeño y (x {:} A / vdash M) sea una familia indexada de conjuntos iterativos. Entonces (sup (A, xM)), o con una notación más sugerente ({M / mid x {:} A }), es un conjunto iterativo. Parafraseando: un conjunto iterativo es una familia de conjuntos iterativos indexados por un tipo pequeño.

Tenga en cuenta que un conjunto iterativo es un alt="sep man icon" /> Cómo citar esta entrada.

icono de hombre sep
icono de hombre sep

Obtenga una vista previa de la versión PDF de esta entrada en Friends of the SEP Society.

icono inpho
icono inpho

Busque este tema de entrada en el Proyecto de ontología de filosofía de Internet (InPhO).

icono de papeles de phil
icono de papeles de phil

Bibliografía mejorada para esta entrada en PhilPapers, con enlaces a su base de datos.

Otros recursos de internet

  • Enciclopedia de Filosofía de Internet: Matemáticas constructivas
  • Scholarpedia: teoría del tipo computacional
  • nLab: Teoría de tipos

Recomendado: