Bei der abhängig typisierten Programmierung gibt es zwei Hauptmethoden zum Zerlegen von Daten und Durchführen einer Rekursion:
- Abhängiger Mustervergleich : Funktionsdefinitionen werden als Mehrfachklauseln angegeben. Die Vereinheitlichung stellt sicher, dass alle ausgelassenen Fälle unmöglich sind, und ein externer Löser stellt sicher, dass die Rekursion begründet ist.
- Eliminatoren : Jedem induktiven Datentyp ist eine Konstante , die als Induktionsprinzip und als rekursive Funktion dient, die Werte vom Typ zerlegt . Diese sind ausführlicher, haben jedoch den Vorteil, dass sie vollständig sind (alle Fälle werden von abgedeckt ) und durch Konstruktion enden.E D D E D.
Ich habe Eliminatoren für gängige Datentypen gesehen, wie , bei denen der Eliminator im Grunde eine mathematische Induktion ist, oder , bei der der Eliminator im Grunde eine Falte ist.L i s t
Ich habe mehrere Artikel über abhängige Mustervergleiche gelesen, und viele beziehen sich auf Typentheorien, in denen Datentypen definiert werden können, und Eliminatoren werden durch die Theorie bereitgestellt. Zum Beispiel beschreibt Eliminating Dependent Pattern Matching , wie UTT auf Eliminatoren basiert und wie Pattern Matching in Gegenwart von Axiom in Elimination umgewandelt werden kann . Nach meinem Verständnis liefert die Theorie den Eliminator, sobald ein Datentyp definiert ist.
Was ich nicht gefunden habe (oder zumindest nicht erkannt habe, wenn ich es gesehen habe), ist eine gute Beschreibung, wie man die Eliminatoren ableiten kann, sowohl ihre Typen als auch ihre Semantik.
Kann mich jemand auf eine Referenz verweisen, die beschreibt, wie man aus der Definition eines Datentyps einen Eliminator erhalten kann?
fix
und definiert istmatch
. Ich habe keine Referenz zur Hand, aber ich weiß, dass ich etwas darüber gelesen habe, wie dieser Eliminator erzeugt wird. cs.stackexchange.com/questions/104/… kann von Interesse sein.T
definiert Coq ein Induktionsprinzip,T_ind
das ein abhängiger Eliminator ist. Dies wird in Bezug auf Rekursion und Mustervergleich definiert, aber Sie können es im Prinzip als neue Konstante mit demselben Typ (mit derselben Semantik) annehmen.Antworten:
Die kanonische Referenz hierfür ist Peter Dybjer, Induktive Familien , der eine ziemlich umfassende Behandlung von induktiven Familien auf der Basis von Eliminatoren bietet.
quelle
Einige unserer jüngsten Veröffentlichungen zu diesem Thema sind möglicherweise hilfreich, da wir Eliminatoren für Lambda-codierte Datentypen ableiten. In diesem Beispiel finden Sie eine allgemeine Ableitung von Eliminatoren und in diesem Abschnitt die grundlegende Technik, die nur für den Nat-Typ angewendet wird.
quelle