Qu'est-ce que l'Axiome K?

Axiom K est aussi appelé le principe de unicité des preuves d'identité, et c'est un axiome sur la nature de l' type d'identité dans de Martin-Löf dépendants de ce type de théorie. Ce type n'existe pas (et en fait ne peut pas être défini) dans les théories de type plus simples comme le système F, donc c'est probablement la raison pour laquelle vous ne l'avez pas rencontré dans les livres que vous mentionnez.

le type d'identité s'écrit Id(A,x,y) ou aussi x = y et le code de la propriété qui x et y sont égaux (sous le Curry-Howard correspondence). Il y a une façon simple de donner une preuve du type d'identité, et c'est refl : Id(A,x,x), c'est à dire la preuve que x est égal à lui-même.

lors de l'enquête sur le type d'identité dans son thèse, 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 l'identité type.) Il stipule que toute la preuve p d'une égalité de la forme x = x est lui-même égal à la preuve triviale refl. Il s'ensuit que deux épreuves p et q équation x = y sont égaux, d'où le nom alternatif "unicité des preuves d'identité". Ce qui est remarquable, c'est qu'il a prouvé que ce n' suivre les règles standard de la théorie des types. Je recommande la lecture de Dan Licata l'article sur le type d'homotopie la théorie blog si vous voulez comprendre pourquoi, il l'explique beaucoup mieux que moi.

pour répondre à la deuxième partie de votre question: la correspondance des motifs de style ML n'est pas liée à K, puisque ML n'a pas de type d'identité et ne peut donc même pas formuler l'axiome K. D'autre part, K est nécessaire pour l'appariement de motifs dépendants, comme L'a introduit Thierry Coquand dans "Pattern matching with dependent types (1992)". La raison en est qu'il est très facile de prouver K par le filtrage 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épendante tapé les programmes fonctionnels et de leurs épreuves (2000)") que K est le chose que dépendant de la correspondance de modèle ajoute vraiment à l'dépendante de la théorie des types.

mon propre intérêt dans ce sujet est de comprendre exactement pourquoi l'appariement dépendant des motifs nécessite K et comment il peut être restreint pour qu'il ne le soit plus. Le le résultat a été un papier et une nouvelle implémentation du --without-K option dans Agda. L'idée de base est que l'algorithme d'unification utilisé pour l'analyse de cas lors de l'appariement de motifs dépendants ne devrait pas supprimer les équations de la forme x = x, parce que cela nécessite K. je vous recommande de lire le (introduction de) l'article si vous voulez en savoir plus.