Non-Termination of Logic Programs Using Patterns

Resumo Técnico: Não-Terminação de Programas de Lógica Usando Padrões

Enunciado do Problema
Este artigo aborda a detecção automática de não-terminação em programas de lógica (LPs). Enquanto grande parte da pesquisa existente foca na detecção de loops (sequências de reescrita finitas que podem ser repetidas indefinidamente), este trabalho visa a não-terminação sem loop. Estas são sequências de reescrita infinitas que não incorporam nenhum loop, tornando-as inerentemente não periódicas e difíceis de detectar. O autor observa que tais sequências podem surgir de programas de lógica simples, embora os métodos padrão de detecção de loops frequentemente falhem em identificá-las. A motivação é dupla: teórica (estudar formas notáveis de sequências infinitas) e prática (ajudar programadores a identificar consultas que executam para sempre).

Metodologia
O autor adapta uma abordagem originalmente introduzida para reescrita de termos por Emmes et al. (2012) para o domínio da programação lógica. A metodologia central envolve a definição de uma nova técnica de desdobramento (unfolding) que gera "padrões" descrevendo conjuntos potencialmente infinitos de sequências de reescrita finitas.

1. Definições de Padrões:

   • Substituições de Padrão: Definidas como pares $\theta = (\sigma, \mu)$, denotadas por $\sigma \star \mu$, descrevendo um conjunto de substituições $\{\theta(n) = \sigma^n\mu \mid n \in \mathbb{N}\}$.
   • Termos de Padrão: Pares $(s, \theta)$ descrevendo o conjunto $\{s\theta(n) \mid n \in \mathbb{N}\}$.
   • Regras de Padrão: Pares de termos de padrão $(p, q)$ descrevendo um conjunto de regras binárias $\{(p(n), q(n)) \mid n \in \mathbb{N}\}$.

2. Corretude e Desdobramento:

   • Uma regra de padrão é considerada correta em relação a um programa $P$ se o conjunto de regras que ela descreve for um subconjunto do desdobramento binário de $P$ ($binunf(P)$).
   • O autor introduz um novo operador de desdobramento $T^\pi_{P,B}$ que computa regras de padrão a partir de um programa $P$ e um conjunto base de regras de padrão corretas $B$. Este operador utiliza um algoritmo de unificação para termos de padrão para combinar regras, efetivamente "desdobrando" o programa mais rapidamente do que o desdobramento binário tradicional ao capturar subconjuntos infinitos de $binunf(P)$ em representações finitas.

3. Padrões Simples e Unificação:

   • Para tornar a abordagem automatizável, o autor restringe o domínio aos termos de padrão simples, onde as substituições seguem uma estrutura específica envolvendo contextos unários.
   • Um algoritmo de unificação é fornecido para estes termos simples. Ele mapeia termos de padrão simples para termos sobre uma assinatura especializada $\Upsilon$ (usando símbolos unários $c_{a,b}$ para representar incrustações repetidas) e aplica algoritmos de unificação clássicos (por exemplo, Robinson, Martelli-Montanari).
   • O algoritmo é provado parcialmente correto: se terminar com sucesso, produz um unificador mais geral (mgu) para as sequências de padrões de entrada.

4. Critérios de Não-Terminação:

   • Critério Geral (Teorema 3): Adaptado de Emmes et al., este afirma que, se o desdobramento de padrão contiver uma regra da forma $(u \star \sigma \star \mu, u\sigma^a \star \sigma^b\sigma' \star \mu\mu')$ onde $\sigma'$ comuta com $\sigma$ e $\mu$, então existe uma cadeia infinita.
   • Critério Especial (Teorema 5): Uma condição mais facilmente verificável para regras de padrão especiais (um subconjunto de regras simples). Se tal regra existir no desdobramento, o artigo prova a existência de uma cadeia infinita partindo de instâncias específicas do lado esquerdo da regra.

Principais Contribuições
O artigo apresenta quatro contribuições primárias:

1. Nova Técnica de Desdobramento: Um método para produzir regras de padrão corretas para programação lógica, oferecendo uma apresentação mais compacta do que as nove regras de inferência usadas em reescrita de termos e eliminando a necessidade de estratégias de aplicação complexas.
2. Termos de Padrão Simples e Unificação: A definição de uma forma restrita de termos de padrão ("simples") e um algoritmo de unificação correspondente provado como correto.
3. Condição Suficiente Automatizável: Uma condição facilmente verificável (Teorema 5) para detectar não-terminação sem loop de regras de padrão simples.
4. Implementação (NTI): A implementação desta abordagem em uma ferramenta chamada NTI.

Resultados Experimentais
O autor avaliou o NTI em 41 programas de lógica derivados de Sistemas de Reescrita de Termos (TRSs) não-terminantes sem loop da Base de Dados de Problemas de Terminação (TPDB).

• Sucesso: A ferramenta provou com sucesso a não-terminação para 36 dos 41 programas. Notavelmente, teve sucesso em 4 programas (marcados com † nas tabelas) que não haviam sido provados como não-terminantes por nenhum outro analisador de TRS na Competição Internacional de Terminação até 2024.
• Falha: A abordagem falhou em 5 programas, principalmente devido à incompletude do algoritmo de unificação ao usar a "escolha natural" para representantes de termos (conforme discutido no Exemplo 12) ou pela restrição a padrões simples (Exemplo 9).
• Desempenho: Os tempos de execução foram geralmente baixos (abaixo de 300ms para casos de sucesso), embora alguns casos complexos tenham resultado em timeouts.

Significância e Alegações
O autor afirma que sua abordagem é a única ferramenta participante da Competição Internacional de Terminação capaz de refutar a terminação de programas de lógica. Ele observa que, embora exista outra abordagem de Payet (2024) para provar a não-terminação sem loop, esta aborda uma classe diferente de "sem loop" e é incapaz de refutar a terminação dos programas específicos testados neste artigo (Tabelas 1 e 2). Inversamente, a abordagem de Payet (2024) pode refutar a terminação de programas onde este método falha. Assim, as duas abordagens são apresentadas como complementares.

O artigo conclui modestamente, reconhecendo que o algoritmo de unificação é atualmente incompleto e que a restrição a padrões simples limita o escopo (por exemplo, falhando em programas que requerem 1-contextos com variáveis). Trabalhos futuros estão planejados para abordar a completude, estender o desdobramento inicial (Prop. 2) e adaptar a abordagem para TRSs para comparação direta com Emmes et al. (2012).