Estoy leyendo el libro de HoTT y tengo dificultades con la inducción del camino.
Cuando miro el tipo en la sección 1.12.1 :
Con lo que tengo problemas es con la siguiente declaración:
mi primera impresión fue que esta última expresión nodefinela función resultante f : ∏ x , y : A ∏ p : x = A y C ( x , y , p ) ,
pero soloestablece su propiedad.
Esto contrasta con los ejemplos anteriores de los principios de inducción , ind A + B o ind N - existen ecuaciones definitorias para esos elementos - en realidad sabemos cómo construir la función resultante, dadas las premisas. Lo cual está de acuerdo con la "constructividad" de la teoría de tipos anunciada en todo el capítulo.
Volviendo a , sospechaba que (parece) que no está definido. Afirmar que el elemento f simplemente existe parece estar fuera de sintonía con el resto del capítulo. Y, de hecho, la sección 1.12.1 parece enfatizar que mi impresión es incorrecta y de hecho hemos definido
... la función definida por la inducción de ruta de c : ∏ x : A C ( x , x , refl x ) , que además satisface f ( x , x , refl x )
...
Eso me deja completamente confundido, pero tengo la sensación de que este punto es muy importante para todos los desarrollos posteriores. Entonces, ¿con cuál de las dos lecturas para debería ir? ¿O, probablemente, me falta alguna sutileza importante y la respuesta es "ninguna"?
Respuestas:
Es una ilusión que las reglas de cálculo "definen" o "construyen" los objetos de los que hablan. Usted observó correctamente que la ecuación para no la "define", pero no pudo observar que lo mismo es cierto en otros casos también. Consideremos el principio de inducción para la unidad tipo 1 , que parece particularmente "determinado". De acuerdo con la Sección 1.5 del libro HoTT, tenemos i n d 1 : ∏ C : 1 → T y p e C ( ⋆ ) → ∏ x : 1 Pind=A 1
con la ecuación
¿No es el caso de que cada término cerrado de tipo 1 es juiciosamente igual a ⋆ ? Eso depende de detalles desagradables y pruebas complicadas de normalización, en realidad. En el caso de HoTT, la respuesta es "no" porque e podría contener instancias del Axioma de Univalencia, y no está claro qué hacer al respecto (este es el problema abierto en HoTT).e 1 ⋆ e
Podemos eludir el problema con univalance considerando una versión de la teoría tipo que no tiene buenas propiedades de manera que cada término cerrado de tipo es igual a judgmentally ⋆ . En ese caso, es justo decir que sí sabemos cómo calcular con i n d 1 , pero:1 ⋆ ind1
Lo mismo se aplicará al tipo de identidad, ya que cada término cerrado de un tipo de identidad será igual a algunos , y entonces la ecuación para i n d = A nos dirá cómo calcular.refl(a) ind=A
El hecho de que sepamos cómo calcular con términos cerrados de un tipo, no significa que hayamos definido realmente algo porque hay más de un tipo que sus términos cerrados , como intenté explicar una vez.
Por ejemplo, la teoría de tipos de Martin-Löf (sin los tipos de identidad) se puede interpretar teóricamente en el dominio de tal manera que contenga dos elementos ⊥ y ⊤ , donde ⊤ corresponde a ⋆ y ⊥ a la no terminación. Por desgracia, dado que no hay forma de escribir una expresión sin terminación en la teoría de tipos, no se puede nombrar ⊥ . En consecuencia, la ecuación para i n d 1 no no nos dice cómo calcular el ⊥ (las dos opciones obvias ser "entusiasmo" y "pereza").1 ⊥ ⊤ ⊤ ⋆ ⊥ ⊥ ind1 ⊥
En términos de ingeniería de software, diría que tenemos una confusión entre la especificación y la implementación . Los axiomas HoTT para los tipos de identidad son una especificación . La ecuación no nos dice cómo calcular o cómo construir i n d = Cind=C(C,c,x,x,refl(x))≡c(x) ind=C , sino más bien que sin embargo está "implementado", requerimos que satisfaga la ecuación. Es una pregunta separada si tal i n d = C se puede obtener de manera constructiva.ind=C ind=C
Por último, estoy un poco cansado de cómo usas la palabra "constructivo". Parece que piensas que "constructivo" es lo mismo que "definido". Según esa interpretación, el oráculo de detención es constructivo, porque su comportamiento se define por el requisito que le imponemos (es decir, que genera 1 o 0 según si la máquina dada se detiene). Es perfectamente posible describir objetos que solo existen en un entorno no constructivo. Por el contrario, es perfectamente posible hablar de manera constructiva sobre propiedades y otras cosas que en realidad no se pueden calcular. Aquí hay uno: la relación definida por H ( n , d )H⊆N×{0,1}
es constructiva, es decir, no hay nada de malo en esta definición desde un punto de vista constructivo. Sucede que de manera constructiva no se puede demostrar que H es una relación total, y su mapa característico χ H : N × { 0 , 1 } → P r o p no factoriza a través de b o o l
Anexo: El título de su pregunta es "¿Es la inducción de ruta constructiva?" Después de haber aclarado la diferencia entre "constructivo" y "definido", podemos responder la pregunta. Sí, se sabe que la inducción de ruta es constructiva en ciertos casos:
Si nos limitamos a la teoría de tipos sin Univalencia para que podamos mostrar una fuerte normalización, entonces la inducción de ruta y todo lo demás es constructivo porque hay algoritmos que realizan el procedimiento de normalización.
Existen modelos de realizabilidad de la teoría de tipos, que explican cómo cada término cerrado en la teoría de tipos corresponde a una máquina de Turing. Sin embargo, estos modelos satisfacen el Axioma K de Streicher, que descarta la Univalencia.
Hay una traducción de la teoría de tipos (nuevamente sin Univalencia) a la teoría de conjuntos constructiva CZF. Una vez más, esto valida el axioma K. de Streicher.
Hay un modelo de grupo dentro de los modelos de realizabilidad que nos permite interpretar la teoría de tipos sin Streicher's K. Este es un trabajo preliminar de Steve Awodey y yo.
Realmente necesitamos resolver el estado constructivo de la Univalencia.
fuente
No soy una persona de HoTT, pero arrojaré mis dos centavos.
Getting rid of the subscripts leads to the general inductive definition.
Hope that helps!
PS. I'm no HoTT guy, so I'm assuming `Axiom K'. More precisely, I'm assuming that an elemente of type E must be the result of repeated applications of constructor of E . Hasta donde sé, HoTT, probablemente el capítulo 2 en adelante, desecha esta noción ... y eso no tiene absolutamente ningún sentido para mí.
fuente
Soy un tipo aficionado de HoTT, así que intentaré complementar la ya excelente respuesta de Moisés. Déjame tomar el tipoA × B as an example. The basic principle of constructive type theory, as outlined by Martin-Löf, is that *every element of A×B is described as being in the image of the constructor:
But sincepair is a constructor (and so is in particular injective), this means exactly that to build a function f:A×B→C , it suffices to describe it's action on a pair of elements in A and B , so
But this is only half of the story: what happens if this newly constructedf is applied to a given pair(a,b) ? Well then f should agree with its defining function f′ , i.e.
Entonces verá que la definición de un eliminador para el tipo inductivo con constructores dados viene en 2 pasos:
Un principio de existencia , que describe el tipo dei n d .
a coherence principle which defines the computational behavior ofind . In category theory, this would correspond to uniqueness of the eliminator in some sense.
Let me argue that this is the same for the=A type. We want to build, given x,y:A and p:x=y , an element of C (we're forgetting the dependencies for simplification). To do that, we need to assume that p was built using a constructor for the type x=y , which can only be refl(z) for some z . This means that to give a function
Ahora, ¿qué dice el principio de coherencia? Bueno, simplemente que si se aplica a un constructor conocido,F debería comportarse como F′ , lo que significa
¡Pero eso es exactamente lo que tienes arriba! El mismo principio que nos dio la existencia y coherencia para el eliminador deA × B nos da la existencia y coherencia para el eliminador de =UN .
fuente