Completeness of Synthesis under Realizability Assumptions using Superposition

Resumo Técnico: Completude da Síntese sob Pressupostos de Realizabilidade usando Superposição

Declaração do Problema
O artigo aborda o problema da síntese automática de programas, especificamente a tarefa de derivar um programa livre de recursão a partir de uma especificação lógica de primeira ordem. O desafio central reside na presença de "símbolos não computáveis" dentro da especificação. Esses símbolos, que podem incluir predicados anotados pelo usuário ou funções de Skolem introduzidas durante a busca por prova, não podem aparecer no programa sintetizado final. O programa sintetizado deve ser construído exclusivamente a partir de "símbolos computáveis" (por exemplo, aritmética padrão, funções definidas pelo usuário), ao mesmo tempo que satisfaz uma especificação que pode misturar tanto símbolos computáveis quanto não computáveis.

Trabalhos anteriores de Hozzová et al. [14] introduziram um framework baseado em saturação usando o cálculo de superposição para resolver esse problema. Embora essa abordagem tenha sido provada como correta (qualquer programa derivado é correto), sua completude permaneceu uma questão em aberto. Especificamente, não estava claro se o cálculo poderia garantir encontrar uma solução caso uma existisse (pressuposto de realizabilidade). O artigo identifica cenários específicos onde o cálculo de [14] falha em derivar uma solução mesmo quando um programa computável existe, principalmente devido a limitações na forma como lida com ordenações de termos, funções de seleção e a interação entre literais computáveis e não computáveis.

Metodologia: O Cálculo SUPRA
Os autores propõem um cálculo refinado denominado SUPRA (Superposição com Pressupostos de Realizabilidade) para abordar a incompletude do framework anterior. A metodologia envolve três ajustes técnicos primários à abordagem de síntese baseada em superposição padrão:

1. Ordenações e Seleção Partitionadas:
   O artigo introduz uma ordenação de simplificação "partitionada". Nessa ordenação, qualquer termo não computável ground é estritamente maior que qualquer termo computável ground. Consequentemente, a função de seleção é restringida a sempre selecionar todos os literais máximos em uma cláusula. Isso garante que inferências envolvendo literais não computáveis (que são maiores) sejam priorizadas sobre aquelas envolvendo apenas literais computáveis. Isso impede que o cálculo fique preso em derivações onde restrições não computáveis bloqueiam a resolução de ramos computáveis.

2. Regra de Abstração (Abs):
   Para lidar com casos onde equações não computáveis contêm subtermos computáveis que precisam ser resolvidos antes que o literal não computável possa ser processado, os autores introduzem uma regra de inferência auxiliar chamada Abs. Essa regra abstrai subtermos computáveis dentro de literais não computáveis substituindo-os por variáveis frescas e adicionando restrições de desigualdade (por exemplo, transformando $s[k] \approx t$ em $s[x] \approx t \land x \neq k$). Esse mecanismo separa o raciocínio sobre símbolos não computáveis dos computáveis, permitindo que o cálculo resolva literais não computáveis sem violar a restrição de computabilidade do termo de resposta.

3. Regras de Inferência Refinadas:
   O cálculo utiliza duas variantes da regra de superposição:

   • SupC: Introduz um construtor ite (se-então-senão) no termo de resposta ao bifurcar sobre um literal de igualdade.
   • SupU: Unifica termos de resposta das premissas diretamente, evitando a adição de restrições que poderiam levar a condições não computáveis.
     O cálculo também substitui os "unificadores computáveis" usados em [14] por unificadores mais gerais padrão (MGUs), confiando na ordenação partitionada e na regra Abs para garantir que os termos de resposta resultantes permaneçam computáveis.

Contribuições Principais

• Identificação da Incompletude: O artigo demonstra, por meio de contraexemplos (por exemplo, um cenário de agendamento de workshop e um cenário de manipulação de constantes), que o cálculo em [14] não é completo sob pressupostos de realizabilidade. Ele falha em encontrar soluções quando a seleção de literais ou a ordenação de termos impede inferências necessárias sobre símbolos não computáveis.
• O Framework SUPRA: Os autores definem o cálculo SUPRA, incorporando a ordenação partitionada, a regra Abs e restrições específicas de seleção.
• Prova de Correção: O artigo prova que o SUPRA é correto com respeito à semântica das cláusulas de resposta, garantindo que qualquer programa derivado seja uma solução válida para a especificação de síntese.
• Prova de Completude: A contribuição teórica primária é a prova de que o SUPRA é completo sob o pressuposto de realizabilidade. Os autores mostram que, se um programa computável satisfazendo a especificação existir, o cálculo SUPRA (quando usado exaustivamente com a regra Abs) é garantido a derivar uma solução. A prova constrói um modelo para o conjunto saturado de cláusulas e demonstra que, se nenhuma solução fosse derivada, uma contradição surgiria em relação à satisfatibilidade da especificação negada.

Resultados e Significância
O artigo estabelece que a síntese de programas via prova de teoremas baseada em saturação pode ser tornada completa sob pressupostos de realizabilidade gerenciando cuidadosamente a interação entre símbolos computáveis e não computáveis. A significância deste trabalho reside em fechar a lacuna teórica deixada pela pesquisa anterior [14], fornecendo uma garantia formal de que o processo de síntese terá sucesso se uma solução existir dentro da assinatura computável.

Os autores observam que sua noção de realizabilidade aplica-se a programas livres de recursão; a construção de programas recursivos requer mecanismos (como indução) não cobertos pelo cálculo atual. Além disso, o resultado de completude é condicional: garante encontrar uma solução se uma existir, em vez de provar a existência de uma solução para todas as especificações. O trabalho baseia-se na lógica de primeira ordem padrão com igualdade e não afirma resolver problemas de síntese envolvendo teorias que requerem eliminação de quantificadores (como aritmética linear), a menos que essas teorias sejam tratadas pelas capacidades de raciocínio sobre teorias do provador subjacente.

Em resumo, o artigo refina o cálculo de superposição para síntese introduzindo uma ordenação partitionada e um mecanismo de abstração, provando que essas modificações são suficientes para garantir completude para a síntese de programas livres de recursão na presença de símbolos não computáveis.