PDF de programación - Una teoría computacional acerca de la lógica ecuacional

Universidad de Sevilla

Departamento de Ciencias de la Computación

e Inteligencia Artificial

Una teoría computacional

acerca de la lógica ecuacional

Formalización en ACL2 de la lógica ecuacional
y demostración automática de sus propiedades

Memoria presentada por
José Luis Ruiz Reina
para optar al grado de
Doctor en Matemáticas
por la Universidad de Sevilla

V. B. Director

José Luis Ruiz Reina

D. José Antonio Alonso Jiménez

Sevilla, Junio de 2001

A mis padres, Carmen y José,

y a Inma

Agradecimientos

El trabajo presentado en esta memoria está parcialmente financiado por los proyectos
PB96-0098-C04-04 del Ministerio de Educación y Cultura y TIC2000-1368-C03-02 del
Ministerio de Ciencia y Tecnología.

En primer lugar, quiero expresar mi agradecimiento a José Antonio Alonso Jiménez,
por su dirección y apoyo durante la realización de este trabajo y por haberme hecho
descubrir el mundo del razonamiento automático.

A mis colegas del Departamento de Ciencias de la Computación e Inteligencia Artificial
de la Universidad de Sevilla, que hacen posible el trabajo diario en un entorno de amistad.
En particular, me gustaría mencionar a Miguel Ángel Gutiérrez, Carmen Graciani y Mario
Pérez. Y muy especialmente a Francisco Martín Mateos: su colaboración ha sido muy
importante para el desarrollo de algunas partes de este trabajo.

Al Grupo de Lógica Computacional de la Universidad de Sevilla. Creo que formamos
un grupo de trabajo con muchas posibilidades, tanto en el presente como en el futuro. Las
fructíferas discusiones durante los seminarios han influido positivamente en este trabajo.
A J Moore, Matt Kaufmann y Robert Boyer, creadores del sistema ACL2, sin los
cuales, evidentemente, este trabajo no hubiera sido posible. Agradezco enormemente su
magnífica disposición para responder en todo momento cualquier cuestión relacionada con
ACL2. Hago extensivo este agradecimiento a todos los miembros de la lista de correo de
ACL2.

A mi familia, por su apoyo y paciencia en todo momento. Muy especialmente a mis
padres, Carmen y José, a los que tanto debo por todo lo que me han dado y me siguen
dando en la vida. Gracias.

Y finalmente a Inma. En los momentos bajos siempre ha estado ella con una sonrisa

y unas palabras de ánimo. Tu cariño me ayuda siempre a seguir adelante.

Índice General

1 Introducción

1

2 Una introducción a ACL2

15
2.1 El lenguaje de programación ACL2 . . . . . . . . . . . . . . . . . . . . . . . 17
2.2 La lógica de ACL2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.3 El demostrador automático de ACL2 . . . . . . . . . . . . . . . . . . . . . . 38
2.3.1 El funcionamiento del demostrador . . . . . . . . . . . . . . . . . . . 39
2.3.2 Cómo usar el demostrador . . . . . . . . . . . . . . . . . . . . . . . . 56

3 Términos y sustituciones

63
3.1 Términos de primer orden, sustituciones y ecuaciones . . . . . . . . . . . . . 63
3.1.1 Preliminares
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
3.1.2 Representación de los términos de primer orden en ACL2 . . . . . . 68
3.1.3 Representación de sustituciones en ACL2 . . . . . . . . . . . . . . . 74
3.1.4 Representación de sistemas de ecuaciones en ACL2 . . . . . . . . . . 81
3.2 Los términos como árboles . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
3.2.1 Preliminares
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
3.2.2 La estructura de árbol de los términos . . . . . . . . . . . . . . . . . 86
3.3 Equiparación y subsunción . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
3.3.1 Preliminares
3.3.2 Definición de un algoritmo de equiparación . . . . . . . . . . . . . . 91
3.3.3 Los teoremas principales . . . . . . . . . . . . . . . . . . . . . . . . . 93
3.3.4 Descripción de la demostración . . . . . . . . . . . . . . . . . . . . . 94
3.3.5 Un algoritmo de equiparación ejecutable . . . . . . . . . . . . . . . . 97
3.3.6 El preorden de subsunción entre términos . . . . . . . . . . . . . . . 101
. . . . . . . . . . . . . . . . . 104
3.4.1 Preliminares
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 105
3.4.2 Definición de la relación de subsunción entre sustituciones . . . . . . 106
3.4.3 Propiedades de la subsunción entre sustituciones . . . . . . . . . . . 107
3.4.4 Descripción de la demostración . . . . . . . . . . . . . . . . . . . . . 109

3.4 La relación de subsunción entre sustituciones

4 El retículo de los términos de primer orden

113
4.1 Renombrados . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114
4.1.1 Preliminares
. . . . . . . . . . . . . . . . . 115
4.1.2 Renombrados y términos equivalentes
4.1.3 Renombrados numéricos . . . . . . . . . . . . . . . . . . . . . . . . . 119
4.1.4 La relación de equivalencia renamed y sus congruencias
. . . . . . . 124

vii

viii

Índice General

4.1.5 Renombrado de listas de términos

. . . . . . . . . . . . . . . . . . . 125
4.2 Buena fundamentación de la relación de subsunción . . . . . . . . . . . . . 126
4.3 Ínfimo de dos términos. Anti–unificación . . . . . . . . . . . . . . . . . . . . 132
4.3.1 Preliminares
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132
4.3.2 Anti–unificación y sus propiedades principales . . . . . . . . . . . . . 134
4.3.3 Descripción de la demostración . . . . . . . . . . . . . . . . . . . . . 136
4.3.4 La estrategia del razonamiento compuesto . . . . . . . . . . . . . . . 143
4.4 Un algoritmo de unificación basado en reglas de transformación . . . . . . . 144
4.4.1 Preliminares
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144
4.4.2 Definición de un algoritmo de unificación no determinista . . . . . . 149
4.4.3 Propiedades principales
. . . . . . . . . . . . . . . . . . . . . . . . . 152
4.4.4 Descripción de la demostración . . . . . . . . . . . . . . . . . . . . . 153
4.4.5 Un algoritmo de unificación ejecutable . . . . . . . . . . . . . . . . . 160
4.4.6 Especificaciones basadas en reglas
. . . . . . . . . . . . . . . . . . . 163
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 164
4.5 Supremo de dos términos
4.6 El retículo de los términos de primer orden . . . . . . . . . . . . . . . . . . 169
4.6.1 Preliminares
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 169
4.6.2 El retículo de los términos . . . . . . . . . . . . . . . . . . . . . . . . 170

5 Multiconjuntos y pruebas de terminación

175
5.1 Multiconjuntos: definiciones y propiedades . . . . . . . . . . . . . . . . . . . 176
5.2 Formalización . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 181
5.2.1 Relaciones noetherianas . . . . . . . . . . . . . . . . . . . . . . . . . 181
5.2.2 Multiconjuntos. Relación entre multiconjuntos
. . . . . . . . . . . . 183
5.2.3 Buena fundamentación de las relaciones entre multiconjuntos . . . . 184
5.2.4 Una prueba informal del teorema . . . . . . . . . . . . . . . . . . . . 185
5.2.5 Descripción de la demostración . . . . . . . . . . . . . . . . . . . . . 186
5.2.6 Algunos lemas útiles sobre la relación entre multiconjuntos
. . . . . 192
5.3 El comando defmul . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 194
5.4 Una versión iterativa de la función de Ackermann . . . . . . . . . . . . . . . 196
5.5 La función 91 de McCarthy . . . . . . . . . . . . . . . . . . . . . . . . . . . 199

6 Reducciones abstractas

205
6.1 Reducciones abstractas: conceptos y propiedades . . . . . . . . . . . . . . . 205
6.2 Reducciones abstractas: formalización . . . . . . . . . . . . . . . . . . . . . 214
6.2.1 Representación . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215
6.2.2 Formalización de la clausura de equivalencia: pruebas abstractas . . 217
6.2.3 Enunciado de algunas propiedades . . . . . . . . . . . . . . . . . . . 220
6.3 Reducciones Church-Rosser y normalizadoras . . . . . . . . . . . . . . . . . 224
6.4 El lema de Newman . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 227
6.4.1 Formalización . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 227
6.4.2 Demostración del lema de Newman . . . . . . . . . . . . . . . . . . . 229
6.5 Reducciones convergentes: decidibilidad . . . . . . . . . . . . . . . . . . . . 232
6.5.1 Formalización del resultado . . . . . . . . . . . . . . . . . . . . . . . 232
6.5.2 Descripción de la demostración . . . . . . . . . . . . . . . . . . . . . 236
6.5.3 Un ejemplo . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 238

Índice General

ix

7 Teorías ecuacionales y sistemas de reescritura

Álgebra de pruebas ecuacionales

7.3 Sistemas de reescritura: terminación y formas normales

241
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 242
7.1 Teorías ecuacionales
7.1.1 Preliminares
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 242
7.1.2 Formalización de las teorías ecuacionales . . . . . . . . . . . . . . . . 245
7.1.3
. . . . . . . . . . . . . . . . . . . . 249
. . . . . . . . . . . . . . . . . . . . . . . . . 250
7.1.4 Propiedades principales
7.2 Reducibilidad . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253
7.2.1 Definición y propiedades principales
. . . . . . . . . . . . . . . . . . 253
7.2.2 Descripción de la demostración . . . . . . . . . . . . . . . . . . . . . 255
. . . . . . . . . . . 259
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 259
7.3.1 Preliminares
Sistemas de reescritura . . . . . . . . . . . . . . . . . . . . . . . . . . 260
7.3.2
Órdenes de reducción . . . . . . . . . . . . . . . . . . . . . . . . . . 261
7.3.3
7.3.4 Cálculo de formas normales . . . . . . . . . . . . . . . . . . . . . . . 264
7.4 Confluencia: el teorema de pares críticos de Knuth y Bendix . . . . . . . . 271
7.4.1 Prel