Ranked MSO-enumeration over compressed words

Resumo Técnico: Enumeração Rankeada de MSO sobre Palavras Comprimidas

Enunciado do Problema
O artigo aborda o problema de enumerar as respostas a uma consulta de Ordem Monádica de Segunda Ordem (MSO) fixa sobre uma string que é fornecida em um formato comprimido. Especificamente, a string de entrada $w$ é dada por um Programa de Linha Reta (SLP), que é uma gramática livre de contexto gerando exatamente uma string. O objetivo é computar todas as tuplas $(a_1, \dots, a_k)$ de posições em $w$ que satisfazem uma fórmula MSO fixa $\Phi(x_1, \dots, x_k)$.

Uma restrição crítica deste trabalho é a enumeração rankeada. Diferente dos algorit algoritmos de enumeração padrão onde a ordem de saída é opaca, a enumeração rankeada exige que as tuplas de saída sejam impressas em uma ordem específica, definida pelo usuário, que também é definível por MSO (por exemplo, ordem lexicográfica em tuplas de posições). A métrica de eficiência para tais algoritmos é o tempo de pré-processamento linear (linear no tamanho do SLP, $|G|$) seguido de um atraso constante (um limite constante no tempo entre a saída de tuplas consecutivas).

Antes deste trabalho, a enumeração rankeada para consultas MSO era conhecida para strings e árvores não comprimidas, mas não existiam resultados para dados comprimidos. Além disso, os resultados de enumeração existentes para strings comprimidas (por exemplo, [29]) alcançavam apenas atraso linear de saída e não suportavam a enumeração rankeada.

Metodologia
A solução combina três componentes técnicos primários:

1. Árvores de Fatoração e SLPs de Simon:
   A ferramenta estrutural central é a árvore de fatoração, uma árvore de análise para uma palavra com relação a um morfismo em um monoide finito, onde nós com $\ge 3$ filhos avaliam para o mesmo elemento idempotente. O teorema de Simon garante que tais árvores possuem altura limitada por uma constante dependente do tamanho do monoide.
   O artigo introduz o conceito de um SLP de Simon (SSLP): um SLP que é estruturalmente compatível com uma árvore de fatoração de uma palavra gerada. Os autores provam (Teorema 3.1) que qualquer SLP dado pode ser transformado em um SSLP equivalente em tempo linear. Esta transformação envolve a construção de um transdutor não-determinístico que gera árvores de fatoração e, em seguida, reestrutura a gramática para refletir a hierarquia da árvore, garantindo que a "profundidade contraída por idempotentes" do SLP seja limitada por uma constante ($3|M|$).

2. Travessia de Tempo Constante em Strings Comprimidas:
   Para navegar na string comprimida de forma eficiente, o artigo utiliza e estende técnicas de [26] para travessia de dois caminhos em tempo constante. Os autores definem caminhos comprimidos (sequências de triplas representando movimentos esquerda/direita no DAG do SLP) e mantêm uma estrutura de dados dinâmica (uma árvore binária $B$) que armazena um número constante de caminhos "ativos".
   Crucialmente, eles definem os procedimentos right e left que, dado um caminho na representação comprimida, computam seu sucessor ou predecessor lexicográfico em tempo constante. Isso envolve a divisão de arestas na árvore de travessia e o gerenciamento de subcaminhos "contraídos por idempotentes" dentro de partes específicas do SLP (as partes-$e$).

3. Interpretação MSO e Computação de Sucessor:
   O algoritmo de enumeração é enquadrado como o cálculo da imagem de uma função poliregular (ou, mais genericamente, uma interpretação MSO de string-para-string). O algoritmo computa iterativamente o "sucessor" de uma tupla atual de posições de acordo com a ordem linear definível por MSO.
   A prova envolve a transformação das fórmulas MSO em Autômatos de Estados Finitos Não-Determinísticos (NFAs) e a derivação de um monoide finito $M$. Ao pré-computar elementos do monoide para nós na árvore de fatoração (ou no SSLP equivalente), o algoritmo pode determinar a próxima posição na sequência de enumeração em tempo constante. Ele lida com a transição entre posições analisando os elementos do monoide dos segmentos entre as posições atuais e usando a estrutura da árvore de fatoração para navegar até a próxima posição válida sem descomprimir a string.

Principais Contribuições e Resultados

• Teorema Principal (Teorema 5.1): Para uma fórmula MSO fixa com $k$ variáveis de primeira ordem livres e uma ordem linear definível por MSO em $k$-tuplas, o conjunto de respostas de consulta em uma string comprimida por SLP pode ser enumerado com tempo de pré-processamento linear ($O(|G|)$) e atraso constante. Este é o primeiro resultado desta natureza para enumeração rankeada em dados comprimidos.
• Corolário para Funções Poliregulares (Corolário 5.3): O resultado generaliza-se para funções string-para-string poliregulares. Para uma função poliregular fixa $f$ e um SLP $G$ que produz $w$, os símbolos de $f(w)$ podem ser enumerados da esquerda para a direita com pré-processamento linear e atraso constante. Isto estende um resultado anterior de Bojanczyk [8] (que assumia entrada não comprimida) para o cenário comprimido, apesar do fato de que funções poliregulares não preservam, em geral, o tamanho da compressão.
• Corolário para Successor-MSO (Corolário 5.5): O resultado aplica-se à classe mais ampla de interpretações string-para-string de Successor-MSO, que são estritamente maiores que as funções poliregulares.
• Contribuição Técnica (SLPs de Simon): O artigo estabelece que todo SLP pode ser convertido em um SLP de Simon em tempo linear. Isso torna as árvores de fatoração acessíveis ao cenário de gramática comprimida, uma contribuição notada como sendo de interesse independente.

Significado e Alegações
O artigo afirma dar o "primeiro passo" na direção da enumeração rankeada em dados comprimidos. Ele aborda uma lacuna específica onde algoritmos de enumeração comprimida anteriores (por exemplo, [29]) não podiam controlar a ordem de saída, e algoritmos de enumeração rankeada anteriores (por exemplo, [2, 12, 19]) não podiam lidar com entradas comprimidas.

Os autores enfatizam que sua abordagem depende da estrutura específica das árvores de fatoração e da capacidade de realizar navegação em tempo constante em SLPs. Eles explicitamente notam limitações:

• Os resultados atuais aplicam-se apenas a consultas com variáveis de primeira ordem livres; lidar com variáveis de conjunto livres (o que exigiria atraso linear de saída em vez de atraso constante) é um problema em aberto, pois a abordagem da árvore de fatoração não se estende atualmente a variáveis de conjunto.
• O trabalho está atualmente restrito a strings; estender os resultados para florestas (usando programas de linha reta de florestas) é identificado como trabalho futuro, pendente da combinação de teoremas de fatoração de florestas com técnicas de travessia de SLP de florestas.
• O ranking é restrito a ordens lineares definíveis por MSO; a relação entre este modelo e o ranking baseado em peso (usando transdutores de custo) permanece incerta.

Em resumo, o artigo fornece uma base teórica para o processamento de consultas ordenadas e eficientes em dados altamente comprimidos, demonstrando que o "padrão ouro" de pré-processamento linear e atraso constante é alcançável para consultas MSO em SLPs, desde que a ordem de saída seja definível por MSO.