Non-Derivability Results in Polymorphic Dependent Type Theory

Diese Arbeit zeigt durch die Konstruktion spezifischer Gegenmodelle, dass in der reinen polymorphen abhängigen Typentheorie λP2 weder parametrische Quotiententypen mit Induktionsprinzip noch starke Koinduktionsprinzipien für koinduktive Typen ableitbar sind und dass Funktionaler Extensionalismus für die Beweisbarkeit von Induktionsprinzipien unverzichtbar ist.

Das Wesentliche

Stell dir vor, du bist ein Architekt, der versucht, ein perfektes, logisches Universum zu bauen. In diesem Universum gibt es eine spezielle Sprache, die Typentheorie (genauer gesagt: $\lambda P2$), mit der man nicht nur Zahlen und Listen definieren kann, sondern auch beweisen kann, dass diese Dinge funktionieren.

Der Autor dieses Papers, Herman Geuvers, widmet es seinem Kollegen Stefano Berardi. Er stellt eine wichtige Frage: Was passiert, wenn wir versuchen, die Regeln dieses Universums zu erweitern, um noch mächtigere Werkzeuge zu bauen?

Hier ist die einfache Erklärung der Ergebnisse, verpackt in Alltagsanalogien:

1. Das Problem: Der "leere" Beweis

In diesem logischen Universum können wir Daten wie natürliche Zahlen (0, 1, 2...) oder Listen definieren. Das ist wie das Bauen von Lego-Steinen.
Aber es gibt ein riesiges Loch: Wir können zwar die Steine bauen, aber wir können nicht beweisen, dass sie sich so verhalten, wie wir es erwarten.

• Die Analogie: Stell dir vor, du hast einen Automaten, der Zahlen produziert. Du kannst sagen: "Hier ist eine Null" und "Hier ist die nächste Zahl". Aber du kannst dem Automaten nicht befehlen, sich zu verhalten wie die echten Zahlen, die wir aus der Schule kennen. Er könnte theoretisch auch eine Zahl produzieren, die gar nicht dazugehört, und du hast keine Möglichkeit, das im System zu beweisen. Das nennt man das fehlende Induktionsprinzip. Es ist, als würdest du ein Auto bauen, das fährt, aber du hast keinen Schlüssel, um zu beweisen, dass es wirklich sicher ist.

2. Die Lösung von anderen: Der "Schlüssel"

Andere Forscher haben vorgeschlagen, das Universum zu erweitern, indem sie neue Werkzeuge hinzufügen:

• Identitäts-Typen: Um zu sagen, wann zwei Dinge wirklich gleich sind.
• $\Sigma$-Typen: Um komplexe Pakete zu schnüren.
• Funktionaler Extensionalismus (FunExt): Eine sehr spezielle Regel, die besagt: "Wenn zwei Funktionen für jeden Eingabewert das gleiche Ergebnis liefern, dann sind sie die gleiche Funktion."

Mit diesen Werkzeugen konnte man endlich beweisen, dass die Zahlen sich richtig verhalten.

3. Die große Frage von Geuvers

Geuvers fragt sich nun: Welche dieser neuen Werkzeuge sind wirklich notwendig?
Können wir das Induktionsprinzip schon mit den einfachen Erweiterungen (Identität und Pakete) erreichen? Oder brauchen wir zwingend den "Funktionalen Extensionalismus"?

4. Die Entdeckungen (Die "Counter-Modelle")

Geuvers baut in diesem Papier ein Gegen-Universum (ein Modell), in dem die neuen Werkzeuge existieren, aber die gewünschten Beweise trotzdem scheitern. Er nutzt dafür eine Art "Spiegelwelt" aus ungetypten Lambda-Kalkül-Termen (eine sehr rohe Form von Computercode).

Hier sind seine drei Hauptergebnisse, einfach erklärt:

A. Die "Ströme" (Streams) sind nicht stabil

• Das Szenario: Man kann in der Sprache "unendliche Listen" (Ströme) definieren. Man hofft, dass man beweisen kann, dass zwei Ströme gleich sind, wenn sie sich in ihrem Verhalten nicht unterscheiden (wie zwei identische Musikstücke, die man nur anhört).
• Das Ergebnis: In Geuvers' Gegen-Universum gibt es zwei Ströme, die sich hören wie identische Musikstücke, aber im Inneren (im Code) völlig unterschiedlich aufgebaut sind.
• Die Metapher: Stell dir zwei identische Schallplatten vor. Sie spielen exakt die gleiche Musik ab. Aber wenn man sie zerlegt, sieht man, dass die eine aus Plastik und die andere aus Holz besteht. In diesem Universum kann man beweisen, dass sie nicht gleich sind, obwohl sie sich gleich anhören. Das Ko-Induktionsprinzip (der Beweis, dass sie gleich sind) funktioniert also nicht.

B. Quotienten (Teilen von Mengen) sind nicht parametrisch

• Das Szenario: Ein "Quotient" ist wie das Schneiden von einem großen Stück Stoff in kleinere Stücke, basierend auf einem Muster. Man möchte eine Funktion bauen, die auf dem ganzen Stoff definiert ist, aber man will sie nur auf den kleinen Stücken anwenden.
• Das Ergebnis: Geuvers zeigt, dass man in der reinen Sprache keine universelle Schere bauen kann, die für jedes Muster funktioniert (parametrisch).
• Die Metapher: Es ist, als würdest du versuchen, einen universellen Scherblock zu bauen, der für jede Art von Stoff (Seide, Wolle, Leder) funktioniert. In diesem Universum funktioniert der Block nur für einen bestimmten Stofftyp. Wenn du versuchst, ihn universell einzusetzen, klemmt er.

C. Der wichtigste Fund: Der "Funktional-Extensionalismus" ist der Schlüssel

Das ist das Herzstück des Papers. Geuvers baut ein Universum, in dem:

1. Wir Identitäts-Typen haben (wir wissen, was "gleich" bedeutet).
2. Wir haben die Regel, dass es nur einen Beweis für Gleichheit gibt (UIP).
3. Wir haben Pakete ($\Sigma$-Typen).

Aber: In diesem Universum funktioniert das Induktionsprinzip für natürliche Zahlen immer noch nicht!

• Die Metapher: Stell dir vor, du hast ein Auto mit Motor, Rädern und Lenkrad (die neuen Werkzeuge). Aber es fährt nicht. Warum? Weil dir der Zündschlüssel fehlt.
• Der "Zündschlüssel" ist die Funktional-Extensionalität (FunExt).
• Ohne diese eine spezielle Regel bleibt das System stumm. Man kann die Zahlen definieren, aber man kann nicht beweisen, dass sie sich wie echte Zahlen verhalten. Man braucht also zwingend diese eine Regel, um das Induktionsprinzip zum Laufen zu bringen.

Fazit für den Alltag

Dieses Papier sagt uns: Wenn du ein logisches System bauen willst, das sicher ist und Beweise für Datenstrukturen (wie Zahlen oder Listen) zulässt, reicht es nicht, einfach nur "Gleichheit" und "Pakete" hinzuzufügen. Du musst eine sehr spezifische, starke Regel hinzufügen (die besagt, dass Funktionen gleich sind, wenn sie sich gleich verhalten).

Ohne diese Regel ist das System wie ein Haus, das zwar Wände und ein Dach hat, aber keine Tür, durch die man wirklich hineingehen und die Regeln des Hauses nutzen kann. Es ist ein "leeres" Haus.

Geuvers hat also gezeigt, dass wir nicht einfach "ein bisschen mehr" brauchen, sondern dass wir genau dieses eine, spezielle Werkzeug brauchen, damit die Logik funktioniert.

Technische Zusammenfassung

Hier ist eine detaillierte technische Zusammenfassung des Papers „Non-Derivability Results in Polymorphic Dependent Type Theory" von Herman Geuvers auf Deutsch.

1. Problemstellung und Motivation

Das Paper adressiert fundamentale Limitierungen des reinen Kalküls der Konstruktionen (CC) und insbesondere seines Teilsystems $\lambda P2$ (polymorphe abhängige Typtheorie zweiter Ordnung).

• Hintergrund: In $\lambda P2$ können Datentypen (wie natürliche Zahlen, Listen) durch impredikative Kodierungen (z. B. Church-Zahlen) definiert werden. Zwar lassen sich diese Typen definieren, aber die zugehörigen Induktionsprinzipien sind in diesem System nicht ableitbar. Es wurde bereits gezeigt (u.a. in [12]), dass keine „kluge" Kodierung existiert, die das Induktionsprinzip für natürliche Zahlen in reinem $\lambda P2$ beweist.
• Aktuelle Forschung: In neueren Arbeiten ([1], [8]) wurde gezeigt, dass Induktion und Ko-Induktion möglich werden, wenn $\lambda P2$ um bestimmte Features erweitert wird:
  1. Identitätstypen (Identity Types)
  2. Eindeutigkeit von Identitätsbeweisen (UIP - Uniqueness of Identity Proofs)
  3. Funktionale Extensionalität (FunExt)
  4. $\Sigma$-Typen (stärkere existenzielle Typen)
• Offene Fragen: Es war unklar, welche dieser Erweiterungen notwendig sind. Können Quotiententypen oder Ko-Induktionsprinzipien (z. B. für Streams) bereits in reinem $\lambda P2$ definiert werden? Ist funktionale Extensionalität zwingend erforderlich, um Induktion zu beweisen?

Das Ziel des Papers ist es, durch die Konstruktion spezifischer Gegenmodelle zu zeigen, dass bestimmte Prinzipien in $\lambda P2$ (und in bestimmten Erweiterungen) nicht ableitbar sind.

2. Methodik

Der Autor verwendet eine semantische Methode, die auf der Konstruktion von Gegenmodellen (Counter-Models) basiert.

• Polyset-Modelle: Die Beweise stützen sich auf eine Semantik, die auf schwach extensionalen Kombinator-Algebren (WECA) aufbaut. Diese Modelle sind eine Form von Realisierbarkeitsssemantik.
• Aufbau der Modelle:
  • Die Typen werden als Teilmengen einer Kombinator-Algebra interpretiert (Polysets).
  • Terme werden als Elemente der Algebra interpretiert.
  • Ein zentrales Werkzeug ist die Verwendung von ungetypten $\lambda$-Termen (modulo $\beta$- oder $\beta\eta$-Gleichheit) als Basis für die Algebra.
• Strategie: Um zu zeigen, dass ein Prinzip (z. B. Induktion oder Ko-Induktion) nicht ableitbar ist, konstruiert Geuvers ein Modell, in dem die Interpretation des entsprechenden Typs leer ist (d. h., der Typ ist nicht inhabitiert), obwohl die zugrundeliegenden Datentypen existieren. Da die Soundness-Eigenschaft gilt (ableitbare Typen müssen in allen Modellen inhabitiert sein), beweist die Existenz eines solchen Modells die Nicht-Ableitbarkeit.

3. Hauptergebnisse und Beiträge

Das Paper liefert negative Ergebnisse für mehrere zentrale Fragen:

A. Nicht-Ableitbarkeit von Ko-Induktion für Streams

• Behauptung: Der in $\lambda P2$ definierbare Stream-Typ (als existenzieller Typ kodiert) ist keine finale Ko-Algebra.
• Ergebnis: Es gibt keine Terme, die das Ko-Induktionsprinzip (Bisimilarität impliziert Gleichheit) oder die Eindeutigkeit des Corekursors beweisen.
• Beweis: Es wird ein Modell konstruiert, in dem zwei verschiedene Streams ($s_1, s_2$) existieren, die bisimilar sind (d.h. sie haben dieselbe Kopf- und Schwanzstruktur), aber im Modell nicht gleich sind ($s_1 \neq s_2$). Dies widerlegt die Gültigkeit des Ko-Induktionsprinzips in reinem $\lambda P2$.

B. Nicht-Ableitbarkeit parametrischer Quotiententypen

• Definition: Ein parametrischer Quotiententyp $\sigma/R$ erfordert einen polymorphen Klassifizierer cls und einen Rekursor recq, die für beliebige Relationen $R$ funktionieren.
• Ergebnis: Solche parametrischen Quotiententypen sind in $\lambda P2$ nicht definierbar.
• Beweis: Es wird gezeigt, dass in einem Modell auf Basis von $\lambda$-Termen der Klassifizierer cls konstant sein müsste, was zu einem Widerspruch führt, wenn man spezifische Relationen (wie die Gleichheit auf Booleschen Werten) betrachtet.
• Nuance: Es wird angemerkt, dass nicht-parametrische Quotienten (für spezifische Relationen) existieren können, aber keine universelle, polymorphe Lösung.

C. Die Notwendigkeit funktionaler Extensionalität (FunExt) für Induktion

Dies ist das zentrale und überraschendste Ergebnis des Papers.

• Kontext: Awodey, Frey und Speight ([1]) zeigten, dass Induktion mit $\Sigma$-Typen, Identitätstypen und UIP möglich ist.
• Frage: Sind $\Sigma$-Typen und UIP allein ausreichend, oder ist funktionale Extensionalität (FunExt) zwingend notwendig?
• Ergebnis: Selbst wenn $\lambda P2$ um $\Sigma$-Typen und Identitätstypen (mit UIP) erweitert wird, ist das Induktionsprinzip für natürliche Zahlen nicht ableitbar, solange FunExt fehlt.
• Beweis: Der Autor konstruiert ein Modell über die Algebra $\Lambda_{id}$ (erweiterte $\lambda$-Kalküle mit Konstanten für Identitätstypen). In diesem Modell:
  1. Gelten die Regeln für Identitätstypen.
  2. Gilt UIP (alle Beweise für $x=y$ sind gleich).
  3. Gilt nicht FunExt (es gibt Funktionen, die punktweise gleich, aber nicht gleich sind).
  4. Das Induktionsprinzip für natürliche Zahlen ist im Modell leer (nicht inhabitiert).
• Schlussfolgerung: Funktionale Extensionalität ist der kritische Faktor, der die Ableitung von Induktionsprinzipien in diesen Systemen erst ermöglicht.

4. Technische Details der Modelle

• WECA (Weakly Extensional Combinatory Algebra): Die Modelle basieren auf Algebren von $\lambda$-Termen. Ein Schlüsselbeispiel ist die Menge der offenen $\lambda$-Terme modulo $\beta$-Gleichheit.
• Polyset-Struktur: Die Typen werden als Mengen von Realisierern (Teilmengen der Algebra) interpretiert.
• Erweiterung für Identitätstypen: Um Identitätstypen und $\Sigma$-Typen zu modellieren, wird die Algebra um Konstanten für refl (Reflexivität) und J (Eliminator) erweitert. Die Reduktionsregeln werden so gewählt, dass sie die gewünschten Eigenschaften (wie UIP) erzwingen, aber andere (wie FunExt) ausschließen.
• Gegenbeispiel für FunExt: Im Modell werden zwei Funktionen $f, g : \text{bool} \to \text{bool}$ konstruiert, die für alle Eingaben das gleiche Ergebnis liefern, aber als Terme in der Algebra nicht gleich sind (unterschiedliche Normalformen). Dies zeigt, dass FunExt im Modell nicht gilt.

5. Bedeutung und Fazit

Das Paper liefert einen wichtigen Beitrag zum Verständnis der Ausdruckskraft und der Grenzen der Typentheorie:

1. Klarheit über notwendige Axiome: Es wird eindeutig gezeigt, dass für die Ableitung von Induktionsprinzipien in Erweiterungen von $\lambda P2$ (wie sie in Homotopy Type Theory oder modernen Beweisassistenten verwendet werden) funktionale Extensionalität unverzichtbar ist. $\Sigma$-Typen und UIP allein reichen nicht aus.
2. Grenzen der impredikativen Kodierung: Es bestätigt, dass impredikative Kodierungen in reinem $\lambda P2$ zwar Datentypen definieren, aber deren universelle Eigenschaften (Induktion, Ko-Induktion, Quotienten) nicht vollständig erfassen können.
3. Methodischer Beitrag: Die Verwendung syntaktisch orientierter, aber modelltheoretischer Gegenbeispiele (basierend auf WECA) bietet eine robuste Methode, um Nicht-Ableitbarkeitsresultate in komplexen Typsystemen zu beweisen.

Zusammenfassend widerlegt das Paper die Hoffnung, dass „kluge Kodierungen" in reinem $\lambda P2$ ausreichen, um die volle Macht von Induktion und Ko-Induktion zu erhalten, und identifiziert die funktionale Extensionalität als den entscheidenden Baustein für die Definierbarkeit dieser Prinzipien in erweiterten Systemen.