Unifying Semantic Path Order and Weighted Path Order

Problema
Ordens Semânticas de Caminho Monotônicas (MSPOs) e Ordens de Caminho Ponderadas (WPOs) são ordens de redução estabelecidas e poderosas, utilizadas para provar a terminação de Sistemas de Reescrita de Termos (TRSs). Embora ambas sejam eficazes, historicamente foram tratadas como abordagens distintas. Trabalhos anteriores demonstraram que as WPOs são instâncias de MSPOs, mas um quadro unificado que tratasse as MSPOs como instâncias de uma WPO generalizada, preservando ao mesmo tempo as propriedades desejáveis de ambas, não havia sido plenamente articulado. Além disso, as construções existentes lutam para alcançar simultaneamente a totalidade no nível ground (crucial para a prova de teoremas) e mecanismos de comparação eficientes em diferentes contextos algébricos e baseados em precedência.

Metodologia
Os autores propõem uma unificação dessas ordens através da introdução da Ordem de Caminho Ponderada Generalizada (GWPO) e de sua variante monotônica, a Ordem de Caminho Ponderada Generalizada Monotônica (MGWPO).

1. Estrutura Fundamental: O núcleo da ordem unificada é construído sobre triplos de redução $(\geq, \succeq, \succ)$, originalmente introduzidos para MSPOs. Um triplo de redução consiste em uma pré-ordem de reescrita $\geq$, um par de ordens estável $(\succeq, \succ)$ onde $\succ$ é bem-fundamentado, e uma condição de harmonia que liga a pré-ordem e o par de ordens.
2. Definição de GWPO: A GWPO ($>_G$) é definida usando dois pares de relações, $(\succeq_A, \succ_A)$ e $(\succeq_B, \succ_B)$. Um termo $s$ é maior que $t$ se:
   • $s \succ_A t$, ou
   • $s \succeq_A t$ e condições recursivas específicas envolvendo subtermos e comparações lexicográficas se mantêm, potencialmente utilizando o segundo par $(\succeq_B, \succ_B)$ para comparação adicional.
3. Monotonicidade: Para garantir que a ordem seja fechada sob contextos (um requisito para ordens de redução), a MGWPO ($>_{MG}$) é definida como a interseção $\geq_A \cap \geq_B \cap >_G$.
4. Pares de Redução: O quadro é estendido para pares de redução $(\geq, >)$ incorporando status parciais ($\pi$). Isso permite um tratamento mais flexível dos argumentos de funções, generalizando a abordagem padrão da WPO.
5. Lógica de Unificação:
   • WPO como MGWPO: Uma WPO padrão é mostrada como uma MGWPO onde o triplo $A$ é induzido por uma álgebra fracamente simples e o triplo $B$ é induzido por uma precedência.
   • MSPO como MGWPO: Uma MSPO é mostrada como uma MGWPO onde o triplo $A$ é trivial e o triplo $B$ corresponde ao triplo de redução da MSPO. Inversamente, os autores provam que qualquer MGWPO pode ser representada como uma MSPO construindo uma combinação lexicográfica específica dos triplos subjacentes.

Principais Contribuições

• Generalização: O artigo introduz GWPOs e MGWPOs, demonstrando que tanto MSPOs quanto WPOs são instâncias específicas deste quadro generalizado.
• Totalidade no Nível Ground: Os autores identificam que, enquanto as WPOs suportam naturalmente a totalidade no nível ground (comparando quaisquer dois termos ground distintos), as MSPOs não o fazem. O quadro MGWPO permite a construção de ordens de redução totais no nível ground que podem orientar equações (por exemplo, para os combinadores S e K) que eram anteriormente difíceis de lidar com construções existentes.
• Otimização: A ordem unificada oferece uma otimização para a comparação. Se uma diminuição estrita for detectada através do primeiro componente ($\succ_A$), a comparação termina imediatamente sem verificações recursivas. Isso imita a eficiência da Ordem de Knuth-Bendix (KBO) em vez da Ordem de Caminho Lexicográfica (LPO).
• Melhoria de Complexidade: Ao impor a propriedade de subtermo na ordem estrita $\succ_A$, os autores derivam um procedimento para decidir comparações de MGWPO em tempo linear em relação ao tamanho dos termos (medido pelo número de comparações de relações base), melhorando a complexidade de tempo quadrática típica de definições semelhantes à LPO.
• Unificação de Pares de Redução: O artigo estende esses resultados para pares de redução com status parciais, provando que MGWPOs e MSPOs podem ser unificadas neste contexto também, desde que condições específicas de simplicidade sejam atendidas.

Resultados
Os autores implementaram uma ferramenta de terminação prototípica baseada no método de pares de dependência usando os pares de redução propostos. A avaliação foi conduzida em 1.528 TRSs finitos do Banco de Dados de Problemas de Terminação (TPDB) com um limite de tempo de um minuto.

• Desempenho: A configuração GWPO provou a terminação de 591 sistemas, e a configuração SPO (Ordem Semântica de Caminho) provou 595 sistemas, comparado a 486 para a WPO padrão.
• Comparação: As configurações resolveram conjuntos diferentes de problemas. A configuração SPO foi capaz de resolver problemas onde o componente algébrico não era "fracamente simples" em relação ao status parcial, uma condição exigida para a GWPO.
• Estado da Arte: Os autores notam que, embora seus métodos provem mais instâncias de terminação do que a WPO padrão, cada problema resolvido por sua ferramenta também foi resolvido pelos provadores de última geração AProVE ou NaTT. Consequentemente, os autores não afirmam ter resolvido novos problemas que anteriormente eram insolúveis, mas sim demonstraram a unificação teórica e os ganhos específicos de eficiência de sua abordagem.

Significância
O artigo reivindica significância principalmente na unificação teórica de duas classes principais de ordens de redução. Ao mostrar que as MSPOs são instâncias de GWPOs (e vice-versa), o trabalho fornece um quadro único que herda propriedades desejáveis de ambas:

1. Permite a construção de ordens totais no nível ground, uma característica crítica para métodos de prova de teoremas como o cálculo de superposição, que não estava naturalmente disponível para MSPOs.
2. Oferece um mecanismo para otimizar a comparação evitando verificações recursivas quando uma diminuição estrita é encontrada no componente algébrico primário, potencialmente levando a complexidade de tempo linear em contextos específicos.
3. Esclarece a relação entre interpretações algébricas e ordens baseadas em precedência, traçando essas conexões de volta a observações anteriores sobre a Ordem de Knuth-Bendix e as Ordens Semânticas de Caminho.

O trabalho serve como um passo fundamental, detalhado ainda mais na dissertação do primeiro autor, para fechar a lacuna entre ordens semânticas e ordens de caminho ponderadas, oferecendo um conjunto de ferramentas mais flexível e potencialmente eficiente para análise de terminação.