¿Cuáles son los diferentes enfoques para formalizar la teoría de tipos en el contexto habitual del modelo teórico?

Question

Por lo general, cuando la formalización de un sistema de tipo de teoría, por lo que he visto, los autores normalmente, o simplemente tomar las ideas básicas de trabajo con derivaciones, reglas, juicios y como nociones básicas, explicando de manera informal, y definir el tipo de teoría que proporciona una lista de las normas correspondientes, o formalizar en la teoría de conjuntos (e.x". un tipo de teoría consiste en un conjunto R de reglas tales que...").

Sin embargo, a menudo la gente habla de los modelos de tipo de teorías, por ejemplo, de ncatlab:

Los modelos de ML tipo de teoría, depende crucialmente de si se considera la variante de extensional tipo de teoría o de intensional tipo de teoría.

Los modelos de la extensional versión son (sólo) a nivel local cartesiano categorías cerradas.

¿Qué se entiende por esto? Presumiblemente, hay alguna manera de que en realidad la formalización de la teoría tipo como un honesto a la bondad del modelo teórico de la teoría (ya sea de primer orden, o tal vez de segundo orden me imagino), por lo que el modelo de un sistema de tipo de teoría en cuestión significa que la cosa habitual en el modelo de la teoría.

Mi pregunta es: ¿hay alguna enfoques comunes en la literatura para definir el tipo de teoría como un honesto a la bondad de la teoría, y, por tanto, el uso del término "modelo" de la misma como el modelo-teóricos de la noción, o "modelo de un tipo de teoría" significa algo diferente? Existe aún una definición formal de lo que es "modelo de un tipo de teoría" o "teoría del tipo de teorías" significa, en general, en la literatura, o son estas definiciones, simplemente, entendida de manera ad-hoc manera, y sólo se especifica completamente cuando se habla de tipo específico teorías (es decir, "modelos de MLTT", "modelos de HOTT")? Si este es el caso, la restricción para determinado tipo de teorías, tener nociones como "la teoría de la MLTT" o "la teoría de la HOTT", por ejemplo, ha formalizado en el modelo usual de la teoría de contexto?

Answer 1

Esta pregunta en realidad es un poco difícil porque lo que la mejor respuesta es todavía un tema de investigación y debate.

Primero de todo, dependiente del tipo de teoría no es, definitivamente, una de primer orden de la teoría, por lo que necesita un tipo diferente de "modelo" a la noción habitual de primer orden de la lógica del modelo de la teoría. Ahora el problema no es que no hay una buena noción de modelo para el tipo de teoría, sino que hay varios, y tienen diferentes ventajas y desventajas, y no está claro cual es la mejor manera o si incluso hemos descubierto la mejor manera sin embargo.

Todas estas nociones se basan en la idea básica de que debería haber una categoría donde los contextos en tipo de teoría se interpretan como objetos en la categoría, y cada objeto viene equipado con una noción de tipo y plazo que se utilizan para interpretar los tipos y términos en dependiente del tipo de teoría. El más antiguo tipo de modelo es saber como contextuales categoría, de Cartmell, Generalizada algebraicas teorías contextuales y categorías. Estos tienen la ventaja de estar muy cerca de la sintaxis de tipo de teoría, pero tiene un poco de la definición técnica y por lo tanto puede ser difícil trabajar con ellos. En el otro extremo están localmente cartesiano categorías. Estos tienen un relativamente fácil de definición utilizando bien estudiado ideas a partir de la categoría de la teoría, pero con dos desventajas principales. En primer lugar, sólo para interpretar el tipo de teoría en un local cartesiana cerrada categoría es altamente no trivial (ver Hofmann, En la Interpretación de la Teoría Tipo Localmente Cartesiano Categorías Cerradas). En segundo lugar, en general localmente cartesiana cerrada categoría no hay realmente sólo una forma de interpretar la identidad de tipos, y el uso de esta interpretación siempre se llega a un modelo de tipo extensional de la teoría. Este segundo punto hace localmente cartesiano categorías cerradas que no es tan útil para HoTT, donde es importante que la identidad de tipos no extensional. Entre las categorías contextuales y localmente cartesiana cerrada categorías existen varias definiciones incluidas las categorías con las familias, las categorías con los atributos y la comprensión de las categorías, que intenta encontrar un equilibrio.

Ver el nlab página en Modelos Categóricos de Tipos Dependientes para obtener más información.

Una pregunta de investigación en curso es qué tipo de modelo debe jugar el papel de local cartesiana cerrada categoría para intensional dependiente del tipo de teoría. Existe un consenso general de que esto se debe hacer uso de las ideas de homotopical álgebra como débil factorización del sistemay, a continuación, la interpretación de identidad tipo de uso de las ideas en Awodey y Warren, Homotopy teórico de los modelos de tipos de identidad. Por ejemplo, en general, hay una "coherencia teorema" en Lumsdaine y Warren, Los universos locales del modelo: un alto coherencia de la construcción para dependientes tipo de teorías, que muestra cómo interpretar intensional tipo de teoría en un número de categorías. Estos incluyen localmente cartesiano categorías cerradas, que también vienen equipados con un tipo de estructura de homotopical álgebra conocido como derecho de la correcta estructura del modelo.

Answer 2

Su entendimiento es un poco al revés: primero y segundo orden de la lógica son casos especiales de tipo de teorías, es sólo que por lo general son de la onuescrito, es decir, que tienen un solo tipo, que se suele llamar una especie o de un universo de discurso. La noción de un "modelo de tipo-teoría" se aplica a los de primer y segundo orden de la lógica: modelos de la lógica de primer orden son Heyting categorías, mientras que los modelos de segundo orden de la lógica son toposes.

¿Cómo funciona este alinee con el modelo habitual de la teoría? Un primer orden de la teoría es una lógica de primer orden complementarse con un poco de firma y los axiomas. El modelo de primer orden de la teoría (en el tipo de la teoría de la sensación) es, entonces, un Heyting categoría complementado con un sonido (con respecto a los axiomas) interpretación de la firma en el interior de la Heyting categoría. En particular, al restringir su tipo en la teoría de modelos, para que el ambiente categoría es la categoría de conjuntos, recuperar la noción de un modelo de modelo clásico de la teoría.

¿Por qué son los modelos de tipo de teorías categorías? Es porque podemos pensar en el tipo de teorías de primer y segundo orden de la lógica como presentaciones de categorías por los generadores (la lógica y la no-lógica de la firma de los tipo /primera/segunda-el fin de la teoría) y las relaciones (las reglas de inferencia/lógicas y no lógicas de los axiomas). Es decir, los datos que van en la especificación de tipo/primera/segunda-el fin de la teoría es la misma de los datos que especifica las categorías, por lo que las categorías son simplemente el tipo de teorías, pero visto desde un punto de vista diferente. (Una advertencia: yo creo que el tipo de teorías en ciencias de la computación son un poco más general y tal vez un poco por delante de la categórica/modelo de la teoría de la imagen).

Tenga en cuenta que el modelo de la teoría en sí sólo es coherente con el, pero no depende de el tipo de teoría (es decir, en las reglas de inferencia de la lógica). Más bien, el modelo de la teoría comienza por decidir para interpretar las proposiciones como característica morfismos a algún objeto de la verdad, los valores, y cómo éste se encuentra en el ambiente de la categoría en que se está haciendo en el modelo de la teoría determina el tipo de teoría que estás interpretación (por ejemplo, esta es la forma continua de la lógica y su funky reglas de inferencia surgen de continuo modelo de teoría donde decidimos de los modelos que se métrica espacios en lugar de conjuntos y de la verdad de los valores no-negativos reales).