PDF de programación - Inserción y fusión con listas ordenadas: un ejemplo de razonamiento automático con ACL2

Inserción y fusión con listas ordenadas: un ejemplo de

razonamiento automático con ACL2

F. Palomo Lozano

, I. Medina Bulo

y

y
ffrancisco.palomo; [email protected]
y

, J. A. Alonso Jiménez

Departamento de Lenguajes y Sistemas Informáticos

Universidad de Sevilla

[email protected]



y



Departamento de Ciencias de la Computación e Inteligencia Artificial

Universidad de Cádiz

Palabras clave: Lógica Computacional, métodos formales, razonamiento automático, len-
guaje de programación aplicativo, ACL2, NQTHM

Resumen

En este artículo presentamos un ejercicio de formalización y demostración automática en
ACL2, un sistema de razonamiento automático que proviene de NQTHM, el demostrador de
teoremas de Boyer y Moore. Partiendo de la definición de dos operaciones esenciales so-
bre listas ordenadas, discutimos aspectos de formalización, descubrimiento de propiedades,
ejecutabilidad y mejora de la eficiencia computacional.

Ya en1949, se hizo patente la dificultad de crear programas que se ejecutaran según lo especifi-

1 Introducción

cado. Fue el propio Turing quien, siguiendo las ideas de vonNeumann y Goldstine, planteó la
necesidad de afrontar formalmente los problemas de corrección parcial y terminación. Herederos
de estas ideas, McCarthy, Dijkstra, Floyd y Hoare las desarrollaron durante tres décadas.

El amplio desarrollo de los métodos formales ha dado lugar a una nueva disciplina denomina-
da CAR (Computer-Aided Reasoning), que tiene entre sus objetivos el desarrollo de herramientas
informáticas que proporcionen asistencia en su empleo. Estas herramientas suelen denominarse
genéricamente «sistemas de razonamiento automático» e incluso «demostradores automáticos de
teoremas».

Dentro del amplio espectro de sistemas de razonamiento automático, existen varios especial-
mente adecuados para la especificación y verificación formal de sistemas informáticos. Uno de
ellos, ACL2, merece especial atención ya que formaliza un subconjunto de un lenguaje de pro-
gramación real y con él se han obtenido grandes éxitos en la verificación formal automatizada
tanto de sistemas de hardware como de software, además de en la demostración por computador
de conocidos teoremas de la Lógica y de las Matemáticas.

Facultad de Informática y Estadística. Avda. Reina Mercedes, s/n. 41012 Sevilla. España.
Escuela Superior de Ingeniería de Cádiz. C/ Chile, s/n. 11003 Cádiz. España.


y

Se expondrá a continuación una breve descripción de ACL2, de ningún modo exhaustiva,
atendiendo a los diferentes puntos de vista desde los que puede observarse. Posteriormente, se
propondrá un ejemplo sobre cómo razonar formalmente acerca de las propiedades de los progra-
mas en ACL2; éste incluirá un caso de descubrimiento automático. Los ficheros ACL2 con el
ejemplo completo, algo ampliado, y la demostración producida por el sistema (unas 50 páginas)
están disponibles públicamente en www-cs.us.es/~fpalomo/listas-ordenadas.html.

2 Las tres visiones de ACL2

ACL2 (A Computational Logic for Applicative Common Lisp) [6, 7] es el sucesor de NQTHM, el
demostrador de teoremas de Boyer y Moore [1, 3]. ACL2 ha sido desarrollado durante la última
década, principalmente por Moore y Kaufmann, y continúa en evolución. Intenta hacer realidad,
con bastante éxito, el deseo de McCarthy de disponer de un sistema capaz de demostrar teoremas
sobre programas escritos en LISP (puro).

Puede encontrarse una descripción concisa de ACL2 en [4]. En realidad, para definir qué es

ACL2 hay que enfocarlo desde tres puntos de vista distintos:

1. Desde un punto de vista lógico.

2. Desde la perspectiva de los lenguajes de programación.

3. Desde el enfoque de los sistemas de razonamiento automático.

2.1 ACL2 es una Lógica Computacional
ACL2 es una lógica de primer orden sin cuantificadores y con igualdad1. Su sintaxis coincide
con la del lenguaje de programación COMMON LISP. Esto quiere decir que un término de la
lógica es una constante, un símbolo de variable o la aplicación de un símbolo de función (o de

una-expresión)-ario a términos. Formalmente, en ACL2 no existen símbolos de predicado,
inducción matemática sobre los"0-ordinales. La regla de instanciación funcional permite susti-

Las reglas de inferencia son las del cálculo proposicional con igualdad junto con instancia-
ción de variables, inducción e instanciación funcional. Todas permiten deducir nuevos teoremas
a partir de otros ya conocidos3. La regla de instanciación de variables permite sustituir variables
en un teorema por términos para obtener otro teorema. La regla de inducción permite reducir la
demostración de un teorema a un conjunto finito de casos empleando una forma muy potente de

aunque a las funciones booleanas se las denomine informalmente «predicados».

Entre sus axiomas se incluyen los de la lógica proposicional con igualdad y los necesarios pa-
ra trabajar cómodamente con los tipos de datos de uso más común: números (enteros, racionales
y complejos racionales)2, caracteres, cadenas de caracteres, símbolos y listas.

tuir funciones en un teorema por otras para obtener un nuevo teorema, siempre que las antiguas
fueran introducidas por el principio de encapsulado que se explica a continuación y las nuevas
cumplan sus axiomas de restricción.

La lógica incluye también dos principios de extensión: definición y encapsulado. Ambos per-
miten añadir nuevos símbolos de función y axiomas a la lógica preservando su consistencia. El
principio de definición es esencial, ya que permite introducir nuevos símbolos de función y aso-
ciarles (axiomáticamente) una definición; para preservar la consistencia, el sistema únicamente

1O, recíprocamente, una lógica proposicional con igualdad extendida con símbolos de variable y función.
2Una reciente extensión de ACL2, denominada ACL2 (r), amplía la axiomatización para incluir a los reales.
3Por supuesto que, inicialmente, los únicos teoremas conocidos son los axiomas.

admite una función bajo este principio si puede demostrar su terminación bajo ciertas condicio-
nes. El principio de encapsulado permite introducir nuevos símbolos de función restringidos
por axiomas a tener ciertas propiedades; para preservar la consistencia, el sistema exige que se
proporcionen «testigos» de la existencia de tales funciones. La instanciación funcional es una
regla de inferencia derivada de él. El papel que juega el principio de encapsulado en el desarrollo
estructurado de teorías se explica en [5].

La ausencia de cuantificación hace que el carácter de la lógica sea fundamentalmente cons-
tructivo: más que enunciar el hecho de que un cierto objeto existe, se ha de exponer una función
computable que construya un objeto con las propiedades deseadas.

Otro aspecto interesante es la ausencia de tipos4 y el carácter total de la lógica. Las funciones
introducidas bajo el principio de definición han de ser funciones recursivas totales. Aunque esto
último constituya una limitación teórica, en la práctica, la mayoría de las funciones parciales
que solemos definir pueden ser generalizadas convenientemente para obtener funciones totales
equivalentes bajo sus dominios de definición. Posteriormente un mecanismo extra-lógico basado
en protecciones permite declarar el dominio que se pretende que dichas funciones tengan en
ejecución.

2.2 ACL2 es un lenguaje de programación aplicativo

Toda función admitida bajo el principio de definición de ACL2 es una función de COMMON
LISP. El recíproco no es cierto, ya que para razonar en la lógica ACL2 sobre una función su
ejecución debe sólo depender de sus parámetros reales5: a iguales parámetros, igual resultado.
Por otro lado, los lenguajes de programación convencionales permiten «definir» funciones cuya
terminación no está garantizada.

Esto hace que sea posible pensar en ACL2 como en un lenguaje de programación aplicati-
vo. Más explícitamente, puede considerarse que es un subconjunto de COMMON LISP libre de
efectos colaterales.

2.3 ACL2 es un sistema de razonamiento automático

Cuando se suministra un posible teorema a ACL2, o se extiende la lógica mediante uno de los
principios de extensión siendo necesario comprobar que se cumplen ciertas condiciones, ACL2
se comporta como un demostrador de teoremas.

Como tal, emplea una serie de técnicas de prueba en su búsqueda de una demostración del
supuesto teorema. Cada técnica de prueba puede verse como un proceso que recibe una fórmula
como entrada y produce un conjunto de fórmulas como resultado: la fórmula de entrada es un
teorema si cada una de las resultantes lo es.

Por supuesto, puede que un proceso no sea aplicable a una fórmula. En tal caso, el proceso
no falla, sino que produce un conjunto que contiene únicamente a dicha fórmula. Por otro lado,
si un proceso es capaz de demostrar que una determinada fórmula es un teorema, devuelve el
conjunto vacío.

Cuando el usuario proporciona una conjetura al sistema, su fórmula se convierte en el obje-
tivo de la demostración y pasa secuencialmente por cada uno de los procesos hasta que uno de
ellos sea aplicable. Éste produce un conjunto de subobjetivos que reemplazan al objetivo original
y todo comienza de nuevo. Esto continúa hasta que no quedan subobjetivos pendientes de demos-
trar o hasta que se cumplen determinadas condiciones de terminación que indican que el sistema

4Sin embargo, un primitivo sistema de deducción de tipos está presente internamente en el sistema.
5De lo contrario, su definición no bastaría: sería necesario introducir el concepto de «estado global».

no puede completar la demostración de la conjetura (incluso, a veces, aparece un ciclo); en este
último caso la conjetura inicial puede o no ser un teorema. Como se observa, el razonamiento es
regresivo. Describamos, brevemente, cada proceso.

El proceso de simplificación incluye procedimientos de decisión para la lógica proposicional,
la igualdad y la aritmética lineal. También se encarga de la reescritura de términos y de las
meta-funciones [2], que son simplificadores que el usuario define