💻 computer science

Definitional Inversion, Without Normalisation

Dieses Paper führt eine neuartige domänentheoretische Beweistechnik ein, die definitorische Inversionseigenschaften für abhängige Typsysteme etabliert, ohne sich auf Normalisierung zu verlassen, wodurch die metatheoretische Analyse nicht-normalisierender Systeme wie Idris und Lean sowie solcher mit Type-in-Type ermöglicht wird.

Ursprüngliche Autoren: Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

Veröffentlicht 2026-07-16

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Mario Carneiro, Thierry Coquand, Adrien Frabetti Mathieu, Meven Lennon-Bertrand, Paul-André Melliès, Stephanie Weirich

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 riesige, magische Bibliothek, in der jedes Buch ein mathematischer Beweis ist und die Regale selbst aus Logik bestehen. Dies ist die Welt der abhängigen Typsysteme (dependent type systems), der geheimen Triebwerk hinter modernen Beweisassistenten wie Lean und Programmiersprachen wie Idris. In dieser Welt sind die Regeln extrem streng: Wenn Sie versuchen, eine „Katze“ in ein Regal zu legen, das mit „Zahlen“ beschriftet ist, sollte das Sicherheitssystem der Bibliothek (der Type Checker) sofort „Error!“ schreien und Sie stoppen. Diese Sicherheit beruht auf einem Konzept namens definitorische Gleichheit (definitional equality), dem Weg der Bibliothek, um zu entscheiden, ob zwei Dinge im Wesentlichen dasselbe sind. Ist zum Beispiel ein „Quadrat“ einfach ein „Rechteck mit gleichen Seiten“? Wenn das System Ja sagt, behandelt es sie als identisch.

Das Überprüfen dieser Regeln ist jedoch knifflig. Traditionell mussten Mathematiker, um die Sicherheit der Bibliothek zu beweisen, zeigen, dass sich jedes einzelne Buch auf seine einfachste, grundlegendste Form reduzieren lässt (ein Prozess namens Normalisierung). Aber viele moderne, leistungsstarke Bibliotheken sind so konzipiert, dass sie unendlich oder selbstreferenzierend sind, was bedeutet, dass sie nicht auf eine endgültige Form vereinfacht werden können. Es ist, als würde man versuchen, ein Fraktal zu glätten; man findet immer wieder mehr Details. Lange Zeit konnten wir die Sicherheit eines Systems nicht beweisen, wenn es nicht vereinfacht werden konnte. Dieses Paper führt einen neuen Weg ein, um die Sicherheit der Bibliothek zu prüfen, ohne das Fraktal zuerst glätten zu müssen.

Das unendliche Rätsel und der magische Spiegel

Betrachten Sie ein abhängiges Typsystem als ein riesiges, sich selbst prüfendes Puzzle. Die Teile sind Typen (wie „Zahlen“ oder „Funktionen“), und das Ziel ist es, sicherzustellen, dass die Teile, wenn man sie zusammensteckt, perfekt passen. Die wichtigste Regel in diesem Puzzle ist die definitorische Inversion (definitional inversion). Es ist die Logik, die besagt: „Wenn zwei komplexe Strukturen gleich aussehen, müssen auch ihre Bestandteile gleich sein.“ Wenn Sie zum Beispiel zwei Funktionstypen haben, die identisch sind, beweist das Paper, dass auch deren Eingabetypen und Ausgabetypen identisch sein müssen. Dies ist entscheidend, da es dem Computer ermöglicht, komplexen Code sicher in kleinere Teile zu zerlegen, ohne verwirrt zu werden.

Jahrzehntelang war die einzige Möglichkeit, zu beweisen, dass diese Teile zusammenpassen, die Verwendung einer Methode namens Konfluenz (Confluence – Prüfung, ob verschiedene Pfade der Vereinfachung zum selben Ergebnis führen) oder logischer Relationen (Logical Relations – eine komplexe Methode, um zu vergleichen, wie Terme sich verhalten). Aber diese alten Werkzeuge stießen an eine Grenze. Die Konfluenz bricht zusammen, wenn man bestimmte „extensionale“ Regeln hinzufügt (wie $\eta$ -Gesetze, die besagen, dass eine Funktion vollständig durch das definiert ist, was sie tut, und nicht durch die Art, wie sie geschrieben ist). Logische Relationen erfordern meist, dass das System „normalisierend“ ist (also in der Lage ist, zu stoppen), was viele leistungsstarke, reale Programmiersprachen ausschließt, die unendliche Schleifen oder selbstreferenzierende Typen erlauben.

Der neue Ansatz: Eine Landkarte der Möglichkeiten

Die Autoren, ein Team aus Informatikern und Mathematikern, schlagen eine frische Strategie vor, die auf der Domänentheorie (domain theory) basiert. Anstatt zu versuchen, die Puzzleteile in eine einzige endgültige Form zu zwingen, bauen sie eine Landkarte aller möglichen Verhaltensweisen.

Stellen Sie sich vor, Sie versuchen, ein mysteriöses Wesen in einem dunklen Wald zu identifizieren.

Der alte Weg: Sie warten darauf, dass das Wesen aufhört sich zu bewegen und seine wahre, endgültige Form offenbart. Wenn das Wesen niemals aufhört sich zu bewegen (weil es eine unendliche Schleife ist), können Sie es nicht identifizieren, und der Wald ist unsicher.
Der neue Weg: Sie warten nicht darauf, dass es aufhört. Stattdessen beobachten Sie seine Fußabdrücke. Sie stellen fest, dass es einen „Linken Fuß“-Abdruck hinterlässt, dann einen „Rechten Fuß“-Abdruck, dann wieder einen „Linken Fuß“. Selbst wenn das Wesen niemals aufhört zu laufen, können Sie seine Gestalt dennoch ableiten, indem Sie das Muster seiner Schritte beobachten.

In der Sprache des Papers werden diese „Fußabdrücke“ als kompakte Elemente (compact elements) oder endliche Beobachtungen (finite observations) bezeichnet. Die Autoren konstruieren eine mathematische „Domäne“ (einen strukturierten Raum), in der jeder Typ nicht durch eine endgültige Antwort repräsentiert wird, sondern durch die Menge aller endlichen Dinge, die man über ihn beobachten kann. Sie nutzen eine Technik namens finitäre Projektoren (finitary projectors), um diese Domäne in handhabbare Stücke zu schneiden.

Was sie herausgefunden haben

Mit dieser „Fußabdruck“-Methode hat das Team erfolgreich bewiesen, dass die definitorische Inversion auch in Systemen gilt, die:

Niemals mit der Vereinfachung aufhören (nicht-normalisierend), wie etwa jene mit einer „Type-in-Type“-Regel (wo ein Typ sich selbst enthalten kann).
$\eta$ -Gesetze einschließen, welche knifflige Regeln sind, die Funktionen und Paare intuitiver agieren lassen, aber traditionelle Beweismethoden brechen.

Sie haben dies an einer kleinen Kernversion einer Typentheorie namens MLTT $\eta$ (Martin-Löf Type Theory mit $\eta$ -Gesetzen) demonstriert. Sie zeigten, dass selbst in diesem chaotischen, potenziell unendlichen System, wenn zwei Typen gleich sind, auch ihre Bausteine gleich sein müssen. Dies ist eine große Sache, denn es beweist, dass das „Sicherheitsnetz“ des Typsystems funktioniert, selbst wenn das System erlaubt ist, unordentlich und unendlich zu sein.

Das Team hat gezeigt, dass ihre Methode robust ist. Sie haben ihren Beweis erweitert, um Folgendes einzubeziehen:

Abhängige Summen (Paare von Daten).
Einheitstypen (Unit types – ein Typ mit nur einem Wert).
Fixpunkt-Kombinatoren (Werkzeuge, die unendliche Rekursion ermöglichen).
Natürliche Zahlen mit Pattern Matching.
Identitätstypen (Beweis, dass zwei Dinge dasselbe sind).
Beweis-irrelevante Propositionen (wo der Inhalt eines Beweises nicht zählt, sondern nur, dass er existiert).

Sie haben sogar ein Modell für ein „Universum strikter Propositionen“ gebaut und damit gezeigt, dass ihre Technik die komplexen Merkmale beherrscht, die in realen Werkzeugen wie Lean, Agda und Rocq zu finden sind.

Die Grenzen und die Zukunft

Das Paper ist sehr klar darüber, was es nicht tut. Es beweist nicht, dass diese Systeme „normalisierend“ sind (also dass sie immer anhalten). Tatsächlich arbeitet es explizit für Systeme, die nicht anhalten. Es löst auch nicht das Problem der „Neutrals“ (Variablen, die noch nicht ausgefüllt wurden) auf die gleiche Weise, wie es dies für geschlossene Terme tut, obwohl es andeutet, wie dies in der Zukunft möglich sein könnte.

Die Autoren haben ihre mathematischen Beweise bereits in Code umgesetzt und sie dreimal in drei verschiedenen Beweisassistenten (Agda, Lean und Rocq) verifiziert. Dies deutet darauf hin, dass ihre Methode nicht nur eine theoretische Idee, sondern ein praktisches Werkzeug ist.

Das Fazit

Dieses Paper ist wie das Überreichen einer neuen Brille an die Erbauer der magischen Bibliothek. Früher konnten sie die Sicherheit der Bibliothek nur prüfen, wenn die Bücher statisch und fertig waren. Jetzt können sie die Sicherheit von Büchern prüfen, die noch geschrieben werden, oder Büchern, die sich ewig selbst referenzieren. Indem sie sich auf das beobachtbare Verhalten (die Fußabdrücke) statt auf das endgültige Ziel (das Anhalten) konzentrieren, haben sie die Tür zur Verifizierung der mächtigsten, komplexesten und potenziell unendlichen Typsysteme geöffnet, die wir uns vorstellen können. Dies ebnet den Weg für Projekte wie „Lean4Lean“ und „MetaRocq“ – Projekte, bei denen Beweisassistenten ihren eigenen Code verifizieren, und macht die Werkzeuge, die wir zum Aufbau von Mathematik und Software verwenden, noch vertrauenswürdiger.

Technisches Resümee: Definitionale Inversion ohne Normalisierung

Problemstellung
Abhängige Typsysteme bilden die Grundlage kritischer Beweisassistenten (Agda, Lean, Rocq) und Programmiersprachen (Idris, abhängendes Haskell). Die Etablierung ihrer metatheoretischen Eigenschaften, insbesondere der definitionale Inversionsprinzipien (Injektivität und No-Confusion von Typkonstruktoren), ist essenziell für den Nachweis der Korrektheit, der Eindeutigkeit von Typen und der Kernel-Verifizierung. Bestehende metatheoretische Werkzeuge stehen jedoch vor schwerwiegenden Einschränkungen:

Konfluenz-basierte Ansätze: Diese haben Schwierigkeiten mit modernen Features wie $\eta$ -Gesetzen. Während Konfluenz für die $\beta$ -Reduktion funktioniert, führt die Kombination mit typisierter Konversion und $\eta$ -Gesetzen (z. B. für Funktionen oder Paare) oft zu nicht-konfluenten Systemen oder erfordert komplexe, nicht-standardisierte Präsentationen.
Normalisierungs-basierte Ansätze (Logische Relationen): Traditionelle logische Relationen beruhen auf der Existenz von Normalformen. Sie versagen bei nicht-normalisierenden Typtheorien (die in der Praxis häufig vorkommen, z. B. durch Verwendung von Type:Type oder Fixpunkt-Kombinatoren). Zudem erfordert der Nachweis der Normalisierung eine Umgebungslogik, die stärker ist als die Objektlogik (oft unter Verwendung von Induktion-Rekursion oder Impredikativität), was es unmöglich macht, die Metatheorie von Beweisassistenten in sich selbst zu untersuchen (z. B. Lean4Lean, MetaRocq).

Das Paper adressiert den spezifischen Fall von MLTT $\eta$ , einer Variation der Typtheorie von Martin-Löf mit abhängigen Produkten, $\beta$ - und $\eta$ -Gleichungen sowie einer Type:Type-Universe. Dieses System verhindert Konfluenz (aufgrund von $\eta$ ) und Normalisierung (aufgrund von Type:Type), wodurch seine dimensionalen Inversions-Eigenschaften bisher unbewiesen blieben.

Methodik
Die Autoren schlagen eine neue Beweistechnik vor, die auf der Domänentheorie basiert, speziell unter Verwendung von finitären Projektionen. Die zentrale Erkenntnis besteht darin, Typen nicht durch ihre Normalformen (die möglicherweise nicht existieren) zu interpretieren, sondern durch ihr „beobachtbares Verhalten“ mittels kompakter Elemente in einer Scott-Domäne.

Domänenkonstruktion: Die Autoren konstruieren eine Domäne $D$ $D$ als Lösung einer rekursiven Domänen-Gleichung, welche die Typkonstruktoren ( $\Pi$ $Π$ , $\mathcal{U}$ $U$ , etc.) repräsentiert. Die Domäne wird als Limit einer aufsteigenden Sequenz endlicher Approximationen ( $C_n$ $C_{n}$ ) aufgebaut, wobei die Elemente kompakt sind (was endliche Beobachtungen repräsentiert).
- Entscheidend ist, dass das Modell $\bot$ mit $\lambda x.\bot$ identifiziert, um die $\eta$ -Gesetze für Funktionen zu erfüllen, während $\Pi$ -Konstruktoren von $\mathcal{U}$ unterscheidbar bleiben, um Disjunktheit zu gewährleisten.
Semantische Typisierung: Eine semantische Typisierungsrelation wird auf den kompakten Elementen der Domäne definiert. Diese Relation wird mittels finitärer Projektoren (stetige Abbildungen $p: D \to D$ , sodass $p(\alpha) \le \alpha$ und $p(p(\alpha)) = p(\alpha)$ gilt) formuliert. Ein Typ wird als finitärer Projektor interpretiert, und ein Term steht in Relation zu einem Typ, wenn seine Denotation ein Fixpunkt dieses Projektors ist.
Logische Relation: Eine logische Relation wird über die syntaktischen Terme und die semantischen Zeugen (kompakte Elemente) definiert. Im Gegensatz zu traditionellen logischen Relationen, die rekursiv auf Typ-Normalformen operieren, rekuriert diese Relation auf der Stufe (Stage) $n$ $n$ der kompakten Elemente und der Struktur des semantischen Zeugen.
- Die Relation behandelt offene Terme, indem sie neutrale Terme als $\bot$ interpretiert, wodurch die Komplexität von Kripke-artiger Quantifizierung vermieden wird, während sie dennoch die Inversion in offenen Kontexten unterstützt.
- Die Relation ist bis zur Head-Reduktion definiert und integriert $\beta$ - und $\eta$ -Regeln direkt in die Struktur der logischen Relation.
Adequanz: Die Autoren beweisen ein Adequanztheorem: Wenn zwei Terme in der Syntax definitional gleich sind, sind sie in der logischen Relation verwandt. Dies ermöglicht die Ableitung syntaktischer Eigenschaften (wie Injektivität) aus semantischen Eigenschaften (Disjunktheit von Domänenelementen).

Zentrale Beiträge

Neue Beweistechnik: Eine domänentheoretische Methode zum Nachweis der dimensionalen Inversion (Injektivität und No-Confusion) ohne Abhängigkeit von Normalisierung oder Konfluenz.
Umgang mit $\eta$ und Nicht-Normalisierung: Die Technik beweist erfolgreich die Injektivität für Systeme mit $\eta$ -Gesetzen und Type:Type (oder Fixpunkt-Kombinatoren) – eine Kombination, die für Standardmethoden bisher unzugänglich war.
Schwache Umgebungslogik: Der Beweis stützt sich lediglich auf die Basisinduktion über natürliche Zahlen und vermeidet starke logische Prinzipien (wie Induktion-Rekursion), die für Normalisierungsbeweise erforderlich sind. Dies macht ihn geeignet für Selbst-Verifizierungs-Projekte (z. B. den Nachweis von Eigenschaften von Lean innerhalb von Lean).
Erweiterbarkeit: Die Technik wird an MLTT $\eta$ demonstriert und zeigt, dass sie auf reichere Theorien skalierbar ist, einschließlich:
- Abhängiger Summen ( $\Sigma$ ) und des Unit-Typs ($1$) mit $\eta$ -Gesetzen.
- Allgemeiner Rekursion via eines Fixpunkt-Kombinators ( $Y$ ).
- Natürlicher Zahlen ( $\mathbb{N}$ ) mit Pattern Matching.
- Beweis-relevanter Identitätstypen ($Id$) mit Transport.
- Einer Universe von strikten Propositionen ($Prop$) mit definitionaler Beweis-Irrelevanz.
Mechanisierung: Die Ergebnisse wurden in Agda, Lean und Rocq mechanisiert, wobei die verschiedenen oben genannten Erweiterungen abgedeckt werden.

Ergebnisse

Injektivität von $\Pi$ : Das Paper beweist, dass wenn $\Pi x:A.B \equiv \Pi x:A'.B'$ , dann $A \equiv A'$ und $B \equiv B'$ .
Disjunktheit: Typkonstruktoren sind disjunkt (z. B. $\Pi x:A.B \not\equiv \mathcal{U}$ ).
Subject Reduction und Progress: Als Konsequenzen der Inversionsprinzipien leiten die Autoren Progress- und Preservation-Theoreme ab und etablieren damit die Soundness der Sprache als Programmiersprache.
Scheitern von UIP: Das Modell zeigt, dass die Uniqueness of Identity Proofs (UIP/K-Regel) in diesem System nicht ableitbar ist, da das Domänenmodell zwischen verschiedenen Beweisen der Identität unterscheidet.

Bedeutung
Das Paper beansprucht, eine „blinde Stelle“ in der Metatheorie abhängiger Typsysteme zu füllen. Durch die Entkopplung der dimensionalen Inversion von der Normalisierung ermöglicht die Technik die rigorose Untersuchung nicht-normalisierender Systeme und Systeme mit reichen Gleichungstheorien (wie $\eta$ ), die in modernen Beweisassistenten und Programmiersprachen vorherrschen.

Die Autoren positionieren diese Arbeit als einen grundlegenden Schritt für Projekte wie Lean4Lean und MetaRocq, die darauf abzielen, die Metatheorie von Beweisassistenten innerhalb dieser selbst zu verifizieren. Da diese Projekte die Normalisierung der Objektlogik nicht voraussetzen können (aufgrund des Gödelschen Unvollständigkeitssatzes), bietet dieser domänentheoretische Ansatz einen gangbaren Weg zur Verifizierung von Kernen und zur Sicherstellung der Korrektheit von Typisierungsalgorithmen, ohne eine stärkere Umgebungslogik zu benötigen. Die Autoren deuten zudem potenzielle Anwendungen für dependente Programmiersprachen an, die nicht-terminierende Features oder graduelle Typisierung nutzen, wo die traditionelle, auf Terminierung basierende Metatheorie versagt.