Engineering-Übersetzung der formalen Theoreme
Das Papier §4.4 gibt 6 zentrale metatheoretische Theoreme. Hier listen wir die Beweise nicht auf; wir übersetzen jedes Theorem nur in „was es für eine echte Agent Runtime bedeutet". Confluence zu verstehen ist der Schlüssel zum Verständnis des Werts des gesamten Papiers.
Engineering-Übersetzungstabelle der sechs Theoreme
[Originale Schlussfolgerung des Papiers §4.4]
| Theorem | Abschnitt | Engineering-Übersetzung |
|---|---|---|
| Preservation (Thm 59) | §4.4.1 | Nach jeder Regelanwendung bleibt die Registry well-formed: Parent-Zeiger bleiben innerhalb der Registry, Provisionen verschiedener Fibers sind disjunkt, und der Committed View zeigt nur auf installed Fibers. Bedeutung: Die Laufzeit befindet sich nie in einem Zustand mit „dangling Fiber-Referenzen" oder „zwei Plugins, die beide behaupten, 'database' bereitzustellen". |
| Recovery Exactness (Thm 61) | §4.4.2 | Unter der Voraussetzung der pairwise independence ist für ein Episode [b, u] eines Fibers n die Anwendung seines Accumulators äquivalent zum Zustand „n wurde nie geladen" (abgesehen von Control Fields). Bedeutung: Nach dem Entladen eines Plugins ist der Umgebungszustand äquivalent dazu, dass es nie existiert hat — entscheidend für HMR und den heißen Austausch von Plugins. |
| Ordering (Thm 63) | §4.4.3 | Provider müssen vor Consumers aktiviert und nach ihnen entladen werden; die Abhängigkeitsauflösung (Committed View), die ein Consumer während eines Episode liest, ist invariant. Bedeutung: Verbindungspools werden erst geschlossen, wenn alle Verbindungen zurückgegeben wurden; Datenbanken werden erst geschlossen, wenn alle Transaktionen committet wurden; kein „Race Condition, bei dem der Consumer einen halb geschlossenen Provider liest". |
| Resolution Coherence (Thm 64) | §4.4.3 | Alle Iterationen einer Transition laufen unter demselben Committed View; wenn sich Target mittendrin ändert, schließt die Transition entweder zu Active ab oder tritt über L-Divert/L-Raise in Unloading ein und rollt vollständig zurück. Bedeutung: Beim asynchronen Laden von Komponenten gibt es kein „halb alt, halb neu" — ein Teil der Effects kann nicht alte Abhängigkeiten verwenden, während ein anderer neue verwendet. |
| Progress (Thm 66) | §4.4.4 | Unter der Annahme, dass ≺ azyklisch ist, len(e_n) ≤ K und Fiber-Namen endlich sind, hat ein Non-Quiescent-Zustand immer eine anwendbare Regel, und die Anzahl der Schritte pro Fiber ist beschränkt. Bedeutung: Das System kann nicht deadlocks (Guards werden immer freigegeben); jede Konfigurationsänderung erreicht schließlich einen stabilen Zustand. |
| Confluence (Thm 73) | §4.4.5 | Unter den Annahmen von pairwise independence, component total on provision und no failure ist es gleich, wie viele Lade-/Entlade-/Ersetzungsvorgänge stattfinden — solange die endgültige Konfiguration identisch ist, ist der stabile Zustand äquivalent zu einem sauberen Start ab dieser Endkonfiguration. Bedeutung: Dynamische Geschichte hinterlässt keine Spur — nachdem ein Agent seine eigenen Komponenten wiederholt ersetzt hat, ist das äquivalent zu einem einmaligen Start der Endkonfiguration. Das ist der theoretische Grundstein des „selbst-evolvierenden Agenten". |
Confluence: Dynamische Geschichte hinterlässt keine Spur
Confluence ist der Höhepunkt dieser Theorie und verdient eine eigene Darstellung.
Anschauliche Aussage: Nachdem das System eine beliebige Anzahl dynamischer Lade-, Entlade- und Ersetzungsvorgänge durchlaufen hat, ist — solange die Endkonfiguration identisch ist — der stabile Zustand äquivalent zu dem, der durch einen sauberen Start ab der Endkonfiguration entsteht.
Für einen selbst-evolvierenden Agenten bedeutet das: Angenommen, der Agent ersetzt das Werkzeug A dreimal hintereinander, entlädt und installiert Skill B zweimal neu und passt den Isolation-Realm von Sub-Agent C an; solange seine endgültige Komponentenkonfiguration mit der von „einem sauberen Start" identisch ist, ist der stabile Zustand der Laufzeit (welche Komponenten aktiv sind, ihre Committed Views, der akkumulierte Umgebungszustand) äquivalent zu dem sauberen Start. Dynamische Geschichte hinterlässt keine Spur.
Das ist eine Garantie, die andere DI/HMR-Frameworks nicht bieten:
- Traditionelle DI unterstützt keinen Laufzeitaustausch, also gibt es keine Confluence zu sprechen;
- HMR verlangt von Entwicklern, Zustandsmigrationsfunktionen von Hand zu schreiben, ohne formale Garantie, dass die Migration korrekt ist;
- Container-Orchestrierung „Neustart = sauber" verwirft den gesamten Zustand grobkörnig, das ist keine Äquivalenz derselben Granularität.
[Originale Schlussfolgerung des Papiers §4.4.5] Beachten Sie die Vorbedingungen von Confluence:
- pairwise independence: Effects sind unabhängig voneinander oder kommutieren (Def 19);
- component total on provision: Jedes Component installiert tatsächlich alle deklarierten Keys (Def 69);
- no failure: Failure-Szenarien werden ausgeschlossen.
[Originale Schlussfolgerung des Papiers §4.4.5] Confluence schließt Failure-Szenarien aus (L-Raise in §4.3.4) — denn Failures sind eine echte Quelle von Divergenz: ein Schedule kann scheitern, ein anderer erfolgreich sein, aber Cor 62 garantiert, dass der Beitrag eines failed Fiber zum State 0 ist (die Seiteneffekte der gescheiterten Komponente werden vollständig zurückgerollt und beeinflussen andere Fibers nicht). „Failure" bricht also nicht die Zustandskonsistenz, führt aber dazu, dass zwei dynamische Pfade divergieren (einer mit Failure, einer ohne).
Was diese Beweise nicht garantieren
[Originale Schlussfolgerung des Papiers §6.1, §6.3] Die formalen Beweise decken nur die über den Context verwalteten Seiteneffekte. Sie garantieren nicht, dass:
- Die von Entwicklern geschriebenen Inverses notwendigerweise korrekt sind (die Witness-Bedingung
g(δ)=γist eine Pflicht, nicht verifiziert); - Seiteneffekte außerhalb des Context (direkte Modifikation von globalen Variablen, Dateien, Datenbanken, externen Systemen) rückgängig gemacht werden können;
- Externe Emissionen (Netzwerkanfragen, Nachrichten, E-Mails, Zahlungen) automatisch zurückgerollt werden können — einmal ausgesandt, überschreiten sie die Systemgrenze;
- Die Sicherheit nicht vertrauenswürdiger Plugins — Zugriffssteuerung auf Context-Ebene kann ein Prozess/Container/WASM-Sandbox nicht ersetzen;
- Confluence unter Failure-Szenarien (explizit ausgeschlossen);
- Versions- und Strukturkompatibilität von Abhängigkeitsschlüsseln (§6.6 offenes Problem).
Für detaillierte Vorbedingungen und Grenzen siehe Grenzen und Gesamtbewertung. Wie diese Theorie auf DeepSeek Harness landet, siehe Die Beziehung zu DeepSeek Harness.