PDF de programación - Razonamiento autoático en programación genérica con ACL2: estudio de un caso

con ACL2: estudio de un caso

y

y
finmaculada.medina; [email protected]
y

Departamento de Lenguajes y Sistemas Informáticos

Universidad de Sevilla

[email protected]



y



I. Medina Bulo

, J. A. Alonso Jiménez

, F. Palomo Lozano

Razonamiento automático en programación genérica

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, programación genérica, algoritmos genéricos, ACL2

Resumen

En este artículo se estudia un caso de formalización y demostración automática en ACL2
relacionado con la programación genérica. Tras una definición axiomática del concepto de
orden estricto débil se demuestran sus propiedades esenciales para, a continuación, formali-
zar las listas ordenadas genéricas junto a sus operaciones de inserción y fusión. Para terminar,
se realiza una instanciación de las operaciones genéricas y de sus propiedades.

1 Introducción

El desarrollo de los métodos formales en los últimos treinta años ha dado lugar a una nueva disci-
plina denominada CAR (Computer-Aided Reasoning), que tiene entre sus objetivos el desarrollo
de herramientas informáticas que proporcionen asistencia en su empleo. Estas herramientas sue-
len denominarse genéricamente «sistemas de razonamiento automático».

Dentro de los sistemas de razonamiento automático adecuados para la especificación y veri-
ficación formal de sistemas informáticos, uno de ellos, ACL2 (A Computational Logic for Appli-
cative Common Lisp), merece especial atención ya que formaliza un subconjunto de un lenguaje
de programación real, COMMON LISP. La mayor parte de las ideas presentes en ACL2 [5, 6]
provienen de NQTHM, el demostrador de teoremas de Boyer y Moore [1, 2].

Por otro lado, el paradigma de la programación genérica [8] ha madurado a partir de lengua-
jes como TECTON [7] e incluso se ha mezclado con otros paradigmas, como en C++ que incluso
posee una biblioteca estándar, la STL (Standard Template Library), de contenedores y algoritmos
genéricos. La programación genérica requiere, si cabe, mayor formalización que la convencional
ya que un algoritmo genérico no es más que una abstracción de muchos otros que resulta de
generalizar tipos y operaciones concretas.

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

Debido a esto, parece necesario para razonar sobre programas genéricos un formalismo ló-
gico muy potente que incluya el concepto de tipo y que sea de orden superior. No obstante,
mostraremos cómo es posible salvar estas vicisitudes con una lógica en apariencia más débil
como es el caso de ACL2: una lógica de primer orden sin cuantificadores y con igualdad, que
contiene únicamente dos principios de extensión y que carece de tipos.

Estos principios de extensión permiten 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 intro-
ducir nuevos símbolos de función y asociarles (axiomáticamente) una definición; para preservar
la consistencia, el sistema únicamente admite una función bajo este principio si puede demostrar
su terminación bajo ciertas condiciones. El principio de encapsulado permite introducir nue-
vos 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.
Este segundo principio juega un importante papel en el desarrollo estructurado de teorías, como
se explica en [4].

Se presenta a continuación el estudio de un caso de razonamiento formal sobre programas
genéricos en ACL2. En él aparecen (entre otras cosas) diversas funciones definidas de manera
análoga a como se hace en COMMON LISP, ya que ACL2 es también un lenguaje de programa-
ción aplicativo derivado de él. Puede encontrarse una descripción concisa de ACL2 en [3]. Los
ficheros con el ejemplo completo, algo ampliado, y la demostración producida por el sistema
están disponibles públicamente en www-cs.us.es/~fpalomo/listas-ordenadas.html.

2 Operaciones sobre listas ordenadas genéricas

El ejemplo escogido es una generalización del descrito en [10]. En éste se formalizaba en ACL2
el conjunto de las listas ordenadas de números racionales y dos operaciones sobre dicho conjunto,
insercion y fusion. En este trabajo se elimina el requisito de que los elementos de la lista
tengan que ser de tipo «número racional». En realidad, se aprovecha la ausencia de tipos en
ACL2 para relajar aún más la definición permitiendo incluso que, potencialmente, las listas no
sean homogéneas.

2.1 El problema del orden

Puesto que ahora las operaciones han de ser abstractas, por ser las listas de tipo arbitrario, y
no disponemos de tipos, parece que la única solución es introducir una función de comparación
como parámetro de las operaciones de inserción y fusión, dando lugar así a una lógica de orden
superior.

Una solución en ACL2 consiste en utilizar el segundo principio de extensión para introducir
un nuevo símbolo de función restringido por axiomas oportunos a cumplir las propiedades que
se esperan de una función de comparación. Pero, cabe preguntarse cuáles deben ser dichas
propiedades, ya que existen diversas nociones formales que permiten abstraer nuestro concepto
informal de «orden». ¿Es más adecuado emplear un orden total que uno parcial? ¿Basta con un
preorden? ¿Qué conviene entender por elementos equivalentes?

Tomemos como ejemplo la función booleana < de ACL2. Sobre el conjunto de los números
es un orden estricto total y, sin embargo, no lo es sobre el de los objetos de ACL2. En efecto, un
intento de demostrar la siguiente propiedad fracasará:

(defthm tricotomica

(or (< a b) (< b a) (= a b))
:rule-classes nil)

:::

:::
:::

This simplifies, using trivial observations, to

Goal’’
(IMPLIES (AND (<= B A) (<= A B))

(EQUAL A B)).

This forcibly simplifies, using linear arithmetic, to

Goal’’’
(IMPLIES (<= A A) (EQUAL A A)).

[1]Subgoal 2, below, will focus on
(ACL2-NUMBERP A),

[1]Subgoal 1, below, will focus on
(ACL2-NUMBERP B),

Para comprender el porqué, basta inspeccionar parte de la salida que produce ACL2 en res-

puesta a la anterior conjetura (aparecen subrayados los puntos clave):

But simplification reduces this to T, using primitive type reasoning.

q.e.d. (given two forced hypotheses)

Modulo the following two forced goals, that completes the proof of
the input Goal. See :DOC forcing-round.

Esto significa que puede demostrarlo, siempre que a y b sean números, pero no en general.
De hecho, se puede comprobar que no se cumple si tomamos nil y t como valores de a y b.
Aunque pueda parecer irrelevante (ciertamente, la función < se emplea para comparar números)
no hay que olvidar que ACL2 es una lógica sin tipos de funciones totales y que es importante
poder razonar sobre éstas con las mínimas restricciones.

2.2 Formalización de los conceptos de orden y equivalencia

No es difícil ver que el concepto de orden total es demasiado restrictivo para muchas apli-
caciones prácticas. Seguiremos así el criterio empleado en la biblioteca STL de C++, donde se
incluye entre las precondiciones de los algoritmos genéricos que emplean una función (u opera-
dor) de comparación que ésta tenga estructura de orden estricto débil. La idea de emplear esta
noción de orden en algoritmos genéricos aparece ya en TECTON y de ahí pasa a la STL [9]. Esta
elección se ha demostrado adecuada para aplicaciones industriales, como refleja el hecho de que
esta biblioteca fuera elegida para formar parte del estándar ANSI/ISO de C++.

Recuérdese que un orden estricto (parcial) es un conjuntoA con una relación1 binaria que
8a2A::a;a
8a;b;
2A:a;b^b;
=a;

8a;b2A:a;b=:b;a
8a;b;
2A::a;b^:b;a^:b;
^:
;b=:a;
^:
;a

cumple las siguientes propiedades:

Un orden estricto débil (en adelante, OED) es un orden estricto que cumple además la si-

guiente propiedad, que expresa el hecho de que la «incomparabilidad» ha de ser transitiva:

de donde se deduce esta otra:

(antirreflexiva)
(transitiva)

(antisimétrica)

1Representaremos a las relaciones mediante funciones booleanas.

Dado un OEDhA;i, éste induce la siguiente relación binaria:
8a;b2A:ea;b=:a;b^:b;a
8a;b;
2A:ea;b^eb;
=ea;


que se puede demostrar que es una relación de equivalencia (es decir, reflexiva, simétrica y tran-
sitiva), recibiendo por ello el nombre de equivalencia inducida por el OED. Nótese que dos
elementos son equivalentes si, y sólo si, son incomparables. En función de esta nueva relación,
el tercer axioma de los OED queda:

(transitiva de la equivalencia)

Por ejemplo, el conjunto de las cadenas de caracteres con la relación «tener menor longitud
que» es un OED, estando sus clases de equivalencia formadas por cadenas de igual longitud.
Otro ejemplo de OED es el conjunto de los objetos de ACL2 con la función booleana ACL2::<,
aunque sus clases de equivalencia tienen una estructura más compleja:

(defthm caracterizacion-clases-equivalencia-<

(iff (and (not (< a b)) (not (< b a)))

(or (equal a b)

(and (or (not (acl2-numberp a)) (equal a 0))

(or (not (acl2-numberp b)) (equal b 0)))))

:rule-classes nil)

A continuación realizaremos una formalización general de los OED en ACL2. Por convenien-
cia notacional empleamos los símbolos de función < e = para representar la relación del OED y
su equivalencia inducida; también introducimos la siguiente macro:

(defmacro <= (a b)

‘(not (< ,b ,a)))

Para que no haya conflicto entre estos símbolos y los ya disponibles en ACL2 los definimos
en un paquete de nombre OED. Una vez hecho esto, extendemos la lógica mediante encapsula-
do añadiendo únicamente un símbolo de función binario < restringido por los tres axiomas de
los OED. Como testigo de la existencia de tal fu