Intuition hinter strenger Positivität?

Ich frage mich, ob mir jemand die Intuition geben kann, warum die strikte Positivität induktiver Datentypen eine starke Normalisierung garantiert.

Um es klar zu sagen, ich sehe, wie negative Vorkommen zu Divergenz führen, dh indem ich definiere:

data X where Intro : (X->X) -> X

wir können eine abweichende Funktion schreiben.

Aber ich frage mich, wie können wir beweisen, dass streng positive induktive Typen keine Divergenz zulassen? dh gibt es eine Induktionsmaßnahme, mit der wir einen Beweis für eine starke Normalisierung erstellen können (unter Verwendung logischer Beziehungen oder ähnlichem)? Und wo bricht ein solcher Beweis für negative Ereignisse zusammen? Gibt es gute Referenzen, die eine starke Normalisierung für eine Sprache mit induktiven Typen zeigen?

Es klingt so, als ob Sie einen Überblick über Normalisierungsargumente für Typsysteme mit positiven Datentypen wünschen. Ich würde Nax Mendlers Doktorarbeit empfehlen: http://www.nuprl.org/documents/Mendler/InductiveDefinition.html .

Wie das Datum schon sagt, ist dies eine ziemlich klassische Arbeit. Die grundlegende Intuition ist, dass eine Ordnungszahl jedem Element eines positiven induktiven Typs zugeordnet werden kann, z. B. für den Datentyp$\lambda$

Inductive Ord = Zero : Ord | Suc : Ord -> Ord | Lim : (Nat -> Ord) -> Ord

Wir würden bekommen:

wobei über Termen mit normalen Formen liegt. Die Einschränkung ist, dass diese Interpretation nur im dritten Fall definiert wird, wenn eine normale Form hat, was einige Sorgfalt in den Definitionen erfordert.$n$$f\ n$

Man kann dann rekursive Funktionen durch Induktion über diese Ordnungszahl definieren.

Beachten Sie, dass diese Datentypen bereits in der klassischen Mengenlehre definiert werden können, wie in dem hervorragenden Artikel über induktive Familien von Dybjer ( http://www.cse.chalmers.se/~peterd/papers/Inductive_Families.pdf ) angegeben. Da die Funktionsräume jedoch so groß sind, Orderfordern Typen wie die Interpretation wirklich große Ordnungszahlen.

Eine weitere gute Quelle, um über streng positive Typen hinauszugehen, ist die Doktorarbeit von Ralph Matthes: http://d-nb.info/956895891

Er diskutiert in Kapitel 3 Erweiterungen von System F mit (streng) positiven Typen und beweist in Kapitel 9 viele starke Normalisierungsergebnisse. In Kapitel 3 werden einige interessante Ideen diskutiert.

1. Wir können die kleinsten Fixpunkte für jeden Typ mit der freien Variablen hinzufügen , solange wir einen Monotonie-Zeugen bereitstellen können . Diese Idee ist bereits in Mendlers Werk vorhanden, das Cody erwähnte. Solche Zeugen existieren kanonisch für jeden positiven Typ, weil diese syntaktisch monoton sind.$\rho$$\alpha$$\forall \alpha \forall \beta.\, (\alpha \to \beta) \to \rho \to \rho[\beta/\alpha]$

2. Wenn wir von streng positiven zu positiven Typen wechseln, können die induktiven Typen nicht mehr als Bäume betrachtet werden (die W-Typ-Codierung). Stattdessen führen diese eine Form der Impredikativität ein, da die Konstruktion eines positiven induktiven Typs bereits über den Typ selbst quantifiziert. Beachten Sie, dass dies eine etwas milde Form der Impredikativität ist, da die Semantik solcher Typen immer noch durch die ordinale Iteration monotoner Funktionen erklärt werden kann.

3. Matthes liefert auch einige Beispiele für positive induktive Typen. Besonders interessant sind

   • die Art der Fortsetzungen , wobei in nicht vorkommt .$\mu.\, 1 + ((\alpha \to \rho) \to \rho)$$\alpha$$\rho$
   • Der Typ , der für jeden Typ funktioniert, indem er in einen positiven Typ umgewandelt wird. Beachten Sie, dass hierdurch die Impredikativität von System F sehr stark genutzt wird.$\mu \alpha \forall \beta.\, (\alpha \to \beta) \to \rho[\beta/\alpha]$$\rho$

Matthes verwendet auch positive induktive Typen, um die doppelte Negation zu analysieren, beispielsweise in diesem Artikel: https://www.irit.fr/~Ralph.Matthes/papers/MatthesStabilization.pdf . Er führt eine Erweiterung von Parigots und beweist eine starke Normalisierung.$\lambda\mu$

Ich hoffe, dass dies bei Ihrer Frage hilft.