Co to jest Axiom K?

Question

Zauważyłem, że dyskusja "Axiom K" pojawia się częściej od czasu HoTT. Uważam, że jest to związane z dopasowywaniem wzorców. Jestem zaskoczony, że nie mogę znaleźć odniesienia w TAPL, ATTAPL lub PFPL.

• Co to jest Axiom K?
• Czy jest używane do dopasowywania wzorców w stylu ML jak w SML (lub tylko zależne dopasowywanie wzorca)?
• Jakie jest właściwe odniesienie dla Axiom K?

Answer 1

Axiom K nazywana jest także zasada wyjątkowości tożsamości dowodzi, i to jest aksjomat o naturze rodzaju tożsamości w zależnej teorii typów Martin-LOF. Ten typ nie istnieje (i w rzeczywistości nie może być zdefiniowany) w prostszych typach teorii, takich jak System F, więc jest to prawdopodobnie powód, dla którego go nie spotkałeś w wymienionych książkach.

Typ tożsamość jest napisane jak Id(A,x,y) lub też x = y i koduje tę właściwość, że x i y są równe (pod Curry-Howard correspondence). Istnieje jeden podstawowy sposób na przedstawienie dowodu tożsamości, a to jest refl : Id(A,x,x), tj. Dowód, że x jest równy sobie.

Podczas badania rodzaju tożsamości w jego thesis, Thomas Streicher wprowadził nowy eliminator dla typu tożsamości, który nazwał K (jako następną literę alfabetu po J, standardowy eliminator dla typu tożsamości). Stwierdza on, że każdy dowód p równości w postaci x = x sam jest równy banalnemu dowodowi refl. Z tego wynika, że ​​dwa dowolne równania p i q z równańsą równe, stąd alternatywna nazwa "niepowtarzalność dowodów tożsamości". Godne uwagi jest to, że udowodnił, że nie wynika to ze standardowych reguł teorii typów. Polecam lekturę Dan'a Licaty: article on the homotopy type theory blog, jeśli chcesz zrozumieć, dlaczego nie, tłumaczy to znacznie lepiej niż ja.

Aby odpowiedzieć na drugą część pytania: dopasowywanie wzorców w stylu ML nie ma związku z K, ponieważ ML nie ma typu tożsamości, a zatem nie może nawet sformułować aksjomatu K. Z drugiej strony, K jest wymagane do dopasowywania wzorców zależnych wprowadzonego przez Thierry'ego Coquanda w "Dopasowaniu wzorców do typów zależnych (1992)". Powodem tego jest to, że jest to bardzo łatwe do udowodnienia K dopasowując wzór na konstruktora refl typu Tożsamość:

K : (p : x = x) -> p = refl 
K refl = refl 

W rzeczywistości, Conor McBride pokazał w swojej pracy ("Zależnie wpisane funkcjonalne programy i ich dowody (2000) "), że K jest tylko jedną rzeczą, że zależne dopasowywanie wzorów naprawdę dodaje teorię typu zależnego.

Moje własne zainteresowanie tym tematem polega na dokładnym zrozumieniu, dlaczego zależne porównywanie wzorców wymaga K i jak można go ograniczyć, tak aby już nie było. W rezultacie uzyskano paper i nową implementację opcji Agda w wersji --without-K. Podstawową ideą jest to, że algorytm unifikacji używany do analizy przypadku podczas zależnego porównywania wzorców nie powinien usuwać równań w postaci x = x, ponieważ wymaga tego K. Zalecam przeczytanie (wprowadzenie) artykułu, jeśli chcesz dowiedzieć się więcej.