Reducción de productos en HoTT a codificaciones de iglesia / scott

Así que actualmente estoy revisando el libro de HoTT con algunas personas. Afirmé que la mayoría de los tipos inductivos que veremos se pueden reducir a tipos que contienen solo tipos de función dependientes y universos tomando el tipo del recurrente como inspiración para el tipo equivalente. Comencé a esbozar cómo pensaba que esto funcionaría y después de algunos tropiezos llegué a lo que pensé que era una respuesta.

\cdot \times \cdot \equiv \prod_{A, B, C : U} (A \to B \to C) \to C

$\cdot \times \cdot \equiv \prod_{A, B, C : \mathcal{U}} (A \to B \to C) \to C$

(\cdot, \cdot) \equiv λ a : A . λ b : B . λ C : U . λ g : A \to B \to C . g (a) (b)

$(\cdot, \cdot) \equiv \lambda a : A. \lambda b : B. \lambda C : \mathcal{U}. \lambda g : A \to B \to C. g(a)(b)$

i n d_{A \times B} \equiv λ C . λ g . λ p . g (p r_{1} (p)) (p r_{2} (p))

$ind_{A \times B} \equiv \lambda C. \lambda g. \lambda p. g(pr_1(p))(pr_2(p))$

Esto proporciona las ecuaciones de definición correctas (se omiten las ecuaciones de definición para y ), pero esto significaría que tendría el tipo incorrecto. $pr_1$ $pr_2$ $ind_{A \times B}$

{ind}_{A \times B} : \prod_{C : A \times B \to U} (\prod_{a : A} \prod_{b : B} C ((a, b))) \to \prod_{p : A \times B} C ((p r_{1} (p), p r_{2} (p)))

$\text{ind}_{A \times B} : \prod_{C : A \times B \to \mathcal{U}} (\prod_{a:A} \prod_{b:B} C((a, b))) \to \prod_{p : A \times B} C((pr_1(p), pr_2(p)))$

Y no parece haber una solución simple para esto. También pensé en la siguiente definición.

i n d_{A \times B} \equiv λ C . λ g . λ p . p (C (p)) (g)

$ind_{A \times B} \equiv \lambda C. \lambda g. \lambda p. p(C(p))(g)$

Pero esto simplemente no teclea.

$uniq_{A \times B}$ $C((pr_1(p), pr_2(p)))$ $C(p)$ $uniq_{A \times B}$ $uniq_{A \times B}$

Parece que podemos definir el recursor aquí pero no el inductor. Podemos definir algo que se parece bastante al inductor pero que no lo logra. La recursividad nos permite realizar la lógica tomando este tipo como el significado de la conjunción lógica, pero no nos permite probar cosas sobre productos que parecen carecer.

¿Podemos hacer el tipo de reducción que afirmé que se puede hacer? Es decir, ¿podemos definir un tipo utilizando solo tipos de función dependientes y universos que tengan una función de emparejamiento e inductor con las mismas ecuaciones y tipos de definición que los productos? Es mi creciente sospecha de que hice una afirmación falsa. Parece que somos capaces de acercarnos tan frustrantemente, pero no logramos hacerlo. Si no podemos definirlo, ¿qué tipo de argumento explica por qué no podemos? ¿Los productos presentados en el libro de HoTT aumentan la fortaleza del sistema?

type-theory type-checking dependent-types homotopy-type-theory Jake
fuente

Según tengo entendido, la codificación habitual de la Iglesia nos da un tipo que admite la eliminación no dependiente (recurrente), pero no la eliminación dependiente (inductor). Su pregunta podría estar relacionada con esta . No estoy seguro si HoTT cambia algo con respecto a esto.

chi

Esto parece útil Según tengo entendido, mi pregunta sería respondida para el cálculo predictivo de los tipos de construcciones (Coq menos (co) inductivo). He estado buscando documentos que revisen estos modelos (modelos de CoC que no son modelos de CiC) pero no puedo encontrar ninguno. ¿Por casualidad tienes una fuente?

Jake

Lamentablemente no tengo una referencia para compartir. También me interesaría tener una fuente para citar este hecho del folklore.

chi

También sigo encontrando referencias folclóricas a este hecho, pero parece que no puedo encontrar una explicación.

Jake

Buena pregunta, pero no encajaría mejor en cstheory.stackexchange.com

Martin Berger

Respuestas:

La referencia estándar que a menudo doy es que la inducción no es derivable en la teoría del tipo dependiente de segundo orden por Herman Geuvers, que dice que no hay ningún tipo

N : T y p e

$N : \mathrm{Type}$

Z : N S : N \to N

$Z:N\qquad S:N\rightarrow N$

tal que

i n d : Π P : N \to T y p e . P Z \to (Π m : N . P m \to P (S m)) \to Π n : N . P n

$\mathrm{ind}:\Pi P:N\rightarrow \mathrm{Type}.P\ Z\rightarrow (\Pi m:N.P\ m\rightarrow P\ (S\ m))\rightarrow \Pi n:N. P\ n$

es demostrable Esto sugiere que, de hecho, dicha codificación no puede funcionar para pares como usted describe.

El sistema para el que está probado es un subconjunto del cálculo de construcciones, que contiene tipos de productos potentes y un universo. Sospecho que este resultado puede extenderse al sistema que le interesa, dependiendo de lo que tenga.

Lamentablemente, no sé la respuesta completa a su pregunta. Sospecho que agregar internamente ciertos principios de parametricidad es exactamente lo que se requiere para que estas codificaciones funcionen con el principio de inducción completo. Neel Krishnaswami, cuyo conocimiento es un superconjunto estricto, escribió un artículo en este sentido con Derek Dreyer:

Internalización de la parametricidad relacional en el cálculo extensivo de construcciones

También es interesante el siguiente artículo de Bernardy, Jansson y Patterson (Bernardy ha pensado profundamente en estos temas):

Parametricidad y tipos dependientes

Obviamente, la parametricidad tiene una fuerte relación con HoTT en general, pero no sé cuáles son los detalles. Creo que Steve Awodey ha considerado estas preguntas, ya que el truco de codificación es útil en contextos donde realmente no sabemos cómo deberían ser los eliminadores.

cody
fuente

Para que su idea funcione, necesita algo extra, como se señaló en la respuesta de @ cody. Sam Speight trabajó bajo la supervisión de Steve Awodey para ver qué se puede lograr en HoTT usando un universo impredecible , vea Codificaciones impredecibles de tipos inductivos en la publicación del blog de HoTT .

Andrej Bauer
fuente