💻 computer science

Constructing (Co)inductive Types via Large Sizes

Dieser Artikel schlägt eine konsistente Erweiterung der intensionalen Typentheorie um einen großen Typ von Größen und parametrische Quantoren vor, um sowohl induktive als auch koinduktive Typen zu konstruieren, und überwindet dabei die Einschränkungen früherer Ansätze sowie die Inkonsistenz der aktuellen Implementierung von Größen in Agda.

Ursprüngliche Autoren: Bastiaan Laarakker, Daniël Otten, Benno van den Berg

Veröffentlicht 2026-05-01

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Bastiaan Laarakker, Daniël Otten, Benno van den Berg

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie bauen eine massive, sich selbst referenzierende Wissensbibliothek. In dieser Bibliothek kann jedes Buch (ein „Typ") Referenzen zu anderen Büchern enthalten, und manchmal bezieht sich ein Buch auf sich selbst. Um zu verhindern, dass diese Bibliothek in Chaos oder unendliche Schleifen kollabiert, benötigen Sie strenge Regeln darüber, wie diese Bücher geschrieben und gelesen werden können.

Dieser Artikel handelt vom Entwurf eines besseren Regelwerks für eine bestimmte Art von Bibliothek, die als „Beweisassistent" (wie Agda oder Lean) bezeichnet wird. Diese Werkzeuge helfen Mathematikern und Programmierern, Code zu schreiben, der garantiert funktioniert, und Beweise zu führen, die garantiert wahr sind.

Hier ist die Aufschlüsselung der Ideen des Artikels unter Verwendung einfacher Analogien:

1. Das Problem: Das „Stoppschild" versus das „Tachometer"

Derzeit verwenden Beweisassistenten einen „Stoppschild"-Ansatz (genannt syntaktische Prüfungen), um sicherzustellen, dass Programme nicht ewig laufen. Sie betrachten die Form des Codes. Wenn eine Funktion sich selbst aufruft, prüft der Computer: „Haben Sie ein kleineres Datenelement an den nächsten Aufruf übergeben?" Wenn ja, ist es sicher. Ist der Code komplex, könnte der Computer verwirrt sein und sagen: „Nein, ich kann nicht beweisen, dass dies stoppt", selbst wenn es tatsächlich stoppt.

Die Lösung des Artikels: Anstatt die Form des Codes zu betrachten, schlagen die Autoren vor, jedem Datenelement ein Größen-Label (wie ein Tachometer oder ein Höhenmarker) zu geben.

Induktive Typen (wie eine Liste von Zahlen) werden mit einer „Höhe" versehen. Eine rekursive Funktion muss immer in der Höhe absteigen.
Koinduktive Typen (wie ein unendlicher Datenstrom) werden mit einer „Tiefe" versehen. Eine rekursive Funktion muss immer tiefer gehen, um produktiv zu sein.

2. Der Fehler im aktuellen System: Der „magische Unendlichkeitswert"

Im aktuellen System (Agda) gibt es ein spezielles Label namens Unendlich ( $\infty$ ). Es soll die „größtmögliche Größe" sein, die alles abdeckt.

Die Analogie: Stellen Sie sich ein Lineal vor, das am ganzenden Ende eine Markierung für „Unendlich" hat. Das Problem ist, dass die Autoren dieses Artikels feststellten, dass Sie, wenn Sie versuchen, dieses Lineal zur Messung zu verwenden, versehentlich beweisen können, dass „Unendlich kleiner als Unendlich" ist. Dies bricht die Mathematik und macht das gesamte System inkonsistent (wie ein Lineal, das besagt, ein Meter sei kürzer als ein Meter).

3. Der neue Ansatz: Die „parametrische Menge"

Die Autoren schlagen eine neue Art vor, mit diesen Größen umzugehen, ohne ein einzelnes „Unendlich"-Label zu verwenden. Sie führen zwei spezielle Werkzeuge ein: Parametrische Existenzialquantoren ( $\exists$ ) und Parametrische Allquantoren ( $\forall$ ).

Stellen Sie sich diese als zwei verschiedene Arten vor, eine Menschenmenge (die Größen) zu betrachten:

Der Induktive Typ (Die „Existenzial"-Menge):
- Die Idee: Ein endlicher Baum (wie ein Stammbaum) hat eine bestimmte Höhe, aber wir müssen nicht genau wissen, wie hoch er ist, um ihn zu verwenden. Wir müssen nur wissen, dass es irgendwo eine Höhengrenze gibt.
- Die Metapher: Stellen Sie sich vor, Sie suchen eine bestimmte Person in einer Menge. Sie müssen nicht jeden sehen; Sie müssen nur wissen, dass es eine Person in der Menge gibt, die die Beschreibung erfüllt. Die „Größe" bleibt abstrakt und verborgen. Sie können nicht auf die spezifische Zahl schauen; Sie wissen nur, dass eine Grenze existiert. Dies verhindert das Paradoxon „Unendlich ist kleiner als Unendlich".
Der Koinduktive Typ (Die „All"-Menge):
- Die Idee: Ein unendlicher Strom (wie ein Live-Videostream) kann für jede Zeitspanne beobachtet werden.
- Die Metapher: Stellen Sie sich vor, Sie schauen einem Theaterstück zu. Um zu sagen, das Stück sei „unendlich", müssen Sie in der Lage sein, es für jede Dauer zu beobachten, die Sie wählen. Die „Größe" ist hier ein Versprechen, dass die Daten standhalten, egal wie tief Sie schauen.

4. Der magische Trick: Der Bau der Bibliothek

Die Autoren zeigen, wie diese komplexen Typen (die Bibliotheksbücher) mit diesen „Mengen"-Werkzeugen gebaut werden können:

Schritt 1: Sie bauen „Approximationen" der Typen in jeder möglichen Größe (wie den Bau eines Hausmodells in 1 Fuß Höhe, 2 Fuß Höhe usw.).
Schritt 2: Sie verwenden das Existenzial-Werkzeug, um alle Approximationen mit „endlicher Höhe" zu einem echten induktiven Typ zu bündeln.
Schritt 3: Sie verwenden das All-Werkzeug, um alle Approximationen mit „unendlicher Tiefe" zu einem echten koinduktiven Typ zu bündeln.

Warum ist dies besser?
Frühere Versuche konnten nur „endlich verzweigte" Bäume bauen (wie einen Stammbaum, bei dem jeder eine begrenzte Anzahl von Kindern hat). Diese neue Methode kann unendlich verzweigte Bäume bauen (wo ein Knoten eine unendliche Anzahl von Kindern haben kann), was viel leistungsfähiger und flexibler ist.

5. Der Beweis: Das „Realisierbarkeits"-Modell

Um zu beweisen, dass ihr neues System die Mathematik nicht zerstört, bauten sie ein „Realisierbarkeits-Modell".

Die Analogie: Stellen Sie sich einen Richter in einem Gerichtssaal vor. Der Richter nimmt nicht nur das Wort der Anwälte; er prüft die Beweise gegen ein spezifisches, sehr großes und sehr strenges Regelbuch.
Das Regelbuch: Sie interpretierten ihre „Größen" nicht als einfache Zahlen, sondern als überabzählbare Ordinalzahlen (ein Konzept aus der fortgeschrittenen Mathematik, das „größer" ist als die Menge aller natürlichen Zahlen).
Das Ergebnis: Indem sie Größen als diese massiven, überabzählbaren Zahlen behandelten, bewiesen sie, dass ihre „parametrischen" Regeln (die die spezifische Größe verstecken) perfekt funktionieren. Das System ist konsistent, was bedeutet, dass es nicht versehentlich beweisen wird, dass „Unendlich kleiner als Unendlich" ist.

Zusammenfassung

Der Artikel löst einen Fehler in aktuellen Beweisassistenten, bei dem ein „magischer Unendlichkeits"-Label logische Widersprüche verursacht. Sie ersetzen ihn durch ein System, das Größen als verborgene, abstrakte Grenzen behandelt.

Für endliche Dinge: Sie sagen: „Es gibt eine Grenze, aber wir werden sie nicht ansehen."
Für unendliche Dinge: Sie sagen: „Es funktioniert für jede Grenze, die Sie wählen."

Dies ermöglicht ihnen, komplexe, unendliche Datenstrukturen sicher zu konstruieren und sicherzustellen, dass der Beweisassistent ein zuverlässiges Werkzeug für Mathematik und Programmierung bleibt.

1. Problemstellung

Beweisassistenten (z. B. Agda, Lean, Rocq) verlassen sich auf abhängige Typentheorie, um Konsistenz und Entscheidbarkeit zu gewährleisten. Eine kritische Anforderung ist, dass alle rekursiven Funktionen total (terminierend) und alle ko-rekursiven Funktionen produktiv sein müssen.

Aktuelle Einschränkungen: Die meisten Systeme erzwingen Totalität durch syntaktische Prüfungen (z. B. strukturelle Rekursion oder Size-Change-Terminierung). Diese Prüfungen sind oft restriktiv, nicht-modular und empfindlich gegenüber Code-Refaktorierungen.
Größentypen (Sized Types): Eine typbasierte Alternative verwendet „Größen" (Ordinalzahlen), um Typen zu annotieren und die Terminierung durch wohlgeordnete Induktion über die Größe zu beweisen.
Die Agda-Inkonsistenz: Agda implementiert Größentypen, führt jedoch eine größte Größe ( $\infty$ ) ein, um den vollständigen induktiven/koinduktiven Typ als seine Approximation bei $\infty$ zu definieren. Dies führt zu einer logischen Inkonsistenz: Das System beweist $\infty < \infty$ , was die Irreflexivität strikter wohlgeordneter Mengen verletzt.
Bisherige theoretische Arbeiten: Frühere Versuche, dies mittels parametrischer Quantoren zu beheben (existenzielle $\exists$ für induktive, universelle $\forall$ für koinduktive Typen), waren begrenzt. Insbesondere konnten sie nur endlich verzweigende induktive Typen konstruieren, da der Größentyp als Menge der natürlichen Zahlen ( $\mathbb{N}$ ) interpretiert wurde, der die für unendlich verzweigende Strukturen notwendigen Limes-Ordinalzahlen fehlen.

Ziel: Eine konsistente Typentheorie konstruieren, die alle (ko)induktiven Typen (einschließlich unendlich verzweigender) unter Verwendung von Größentypen und parametrischen Quantoren unterstützt, ohne sich auf eine inkonsistente größte Größe zu verlassen.

2. Methodik

Die Autoren erweitern die Martin-Löf-Typentheorie (MLTT) um spezifische Merkmale, um diese Konstruktion zu erreichen und ihre Konsistenz durch ein Realisierbarkeitsmodell zu beweisen.

A. Die erweiterte Typentheorie

Die Theorie umfasst Standard-MLTT-Merkmale (Universen, $\Sigma$ , $\Pi$ , Identitätstypen) sowie:

Ein Typ der Größen (Size):
- Ausgestattet mit einer Null ($0$) und einem Nachfolger ( $\uparrow i$ ).
- Geordnet durch eine Präordnung ( $\leq$ ), die als bloße Proposition kodiert ist.
- Kritisch: Size ist ein großer Typ (nicht im Universum $U$ ), aber die Quantifizierung darüber kann kleine Typen ergeben.
Parametrische Quantoren:
- $\exists i. A(i)$ (Existenziell): Repräsentiert die Vereinigung von Approximationen. Terme sind Paare $\langle s, a \rangle$ , wobei die Größe $s$ jedoch abstrahiert ist (kann nicht per Pattern Matching untersucht werden). Die Elimination ist auf kleine Typen beschränkt.
- $\forall i. A(i)$ (Universell): Repräsentiert den Schnitt von Approximationen. Funktionen wirken uniform auf jede Größe.
- Parametizitäts-Axiome: Die Theorie enthält Axiome, die besagen, dass diese Quantoren mit Typkonstruktoren kommutieren (z. B. $\Pi x:A. \exists i. B(x,i) \simeq \exists i. \Pi x:A. \exists j < i. B(x,j)$ ). Dies internalisiert die Idee, dass Größen uniform behandelt werden.
Wohlgeordnete Induktion (fix):
- Ein Fixpunktoperator, der Definitionen durch Induktion über Größen erlaubt: $fix\ f : \forall i. A(i)$ gegeben $f : \forall i. ((\forall j < i. A(j)) \to A(i))$ .
- Die $\beta$ -Regel ist propositional (nicht definitorisch), um die Entscheidbarkeit der Typprüfung zu erhalten.

B. Konstruktion von (ko)induktiven Typen

Die Autoren kodieren (ko)induktive Typen als initiale Algebren und finale Koalgebren für polynomiale Endofunktoren ( $F$ ).

Ordinal-Approximationen: Sie definieren größenindizierte Funktoren $F[\exists -]$ und $F[\forall -]$ . Mithilfe des fix-Operators konstruieren sie initiale Algebren ( $\mu_3 F$ ) und finale Koalgebren ( $\nu_2 F$ ) für diese größenindizierten Funktoren. Diese repräsentieren den Typ, der bei einer bestimmten Größe abgeschnitten ist.
Vollständige Typen durch Quantifizierung:
- Induktive Typen: Definiert als $\mu F := \exists i. (\mu_3 F) i$ . Der existenzielle Quantor sammelt alle Terme, die durch eine Größe beschränkt sind.
- Koinduktive Typen: Definiert als $\nu F := \forall i. (\nu_2 F) i$ . Der universelle Quantor stellt sicher, dass Terme in jeder Tiefe beobachtbar sind.
Behandlung unendlich verzweigender Typen: Die entscheidende Innovation besteht darin zu zeigen, dass polynomiale Funktoren mit dem existenziellen Quantor schwach kommutieren. Dies erfordert die Existenz von Limes-Ordinalzahlen (Suprema von Folgen von Größen), was unmöglich ist, wenn Größen nur $\mathbb{N}$ sind.

C. Konsistenzbeweis: Realisierbarkeitsmodell

Um zu beweisen, dass die Theorie konsistent ist, konstruieren die Autoren ein Realisierbarkeitsmodell basierend auf Hylands Effektivem Topos.

Interpretation von Typen:
- Kleine Typen: Interpretiert als Partielle Äquivalenzrelationen (PERs) auf natürlichen Zahlen (berechenbare Daten).
- Große Typen: Interpretiert als Assemblies (Mengen mit Berechenbarkeitsrelationen).
Interpretation von Size:
- Der Typ Size wird als $\nabla \omega_1$ interpretiert, wobei $\omega_1$ die erste überabzählbare Ordinalzahl ist (die Menge aller abzählbaren Ordinalzahlen).
- Es wird die „volle" Realisierbarkeitsrelation zugewiesen, was bedeutet, dass Morphismen alle Größen uniform behandeln müssen (Parametizität).
Validierung:
- Da $\omega_1$ Limes-Ordinalzahlen enthält, validiert das Modell die Parametizitäts-Axiome, die für unendlich verzweigende induktive Typen erforderlich sind.
- Das Modell validiert Impredikativität (Quantifizierung über große Typen ergibt kleine Typen) und Eindeutigkeit von Identitätsbeweisen (UIP), obwohl die Syntax diese nicht voraussetzt. Dies zeigt, dass die Syntax mit stärkeren Theorien (wie der Homotopie-Typentheorie) kompatibel ist, ohne durch sie eingeschränkt zu werden.

3. Hauptbeiträge

Allgemeine Konstruktion von (ko)induktiven Typen: Im Gegensatz zu früheren parametrischen Ansätzen, die auf endlich verzweigende Typen beschränkt waren, konstruiert diese Arbeit alle (ko)induktiven Typen, einschließlich unendlich verzweigender (z. B. Brouwer-Ordinalzahlen, Modelle der konstruktiven Mengenlehre).
Auflösung der Agda-Inkonsistenz: Durch den Ersatz der inkonsistenten „größten Größe" ( $\infty$ ) durch parametrische Quantoren über einen großen Typ von Größen bieten die Autoren eine konsistente Alternative zur aktuellen Implementierung von Agda.
Parametrische Quantoren als Mechanismus: Sie demonstrieren, dass die Internalisierung von Parametizität durch $\exists$ und $\forall$ über Größen die notwendige Abstraktion effektiv erzwingt, um nicht-terminierendes Verhalten und logische Inkonsistenzen zu verhindern.
Robustes Realisierbarkeitsmodell: Die Konstruktion eines Modells, in dem Size als $\omega_1$ interpretiert wird, liefert eine rigorose semantische Begründung für die Theorie und beweist, dass die Parametizitäts-Axiome konsistent sind.

4. Ergebnisse

Theoretische Korrektheit: Das Paper beweist, dass die initiale Algebra und die finale Koalgebra für jeden polynomialen Endofunktor innerhalb der erweiterten Theorie existieren.
Konsistenz: Das Realisierbarkeitsmodell bestätigt die Konsistenz der Theorie. Es zeigt, dass die Axiome für parametrische Quantoren gelten, wenn Größen als eine überabzählbare Ordinalzahl interpretiert werden.
Kompatibilität: Die Konstruktionen verlassen sich in der Syntax nicht auf UIP oder Impredikativität, was die Ergebnisse mit der Homotopie-Typentheorie (HoTT) kompatibel macht, obwohl das Modell diese Eigenschaften erfüllt.

5. Bedeutung und zukünftige Arbeit

Auswirkung auf Beweisassistenten: Diese Arbeit bietet einen Weg, Größentypen in Beweisassistenten (wie Agda) ohne die aktuelle Inkonsistenz, die durch die $\infty$ -Größe verursacht wird, zu implementieren. Sie ermöglicht eine modularere und kompositionelle Terminierungsprüfung.
Berechenbares Verhalten: Die Autoren erkennen an, dass die Theorie zwar konsistent ist, die aktuelle Syntax jedoch kein berechenbares Verhalten für die Parametizitäts-Axiome besitzt (sie sind Axiome, keine Reduktionsregeln). Zukünftige Arbeiten müssen dies mit interner Parametizität verbinden (z. B. durch Brückentypen oder kubische Typentheorie), um in der Praxis Entscheidbarkeit und Kanonizität zu gewährleisten.
Entscheidbarkeit der Ungleichheit: Das Modell impliziert, dass Ungleichheit bei Größen aufgrund von Suprema im Allgemeinen nicht entscheidbar ist. Die Autoren schlagen einen hybriden Ansatz (definitorische vs. propositionale Ungleichheit) für die praktische Implementierung vor.
Verallgemeinerung: Das Modell könnte potenziell auf andere partielle Kombinatoralgebren verallgemeinert oder mit Effekten und Univalenz integriert werden.

Zusammenfassend überbrückt das Paper erfolgreich die Lücke zwischen dem theoretischen Bedarf an parametrischen Größentypen und der praktischen Anforderung an Konsistenz und ermöglicht die Konstruktion komplexer (ko)induktiver Typen in einem fundierten typentheoretischen Rahmen.