Anti-unification in absorptive theories

Abstract

A anti-unificação consiste em determinar uma expressão que represente a estrutura comum a duas expressões dadas, denominada generalização dessas expressões. O desenvolvimento de procedimentos de anti-unificação para o cálculo de generalizações tem adquirido importância crescente em áreas como análise de programas, detecção de clones e raciocínio simbólico. Enquanto os trabalhos iniciais se concentraram na anti-unificação sintática, aplicações modernas frequentemente exigem raciocínio módulo teorias equacionais. Esta tese dedica-se à anti-unificação em teorias absortivas, nas quais determinados símbolos de operação “absortivos” satisfazem os axiomas f(εf , x) ≈ εf and f(x, εf ) ≈ εf para uma constante “absorvente” relativa εf ; exemplos incluem multiplicação e zero, conjunção e falso, interseção e conjunto vazio. Neste trabalho são apresentadas ferramentas conceituais e um algoritmo correto para anti-unificação modulo teorias absortivas, formalizado por meio de um conjunto de regras de inferência que transformam configurações, estruturas que codificam problemas de anti-unificação e soluções parciais. São demonstradas propriedades de preservação das configurações sob a aplicação das regras de inferência, garantindo a correção do algoritmo. Uma contribuição central deste trabalho é o refinamento da análise de completude de um algoritmo apresentado na 12ª International Joint Conference on Automated Reasoning (2024). São identificadas generalizações adicionais não consideradas anteriormente, as regras de inferência são melhoradas, e demonstra-se como as soluções correspondentes podem ser calculadas a partir das configurações finais. Esta tese também aborda teorias que podem incluir símbolos funcionais absortivos, comutativos e absortivo-comutativos, que, para abreviar, chamamos de teorias absortivocomutativas. Propõe-se um novo conjunto de regras de inferência, acompanhado da prova de correção do algoritmo resultante, estendendo a aplicabilidade da abordagem a estruturas de termos mais expressivas encontradas em cenários práticos. Além disso, é tratado o caso restrito de anti-unificação para generalizações lineares, nas quais cada variável ocorre no máximo uma vez nas soluções. O algoritmo é adaptado para o caso linear absortivo e comutativo, provando-se sua correção e completude. No caso linear puramente absortivo, o algoritmo computa um conjunto mínimo e completo de generalizações.