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

Questo lavoro identifica e formalizza in Lean 4 un limite di orientabilità globale per i ricorsori duplicanti, dimostrando l'impossibilità di prove composizionali dirette su un sistema minimale e proponendo una via d'uscita tramite criteri basati su proiezioni e una catena di certificazione completa per la terminazione e la confluenza.

L'essenziale

Il Muro Invisibile e la Chiave Magica: Una Storia di Computer che si Ripetono

Immagina di avere un robot molto intelligente, ma un po' testardo, che deve risolvere un problema. Questo robot segue delle regole precise (chiamate "sistema di riscrittura") per trasformare un'istruzione complessa in una risposta semplice. Il problema è che, a volte, il robot deve copiare una parte dell'istruzione e usarla due volte invece di una.

Gli scienziati Moses Rahnama e Mina Analytics hanno scoperto qualcosa di incredibile su come questi robot pensano (o meglio, su come proviamo a dimostrare che non impazziranno mai).

Ecco la storia divisa in tre atti.

1. Il Problema: Il Robot che si Copia (L'Impasse)

Immagina che il tuo robot abbia una regola speciale:

"Se devi fare un passo, prendi il tuo strumento (chiamiamolo 'S'), fanne una copia, e poi usa la copia insieme all'originale per il prossimo passo."

In termini matematici, questo si chiama duplicazione.
Il problema sorge quando proviamo a dimostrare che il robot si fermerà prima o poi (in gergo tecnico: "termina").

Per farlo, usiamo solitamente un "contatore globale". Immagina di avere un termometro che misura la "pesantezza" o la "complessità" di tutto il lavoro del robot. Se ogni volta che il robot fa un passo, il termometro scende di un grado, sappiamo che prima o poi arriverà a zero e si fermerà.

Ma qui succede la magia (o il trucco):
Quando il robot duplica lo strumento 'S', il termometro globale vede due 'S' invece di uno. Poiché due pesano più di uno, il termometro sale invece di scendere!
È come se il robot, per fare un passo avanti, dovesse sollevare due pesi invece di uno. Nessun termometro semplice (che somma le parti) può dimostrare che il robot si fermerà, perché la "copia" sembra rendere il lavoro infinito.

Gli scienziati hanno costruito un piccolo robot di prova (chiamato KO7) con solo 7 pezzi e 8 regole. Hanno dimostrato, con un computer che controlla ogni singolo passaggio (usando un linguaggio chiamato Lean 4), che nessun termometro globale semplice può mai dimostrare che questo robot si fermerà. È un muro invalicabile per certi metodi.

2. La Soluzione: La Chiave Magica (La Fuga Modulare)

Se il termometro globale fallisce, come facciamo a sapere che il robot non impazzisce?
La risposta è: non guardare tutto insieme, guarda solo la parte importante.

Immagina che il robot stia correndo una maratona.

• Il metodo globale guarda l'intera massa del runner: i vestiti, le scarpe, la borraccia, il sudore. Se il runner duplica la borraccia, il peso totale aumenta e sembra che non finisca mai.
• Il metodo modulare (la "Chiave Magica") ignora la borraccia e guarda solo il passo.

Nel nostro caso, il robot ha un contatore segreto (chiamato n). Ogni volta che fa un passo, questo contatore diminuisce (da n a n-1). La parte duplicata (lo strumento 'S') è intrappolata in una scatola che non influisce sul contatore.
Gli scienziati hanno mostrato che se usiamo un metodo chiamato Coppie di Dipendenza (Dependency Pairs), possiamo "proiettare" il nostro sguardo solo sul contatore, ignorando la copia inutile.
È come se dicessimo: "Non mi importa se hai due borracce, mi importa solo che il tuo contatore di passi scenda."

Questo metodo funziona! Il robot si ferma. Ma funziona solo perché smettiamo di guardare tutto insieme e ci concentriamo solo sulla parte che conta.

3. La Verifica: Il Certificato di Sicurezza

Per essere sicuri al 100%, gli scienziati hanno fatto due cose:

1. Hanno costruito un "Robot di Sicurezza" (SafeStep): Hanno creato una versione del robot dove le regole sono un po' più rigide (come mettere un lucchetto sulla scatola della borraccia). Su questa versione sicura, hanno dimostrato matematicamente che il robot si ferma e che tutti i percorsi portano alla stessa risposta finale (confluenza). Hanno anche creato un "pulsante di normalizzazione" certificato che risolve qualsiasi problema per questo robot.
2. Hanno chiamato un arbitro esterno (TTT2): Hanno dato il problema a un altro super-computer famoso (TTT2). Questo computer ha provato 8 strategie diverse.
   • Le 5 strategie che guardavano "tutto insieme" (metodi globali) hanno fallito: "Non so se si ferma" (risultato MAYBE).
   • Le 3 strategie che usavano la "Chiave Magica" (metodi modulari) hanno vinto: "Sì, si ferma!" (risultato YES).

In Sintesi: Cosa abbiamo imparato?

• Il Muro: Quando un sistema duplica informazioni, i metodi di prova che guardano "il tutto sommato" falliscono. È come cercare di pesare un'ombra: più la copi, più diventa grande, e non capisci mai quando finisce.
• La Fuga: La soluzione non è pesare tutto, ma isolare la parte che conta (il contatore) e ignorare il resto. È una questione di prospettiva.
• La Prova: Hanno dimostrato tutto questo con un codice matematico perfetto, controllato da computer, su un sistema minuscolo ma potente.

L'analogia finale:
Immagina di dover contare le foglie di un albero che si sta diradando.

• Se ogni volta che cade una foglia, l'albero ne fa due nuove (duplicazione), un contatore che somma tutte le foglie dirà: "Oh no, le foglie aumentano! L'albero non morirà mai!".
• Ma se guardi solo il tronco, e vedi che ogni anno il tronco si accorcia di un centimetro, sai che l'albero morirà, indipendentemente da quante foglie nuove nascono.

Questo articolo ci dice che per certi problemi complessi, dobbiamo smettere di contare le foglie e iniziare a guardare il tronco.

Sommario tecnico

Ecco un riassunto tecnico dettagliato del documento "The Global Orientation Barrier in Step-Duplicating Recursors", basato sul contenuto fornito.

Titolo: La Barriera di Orientamento Globale nei Recursori con Duplicazione di Passi: Impossibilità, Fuga Modulare e un Testimone Certificato

Autore: Moses Rahnama (Mina Analytics)
Data: Febbraio 2026
Contesto: Teoria della riscrittura dei termini, Verifica formale (Lean 4), Strumenti di terminazione (TTT2).

---

1. Il Problema: Il Conflitto tra Duplicazione e Misurazioni Globali

Il lavoro identifica una barriera fondamentale nella dimostrazione della terminazione per sistemi di riscrittura di termini di primo ordine che contengono recursori con duplicazione di passi (step-duplicating recursors).

Il problema centrale è la distinzione tra due famiglie di metodi di terminazione:

1. Misurazioni Compositive Dirette (Globali): Metodi che assegnano un unico valore di ranking a un termine aggregando i contributi dei suoi sottotermini (es. pesi additivi, interpretazioni polinomiali, ordini di percorso globali).
2. Metodi Basati su Proiezione (Modulari): Metodi come il framework delle Dependency Pairs (DP) con il criterio del sottotermino, che proiettano l'analisi su specifici argomenti, ignorando parti del termine.

Il Caso di Studio (KO7):
L'autore introduce KO7, un calcolo minimale di riscrittura (7 costruttori, 8 regole, nessun legante, nessun sharing) che include un recensore duplicante:
$$rec(b, s, \delta(n)) \to app(s, rec(b, s, n))$$
In questa regola, l'argomento "passo" $s$ appare una volta a sinistra e due volte a destra (una dentro app e una nella chiamata ricorsiva). La struttura app è un costruttore inerte (senza regole di riduzione), intrappolando la copia duplicata di $s$ in modo semanticamente inerte ma sintatticamente reale.

2. Metodologia e Strumenti

L'approccio combina una dimostrazione di impossibilità formalizzata meccanicamente con una validazione empirica esterna:

• Formalizzazione in Lean 4: Circa 7.000 righe di codice che dimostrano teoremi di impossibilità e costruiscono certificati di terminazione per un sottoinsieme sicuro del sistema.
• Validazione Esterna con TTT2/CeTA: Utilizzo dello strumento Tyrolean Termination Tool (TTT2) per verificare la terminazione del sistema completo (non protetto) e del certificato CeTA per la verifica indipendente delle prove.
• Analisi Ablativa: Rimozione della duplicazione per dimostrare che la barriera è causata specificamente da tale meccanismo e non dalla struttura del recensore in sé.

3. Risultati Chiave e Contributi

A. Teorema di Impossibilità (La Barriera)

L'autore formalizza due classi di misurazioni compositive (Definizione 1.1):

1. Livello 1 (Additivo): Pesi fissi per i costruttori, somma dei sottotermini.
2. Livello 2 (Astratto): Funzioni di combinazione arbitrarie, ma con l'assioma che app(x, y) > x e app(x, y) > y.

Teorema 9.1: È stato dimostrato (meccanicamente in Lean) che nessuna misura in queste due classi può orientare strictamente la regola duplicante $rec(b, s, \delta(n)) \to app(s, rec(b, s, n))$ per tutte le istanze di termini.

• Motivo: La duplicazione di $s$ a destra, combinata con l'assioma che app domina i suoi argomenti, forza il valore della misura a destra a essere maggiore o uguale a quello a sinistra, impedendo la diminuzione stretta richiesta per la terminazione.
• Validazione: TTT2 fallisce nel trovare prove utilizzando strategie globali (interpretazioni polinomiali, KBO, matrici), restituendo "MAYBE" (fallimento della ricerca), coerentemente con il teorema di impossibilità.

B. La Fuga Modulare (Dependency Pairs)

Il sistema è comunque terminante. La dimostrazione di terminazione avviene tramite il framework delle Dependency Pairs (DP) con il criterio del sottotermino.

• Meccanismo: Il metodo DP proietta l'analisi solo sul terzo argomento del recensore (il contatore ricorsivo $n$), ignorando l'argomento duplicato $s$ intrappolato sotto app.
• Risultato: La proiezione $\pi(rec^\sharp(b, s, \delta(n))) = \delta(n)$ e $\pi(rec^\sharp(b, s, n)) = n$ mostra una diminuzione stretta ($\delta(n) \to n$).
• Significato: Questo metodo "sfugge" alla barriera violando gli assiomi compositivi (non aggrega tutti i sottotermini, ma ne seleziona uno). TTT2 conferma la terminazione in meno di un secondo usando questo approccio.

C. Il Frammento Sicuro (SafeStep) e Certificazione Completa

Poiché la barriera blocca le prove dirette per il sistema completo, l'autore isola un sotto-relazione protetta (SafeStep) che risolve conflitti locali (es. sovrapposizioni in eqW). Per questo frammento, viene fornita una catena di certificazione completa:

1. Terminazione Forte (SN): Dimostrata tramite una misura computabile tripla-lessicografica $(\delta\text{-flag}, \kappa_M, \tau)$:
   • $\delta\text{-flag}$: Un bit di fase che scende da 1 a 0 quando il wrapper $\delta$ viene consumato.
   • $\kappa_M$: Un ordinamento multiset (Dershowitz-Manna) che gestisce le duplicazioni.
   • $\tau$: Un peso naturale per risolvere i pareggi.
2. Confluenza: Dimostrata tramite il Lemma di Newman, applicato al sistema di riduzione astratto (ARS) delle radici, con l'ipotesi di giunzione locale completamente verificata.
3. Normalizzatore Certificato: Una funzione di normalizzazione totale e corretta, costruita per ricorsione ben fondata sulla misura sopra.
4. Calibrazione Ordinale: La misura è mappata su ordinali inferiori a $\varepsilon_0$ (specificamente sotto $\omega^\omega \cdot 2$), fornendo un limite superiore rigoroso alla complessità.

4. Significato e Implicazioni

• Barriera Architettonica: Il lavoro dimostra che la difficoltà non è intrinseca alla terminazione del sistema (che è vera), ma è un limite metodologico delle misurazioni globali quando affrontano la duplicazione sintattica in contesti inerti.
• Distinzione tra "Semplice" e "Completa": Conferma che i metodi modulari (DP) possono risolvere problemi che i metodi globali (compositivi) non possono, anche su sistemi finiti e semplici come KO7.
• Rafforzamento della Teoria: Fornisce un controesempio meccanizzato preciso che delimita la potenza degli ordini di percorso compositivi rispetto ai metodi basati su proiezione.
• Validazione Pratica: L'uso combinato di Lean (per l'impossibilità e la sicurezza del frammento) e TTT2 (per la terminazione del kernel completo) offre un modello di verifica ibrido robusto.

Conclusione

Il paper stabilisce che per i recursori con duplicazione di passi in assenza di leganti e memoria esterna, nessuna misurazione compositiva globale può provare la terminazione. La soluzione risiede nella decomposizione modulare (Dependency Pairs), che proietta via la massa duplicata irrilevante. Il lavoro fornisce sia una prova di impossibilità formale che una certificazione completa di un sistema di riscrittura che, pur essendo terminante, è invisibile alle tecniche di ordinamento tradizionali.