Edit Distance of Finite-Valued Transducers

Resumo Técnico: Distância de Edição de Transdutores de Valor Finito

Enunciado do Problema
O artigo aborda a computabilidade da distância de edição entre dois transdutores de estado finito. Embora a distância de edição entre transdutores funcionais (onde cada entrada mapeia para no máximo uma saída) seja conhecida por ser computável, o problema é geralmente indecidível para transdutores arbitrários. Os autores investigam se essa computabilidade se estende à classe de transdutores de valor finito, onde cada palavra de entrada mapeia para no máximo $k$ palavras de saída para uma constante fixa $k$. Esta classe é estritamente mais expressiva que os transdutores funcionais, mas retém a decidibilidade para muitos problemas fundamentais (por exemplo, inclusão e equivalência) que são indecidíveis no caso geral.

Metodologia
A solução proposta procede através de uma estratégia de redução que transforma o problema de calcular a distância entre transdutores de valor finito em uma série de subproblemas computáveis envolvendo transdutores sequenciais e um conceito métrico recém-introduzido.

1. Redução para Transdutores Multi-sequenciais:
   Os autores aproveitam o resultado conhecido de que qualquer transdutor de valor finito pode ser efetivamente decomposto em uma união finita de transdutores não ambíguos (e, portanto, funcionais). Eles constroem um autômato produto que sincroniza as execuções de todos os transdutores componentes de dois transdutores de valor finito dados, $T$ e $S$. Esta construção produz dois transdutores multi-sequenciais, $T'$ e $S'$ (uniões finitas de transdutores sequenciais/determinísticos), tais que a distância de edição $d(T, S)$ é preservada e igual a $d(T', S')$.

2. Introdução da Distância Relativa:
   Para calcular a distância entre relações multi-sequenciais (que são uniões de funções sequenciais), os autores introduzem o conceito de distância relativa. A distância relativa de uma função $f$ para uma relação $R$, denotada $\vec{d}(f, R)$, é definida como o supremo sobre todas as entradas $u$ da distância de edição mínima entre $f(u)$ e algum $v \in R(u)$.
   A distância entre duas relações multi-sequenciais $R = \bigcup f_i$ e $S = \bigcup g_j$ é mostrada ser o máximo das distâncias relativas entre cada função componente e a relação oposta:
   $$d(R, S) = \max \left( \max_i \vec{d}(f_i, S), \max_j \vec{d}(g_j, R) \right)$$

3. Decidibilidade da Distância Relativa:
   A computabilidade da distância relativa $\vec{d}(f, R)$ é estabelecida reduzindo-a a dois problemas de limitação:

   • Finitude: Decidir se $\vec{d}(f, R) < \infty$.

   • $k$-Finitude: Decidir se $\vec{d}(f, R) \leq k$ para um inteiro dado $k$.

   • Verificação de Finitude: Os autores constroem um transdutor produto $T$ representando as execuções síncronas de $f$ e dos componentes de $R$. Eles particionam o domínio de $f$ com base em quais componentes de $R$ aceitam a entrada. Para cada partição, analisam os componentes fortemente conexos (CFCs) do transdutor produto. Usando propriedades da conjugação de palavras (especificamente, que uma distância de edição infinita limitada implica conjugação das saídas dos laços), eles provam que a distância relativa é finita se e somente se, para cada caminho de CFCs no produto, existir pelo menos uma relação componente cuja saída de laço seja conjugada à saída de laço da função. Isso reduz o problema à verificação da finitude da distância entre transdutores sequenciais, o que é decidível.

   • Verificação de $k$-Finitude: Para decidir se a distância é limitada por $k$, os autores constroem um autômato finito não determinístico (AFN), $A_{C,k}$, que rastreia o orçamento de edição e os sufixos não correspondentes "sobrando" entre a saída da função e as saídas da relação. A distância relativa é $\leq k$ se e somente se a linguagem aceita por $A_{C,k}$ for idêntica ao domínio do transdutor produto.

Principais Contribuições e Resultados

• Teorema Principal: A distância de edição entre duas relações racionais de valor finito é computável para métricas na família de Levenshtein (Levenshtein, Subsequência Comum Mais Longa e Damerau-Levenshtein).
• Estrutura Algorítmica: O artigo fornece um procedimento construtivo para calcular essa distância, reduzindo o caso de valor finito ao caso multi-sequencial e, subsequentemente, à distância relativa entre uma função sequencial e uma relação multi-sequencial.
• Análise de Complexidade: Os autores observam que seu procedimento resulta em um limite superior de 3-EXPSPACE. Isso surge do espaço exponencial necessário para converter transdutores de valor finito em transdutores multi-sequenciais, seguido por requisitos de espaço exponencial e duplamente exponencial para os cálculos subsequentes de distância relativa. O limite inferior é de pelo menos PSPACE-difícil, pois subsume o problema de equivalência para autômatos não determinísticos.

Significado e Afirmações
O artigo afirma estender a decidibilidade conhecida da distância de edição além dos transdutores funcionais para a classe mais ampla de transdutores de valor finito. Isso é significativo porque os transdutores de valor finito estabelecem um equilíbrio entre poder expressivo e tratabilidade algorítmica, capturando muitos cenários práticos onde uma única entrada pode produzir um conjunto pequeno e limitado de saídas válidas (por exemplo, em processamento de linguagem natural ou síntese de programas).

Os autores enfatizam que seu trabalho fornece uma base para o raciocínio aproximado em sistemas reativos. Na verificação clássica, um sistema é verificado quanto à conformidade exata com uma especificação. O conceito de distância relativa permite raciocinar sobre sistemas que estão "próximos" de uma especificação, acomodando desvios menores. O artigo não afirma otimizar o algoritmo para eficiência, reconhecendo a alta complexidade, mas afirma que o resultado estabelece a possibilidade teórica de calcular essas distâncias em uma classe expressiva motivada pela prática de transdutores. As técnicas também são notadas como adaptáveis a outras métricas de edição, como a distância de Hamming, com modificações mínimas.