Completeness of Synthesis under Realizability Assumptions using Superposition

Resumen Técnico: Completitud de la Síntesis bajo Supuestos de Realizabilidad usando Superposición

Enunciado del Problema
El artículo aborda el problema de la síntesis automática de programas, específicamente la tarea de derivar un programa libre de recursión a partir de una especificación lógica de primer orden. El desafío central radica en la presencia de "símbolos no computables" dentro de la especificación. Estos símbolos, que pueden incluir predicados anotados por el usuario o funciones de Skolem introducidas durante la búsqueda de pruebas, no pueden aparecer en el programa sintetizado final. El programa sintetizado debe construirse únicamente a partir de "símbolos computables" (por ejemplo, aritmética estándar, funciones definidas por el usuario) mientras satisface una especificación que puede mezclar tanto símbolos computables como no computables.

Trabajos anteriores de Hozzová et al. [14] introdujeron un marco basado en saturación utilizando el cálculo de superposición para resolver este problema. Aunque ese enfoque fue demostrado como correcto (cualquier programa derivado es correcto), su completitud permaneció como una pregunta abierta. Específicamente, no estaba claro si el cálculo podía garantizar encontrar una solución si existiera (supuesto de realizabilidad). El artículo identifica escenarios específicos donde el cálculo de [14] falla en derivar una solución incluso cuando existe un programa computable, principalmente debido a limitaciones en cómo maneja los ordenamientos de términos, las funciones de selección y la interacción entre literales computables y no computables.

Metodología: El Cálculo SUPRA
Los autores proponen un cálculo refinado denominado SUPRA (Superposición con Supuestos de Realizabilidad) para abordar la incompletitud del marco anterior. La metodología implica tres ajustes técnicos principales al enfoque de síntesis basado en superposición estándar:

1. Ordenamientos y Selección Particionados:
   El artículo introduce un ordenamiento de simplificación "particionado". En este ordenamiento, cualquier término no computable ground es estrictamente mayor que cualquier término computable ground. En consecuencia, la función de selección está restringida a seleccionar siempre todos los literales máximos en una cláusula. Esto asegura que las inferencias que involucran literales no computables (que son mayores) tengan prioridad sobre aquellas que involucran solo literales computables. Esto evita que el cálculo se quede atascado en derivaciones donde las restricciones no computables bloquean la resolución de ramas computables.

2. Regla de Abstracción (Abs):
   Para manejar casos donde ecuaciones no computables contienen subtérminos computables que necesitan resolverse antes de que el literal no computable pueda procesarse, los autores introducen una regla de inferencia auxiliar llamada Abs. Esta regla abstrae subtérminos computables dentro de literales no computables reemplazándolos con variables frescas y añadiendo restricciones de disigualdad (por ejemplo, transformando $s[k] \approx t$ en $s[x] \approx t \land x \neq k$). Este mecanismo separa el razonamiento sobre símbolos no computables de los computables, permitiendo que el cálculo resuelva literales no computables sin violar la restricción de computabilidad del término de respuesta.

3. Reglas de Inferencia Refinadas:
   El cálculo utiliza dos variantes de la regla de superposición:

   • SupC: Introduce un constructor ite (si-entonces-si-no) en el término de respuesta al ramificar sobre un literal de igualdad.
   • SupU: Unifica términos de respuesta de las premisas directamente, evitando la adición de restricciones que podrían conducir a condiciones no computables.
     El cálculo también reemplaza los "unificadores computables" utilizados en [14] con unificadores generales más generales (MGU) estándar, confiando en el ordenamiento particionado y la regla Abs para asegurar que los términos de respuesta resultantes permanezcan computables.

Contribuciones Clave

• Identificación de la Incompletitud: El artículo demuestra mediante contraejemplos (por ejemplo, un escenario de programación de talleres y un escenario de manipulación de constantes) que el cálculo en [14] no es completo bajo supuestos de realizabilidad. Falla en encontrar soluciones cuando la selección de literales o el ordenamiento de términos impide inferencias necesarias sobre símbolos no computables.
• El Marco SUPRA: Los autores definen el cálculo SUPRA, incorporando el ordenamiento particionado, la regla Abs y restricciones de selección específicas.
• Prueba de Corrección: El artículo demuestra que SUPRA es correcto con respecto a la semántica de las cláusulas de respuesta, asegurando que cualquier programa derivado sea una solución válida para la especificación de síntesis.
• Prueba de Completitud: La contribución teórica principal es la prueba de que SUPRA es completo bajo el supuesto de realizabilidad. Los autores muestran que si existe un programa computable que satisface la especificación, el cálculo SUPRA (cuando se usa exhaustivamente con la regla Abs) garantiza derivar una solución. La prueba construye un modelo para el conjunto saturado de cláusulas y demuestra que si no se derivara ninguna solución, surgiría una contradicción con respecto a la satisfacibilidad de la especificación negada.

Resultados y Significado
El artículo establece que la síntesis de programas mediante demostración de teoremas basada en saturación puede hacerse completa bajo supuestos de realizabilidad gestionando cuidadosamente la interacción entre símbolos computables y no computables. El significado de este trabajo radica en cerrar la brecha teórica dejada por investigaciones anteriores [14], proporcionando una garantía formal de que el proceso de síntesis tendrá éxito si existe una solución dentro de la firma computable.

Los autores señalan que su noción de realizabilidad se aplica a programas libres de recursión; la construcción de programas recursivos requiere mecanismos (como la inducción) no cubiertos por el cálculo actual. Además, el resultado de completitud es condicional: garantiza encontrar una solución si existe una, en lugar de probar la existencia de una solución para todas las especificaciones. El trabajo se basa en la lógica de primer orden estándar con igualdad y no afirma resolver problemas de síntesis que involucran teorías que requieren eliminación de cuantificadores (como la aritmética lineal) a menos que esas teorías sean manejadas por las capacidades de razonamiento sobre teorías del demostrador subyacente.

En resumen, el artículo refina el cálculo de superposición para la síntesis introduciendo un ordenamiento particionado y un mecanismo de abstracción, demostrando que estas modificaciones son suficientes para garantizar la completitud de la síntesis de programas libres de recursión en presencia de símbolos no computables.