The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness

Each language version is independently generated for its own context, not a direct translation.

De Onzichtbare Muur in de Rekenmachine: Een Verhaal over KO7

Stel je voor dat je een enorme, complexe rekenmachine bouwt. Deze machine werkt met blokken die je kunt stapelen, samenvoegen en herschikken volgens een strikt setje regels. Je wilt weten: stopt deze machine ooit, of blijft hij voor eeuwig doorgaan met rekenen?

In de wereld van informatica noemen we dit "terminatie". Meestal is het makkelijk om te bewijzen dat een machine stopt: je telt gewoon de blokken. Als elke stap de stapel kleiner maakt, stopt het vanzelf.

Maar in dit paper (geschreven door Moses Rahnama) ontdekken de auteurs een geheime valkuil, een "onzichtbare muur" die voorkomt dat we dit op de gebruikelijke manier kunnen bewijzen. Ze noemen dit de "Global Orientation Barrier".

Hier is hoe het werkt, vertaald naar alledaagse taal:

1. De Magische Kloon (De "Step-Duplicating Recursor")

Stel je een regel voor in je rekenmachine die zegt: "Als je een stapel hebt, maak dan een kopie van die stapel en doe er nog een nieuwe stapel bij."

In de wiskunde heet dit een duplicerende recursor.

Links (De invoer): Je hebt één blok s.
Rechts (De uitvoer): Je hebt nu twee blokken s (één direct, één in een nieuwe stapel).

Het probleem? De machine is slim genoeg om te stoppen, maar de gewone meetlat die we gebruiken om te bewijzen dat hij stopt, faalt.

2. De "App-Lus" (De Valstrik)

De auteurs hebben een heel klein, simpel systeem bedacht genaamd KO7. Het is als een Lego-set met slechts 7 soorten blokken en 8 regels.
Er zit een speciaal blok in, laten we het app noemen. Dit blok is saai; het doet niets. Het is gewoon een doosje.

Wanneer de machine de "kloon-regel" gebruikt, gebeurt er iets vreemds:
De nieuwe kopie van het blok s wordt opgesloten in een doosje (app).

De realiteit: De machine stopt omdat de "tel-regel" (een ander blokje, delta) kleiner wordt.
De illusie: Voor de gewone meetlat ziet het eruit alsof de machine meer werk heeft gekregen, omdat er nu twee s-blokken zijn in plaats van één. De app-doosjes verbergen de kopieën zo goed dat de meetlat denkt: "Hé, er is meer massa! Dit gaat nooit stoppen!"

Dit noemen ze de "App Trap". De duplicatie is er echt, maar voor de meetlat is het een "dode massa" die niets doet.

3. De Twee Manieren om te Kijken

Het paper vergelijkt twee manieren om te proberen te bewijzen dat de machine stopt:

Manier A: De Global Aggregator (De "Totaal-teller")
Deze methode telt alles bij elkaar op. Hoeveel blokken zijn er? Hoe groot is de stapel?
- Het probleem: Omdat de machine twee kopieën maakt, ziet de teller de stapel groeien. De teller denkt: "Onmogelijk, dit wordt oneindig!"
- Het resultaat: De auteurs bewijzen (met een computer die alles nagerekend heeft in Lean 4) dat deze manier nooit werkt voor dit type machine. Het is een wiskundige onmogelijkheid. Het is alsof je probeert een auto te stoppen door te tellen hoeveel brandstof erin zit, terwijl de auto juist brandstof verbruikt om te bewegen. De teller ziet alleen de toevoer, niet het verbruik.
Manier B: De Modular Breaker (De "Scheur-methode")
Deze methode (genaamd Dependency Pairs) kijkt niet naar de hele stapel, maar splitst het probleem op.
- Ze zeggen: "Laten we de 'dode massa' in de app-doosjes negeren. Kijk alleen naar de 'tel-regel' (delta)."
- Als je alleen naar de tel-regel kijkt, zie je duidelijk dat die kleiner wordt. De machine stopt.
- Het resultaat: Deze methode werkt perfect. Ze "ontsnappen" aan de muur door blind te zijn voor de kopieën die in de doosjes zitten.

4. De Gecertificeerde Bewijslast

De auteurs hebben dit niet zomaar gezegd. Ze hebben:

Een computerbewijs (Lean 4): Ze hebben een programma geschreven dat wiskundig bewijst dat Manier A (de teller) altijd faalt voor dit systeem.
Een externe check (TTT2): Ze hebben de machine voorgelegd aan een beroemde terminatie-tool (TTT2). Die tool kon Manier A niet vinden (het gaf "MAYBE" of faalde), maar Manier B (de scheur-methode) gaf direct "YES, het stopt!".
Een veilige versie: Ze hebben een "veilige versie" van de machine gemaakt (SafeStep) waar ze kunnen bewijzen dat hij stopt, en zelfs een programma hebben geschreven dat elke berekening tot een eindresultaat brengt (een "normalizer").

5. Waarom is dit belangrijk?

Dit paper is een soort "grensverkenning". Het laat zien dat er een fundamentele muur bestaat tussen twee soorten wiskundige bewijzen:

Als je probeert alles in één grote som te tellen, mislukt het bij systemen die dingen kopiëren.
Als je slim bent en alleen kijkt naar de essentie (de tel-regel) en negeert de rommel (de kopieën in doosjes), dan lukt het wel.

De grote les:
Soms is het antwoord op een probleem niet om harder te tellen, maar om te erkennen dat sommige dingen die je ziet (de kopieën) eigenlijk niets betekenen voor het eindresultaat. De "muur" is niet in de machine zelf, maar in onze manier van kijken.

Samenvattend in één zin:
De auteurs hebben bewezen dat je een bepaalde soort rekenmachine niet kunt bewijzen dat hij stopt door gewoon te tellen (want hij maakt te veel kopieën), maar dat je het wel kunt doen door slim te negeren wat er in de "doosjes" zit. En ze hebben dit allemaal met een computer bewezen, zodat niemand het kan ontkennen.

Each language version is independently generated for its own context, not a direct translation.

Hier is een gedetailleerde technische samenvatting van het paper "The Global Orientation Barrier in Step-Duplicating Recursors" van Moses Rahnama, geschreven in het Nederlands.

Titel: De Globale Oriëntatiebarrière in Stap-Duplicerende Recursoren: Onmogelijkheid, Modulaire Ontsnapping en een Gecertificeerd Getuige

Auteur: Moses Rahnama (Mina Analytics)
Datum: Februari 2026
Formalisatie: Lean 4 (ca. 7.000 regels code), geverifieerd door TTT2 en CeTA.

1. Het Probleem

Het paper onderzoekt de terminatie (eindigheid) van eerste-orde herschrijvingssystemen (TRS) die stap-duplicerende recursoren bevatten. Het specifieke probleem is de grens tussen twee families van bewijstechnieken:

Directe/compositionele methoden: Methoden die een globale maatstaf (ranking function) toepassen op het volledige term, waarbij de bijdrage van subtermen wordt opgeteld (aggregatie).
Projectie-gebaseerde methoden: Methoden zoals Dependency Pairs (DP) met subterm-criteria, die zich richten op specifieke argumenten en andere delen van de term negeren.

De kernvraag is of een directe, compositionele maatstaf de terminatie kan bewijzen voor systemen waarbij een recursiestap een argument syntactisch dupliceert (bijv. $f(s, \dots) \to g(s, f(s, \dots))$ ). Het paper toont aan dat dit voor een breed scala aan compositionele methoden onmogelijk is, terwijl projectie-gebaseerde methoden dit probleem omzeilen.

2. Methodologie en Opzet

De auteurs gebruiken een minimalistisch, mechanisch geverifieerd bewijssysteem genaamd KO7 (7 constructors, 8 regels) om deze grens te demonstreren.

De KO7-Calculus: Een eerste-orde herschrijvingssysteem zonder binders, zonder externe geheugen (geen deling/sharing), en zonder object-niveau axioma's. De kernregel is een duplicerende recursor:
$rec(b, s, \delta(n)) \to app(s, rec(b, s, n))$
Hierbij wordt het stap-argument $s$ gedupliceerd: het komt voor in de app-constructor én in de recursieve call.
Vier Ontwerpcriteria: De onmogelijkheid geldt onder strikte voorwaarden:
1. Geen binding-operatoren (geen $\lambda$ -calculi).
2. Boom-semantiek (geen deling; duplicatie is zichtbaar in de termstructuur).
3. Geen object-niveau axioma's (geen idempotentie die duplicatie kan opheffen).
4. Onbeperkte stap-duplicatie (geen guards op $s$ ).
Formalisatie: De resultaten zijn volledig geverifieerd in Lean 4. De terminatie van het volledige, onbeveiligde systeem is extern gevalideerd door TTT2 (Tyrolean Termination Tool) en CeTA (Certifier).

3. De "App Trap" en de Barrière

Een cruciaal architecturaal kenmerk van KO7 is dat de constructor app geen reductieregels heeft. Wanneer de duplicerende regel triggert, belandt het gedupliceerde argument $s$ in app(s, ...) en is daar "gevangen".

Syntactisch: $s$ is verdubbeld.
Semantisch: $s$ kan niet terugkeren als recursie-teller; het is inert.
Het probleem voor directe methoden: Elke compositionele maatstaf die de app-constructor "ziet" (d.w.z. een positief gewicht toekent of voldoet aan subterm-axioma's), moet de waarde van twee kopieën van $s$ optellen. Omdat $s$ willekeurig groot kan zijn, kan de rechterkant van de regel ( $RHS$ ) nooit strikt kleiner zijn dan de linkerkant ( $LHS$ ) voor alle instanties. Dit creëert een globale oriëntatiebarrière.

4. Belangrijkste Bijdragen en Resultaten

A. Onmogelijkheidsstelling (Theorem 9.1)

De auteurs bewijzen machine-verifieerd dat geen enkele maatstaf binnen twee gedefinieerde classes van compositionele methoden de duplicerende recursor strikt kan oriënteren:

Tier 1 (Additief): Maatstaven waarbij de waarde van een term de som is van de gewichten van constructors en subtermen.
Tier 2 (Abstract): Maatstaven met willekeurige combinatiefuncties, mits ze voldoen aan de axioma's dat app(x, y) > x en app(x, y) > y.

Conclusie: Voor deze classes is het onmogelijk om terminatie te bewijzen voor het duplicerende systeem.

B. De Modulaire Ontsnapping (Theorem 9.2)

De auteurs tonen aan dat Dependency Pairs (DP) met een subterm-criterium de barrière omzeilen.

Mechanisme: DP projecteert op het derde argument (de recursieteller $n$ ) en negeert het gedupliceerde argument $s$ (dat in app zit).
Resultaat: De maatstaf $\pi$ oriënteert de regel omdat $\pi(\delta(n)) > \pi(n)$ , terwijl het gedupliceerde $s$ volledig wordt genegeerd. Dit voldoet niet aan de axioma's van de compositionele classes (Tier 1/2), waardoor het de onmogelijkheid ontsnapt.

C. Gecertificeerde Veilige Fragmenten (SafeStep)

Hoewel het volledige systeem terminatie heeft (bewezen door TTT2), is het niet lokaal confluënt (er is een tegenvoorbeeld bij eqW void void).

De auteurs definiëren een SafeStep sub-relatie met guards (bijv. $\delta$ -vlaggen, disequality guards).
Voor dit fragment bewijzen ze:
- Sterke Normalisatie (SN): Via een berekenbare triple-lexicografische maatstaf $(\delta\text{-flag}, \kappa_M, \tau)$ $(δ -flag, κ_{M}, τ)$ .
  - $\delta\text{-flag}$ : Daalt bij de recursiestap.
  - $\kappa_M$ : Een Dershowitz-Manna multiset-orde die duplicatie aankan.
  - $\tau$ : Een tie-breaker voor niet-duplicerende gevallen.
- Confluëntie: Bewezen via Newman's Lemma (SN + lokale confluëntie $\Rightarrow$ confluëntie).
- Gecertificeerde Normalisator: Een totale, correcte normalisatiefunctie is geëxtraheerd uit het bewijs.

D. Empirische Validatie (TTT2)

TTT2 werd gebruikt om het volledige KO7-systeem te testen:

Succes: Dependency Pairs (DP) en Lexicographic Path Orders (LPO) vonden een bewijs voor terminatie (YES).
Mislukking: Alle directe/compositionele methoden (Polynomial Interpretations, KBO, Matrix Interpretations) gaven MAYBE (geen bewijs gevonden binnen de zoekruimte), wat consistent is met de mechanische onmogelijkheidsresultaten.

E. Ordinale Kalibratie

De auteurs hebben de orde-type van de gebruikte maatstaf gekalibreerd:

De upper bound ligt onder $\varepsilon_0$ (specifiek $\omega^\omega \cdot 2$ ).
Er is een mechaniseerde lower-bound bewezen die surjectiviteit onder $\omega^\omega$ aantoont.

5. Significatie en Conclusie

Dit paper levert een scherp theoretisch inzicht in de beperkingen van terminatiebewijzen voor duplicerende systemen:

Fundamentele Grens: Er bestaat een fundamentele barrière voor directe, compositionele methoden bij systemen met onbeperkte stap-duplicatie in een "gevangen" context (zoals app).
Validatie van Modulaire Methoden: Het bevestigt dat modulaire methoden (zoals DP) niet alleen praktisch nuttig zijn, maar noodzakelijk zijn voor systemen die deze specifieke structuur hebben. Ze "ontsnappen" aan de barrière door irrelevante duplicatie te negeren.
Formalisatie: Het paper biedt een volledig mechanisch geverifieerd bewijs (in Lean 4) van zowel de onmogelijkheid als de oplossing, inclusief een gecertificeerde normalisator.
Ablatie: Het bewijs dat het verwijderen van duplicatie (lineaire recursor) de barrière direct opheft, bevestigt dat duplicatie de oorzaak is, niet het recursiepatroon zelf.

Samenvattend demonstreert het paper dat voor een specifieke klasse van herschrijvingssystemen, globale aggregatie faalt terwijl modulaire projectie slaagt, en dit onderscheid is formeel bewezen en geverifieerd.