Formalisme de la théorie des types
Bonjour,
J’essaye de m’initier à la théorie des types dépendants à la Martin-Löf en travaillant sur le polycopié d’Egbert Rijke.
Si j’ai bien compris, le système d’inférence de la théorie des types est purement syntaxique. Les preuves sont construites récursivement par des arbres de preuves dont les noeuds sont les « règles d’inférences » présentées dans le chapitre 1. Par définition, chaque règle d’inférence a un certain nombre de jugements en entrée, et un unique jugement en sortie.
Les jugements sont aussi des objets syntaxiques, présentés comme des séquents de la forme $\Gamma \dashv \mathcal{J}$, où $\mathcal{J}$ est de la forme $A\ \mathrm{type}$, $a : A$, $A \equiv A’ \mathrm{type}$, $a \equiv a’ : A$, où ici, $A$, $A'$, $a$ et $a’$ désignent des termes dans le contexte $\Gamma$. Un contexte $\Gamma$ est défini comme une suite $(x_k : A_k)_{k \leq n}$ d’expressions de la forme $x_k : A_k$, où $x_k$ est une variable, et $A_k$ un terme de $(x_i : A_i)_{i < k}$ et où, pour tout $k$, le jugement $(x_i : A_i)_{i < k} \vdash A_k\ \mathrm{type}$ se dérive à partir des règles d’inférences présentées dans le chapitre.
J’imagine que pour tout faire ça proprement et formellement, il faut faire une bonne grosse récurrence (au niveau méta-théorique, forcément): c’est-à-dire commencer par définir l’ensemble des jugements que le contexte vide permet de dériver, puis ensuite tous les jugements qu’on peut dériver en utilisant des contextes « validés » par la première étape, et ainsi de suite, probablement en faisant attention vu que certaines règles d'inférences semble "augmenter" la longueur du contexte.
Maintenant vient ma question: est-ce que le système présenté dans ce poly est vraiment complet (au sens usuel du terme, pas au sens de logique)? J’ai l’impression qu’il manque quelques trucs « de base » que je n’arrive pas à dériver en utilisant ses axiomes, et qui sont, j’ai l’impression utilisés à des endroits.
Par exemple, dans la « première règle de conversion des variables» (page 4 avec la numérotation du poly, 12 du fichier pdf), les hypothèses sont $\Gamma \vdash A \equiv A’\ \mathrm{type}$ et $\Gamma,\, x: A\, \Delta \vdash \mathcal{J}$, et la conclusion est $\Gamma,\, x : A’,\, \Delta \vdash \mathcal{J}$, la conclusion affirme implicitement que $(\Gamma,\, x : A)$ et $(\Gamma,\, x : A’,\, \Delta)$ sont considérés comme contextes valides.
Puisque $\Gamma,\, x : A$ est sensé être un contexte, on doit avoir $\Gamma \vdash A\ \mathrm{type}$, mais je ne pense pas pouvoir dériver $\Gamma \dashv A’\ \mathrm{type}$ à partir de $\Gamma \vdash A\ \mathrm{type}$ et de $\Gamma \vdash A \equiv A'\ \mathrm{type}$ (en tout cas, je ne vois rien dans les règles présentées qui permettraient de le faire). Dans le même genre, tel que les choses sont présentées, j’ai l’impression qu’on peut avoir $\Gamma \vdash a : A$ sans même avoir $\Gamma \vdash A\ \mathrm{type}$ (ça coince par exemple pour l'exercice 1.1, par exemple, vu que je ne vois pas trop comment introduire un $\Gamma \vdash A\ \mathrm{type}$, qui est utilisé en hypothèse de toutes les règles que je voudrais utiliser pour la résolution). Est-ce que je manque quelque chose? Qu’est-ce qui a été implicitement ajouté pour que tout ça fonctionne correctement?
Si quelqu’un connait une bonne référence qui fait ces choses de manière plus précise et plus formelle, je suis preneur (je précise que je suis intéressé par la théorie des types dépendants).
J’essaye de m’initier à la théorie des types dépendants à la Martin-Löf en travaillant sur le polycopié d’Egbert Rijke.
Si j’ai bien compris, le système d’inférence de la théorie des types est purement syntaxique. Les preuves sont construites récursivement par des arbres de preuves dont les noeuds sont les « règles d’inférences » présentées dans le chapitre 1. Par définition, chaque règle d’inférence a un certain nombre de jugements en entrée, et un unique jugement en sortie.
Les jugements sont aussi des objets syntaxiques, présentés comme des séquents de la forme $\Gamma \dashv \mathcal{J}$, où $\mathcal{J}$ est de la forme $A\ \mathrm{type}$, $a : A$, $A \equiv A’ \mathrm{type}$, $a \equiv a’ : A$, où ici, $A$, $A'$, $a$ et $a’$ désignent des termes dans le contexte $\Gamma$. Un contexte $\Gamma$ est défini comme une suite $(x_k : A_k)_{k \leq n}$ d’expressions de la forme $x_k : A_k$, où $x_k$ est une variable, et $A_k$ un terme de $(x_i : A_i)_{i < k}$ et où, pour tout $k$, le jugement $(x_i : A_i)_{i < k} \vdash A_k\ \mathrm{type}$ se dérive à partir des règles d’inférences présentées dans le chapitre.
J’imagine que pour tout faire ça proprement et formellement, il faut faire une bonne grosse récurrence (au niveau méta-théorique, forcément): c’est-à-dire commencer par définir l’ensemble des jugements que le contexte vide permet de dériver, puis ensuite tous les jugements qu’on peut dériver en utilisant des contextes « validés » par la première étape, et ainsi de suite, probablement en faisant attention vu que certaines règles d'inférences semble "augmenter" la longueur du contexte.
Maintenant vient ma question: est-ce que le système présenté dans ce poly est vraiment complet (au sens usuel du terme, pas au sens de logique)? J’ai l’impression qu’il manque quelques trucs « de base » que je n’arrive pas à dériver en utilisant ses axiomes, et qui sont, j’ai l’impression utilisés à des endroits.
Par exemple, dans la « première règle de conversion des variables» (page 4 avec la numérotation du poly, 12 du fichier pdf), les hypothèses sont $\Gamma \vdash A \equiv A’\ \mathrm{type}$ et $\Gamma,\, x: A\, \Delta \vdash \mathcal{J}$, et la conclusion est $\Gamma,\, x : A’,\, \Delta \vdash \mathcal{J}$, la conclusion affirme implicitement que $(\Gamma,\, x : A)$ et $(\Gamma,\, x : A’,\, \Delta)$ sont considérés comme contextes valides.
Puisque $\Gamma,\, x : A$ est sensé être un contexte, on doit avoir $\Gamma \vdash A\ \mathrm{type}$, mais je ne pense pas pouvoir dériver $\Gamma \dashv A’\ \mathrm{type}$ à partir de $\Gamma \vdash A\ \mathrm{type}$ et de $\Gamma \vdash A \equiv A'\ \mathrm{type}$ (en tout cas, je ne vois rien dans les règles présentées qui permettraient de le faire). Dans le même genre, tel que les choses sont présentées, j’ai l’impression qu’on peut avoir $\Gamma \vdash a : A$ sans même avoir $\Gamma \vdash A\ \mathrm{type}$ (ça coince par exemple pour l'exercice 1.1, par exemple, vu que je ne vois pas trop comment introduire un $\Gamma \vdash A\ \mathrm{type}$, qui est utilisé en hypothèse de toutes les règles que je voudrais utiliser pour la résolution). Est-ce que je manque quelque chose? Qu’est-ce qui a été implicitement ajouté pour que tout ça fonctionne correctement?
Si quelqu’un connait une bonne référence qui fait ces choses de manière plus précise et plus formelle, je suis preneur (je précise que je suis intéressé par la théorie des types dépendants).
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Une bonne référence est l’appendice de http://saunders.phil.cmu.edu/book/hott-online.pdf
Merci pour la référence, mais malheureusement, elle ne me convient pas trop. Je lisais le poly de Rijke précisément car je trouve la présentation de cet appendice trop insuffisante.
Pour citer quelques points qui me chagrinent:
- Toutes les propriétés méta-théoriques du système sont annoncées sans preuve,
- Les définitions précises des objets syntaxiques manipulés sont encore un peu trop rapide à mon gout (même si au moins, il y en a quelques unes).
Ne peut-on pas prouver, par récurrence sur la taille des dérivations de jugements de la forme $\Gamma \vdash A \equiv A'$ avec $A$ un type, que $A'$ est aussi un type?
Si je comprends bien ce que tu dis, tu dis qu'il ne faut pas essayer de construire une dérivation ayant comme hypothèses les deux énoncés $\Gamma \vdash A\ \mathrm{type}$, $\Gamma \vdash A \equiv A'\ \mathrm{type}$ et ayant $\Gamma \vdash A'\ \mathrm{type}$ en conclusion, mais plutôt de montrer que si $\Gamma \vdash A\ \mathrm{type}$ et $\Gamma \vdash A \equiv A'\ \mathrm{type}$ sont dérivables depuis le contexte vide (i.e admissible), alors $\Gamma \vdash A'\ \mathrm{type}$ l'est aussi, ce qui est différent. Est-ce bien cela? En tout cas, ça me semble possible oui (je devrais essayer d'écrire cette récurrence proprement).
Est-il donc implicite tout le long que lorsqu'on cherche à prouver une règle d'inférence (e.g comme dans l'exercice 1.1), on fait l'hypothèse que chacun de ses jugements en hypothèse sont admissibles? Ça ne restreint bien sûr pas la liste des jugements admissibles (qui sont, au fond, ceux qui nous intéressent), mais ce non-dit me surprend un peu.
Oui, tout-à-fait : tu as besoin d'un méta-théorème et non d'un théorème (i.e. qui serait prouvable dans le système de types).
L'exercice 1.1. (tu parles bien de "Give a derivation for the following term conversion rule ..."?) te demande de donner une dérivation, donc ça me semble très différent de la question précédente : ici, tu dois donner une dérivation en partant des hypothèses (sans même supposer qu'elles sont admissibles).
Je parle bien de cet exercice. Je le comprenais comme toi au début, mais tel quel, l'exercice me semble impossible: aucune règle d'inférence ne semble pouvoir annoncer $\Gamma \vdash\ A\ \mathrm{type}$, à partir de $\Gamma \vdash a : A$ et $\Gamma \vdash a : A$, alors que $\Gamma \vdash\ A\mathrm{type}$ est une hypothèse nécessaire aux règles d'affaiblissement et de variable, qu'il me semble falloir utiliser afin de pouvoir utiliser la règle de substitution et conclure.
Page 6 du poly (page 14 du fichier pdf), dans le paragraphe "changing variables", l'auteur annonce produire une dérivation de quelque chose n'ayant que $\Gamma, x : A, \Delta \vdash \mathcal{J}$ comme hypothèse et produit une dérivation ayant aussi $\Gamma\vdash A\ \mathrm{type}$ comme hypothèse. Donc j'ai bien l'impression que l'auteur s'attend en réalité à ce qu'on fasse secrètement l'hypothèse que $\Gamma \vdash A\ \mathrm{type}$ est admissible.
C'est très probablement un point de détail, mais j'ai l'impression de manquer un truc...