Riepilogo Tecnico: Funzioni Expregular

1. Enunciato del Problema e Contesto

Il documento affronta la caratterizzazione delle funzioni da stringhe a stringhe con crescita esponenziale. Mentre la classe delle funzioni regolari (crescita lineare) e delle funzioni poliregolari (crescita polinomiale) è ben compresa, robusta e ammette molteplici caratterizzazioni equivalenti (logiche, basate sugli automi e basate sui trasduttori), il panorama per le funzioni a crescita super-polinomiale è frammentato. I modelli esistenti per la crescita esponenziale, come i sistemi HDT0L, non sono equivalenti tra loro, e non è chiaro quale, se esiste, costituisca una nozione "canonica" di calcolo a stati finiti per questo tasso di crescita.

Una specifica lacuna identificata è lo status delle interpretazioni di insiemi MSO. Queste formalizzazioni logiche estendono le trasduzioni MSO standard utilizzando variabili di insieme (variabili monadiche) per definire l'universo di output, portando naturalmente a dimensioni di output esponenziali. Tuttavia, rimaneva una questione aperta se questa classe possedesse la proprietà cruciale della riflessione della regolarità (ovvero, se l'immagine inversa di un linguaggio regolare sotto la funzione fosse regolare). Risolvere questo aspetto è significativo perché avrebbe posto fine a una congettura maggiore riguardante le strutture automatiche: specificamente, che ogni $\omega$-parola automatica abbia una teoria MSO decidibile.

2. Metodologia e Modelli

Gli autori propongono una nuova classe di funzioni denominata funzioni expregular, definite come quelle calcolabili tramite interpretazioni di insiemi MSO. Per stabilire la robustezza di questa classe, il documento introduce e analizza tre formalismi distinti:

1. Interpretazioni di insiemi MSO: Una formalizzazione logica in cui la stringa di output è definita da una formula MSO sulle posizioni della stringa di input, utilizzando variabili di insieme per generare un universo di configurazioni (che formano le posizioni di output). L'ordine e l'etichettatura dell'output sono definiti da formule MSO.
2. Macchine Yield-Hennie: Un'estensione ramificata delle macchine di Hennie (macchine di Turing a nastro singolo con la proprietà di visite limitate). Queste macchine possono generare sottoprocessi paralleli. L'output è la concatenazione delle lettere prodotte dalle foglie dell'albero di calcolo (il "yield"). Sono vincolate da una condizione di visite limitate su ogni ramo.
3. Trasduttori Ariadne: Un modello sequenziale che estende i trasduttori con sassolini (pebble transducers). Utilizzano uno stack per registrare la storia di un calcolo a visite limitate. Crucialmente, possono accedere all'intero sotto-stack corrispondente alla storia della posizione corrente dell'input. Supportano le operazioni "push" (estendere il calcolo) e "pop" (ripristinare con un aggiornamento inflazionistico per evitare cicli).

3. Contributi e Risultati Chiave

A. Equivalenza dei Modelli

Il contributo tecnico principale è la prova dell'equivalenza tra questi tre modelli:

• Interpretazioni di insiemi MSO $\to$ Macchine Yield-Hennie: Questa è la traduzione più complessa. Gli autori introducono il concetto di semplicità di un intervallo di configurazioni in un "split" (un taglio nella stringa di input). Dimostrano che la semplicità è limitata per qualsiasi interpretazione di insiemi MSO. Per gestire la codifica degli intervalli durante l'esecuzione della macchina, introducono basi di intervalli definibili e imbuto (sequenze di intervalli e split). Ciò permette alla macchina di aggiornare localmente il proprio stato (una colorazione dell'input) mentre attraversa l'input, mantenendo le informazioni necessarie per generare i fattori di output corretti.
• Macchine Yield-Hennie $\to$ Trasduttori Ariadne: Questa traduzione è relativamente diretta. Il trasduttore Ariadne simula la traversata dell'albero dell'esecuzione della macchina Yield-Hennie. Scendere nell'albero corrisponde a fare push sullo stack, mentre salire corrisponde a fare pop.
• Trasduttori Ariadne $\to$ Interpretazioni di insiemi MSO: Questa direzione si basa sulla dimostrazione che il linguaggio delle configurazioni raggiungibili (stack) per un trasduttore Ariadne è regolare. Gli autori lo ottengono traducendo gli automi Ariadne in automi Hennie alternanti. Poiché è noto che gli automi Hennie alternanti riconoscono linguaggi regolari (un risultato di Dartois, Nguyen e Peyrat), le configurazioni dello stack formano un linguaggio regolare, che può quindi essere definito da una formula MSO.

B. Riflessione della Regolarità e Decidibilità

L'equivalenza stabilisce che le interpretazioni di insiemi MSO riflettono la regolarità. Ciò significa che per qualsiasi funzione expregular $f$ e qualsiasi linguaggio regolare $L$, l'immagine inversa $f^{-1}(L)$ è regolare.

• Significato: Questo risultato conferma che le funzioni expregular formano una classe robusta analoga alle funzioni poliregolari, ma per la crescita esponenziale.
• Corollario: Come diretta conseguenza, il documento risolve una congettura di Bárány (e successivamente di Filiot et al.) affermando che ogni $\omega$-parola automatica ha una teoria MSO decidibile. Questo perché le $\omega$-parole automatiche possono essere viste come output di interpretazioni di insiemi MSO su input unari, e la riflessione della regolarità garantisce la decidibilità delle loro teorie.

C. Proprietà di Chiusura

Il documento dimostra che la classe delle funzioni expregular è:

• Chiusa sotto precomposizione da funzioni regolari.
• Chiusa sotto postcomposizione da funzioni poliregolari.
• Non chiusa sotto precomposizione da funzioni poliregolari (viene fornito un controesempio in cui la composizione risulta in una crescita super-esponenziale, superando il limite $2^{O(n)}$ delle funzioni expregular).

4. Significato e Affermazioni

Il documento afferma che le funzioni expregular costituiscono la nozione naturale e robusta di "calcolo a stati finiti esponenziale" per le funzioni da stringhe a stringhe. Questa affermazione è supportata da:

1. Multiple Caratterizzazioni: L'esistenza di tre modelli distinti ed equivalenti (logico, macchina ramificata e macchina sequenziale a stack).
2. Riflessione della Regolarità: La classe soddisfa il requisito standard di robustezza nella teoria dei trasduttori.
3. Decidibilità: La risoluzione della decidibilità delle teorie MSO per le $\omega$-parole automatiche.

Gli autori notano che, sebbene la strumentazione sviluppata (split, imbuto, basi definibili) si estenda probabilmente agli scenari da alberi a stringhe, una generalizzazione ai contesti da alberi ad alberi richiederebbe nuove intuizioni. Evidenziano inoltre che la concisione degli automi Ariadne e degli automi Hennie alternanti (complessità Tower rispetto agli automi a stati finiti) suggerisce che questi modelli sono più concisi delle formule MSO, sebbene una trasformazione elementare tra essi rimanga una questione aperta.

In sintesi, il lavoro fornisce un quadro fondazionale per la comprensione delle funzioni da stringhe a stringhe con crescita esponenziale, colmando il divario tra definizioni logiche e modelli di macchine, e risolvendo problemi aperti di lunga data nella teoria delle strutture automatiche.