💻 computer science

Anti-Unification Completeness Analysis in PVS

Este artigo estabelece formalmente a completude de um algoritmo de anti-unificação sintática baseado em regras dentro do Prototype Verification System (PVS), destacando as principais diferenças entre as formalizações de anti-unificação e unificação.

Autores originais: Mauricio Ayala-Rincón (Universidade Federal de Goiás), Thaynara Arielly de Lima (Universidade Federal de Goiás), Maria Júlia Dias Lima (Universidade de Brasília), Temur Kutsia (RISC/Johannes Kepler Un

Publicado 2026-07-15

📖 6 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Mauricio Ayala-Rincón (Universidade Federal de Goiás), Thaynara Arielly de Lima (Universidade Federal de Goiás), Maria Júlia Dias Lima (Universidade de Brasília), Temur Kutsia (RISC/Johannes Kepler Universität), Marcos Mercandeli-Rodrigues (Universidade de Brasília)

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você tem dois castelos de Lego muito diferentes. Um é uma torre minúscula e simples, e o outro é uma fortaleza enorme e complexa com passagens secretas. Agora, imagine que você quer construir um "projeto mestre" que capture a essência de ambos os castelos. Você quer encontrar as partes que eles compartilham (como "tem uma porta" ou "tem um telhado") e transformar as partes únicas e confusas em espaços reservados genéricos (como "um bloco de alguma cor"). Esse processo de encontrar o terreno comum enquanto esconde as diferenças é chamado de anti-unificação.

Por décadas, cientistas da computação usaram esse truque para corrigir bugs, encontrar códigos copiados e até mesmo transformar softwares lentos em softwares paralelos rápidos. Mas havia um porém: tínhamos uma receita (um algoritmo) para construir esses projetos, mas não tínhmos uma garantia matematicamente sólida de que a receita sempre funcionaria perfeitamente para qualquer par de castelos. Sabíamos que ela não travava (era "sound" ou correta), mas não tínhamos provado que ela encontrava o melhor projeto possível sempre (era "complete" ou completa).

Este artigo é a história de uma equipe de pesquisadores que finalmente construiu essa garantia ausente usando um verificador de provas digital chamado PVS.

O Quebra-Cabeça das Peças "Resolvidas"

Para entender por que isso foi tão difícil, você precisa olhar para como o algoritmo funciona. Ele decompõe os dois castelos peça por peça.

A Parte Fácil: Se ele vê dois tijolos idênticos, ele diz: "Entendido!" e segue em frente.
A Parte Complicada: Se ele vê dois tijolos diferentes (digamos, um vermelho e um azul), ele não desiste como faria em um jogo de correspondência normal. Em vez disso, ele diz: "Ah, estes são diferentes! Vou lembrar desta diferença e continuar procurando por outras incompatibilidades vermelho-versus-azul em outro lugar."

Em um jogo de correspondência normal (chamado "unificação"), encontrar uma diferença significa que você perde imediatamente. Mas na anti-unificação, encontrar uma diferença é, na verdade, o objetivo. O algoritmo tem que manter um diário de registro de cada diferença que encontra.

Os pesquisadores descobriram que provar que o algoritmo funciona para as partes "fáceis" foi surpreendentemente difícil. Na verdade, quando olharam para o trabalho anterior, 91,10% do esforço gasto para provar que o algoritmo era correto foi dedicado a apenas dois casos específicos: lidar com problemas "resolvidos" (onde o algoritmo detecta uma diferença) e problemas "sintáticos" (onde as peças são idênticas). Parece simples, mas provar que o algoritmo registra corretamente essas diferenças sem se confundir exigiu uma quantidade massiva de verificação rigorosa.

O "Livro de História" do Algoritmo

O principal avanço neste artigo é perceber que, para provar que o algoritmo encontra o melhor projeto, você não pode olhar apenas para o passo atual. Você tem que olhar para todo o histórico da computação.

Os autores introduziram uma nova forma de pensar sobre a "memória" do algoritmo. Eles definiram um "Generalizador Total" — um termo sofisticado para um projeto mestre que contabiliza:

As peças que ainda estão esperando para serem verificadas.
As peças que já foram verificadas e marcadas como "diferentes".
A "substituição" (a lista de regras) que o algoritmo está construindo conforme avança.

Eles provaram várias "propriedades de invariância". Pense nelas como regras que dizem: "Não importa quantos passos o algoritmo dê, a lista total de diferenças que ele encontrou até agora nunca desaparece ou muda seu significado". Eles mostraram que, mesmo quando o algoritmo divide um problema grande em subproblemas minúsculos, a "história" do problema original permanece intacta, tal como um quebra-cabeça que mantém a mesma imagem mesmo quando você o divide em peças menores e as embaralha.

O Projeto "Restrito"

Aqui está a reviravolta inteligente. Para fazer a prova funcionar, os autores tiveram que inventar um tipo especial de projeto chamado "Generalizador Total Restrito".

Imagine que você está tentando escrever uma receita. Se você usar ingredientes que já estão na cozinha (variáveis que o algoritmo está usando no momento), você pode acidentalmente mudar a receita enquanto a escreve. Então, os autores disseram: "Vamos usar apenas ingredientes novos e não utilizados para nossa prova". Eles provaram que, se você conseguir encontrar um projeto usando esses ingredientes "novos", você sempre poderá traduzi-lo de volta para um projeto normal.

Ao restringir o projeto a esses ingredientes "novos", eles foram capazes de provar o Teorema 20: O resultado final do algoritmo é sempre pelo menos tão específico quanto qualquer outro projeto que você pudesse criar. Em outras palavras, o algoritmo nunca perde uma solução melhor.

O Que Isso Significa (e o Que Não Significa)

O artigo prova (não apenas sugere) que o algoritmo baseado em regras para anti-unificação sintática é completo. Isso significa que é matematicamente garantido que ele encontrará o generalizador menos geral (o projeto comum mais preciso) para quaisquer dois termos.

No entanto, o artigo é muito cuidadoso sobre o que ele ainda não faz:

Ele não fornece o código final verificado por máquina que você possa executar agora mesmo. Os autores afirmam que a formalização das novas definições e lemas é um "trabalho em progresso".
Ele não afirma ter resolvido a anti-unificação para todos os tipos de matemática (como aqueles envolvendo comutatividade ou associatividade). Ele foca estritamente na anti-unificação "sintática" (o tipo padrão).
Ele não afirma que o algoritmo é rápido ou eficiente em termos de velocidade; ele apenas prova que a lógica está correta e é completa.

O Conclusão

Este artigo é uma dissecação rigorosa, passo a passo, de um algoritmo de computador. Os autores não disseram apenas "funciona". Eles construíram uma fortaleza digital de lógica, verificando cada passo, especialmente as partes entediantes, mas críticas, onde o algoritmo detecta diferenças. Eles mostraram que, ao manter um "livro de história" perfeito da computação e usar uma forma inteligente e "restrita" de pensar sobre soluções, eles podem garantir que o algoritmo sempre encontrará a resposta certa.

Agora que a matemática está provada, a porta está aberta para o próximo passo: extrair "código executável certificado". Isso significa que, no futuro, poderemos pegar este algoritmo e transformá-lo em um software que é garantido pela matemática a nunca cometer erros ao encontrar padrões comuns em códigos ou compostos químicos. Mas, por enquanto, a vitória está na própria prova: o mistério de por que funciona foi finalmente resolvido.

Resumo Técnico: Análise de Completude de Anti-Unificação em PVS

Enunciado do Problema
Este artigo aborda a verificação formal da completude de um algoritmo baseado em regras para anti-unificação sintática dentro do Prototype Verification System (PVS). Enquanto o trabalho anterior dos autores [9] formalizou e verificou mecanicamente com sucesso a terminação e a correção (soundness) deste algoritmo, a prova de completude permaneceu incompleta. O artigo destaca uma disparidade significativa entre a formalização da unificação e da anti-unificação: na unificação, problemas "resolvidos" (termos com símbolos de cabeça diferentes) resultam em falha, e problemas sintaticamente iguais são resolvidos trivialmente. Em contraste, a anti-unificação nunca falha; problemas "resolvidos" indicam diferenças estruturais que devem ser registradas, e problemas sintaticamente iguais exigem que o algoritmo detecte e registre regularidades (repetições) em vez de terminar imediatamente. Os autores observam que mais de 90% do esforço na verificação de correção anterior foi dedicado a esses casos específicos (problemas resolvidos e regras sintáticas), sugerindo que um nível de rigor semelhante, se não maior, é necessário para a completude.

Metodologia
Os autores empregam uma abordagem construtiva e indutiva para provar a completude, evitando argumentos não construtivos baseados no tipo unitário da anti-unificação sintática. A metodologia baseia-se na formalização existente do algoritmo em PVS, que opera sobre configurações válidas consistindo de problemas não resolvidos ( $C_{Uns}$ ), problemas resolvidos ( $C_{Sol}$ ) e uma substituição computada ( $C_{Sub}$ ).

Para preencher a lacuna entre correção e completude, o artigo introduz diversas novas construções teóricas e propriedades de preservação:

Novos Invariantes: Os autores definem "variáveis protegidas" e "substituições laterais" para rastrear o histórico da computação. Crucialmente, eles estabelecem o Lema de Invariância do Problema (Lema 7), que prova que o problema de anti-unificação original é preservado ao longo da derivação através da composição de substituições computadas e laterais.
Conjuntos Estendidos e Totais de AUTs: Para lidar com a reconstrução do problema original a partir de suas partes decompostas, os autores definem o "conjunto estendido de AUTs" ( $C_{Ext}$ ) e o "conjunto total de AUTs" ( $C_{Tot}$ ). Eles provam que esses conjuntos são preservados ou expandidos monotonicamente durante a derivação.
Generalizadores Totais Restritos: Uma contribuição central é a introdução de um "generalizador total restrito" (Definição 19). Esta noção restringe o alcance do generalizador para evitar variáveis usadas pelo algoritmo (rótulos e variáveis protegidas). Os autores provam que, se um generalizador existe, um generalizador restrito existe e é equivalente nos rótulos relevantes. Esta restrição é essencial para o passo indutivo, permitindo a construção de um generalizador para o próximo estado de configuração sem conflitar com as variáveis internas do algoritmo.

A prova procede por indução no número de passos de redução de uma configuração inicial para uma configuração final. Os autores analisam as regras de inferência (Decompose-Function, Decompose-Pair, Solve-Repeated, Solve-Non-Repeated e Syntactic) separadamente, demonstrando como o generalizador restrito pode ser construído ou preservado em cada etapa.

Principais Contribuições

Prova de Completude Formal: O artigo fornece a primeira prova construtiva e mecanicamente verificável de completude para o algoritmo padrão de anti-unificação sintática em PVS.
Noções de Generalizador Refinadas: Os autores introduzem os conceitos de "generalizadores totais" e "generalizadores totais restritos", que são necessários para lidar com a complexidade de rastrear o histórico do problema e as interações de variáveis na anti-unificação, uma complexidade ausente em provas de unificação padrão.
Propriedades de Preservação: O artigo estabelece um conjunto de lemas (Preservação de Rótulos, Invariância de Variáveis Protegidas, Invariância do Problema, Preservação de Classificação) que descrevem rigorosamente como o estado da computação evolui enquanto mantém a integridade do problema original.
Diferenciação da Unificação: O trabalho detalha explicitamente por que a formalização da anti-unificação é mais complexa que a da unificação, especificamente no que diz respeito ao tratamento de subproblemas resolvidos e sintáticos, onde o algoritmo deve registrar diferenças em vez de falhar ou terminar trivialmente.

Resultados
O resultado primário é o Teorema 20 (Completude Forte para Generalizadores Totais Restritos), que afirma que, para qualquer configuração válida alcançável a partir de um estado inicial, qualquer generalizador total restrito é mais geral que a substituição computada da configuração final. Disso, deriva-se o Corolário 21 (Completude Forte), estabelecendo que o algoritmo é completo em relação a quaisquer generalizadores totais. Isso confirma que o algoritmo computa o generalizador menos geral (até renomeação) para qualquer par de termos.

Significância
O artigo afirma que completar o certificado formal para este algoritmo é de "extrema importância" porque permite a extração de código executável certificado para um algoritmo de anti-unificação correto e completo. Isso aborda uma lacuna no campo onde as aplicações práticas de anti-unificação (como detecção de clones de código, paralelização e reparo de software) superaram o desenvolvimento de certificados mecanicamente verificados em assistentes de prova. Ao fornecer uma base rigorosa para a completude, o trabalho equilibra o desenvolvimento teórico com a aplicação prática, oferecendo uma base verificada para extensões futuras de anti-unificação módulo propriedades algébricas (ex: associatividade, comutatividade). Os autores enfatizam que a complexidade desta mecanização reside no registro preciso do histórico de decomposição e na preservação de invariantes, o que a distingue de formalizações de unificação mais simples.

O Quebra-Cabeça das Peças "Resolvidas"

O "Livro de História" do Algoritmo

O Projeto "Restrito"

O Que Isso Significa (e o Que Não Significa)

O Conclusão

Mais como este