Eliminierungsregel für den Gleichheitstyp alias J-Axiom

7

Ich implementiere einen Interpreter für Lambda-Kalkül und möchte jetzt den Gleichheitstyp hinzufügen. Die Einführungsregel dafür ist einfach, aber die Eliminierungsregel ist für mich ziemlich dunkel. Ich habe diesen Stackoverflow-Thread gefunden, aber er erklärt das J-Axiom nur in einem Satz. Wie kann es intuitiv verstanden werden?

盛安安
quelle

Antworten:

7

Ein vollständiges Verständnis dessen, was Jtatsächlich gesagt wurde und warum, ist erst vor relativ kurzer Zeit gekommen. Dieser Blog-Beitrag diskutiert es. Während das Denken in Bezug auf Homotopie und kontinuierliche Funktionen viel Intuition bietet und sich mit einem sehr reichen Bereich der Mathematik verbindet, werde ich versuchen, die folgende Diskussion auf der logischen Ebene zu halten.

Angenommen, Sie haben Gleichheitstypen direkt axiomatisiert (dies sind gruppenförmige Operationen und Gesetze): Wir haben eine Substitution, die funktoriell ist.

Γx:AΓreflx:x=AxΓ,x:A,y:Ap:x=AyΓ,x:A,y:Ap1:y=AxΓ,x:A,y:Ap:x=AyΓ,y:A,z:Aq:y=AzΓ,x:A,y:A,z:Apq:x=Az
(p1)1ppp1refl(pq)1q1p1reflppprefl(pq)rp(qr)
Γ,z:AF(z):UΓ,x:A,y:Ap:x=AyΓ,x:A,y:Asubst(F,p):F(x)F(y)
subst(F,refl)=idsubst(F,pq)=subst(F,q)subst(F,p)subst(λx.c=Ax,p)(q)=qp
Schließlich hätten wir Kongruenzregeln für alles und sagen, dass alles diese Gleichheit respektiert. Hier ist eine der wichtigsten Kongruenzen.
Γ,x:A,y:Ap:x=AyΓ,z:AB(z):UΓ,x:A,y:A,b:B(x)liftB(b,p):x,b=Σx:A.B(x)y,subst(B,p)(b)

Betrachten wir nun einen speziellen Substitutionsfall.

Γc:AΓ,t:Σx:A.c=AxC(t):UΓb:C(c,reflc)Γ,y:A,p:c=Aysubst(C,liftλz.c=z(reflc,p))(b):C(y,p)

Das ist J. Wir können Currying verwenden, um die schönere Form zu erhalten:

Γc:AΓ,y:A,p:c=AyC(y,p):UΓb:C(c,reflc)Γ,y:A,p:c=AyJA,c(C,b,y,p):C(y,p)

Wenn wir damit beginnen J, können wir natürlich alle anderen von mir definierten Strukturen neu definieren.

Wenn wir nun und dann . Wenn wir also , gibt es keine Möglichkeit, von über ein vorgewähltes im Allgemeinen dorthin zu gelangen, es sei denn, . (Aus der Homotopie-Perspektive sagt dass wir das Dreieck mit den Kanten , und füllen können .) Um es stumpfer zu machen, setzen Sie (und ) und wir erhaltenp:x=Ayq:y=Ayliftλz.x=z(p,q):y,p=y,pqy,py,pqpq=ppq=ppqpp=reflxy=xq=pDies ist die erforderliche Gleichheit, die im Allgemeinen nicht zutrifft (weil ein Wert vom Typ eine beliebige Äquivalenz darstellen kann und nichts besagt, dass zwei Äquivalenzen gleich sein müssen, oder äquivalent, weil wir wissen, dass Gruppoide nicht sein können trivial). Damit soll gezeigt werden, dass Dinge auf mehr als eine Weise gleich sein können, dh ein Wert von ist im Allgemeinen nicht so gut wie ein anderer.x=Ayy=y

Es ist zu verstehen, Jdass der Typ induktiv definiert ist und wenig über den Typ für festes und . Eine Möglichkeit, dies zu sehen und warum es so ist, besteht darin, zu untersuchen, wie die Kongruenz bei Gleichheitstypen mit übereinstimmenden Endpunkten aussieht. Wir haben die folgende Regel (ignoriert den Beweisbegriff, er kann mit oder ): Mit wir die Möglichkeit, dies zu tunΣy:A.x=Ayx=AyxyJsubstJ

Γ,x:Ap:x=AxΓ,x:A,q:x=Ax_:q=x=Axpqp1
liftλz.x=zliftλz.x=z(p,p1p):y,p=y,p sodass jeder Punkt gleichwertig war zu jedem anderen Punkt (wenn auch nicht unbedingt trivial). Wenn beide Endpunkte übereinstimmen, haben wir nicht die Flexibilität, die Gleichungen auszuwählen, um zuerst die Eingabegleichheit aufzuheben und dann eine beliebige Gleichheit durchzuführen.

Während Jdie nicht triviale gruppenförmige Struktur von Gleichheitstypen sorgfältig respektiert wird, gibt es in typischen Sprachen mit abhängiger Typisierung keine Möglichkeit, ein nicht triviales Element eines Gleichheitstyps tatsächlich zu definieren. An diesem Punkt stoßen Sie auf eine Weggabelung. Eine Möglichkeit besteht darin, Axiom K hinzuzufügen, das besagt, dass das Groupoid tatsächlich trivial ist, was viele Beweise viel einfacher macht. Die andere Möglichkeit besteht darin, Axiome hinzuzufügen, mit denen Sie die nicht triviale Gruppenstruktur artikulieren können. Das dramatischste Beispiel hierfür ist das Univalenzaxiom, das zur Homotopietypentheorie führt .

Derek Elkins verließ SE
quelle
1
Für die nächste Person, die es sieht: Diese ganze Antwort macht erst Sinn, wenn Sie die Theorie des Homotopietyps verstanden haben.
10.
Gibt es interessante, aber weniger dramatische Möglichkeiten, nicht triviale Gleichheiten auszudrücken als Univalence Axiom?
Łukasz Lew
1
@ ŁukaszLew Sie könnten Ergebnisse erzielen, die durch Univalenz impliziert werden, ohne das Ganze zu übernehmen. Univalenz gibt Ihnen ein -Gruppenoid, aber Sie können nur eine begrenzte Anzahl von Homotopie-Levels behaupten (tatsächlich ist dies effektiv das, was Axiom K tut). Sie können auch die Existenz bestimmter Typen mit nicht trivialen Identitätstypen, z. B. , behaupten oder behaupten, dass ein bereits vorhandener Typ einige nicht triviale Elemente in seinem Identitätstyp enthält. (,1)S1
Derek Elkins verließ SE
1
@ ŁukaszLew Es gibt nicht alles, was ich erwähnt habe. Die Existenz von geht über die Univalenz hinaus. Es und seine Struktur müssen entweder explizit behauptet werden oder es sind höhere induktive Typen erforderlich. In gewissem Sinne spricht die Univalenz nur über die Identitätstypen für das Universum (die Universen). S1
Derek Elkins verließ SE
1
@ ŁukaszLew Als geringfügige Korrektur ist darstellbar (obwohl ich glaube, dass dies etwas schwächer ist, als es ein höherer induktiver Typ geben würde). Trotzdem glaube ich nicht, dass bekannt ist, ob alle höheren Sphären sind oder nicht. Der Punkt ist, dass höhere induktive Typen ein separates Schema von Axiomen sind, die weder von der Univalenz abhängen noch von dieser ableitbar sind, obwohl sie aus denselben Intuitionen stammen und sicherlich interagieren. S1
Derek Elkins verließ SE