L'induction de chemin est-elle constructive?

Je lis le livre HoTT et j'ai du mal avec l'induction de chemin.

Quand je regarde le type dans la section 1.12.1 : je n'ai aucun problème à comprendre ce que cela signifie (je viens d'écrire le type de la mémoire, pour vérifier cela).

$$\text{ind}_{=_A}:\prod_{C:\prod\limits_{x,y:A}(x=_Ay)\to \mathcal{U}} \left( \left(\prod_{x:A}C(x,x,\text{refl}_x)\right) \to \prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p) \right),$$

Ce qui me pose problème, c'est la prochaine déclaration:
ma première impression était que cette dernière expression nedéfinitpasla fonction résultante f : ∏ x , y : A ∏ p : x = A y C ( x , y , p ) , maisindiquesimplementsa propriété.

$$\text{with the equality}\quad \text{ind}_{=_A}(C,c,x,x,\text{refl}_x):\equiv c(x)$$ $$f:\prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p),$$

Cela contraste avec les exemples précédents des principes d'induction , ind A + B ou ind N - il existe des équations définissant ces éléments - nous savons réellement comment construire la fonction résultante, compte tenu des prémisses. Ce qui est en accord avec la "constructivité" de la théorie des types annoncée tout au long du chapitre.$\text{ind}_{A\times B}$$\text{ind}_{A+B}$$\text{ind}_\mathbb{N}$

Pour en revenir à , je me méfiais du fait que (on dirait) qu'il n'est pas défini. Déclarer que l'élément f existe tout simplement semblait en décalage avec le reste du chapitre. Et en effet, la section 1.12.1 semble souligner que mon impression est fausse et nous avons en fait défini$\text{ind}_{=_A}$$f$

... la fonction définie par l' induction de chemin à partir de c : ∏ x : A C ( x , x , refl x ) , qui satisfait par ailleurs f ( x , x , refl x$f:\prod_{x,y:A}\prod_{p:x=_Ay} C(x,y,p),$
$c:\prod_{x:A}C(x,x,\text{refl}_x)$
...$f(x,x,\text{refl}_x):\equiv c(x)$

Cela me laisse complètement perplexe, mais j'ai le sentiment que ce point est très important pour tous les développements ultérieurs. Alors, laquelle des deux lectures pour dois-je choisir? Ou, probablement, il me manque une subtilité importante et la réponse est "ni"? $\text{ind}_{=_A}$

C'est une illusion que les règles de calcul "définissent" ou "construisent" les objets dont elles parlent. Vous avez correctement observé que l'équation pour ne la "définit" pas, mais vous n'avez pas observé que la même chose est également vraie dans d'autres cas. Considérons le principe d'induction pour l'unité de type 1 , qui semble particulièrement évidemment "déterminé". Selon la section 1.5 du livre HoTT, nous avons i n d 1 : ∏ C : 1 → T y p e C ( ⋆ ) → ∏ x : 1$\mathrm{ind}_{=_A}$$1$ avec l'équation i n d 1 ( C , c , ⋆ ) = c . Est-ce que cela "définit" ou "construit" i n d 1 dans le sens où il ne laisse aucun doute sur ce que i n d 1 "fait"? Par exemple, posons C ( x ) = N et a = 42 , et considérons ce que nous pourrions dire sur i n d 1 ( C , 42

$$\mathrm{ind}_1 : \prod_{C : 1 \to \mathtt{Type}} C(\star) \to \prod_{x : 1} P(x)$$ $$\mathrm{ind}_1 (C, c, \star) = c.$$ $\mathrm{ind}_1$$\mathrm{ind}_1$$C(x) = \mathbb{N}$$a = 42$ pour une expression e donnéede type 1 . Votre première pensée pourrait être que nous pouvons réduire cela à 42 car " ⋆ est le seul élément de 1 ". Mais pour être tout à fait précis, l'équation pour i n d 1 n'est applicable que si nous montrons e ≡ ⋆ , ce qui est impossible lorsque e est une variable, par exemple. Nous pouvons essayer de sortir de cela et dire que nous ne sommes intéressés que par le calcul avec des termes fermés, donc e devrait être fermé. $$\mathrm{ind}_1(C, 42, e)$$ $e$$1$$42$$\star$$1$$\mathrm{ind}_1$$e \equiv \star$$e$$e$

N'est-il pas vrai que chaque terme fermé de type 1 est égal au jugement à ⋆ ? Cela dépend en fait de détails désagréables et de preuves compliquées de normalisation. Dans le cas de HoTT, la réponse est "non" car e pourrait contenir des instances de l'Axiome Univalence, et on ne sait pas quoi faire à ce sujet (c'est le problème ouvert dans HoTT).$e$$1$$\star$$e$

Nous pouvons contourner le problème avec univalance en considérant une version de la théorie de type qui ne possède de bonnes propriétés de sorte que chaque terme fermé de type est égal à judgmentally ⋆ . Dans ce cas , il est juste de dire que nous ne savons comment calculer avec i n d 1 , mais:$1$$\star$$\mathrm{ind}_1$

1. Il en va de même pour le type d'identité, car chaque terme fermé d'un type d'identité sera, de manière jugée, égal à quelque , et donc l'équation pour i n d = A nous dira comment calculer.$\mathrm{refl}(a)$$\mathrm{ind}_{=_A}$

2. Tout simplement parce que nous savons calculer avec des termes fermés d'un type, cela ne signifie pas que nous ayons réellement défini quoi que ce soit parce qu'il y a plus dans un type que ses termes fermés , comme j'ai essayé de l'expliquer une fois.

Par exemple, la théorie des types de Martin-Löf (sans les types d'identité) peut être interprétée théoriquement par le domaine de telle manière que contient deux éléments ⊥ et ⊤ , où ⊤ correspond à ⋆ et ⊥ à la non-terminaison. Hélas, puisqu'il n'y a aucun moyen d'écrire une expression non terminale dans la théorie des types, ⊥ ne peut pas être nommé. Par conséquent, l'équation pour i n d 1 ne pas nous dire comment calculer le ⊥ (les deux choix évidents étant « avec impatience » et « paresseuse »).$1$$\bot$$\top$$\top$$\star$$\bot$$\bot$$\mathrm{ind}_1$$\bot$

En termes de génie logiciel, je dirais que nous avons une confusion entre la spécification et la mise en œuvre . Les axiomes HoTT pour les types d'identité sont une spécification . L'équation ne nous dit pas comment calculer avec ou comment construire i n d = C , mais plutôt que cependant je $\mathrm{ind}_{=_C}(C,c,x,x,\mathrm{refl}(x)) \equiv c(x)$$\mathrm{ind}_{=_C}$ est "implémenté", nous exigeons qu'il satisfasse l'équation. Il s'agit d'une question distincte de savoir si un tel i n d = C peut être obtenu de manière constructive.$\mathrm{ind}_{=_C}$$\mathrm{ind}_{=_C}$

Enfin, je suis un peu las de la façon dont vous utilisez le mot «constructif». Il semble que vous pensiez que "constructif" est le même que "défini". Selon cette interprétation, l'oracle Halting est constructif, car son comportement est défini par l'exigence que nous lui imposons (à savoir qu'il génère 1 ou 0 selon que la machine donnée s'arrête). Il est parfaitement possible de décrire des objets qui n'existent que dans un cadre non constructif. Inversement, il est parfaitement possible de parler de manière constructive de propriétés et d'autres choses qui ne peuvent pas réellement être calculées. En voici une: la relation définie par H ( n , d $H \subseteq \mathbb{N} \times \{0,1\}$ est constructif, c'est-à-dire qu'il n'y a rien de mal à cette définition d'un point de vue constructif. Il se trouve que constructivement on ne peut pas montrer que H est une relation totale, et sa carte caractéristique χ H : N × { 0 , 1 } → P r o p ne factorise pas par b o o

$$H(n,d) \iff (d = 1 \Rightarrow \text{$n$-th machine halts}) \land (d = 0 \Rightarrow \text{$n$-th machine diverges})$$ $H$$\chi_H : \mathbb{N} \times \{0,1\} \to \mathsf{Prop}$$\mathtt{bool}$, nous ne pouvons donc pas "calculer" ses valeurs.

Addendum: Le titre de votre question est "L'induction de chemin est-elle constructive?" Après avoir éclairci la différence entre "constructif" et "défini", nous pouvons répondre à la question. Oui, l'induction de chemin est connue pour être constructive dans certains cas:

1. Si nous nous limitons à la théorie des types sans Univalence afin de pouvoir montrer une forte normalisation, alors l'induction de chemin et tout le reste est constructif car il existe des algorithmes qui effectuent la procédure de normalisation.

2. Il existe des modèles de réalisabilité de la théorie des types, qui expliquent comment chaque terme fermé de la théorie des types correspond à une machine de Turing. Cependant, ces modèles satisfont l'Axiom K de Streicher, ce qui exclut l'Univalence.

3. Il y a une traduction de la théorie des types (là encore sans univalence) en théorie des ensembles constructifs CZF. Encore une fois, cela valide l'axiome K. de Streicher

4. Il existe un modèle groupoïde à l'intérieur des modèles de réalisabilité qui nous permet d'interpréter la théorie des types sans le K. de Streicher. Il s'agit d'un travail préliminaire de Steve Awodey et de moi-même.

Nous devons vraiment trier le statut constructif de l'Univalence.

I'm no HoTT person, but I'll throw in my two-cents.

Suppose we are wanting to make a function

$$f_A : \prod_{x,y : A}\prod_{p : x =_A y} C(x,y,p)$$ How would we do this? Well, suppose we're given any $x,y : A$ and a proof of their equality $p : x =_A y$. Since I know nothing about the arbitrary type $A$, I know nothing about the `structure' of $x,y$. However, I know something about the specific equality type: it has a single constructor, $$\mathsf{refl}_a : a =_A a, \text{ for any } a : A$$ Hence, $p \equiv \mathsf{refl}_a$ for some $a : A$, but this would force $x=a=y$. Hence, if we had an element of $C(x,x,\mathsf{refl}_x)$ for any $x : A$; ie if we had a function $$base_C : \prod_{x:A}C(x,x,\mathsf{refl}_x)$$ (for our specific $C$), then our function $f_A$ can be defined as follows: $$f_A(x,y,p) := base_C(x,x,p)$$ .

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 element $e$ of type $E$ must be the result of repeated applications of constructor of $E$. As far as I know, HoTT, probably chapter 2 onwards, throws away this notion ... and that makes absolutely no sense to me.

I'm an amateur HoTT guy, so I'll try to complement Moses' already great answer. Let me take the type $A\times B$ as an example. The basic principle of constructive type theory, as outlined by Martin-Löf, is that *every element of $A\times B$ is described as being in the image of the constructor:

$$\mathrm{pair}\ :\ A\rightarrow B\rightarrow A\times B$$ This philosophy allows us to define elimination: to build a function $f$ out of $A\times B$, it suffices to describe its action on the image of $\mathrm{pair}$.

But since $\mathrm{pair}$ is a constructor (and so is in particular injective), this means exactly that to build a function $f:A\times B\rightarrow C$, it suffices to describe it's action on a pair of elements in $A$ and $B$, so

$$f':A\rightarrow B\rightarrow C$$ is sufficient to describe such an $f$. In conclusion, there is a canonical way to define functions out of $A\times B$, and this can be encapsulated in the type $$(A\rightarrow B\rightarrow C)\rightarrow(A\times B\rightarrow C)$$ but this is exactly the type of $\mathrm{ind}_{A\times B}$.

But this is only half of the story: what happens if this newly constructed $f$ is applied to a given $\mathrm{pair}(a,b)$? Well then $f$ should agree with its defining function $f'$, i.e.

$$f(\mathrm{pair}(a,b))\ :=\ f'\ a\ b$$ i.e. $$\mathrm{ind}_{A\times B}\ f'\ \mathrm{pair}(a,b)\ :=\ f'\ a\ b$$ and this should hold definitionally (or computationally), which means the two should be completely interchangeable in all situations (which is much different from the $=$ in HoTT).

So you see that the definition of an eliminator for inductive type with given constructors comes in 2 steps:

1. an existence principle, which describes the type of $\mathrm{ind}$.

2. a coherence principle which defines the computational behavior of $\mathrm{ind}$. 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 $\mathrm{refl}(z)$ for some $z$. This means that to give a function

$$f:\Pi x, y:A, x=y\rightarrow C$$ it suffices to give a function $$f':\Pi z:A, C$$ which is defined for $\mathrm{refl}(z)$ (again, forgetting the dependencies in $C$).

Now what does the coherence principle say? Well simply that if applied to a known constructor, $f$ should behave like $f'$, which means

$$f\ z\ z\ \mathrm{refl}(z):= f'\ z$$

But that's exactly what you have above! The same principle that gave us the existence and coherence for the eliminator of $A\times B$ gives us the existence and coherence for the eliminator of $=_A$.