Verificación formal en ACL2 del Algoritmo de Buchberger

Abstract

En este trabajo se han desarrollado los elementos necesarios para especificar, implementar y verificar la correción del algoritmo de Buchberger para el cálculo de bases de Gröbner, utilizando para ello un sistema de razonamiento automatizado (ACL2); esto incluye la formalización completa y precisa de toda la teoría matemática subyacente. Concretamente: -El desarrollo de una teoría computacional sobre los anillos de polinomios de múltiples variables. -La obtención de un orden natural a los polinomios de múltiples variables y demostración de su buena fundamentación. -La representación de los conceptos asociados a los ideales polinómicos de manera que sea posible razonar sobre ellos de manera automatizada. -El desarrollo de una teoría computacional sobre las reducciones polinómicas estableciendo su relación con las reduccines abstractas. -La representación de los conceptos asociados a las bases de Gröbner de manera que sea posible razonar sobre ellos de manera automatizada. -La implementación del algoritmo de Buchberger, especificar sus propiedades y demostrar su corrección. -La obtención de un procedimiento de decisión verificado para el problema de la pertenencia al ideal. Como se observa, nuestro énfasis se sitúa en la automatización del razonamiento. Dentro de los sistemas de razonamiento adecuados para este tipo de tareas hemos elegido a ACL2. Este sistema merece especial atención, ya que formaliza un subconjunto de COMMON LISP, un lenguaje de programación real. De hecho, LISP y sus dialectos se han usado tradicionalmente en la escritura de sistemas de Álgebra Computaciones. Por otro lado, ACL2 es especialmente bueno razonando por inducción. En este sentido, estamos ante un demostrados heurístico que incorpora no sólo potentes procedimientos de decisión, sino también estrategias sobre cómo abordar diferentes tipos de pruebas, cuándo expandir la definición de una función o generalizar un término, etc. La mayor parte de las ideas presentes en ACL2 provienen de un sistema anterior, NQTHM, también llamado el demostrador de teoremas de Boyer y Moore. ACL2 comienza a ser desarrollado en 1989 por Boyer, Moore y Kaufmann como una mejora sustancias de NQTHM, estando las últimas versiones desarrolladas fundamentalmente por los dos últimos autores. Hemos demostrado todos los teoremas (del orden de un millar) que aparecen durante la consecución de los objetivos mencionados en este sistema. Desde el punto de vista lógico, ACL2 es una lógica de primer orden con igualdad sin cuantificadores ni tipos y con funciones recursivas totales. La lógica incluye dos principios de extensión importantes, definición y encapsulado, y un principio de inducción que permite razonar sobre las funciones definidas por recursión. Como se observa, la lógica en sí es muy débil; en particular, la ausencia de cuantificadores supone una restricción importante de la lógica de primer orden. El hecho de que las funciones hayan de ser totales y la ausencia de tipos también tienen su impacto en la expresividad. Éste es el precio que hay que pagar por una mayor automatización: generalmente, nos concentramos en escribir las proposiciones y lemas intermedios que permiten al sistema demostrar un teorema complejo, proporcionándole de vez en cuando indicaciones cuando se desvía de nuestro plan preconcebido. Discutamos brevemente la importancia del algoritmo de Buchberger como justificación de su elección para nuestro trabajo. El gran desarrollo sufrido en la última década por el Álgebra Computacional ha dado como resultado la proliferación de numerosos sistemas de propósito general como MATHEMATICA. Éstos son la culminación de los resultados teóricos obtenidos en el último medio siglo, uno de cuyos descubrimientos centrales fue debido a B. Buchberger cuando en 1965 proporcionó un algoritmo para construir bases de Gröbner, que se emplean fundamentalmente para resolver el problema de la pertenencia en ideales polinómicos. h. Hironaka ya había demostrado poco antes la existencia de este tipo de bases, a las que llamó bases estándar, pero su demostración no era constructiva y no arrojaba ninguna luz sobre el problema de cómo calcularlas. El algoritmo de Buchberger, aunque al principio no tuvo demasiada difusión, causó finalmente un gran impacto en áreas muy diversas. Originalmente, se empleó para resolver problemas en Geometría Algebraica, pero ha sido aplicado con éxito en campos tan diversos como la Teoría de la Codificación, Estadística, Investigación Operativa y Teoría de Invariantes. También se ha empleado para automatizar el razonamiento en lógicas modales. Hoy día está implementado en la mayoría de los sistemas como MUPAD, MAPLE y MATHEMATICA, por citar sólo algunos. También existen unos pocos sistemas especialmente diseñados para proporcionar implementaciones particularmente eficientes del algoritmo de Buchberger como COCOA, SINGULAR, y MACAULAY. Es por esto que consideramos que disponer de implementaciones verificadas del algoritmo de Buchberger es importante. No obstante, esta tarea no resulta sencilla y lo primero que puede sorprendernos es la riqueza de estructuras algebraicas subyacentes a la propia definición del algoritmo de Buchberger y el esfuerzo que hay que dedicar a su formalización. Hay que emplear un cuerpo conmutativo de coeficientes para definir los monomios con los que construir polinomios de múltiples variables, los monomios deben poseer un orden admisible con el que inducir otro sobre los polinomios. Luego, hay que construir funciones de reducción apropiadas entre los polinomios. Para asegurar la corrección del algoritmo y proporcionar un procedimiento de decisión verificado para el problema de la pertenencia al ideal aumenta la variedad de estructuras implicadas y el esfuerzo necesario. En primer lugar, hay que definir el concepto de ideal polinómico finitamente generado y su congruencia inducida. Por otro lado, las funciones de reducción conviene estudiarlas en el marco, más general, de las relaciones de reducción abstractas. Sólo entonces, podemos obtener los resultados necesarios sobre las bases de Gröbner. Es en este esfuerzo adicional donde radica la diferencia entre programar el algoritmo y demostrar que es correcto.