Abstract

ACL2 is a computational logic, an automated reasoning system and an applicative programming language, a subset of COMMON LISP, based in pure λ-calculus. It was developed in the University of Texas at Austin (USA) and is based in an untyped quantifier-free first-order logic of total recursive functions with equality. This thesis presents a computational theory about Buchberger's algorithm for Gröbner bases computation in ACL2 in which: (1) Multivariate polynomial rings are formalized. This formalization is abstract: it encapsulates a coefficient ring which is used for the construction of polynomials and the verification of their properties. (2) These rings are equipped with an ordering relation induced by the terms (a lexicographical ordering on terms is defined). Its well-foundedness is proved and a polynomial embedding in ε₀-ordinals is obtained. (3) An executable and verified ACL2 implementation of polynomials with rational coefficients, which is used for the construction of Buchberger's algorithm, is developed. (4) Polynomial ideals are formalized to state the ideal membership problem. The congruence induced by an ideal is defined and its fundamental properties are proved. (5) Reduction relations over polynomials are formalized in the framework of abstract reductions. It is proved that the equivalence relation equals to the congruence induced by the ideal and that the reduction is Noetherian with respect to the underlying polynomial ordering. Algorithms for the computation of normal forms are also presented and it is proved that ideals are closed under them. (6) S-polynomials are formalized and it is proved that the reduction relation induced by a set of polynomials is locally confluent (under certain conditions) and that it is possible to decide its equivalence closure by checking the equality of normal forms. (7) A fully-executable ACL2 implementation of Buchberger's algorithm compliant with the COMMON L ISP standard is built. Its termination and partial correctness are proved and a verified decision procedure for the ideal membership problem is supplied.

Alternate abstract:

ACL2 es una lógica computacional, un sistema de razonamiento automatizado y un lenguaje de programación aplicativo, un subconjunto de COMMON LISP, basado en cálculo λ puro. Fue desarrollado en la Universidad de Texas en Austin (EE. UU.) y se basa en una lógica de primer orden de funciones recursivas totales con igualdad no tipificadas y sin cuantificadores. Esta tesis presenta una teoría computacional sobre el algoritmo de Buchberger para el cálculo de bases de Gröbner en ACL2 en el que: (1) Se formalizan anillos polinómicos multivariados. Esta formalización es abstracta: encapsula un anillo de coeficientes que se utiliza para la construcción de polinomios y la verificación de sus propiedades. (2) Estos anillos están dotados de una relación de ordenación inducida por los términos (se define un ordenamiento lexicográfico sobre los términos). Se prueba su fundamentación y se obtiene un polinomio incrustado en ε0-ordinales. (3) Se desarrolla una implementación ACL2 ejecutable y verificada de polinomios con coeficientes racionales, que se utiliza para la construcción del algoritmo de Buchberger. (4) Los ideales polinómicos se formalizan para enunciar el problema de pertenencia ideal. Se define la congruencia inducida por un ideal y se prueban sus propiedades fundamentales. (5) Las relaciones de reducción sobre polinomios se formalizan en el marco de reducciones abstractas. Se prueba que la relación de equivalencia es igual a la congruencia inducida por el ideal y que la reducción es noetheriana con respecto al ordenamiento polinomial subyacente. También se presentan algoritmos para el cálculo de formas normales y se prueba que los ideales se cierran bajo ellos. (6) Se formalizan S-polinomios y se prueba que la relación de reducción inducida por un conjunto de polinomios es localmente confluente (bajo ciertas condiciones) y que es posible decidir su clausura de equivalencia comprobando la igualdad de las formas normales. (7) Se crea una implementación ACL2 completamente ejecutable del algoritmo de Buchberger que cumple con el estándar COMMON L ISP. Se prueba su terminación y corrección parcial y se proporciona un procedimiento de decisión verificado para el problema de membresía ideal.