Ranked MSO-enumeration over compressed words

Riepilogo Tecnico: Enumerazione MSO Ordinata su Parole Compresse

Enunciato del Problema
Il documento affronta il problema di enumerare le risposte a una query Monadica del Secondo Ordine (MSO) fissa su una stringa fornita in formato compresso. Nello specifico, la stringa di input $w$ è data da un Programma a Linea Reta (SLP), ovvero una grammatica context-free che genera esattamente una stringa. L'obiettivo è calcolare tutte le tuple $(a_1, \dots, a_k)$ di posizioni in $w$ che soddisfano una formula MSO fissa $\Phi(x_1, \dots, x_k)$.

Un vincolo critico di questo lavoro è l'enumerazione ordinata (ranked enumeration). A differenza degli algoritmi di enumerazione standard dove l'ordine di output è opaco, l'enumerazione ordinata richiede che le tuple vengano stampate in un ordine specifico, definito dall'utente, che sia esso stesso definibile tramite MSO (ad esempio, l'ordine lessicografico sulle tuple di posizioni). La metrica di efficienza per tali algoritmi è il tempo di pre-elaborazione lineare (lineare rispetto alla dimensione dell'SLP, $|G|$) seguito da un ritardo costante (un limite costante sul tempo tra l'output di tuple consecutive).

Prima di questo lavoro, l'enumerazione ordinata per query MSO era nota per stringhe e alberi non compressi, ma non esistevano risultati per i dati compressi. Inoltre, i risultati di enumerazione esistenti per stringhe compresse (ad esempio [29]) ottenevano solo un ritardo lineare rispetto all'output e non supportavano l'enumerazione ordinata.

Metodologia
La soluzione combina tre componenti tecniche primarie:

1. Alberi di Fattorizzazione e Simon SLP:
   Lo strumento strutturale centrale è l'albero di fattorizzazione, un albero di parsing per una parola rispetto a un morfismo in un monoide finito, dove i nodi con $\ge 3$ figli valutano lo stesso elemento idempotente. Il teorema di Simon garantisce che tali alberi abbiano un'altezza limitata da una costante dipendente dalla dimensione del monoide.
   Il documento introduce il concetto di Simon SLP (SSLP): un SLP che è strutturalmente compatibile con un albero di fattorizzazione della parola generata. Gli autori dimostrano (Teorema 3.1) che qualsiasi SLP può essere trasformato in un SSLP equivalente in tempo lineare. Questa trasformazione prevede la costruzione di un trasduttore non deterministico che genera alberi di fattorizzazione e poi la ristrutturazione della grammatica per riflettere la gerarchia dell'albero, assicurando che la "profondità contratta dagli idempotenti" dell'SLP sia limitata da una costante ($3|M|$).

2. Traversamento in Tempo Costante in Stringhe Compresse:
   Per navigare la stringa compressa in modo efficiente, il documento utilizza ed estende le tecniche di [26] per il traversamento a due vie in tempo costante. Gli autori definiscono percorsi compressi (sequenze di triple che rappresentano movimenti destra/sinistra nel DAG dell'SLP) e mantengono una struttura dati dinamica (un albero binario $B$) che memorizza un numero costante di percorsi "attivi".
   Crucialmente, definiscono le procedure right e left che, dato un percorso nella rappresentazione compressa, calcolano il suo successore o predecessore lessicografico in tempo costante. Ciò comporta la divisione degli archi nel grafo di traversamento e la gestione di sottopercorsi "contratti dagli idempotenti" all'interno di parti specifiche dell'SLP (le parti-$e$).

3. Interpretazione MSO e Calcolo del Successore:
   L'algoritmo di enumerazione è inquadrato come il calcolo dell'immagine di una funzione poliregolare (o più generalmente, un'interpretazione MSO stringa-su-stringa). L'algoritmo calcola iterativamente il "successore" di una tupla di posizioni corrente secondo l'ordine lineare definibile in MSO.
   La prova prevede la trasformazione delle formule MSO in Automi a Stati Finiti Non Deterministici (NFA) e la derivazione di un monoide finito $M$. Precomputando gli elementi del monoide per i nodi nell'albero di fattorizzazione (o l'equivalente SSLP), l'algoritmo può determinare la posizione successiva nella sequenza di enumerazione in tempo costante. Gestisce la transizione tra le posizioni analizzando gli elementi del monoide dei segmenti tra le posizioni correnti e utilizzando la struttura dell'albero di fattorizzazione per navigare verso la posizione successiva valida senza decomprimere la stringa.

Contributi Principali e Risultati

• Teorema Principale (Teorema 5.1): Per una formula MSO fissa con $k$ variabili di primo ordine libere e un ordine lineare MSO-definibile su $k$-tuple, l'insieme delle risposte alla query su una stringa compressa tramite SLP può essere enumerato con tempo di pre-elaborazione lineare ($O(|G|)$) e ritardo costante. Questo è il primo risultato di questo tipo per l'enumerazione ordinata su dati compressi.
• Corollario per Funzioni Poliregolari (Corollario 5.3): Il risultato si generalizza alle funzioni stringa-su-stringa poliregolari. Per una funzione poliregolare fissa $f$ e un SLP $G$ che produce $w$, i simboli di $f(w)$ possono essere enumerati da sinistra a destra con pre-elaborazione lineare e ritardo costante. Questo estende un precedente risultato di Bojanczyk [8] (che assumeva input non compressi) al contesto compresso, nonostante il fatto che le funzioni poliregolari non preservino generalmente la dimensione della compressione.
• Corollario per Successor-MSO (Corollario 5.5): Il risultato è valido per la classe più ampia di interpretazioni stringa-su-stringa Successor-MSO, che sono strettamente più grandi delle funzioni poliregolari.
• Contributo Tecnico (Simon SLPs): Il documento stabilisce che ogni SLP può essere convertito in un Simon SLP in tempo lineare. Ciò rende accessibili gli alberi di fattorizzazione nel contesto della grammatica compressa, un contributo notato come di interesse indipendente.

Significato e Rivendicazioni
Il documento sostiene di aver compiuto il "primo passo" nella direzione dell'enumerazione ordinata su dati compressi. Affronta una lacuna specifica dove i precedenti algoritmi di enumerazione compressa (ad esempio [29]) non potevano controllare l'ordine di output, e i precedenti algoritmi di enumerazione ordinata (ad esempio [2, 12, 19]) non potevano gestire input compressi.

Gli autori sottolineano che il loro approccio si basa sulla struttura specifica degli alberi di fattorizzazione e sulla capacità di eseguire la navigazione in tempo costante sugli SLP. Evidenziano esplicitamente alcune limitazioni:

• I risultati attuali si applicano solo a query con variabili di primo ordine libere; la gestione di variabili di insieme libere (che richiederebbe un ritardo lineare rispetto all'output anziché costante) è un problema aperto, poiché l'approccio dell'albero di fattorizzazione non si estende attualmente alle variabili di insieme.
• Il lavoro è attualmente limitato alle stringhe; l'estensione dei risultati ai boschi (utilizzando programmi a linea retta per boschi) è identificata come lavoro futuro, in attesa della combinazione dei teoremi di fattorizzazione per boschi con le tecniche di traversamento di SLP per boschi.
• L'ordinamento è limitato agli ordini lineari definibili in MSO; la relazione tra questo modello e l'ordinamento basato su pesi (usando trasduttori di costo) rimane poco chiara.

In sintesi, il documento fornisce una base teorica per l'elaborazione efficiente di query ordinate su dati altamente compressi, dimostrando che il "gold standard" di pre-elaborazione lineare e ritardo costante è raggiungibile per le query MSO su SLP, a condizione che l'ordine di output sia MSO-definibile.