J'ai remarqué que la discussion sur "Axiome K" revient plus souvent depuis HoTT. Je crois que c'est lié à l'appariement de modèles. Je suis surpris de ne pas trouver de référence dans TAPL, ATTAPL ou PFPL.Qu'est-ce que Axiom K?
Axiom K est aussi appelé le principe de l'unicité des preuves identité, et il est un axiome de la nature du type d'identité en théorie de type dépendant de Martin-Löf. Ce type n'existe pas (et ne peut d'ailleurs pas être défini) dans des théories de type plus simples telles que System F, c'est probablement la raison pour laquelle vous ne l'avez pas rencontré dans les livres que vous mentionnez.
Le type d'identité est écrit Id(A,x,y) ou encore x = y et code la propriété qui x et y sont égaux (sous la Curry-Howard correspondence). Il existe un moyen fondamental de donner une preuve du type d'identité, à savoir refl : Id(A,x,x), c'est-à-dire la preuve que x est égal à lui-même. Thomas Streicher a introduit un nouvel éliminateur pour le type d'identité qu'il a appelé K (comme la lettre suivante dans l'alphabet après J, l'éliminateur standard pour le type d'identité). Il stipule que toute preuve p d'une égalité de la forme x = x est elle-même égale à la preuve triviale refl. À partir de cela, il s'ensuit que deux preuves p et q de équation x = y sont égales, d'où le nom alternatif "unicité des preuves d'identité". Ce qui est remarquable, c'est qu'il a prouvé que cela ne fait pas et non d'après les règles standard de la théorie des types. Je vous recommande de lire le article on the homotopy type theory blog de Dan Licata si vous voulez comprendre pourquoi, il l'explique bien mieux que moi.
Pour répondre à la deuxième partie de votre question: La correspondance de modèle ML n'est pas liée à K, car ML n'a pas de type d'identité et ne peut donc même pas formuler l'axiome K. D'autre part, K est requis pour l'appariement de motifs dépendants tel qu'introduit par Thierry Coquand dans "Pattern matching with dependent dependent (1992)". La raison de cela est qu'il est très facile de prouver K par correspondance de motif sur le constructeur refl du type d'identité:
K : (p : x = x) -> p = refl
K refl = refl
En fait, Conor McBride a montré dans sa thèse («Dépendamment typé programmes fonctionnels et leurs preuves (2000) ") que K est le seulement chose que la correspondance de modèle dépendant ajoute vraiment à la théorie des types dépendants.
Mon propre intérêt pour ce sujet est de comprendre exactement pourquoi l'appariement de motifs dépendants nécessite K et comment il peut être restreint de sorte qu'il ne le soit plus. Le résultat était paper et une nouvelle implémentation de l'option --without-K dans Agda. L'idée de base est que l'algorithme d'unification utilisé pour l'analyse de cas pendant le couplage dépend ne devrait pas supprimer les équations du formulaire x = x, car cela nécessite K. Je vous recommande de lire l'introduction du document si vous voulez en savoir plus.
Si 'Id {A: Set a}: a -> a -> Set _' est défini par le constructeur unique' refl: forall {x: A}. Id x x', alors qu'est-ce qui pose problème pour faire correspondre une valeur de type 'Id x x' avec' refl'? – Cactus
La raison est que Id n'est pas une famille de types de données définis de manière inductive, mais plutôt une famille de types de données définie de manière inductive. Cela signifie que vous ne pouvez en principe correspondre qu'à une valeur de 'Id x y' si' x' et 'y' sont des variables distinctes. Ce serait très ennuyeux donc Agda utilise l'unification pour permettre la correspondance sur 'refl' dans d'autres situations: elle unifie les indices' x; x' du type de données avec les indices 'x ', x'' du constructeur. Après un pas, ceci se traduit par 'x = x', mais c'est exactement ce que nous avons besoin de K pour nous débarrasser de cette équation (lisez mon article pour la version plus longue). – Jesper
Normalement, l'appariement de motifs dépend de K, mais Agda vous permet également de le faire sans K, donc ni l'appariement de motif dépendant ni l'axiome K n'implique l'autre. L'axiome K dit fondamentalement que 2 preuves du même terme sont égales, éliminant la structure de groupoïde supérieure des types. –
@ 盛安安 ai-je commencé à demander (dans le deuxième point de la puce), "Est-il nécessaire" et pourquoi je l'ai changé à "Est-il utilisé". Donc, il semble qu'il est habituellement utilisé mais vous pouvez l'éviter (avec Agda au moins). –
@ 盛安安 "en éliminant la structure de type groupoïde plus élevée" - s'applique-t-elle uniquement aux types à travers la lentille de HoTT (ou est-ce que d'autres TT ont une structure de groupoïde plus élevée ou est-ce que je n'ai aucun sens)? –