En el libro de Hott, ¿son redundantes la mayoría de los formadores de tipos? Y si es así, ¿por qué?

En el capítulo 1 y el Apéndice A del libro de Hott , se presentan varias familias de tipos primitivos (tipos de universo, tipos de funciones dependientes, tipos de pares dependientes, tipos de coproductos, tipo vacío, tipo de unidad, tipo de número natural y tipos de identidad) para formar la base para la teoría del tipo de homotopía.

Sin embargo, parece que, dados los tipos de universo y los tipos de función dependientes, puede construir todos estos otros tipos "primitivos". Por ejemplo, el tipo Vacío podría definirse como

ΠT:U.T

Supongo que los otros tipos también podrían construirse de manera similar a como están en CC puro (es decir, simplemente derivar el tipo de la parte inductiva de la definición).

Muchos de estos tipos se vuelven explícitamente redundantes por los tipos inductivos / W que se presentan en los capítulos 5 y 6. Pero los tipos inductivos / W parecen ser una parte opcional de la teoría ya que hay preguntas abiertas sobre cómo interactúan con HoTT (en al menos cuando salió el libro).

Así que estoy muy confundido acerca de por qué estos tipos adicionales se presentan como primitivos. Mi intuición es que una teoría fundamental debería ser lo más mínima posible, y redefinir un tipo vacío redundante como primitivo en la teoría parece muy arbitrario.

¿Se hizo esta elección?

por algunas razones metateóricas que desconozco?
por razones históricas, para hacer que la teoría de tipos se parezca a teorías de tipos pasadas (que no necesariamente intentaban ser fundamentales)?
para la "usabilidad" de las interfaces de computadora?
para obtener alguna ventaja en la búsqueda de pruebas que desconozco?

type-theory dependent-type homotopy-type-theory usuario833970
fuente

Son redundantes, pero no de la manera que estás sugiriendo. Debería preguntarse para qué sirve la "minimidad de la base". ¿Y nos importa el propósito?

Andrej Bauer

Supongo que el trabajo técnico es mínimo por convención, donde las cosas no necesitan ser mínimas si obviamente es conveniente o se señala explícitamente lo contrario. El libro incluso se adhiere a esto en otros lugares, como cuando define los tipos de truncamiento (definidos por reglas, pero explícitamente no mínimos). Por ejemplo, si veía los nats definidos en términos de 0,1,10, el sucesor y la operación de potencia, estaría confundido, pero al menos podría ver por qué es conveniente a nivel notorio. Hott es un área de estudio mucho más compleja y quiero saber si me falta algo obvio.

user833970

Me interesaría saber cómo pueden ser perjudiciales. ¿Debo hacer una nueva pregunta al respecto?

user833970

@AndrejBauer Me gustaría saber por qué también serían perjudiciales. Mi razonamiento para creer que el lenguaje fundamental debería ser mínimo es el razonamiento detrás de la navaja de afeitar de occam, es una complejidad adicional injustificada. ¿Por qué parar ahí? ¿Por qué no agregar también listas, cadenas, pares, triples, vectores? Esas parecen elecciones arbitrarias, ¿qué las justifica? Editar: Acabo de notar que esta pregunta tiene respuestas; pero dejaré este comentario aquí solo para señalar por qué también me interesaría eso.

MaiaVictor

Escribiré una publicación de blog.

Andrej Bauer

Respuestas:

Permítanme explicar por qué la codificación sugerida del tipo vacío no funciona. Necesitamos ser explícitos sobre los niveles del universo y no barrerlos debajo de la alfombra.

Cuando las personas dicen "el tipo vacío", pueden significar una de dos cosas:

Un solo tipo que está vacío con respecto a todos los tipos. Tal tipo tiene la regla de eliminación: por cada y tipo de familia , hay un mapa . $E$ $n$ $A : E \to U_n$ $e_{n,A} : E \to A$
Una familia de tipos , uno para cada nivel de universo , de modo que es "el tipo vacío de ". Tal tipo tiene que satisfacer , obviamente, y también: para cada familia de tipo , hay un mapa . $E_k$ $k$ $E_k$ $U_k$ $E_k : U_k$ $A : E_{k} \to U_k$ $e_{k,A} : E_{k} \to A$

Sin ninguna condición, cuando las personas dicen "tipo vacío" esperan el primer significado anterior.

¿Cómo podemos obtener ? Un primer intento podría ser algo como $E$ pero este es precisamente el tipo de barrido debajo de la alfombra que crea confusión. Debemos escribir niveles explícitos del universo. Si escribimos algo como

E = Π (T : U) . T

$E = \Pi (T : U) \,.\, T$

entonces obtenemos una secuencia de tipos

, una para cada nivel

. Podríamos esperar que esta secuencia sea del tipo vacío en el sentido anterior, pero no lo es, porque

está en

pero se supone que está en

E_{k} = Π (T : U_{k}) . T

$E_k = \Pi (T : U_k) \,.\, T$

E_{0}, E_{1}, E_{2}, \dots

$E_0, E_1, E_2, \ldots$

k

$k$

E_{k}

$E_k$

U_{k + 1}

$U_{k+1}$

U_{k}

$U_k$

Otro intento es pero ahora tienes que explicar quése supone que es" ". Es posible que sienta la tentación de decir que hay un tipo de niveles de universo, por lo que

E = Π n . Π (T : U_{n}) . T

$E = \Pi n \,.\,\Pi (T : U_{n}) \,.\, T$

Π n

$\Pi n$

L

$L$

Ahora has caído en una trampa, porque te preguntaré: ¿en qué universo vive

? ¿Y en qué universo vive

? Esto no va a funcionar.

E = Π (n : L) . Π (T : U_{n}) . T

$E = \Pi (n : L) \,.\,\Pi (T : U_{n}) \,.\, T$

E

$E$

L

$L$

$U$ $B : U \to U$ $\Pi (X : U) B(X)$ $U$ $U$ $\Pi (X : U) X$ $U$

Se pueden organizar universos impredecibles. Sin embargo, un famoso teorema de Thierry Coquand (si no me equivoco) muestra que tener dos universos impredecibles, uno contenido en el otro, conduce a una contradicción.

La moraleja de la historia es: simplemente axiomatiza el tipo vacío directamente y deja de codificar cosas.

Andrej Bauer
fuente

Ese es un razonamiento convincente para axiomatizar el tipo vacío, pero todavía tengo curiosidad sobre el razonamiento para axiomatizar todas esas cosas más pesadas.

MaiaVictor

@MaiaVictor: a diferencia de qué?

Andrej Bauer

¿Lo siento? Solo quiero decir que justificaste convincentemente por qué es una buena idea axiomatizar el tipo vacío en particular. Pero OP también preguntó sobre otras cosas: "tipos de universo, tipos de funciones dependientes, tipos de pares dependientes, tipos de coproductos, tipo vacío, tipo de unidad, tipo de número natural y tipos de identidad" (que supongo que también son primitivas en el sistema propuesto en el Libro de HoTT). (Estoy, obviamente, no le pide que justifique los de todo, sólo se manifiesta mi interés.)

MaiaVictor

1 = \prod_{X : U} (X \to X)

$\mathbb{1} = \prod_{X : U} (X \to X)$

@IngoBlechschmidt curioso por saber qué tipo de problemas! Me parece bien ...

MaiaVictor

Estás haciendo varias preguntas que son similares pero distintas.

¿Por qué el libro HoTT no usa codificaciones de la Iglesia para los tipos de datos?

Las codificaciones de la iglesia no funcionan en la teoría de tipo Martin-Löf, por dos razones.

$n$ $k < n$

En segundo lugar, incluso si definió tipos de datos como los números naturales con codificaciones de la Iglesia, para hacer pruebas con estos tipos, necesita principios de inducción para probar cosas sobre ellos. Para derivar los principios de inducción para las codificaciones de la Iglesia, debe utilizar un argumento basado en la parametricidad de Reynolds, y la cuestión de cómo internalizar los principios de parametricidad en la teoría de tipos aún no está completamente resuelta. (El estado del arte es Nuyts, Vezzosi y Devriese's ICFP 2017 Cuantificadores paramétricos para la teoría del tipo dependiente : ¡tenga en cuenta que esto es mucho después de que se escribió el libro HoTT!)
A continuación, se pregunta por qué la base no es mínima. Esta es en realidad una de las características sociológicas distintivas de los fundamentos de la teoría de los tipos: los teóricos de los tipos consideran que tener un pequeño conjunto de reglas es una conveniencia técnica, sin mucha importancia fundamental. Es mucho, mucho más importante tener el conjunto correcto de reglas, en lugar del conjunto más pequeño de reglas.

Desarrollamos teorías de tipo para ser utilizadas por matemáticos y programadores, y es muy, muy importante que las pruebas realizadas dentro de la teoría de tipo sean las que los matemáticos y programadores consideran que se hacen de la manera correcta. Esto se debe a que los argumentos que los matemáticos suelen considerar que tienen un buen estilo suelen estar estructurados utilizando los principios algebraicos y geométricos clave del dominio de estudio. Si tiene que usar codificaciones complicadas, se pierde u oculta mucha estructura.

Esta es la razón por la que incluso las presentaciones teóricas de tipo de lógica clásica proposicional invariablemente dan todos los conectivos lógicos, aunque sea formalmente equivalente a una lógica con solo NAND. Claro, todos los conectores booleanos se pueden codificar con NAND, pero esa codificación oculta la estructura de la lógica.

Neel Krishnaswami
fuente

Gracias por esta respuesta! Necesitaré leer ese documento (y el tuyo) y podría tener más sentido. Pero, pensé que la jerarquía del universo fue diseñada para que parezca que puedes hacer cosas predicativas: por ejemplo (λA: U.λa: Aa) (ΠA: UA → A) se desugaría a (λA: Un + 1.λa: Aa) (ΠA: Un.A → A). Creo que es una extraña elección editorial no explicar esto, cada libro de lógica que conozco señala varias codificaciones mínimas más como CNF, DNF, NAND, etc. Y cualquiera que esté acostumbrado a establecer la teoría espera una codificación "natural" de los Nats, para demostrar la teoría. Pero eso puede ser solo mis prejuicios clásicos.

user833970

eso debería ser "impredecible" en mi último comentario

user833970

\prod (T : U_{n}) . T

$\prod (T : U_n) . T$

U_{n}

$U_n$

U_{n + 1}

$U_{n+1}$

U_{n}

$U_n$

Quizás estoy malinterpretando algo sobre las jerarquías del universo. Pensé que nunca nos importa en qué universo específico se encuentra un tipo, solo que los números del universo se pueden asignar cuando queremos verificar una prueba. Entonces, técnicamente ΠT: UT es una familia de tipos indexados sobre universos. Al igual que la identidad polimórfica es una familia de tipos indexados sobre universos. ¿Pero no tenemos el mismo problema con la identidad polimórfica? Realmente agradecería que si pudieras ampliar las últimas 2 oraciones, no creo que entienda.

user833970

Cuando dice que no tiene las propiedades de eliminación correctas, ¿quiere decir que una vez que se repara el universo, hay tipos en universos superiores que no pueden sintetizarse directamente con un término de ΠT: Un.T?

user833970