Derivaciones perezosas en Programación Lógica con restricciones ecuacionales^{∗}

María José Ramis ^{‡}  Javier Piris ^{‡}  María Alpuente ^{‡}

Resumen

El lenguaje CLP(H/E) es una instancia del esquema CLP [17] que resuelve ecuaciones bajo una teoría de la igualdad presentada como una teoría ecuacional de Horn E [1, 2]. CLP(H/E) aúna el estilo de programación lógica basado en cláusulas de Horn, el paradigma basado en ecuaciones (condicionales) y la programación con restricciones. Como núcleo de su semántica operacional, en [1, 2] se define un procedimiento incremental que semidecide la solubilidad de las ecuaciones en la estructura H/E y que está basado en un cálculo de narrowing. La terminación de este cálculo no está garantizada, por el hecho de que el conjunto de E-unificadores de un par de términos es sólo semidecidible. En este trabajo se considera una versión perezosa del lenguaje CLP(H/E) que retrasa el problema de la E-unificación de las ecuaciones hasta haber resuelto completamente el resto de átomos en el objetivo. Para optimizar los algoritmos se propone un conjunto de transformaciones sintácticas que simplifica las restricciones y, en ocasiones, es capaz de detectar su insatisfacibilidad.

Palabras clave: Programación lógica con restricciones, Programación lógica ecuacional, Sistemas de Reescritura, Unificación Universal, Resolución perezosa.

1 Introducción

Uno de los problemas que, en los últimos años, han atraído con más fuerza el interés de los investigadores en el campo de la Programación Lógica es el de la integración de dos de las familias más prometedoras de lenguajes declarativos: los lenguajes lógicos y los ecuacionales [5, 6, 9, 13, 18]. Recientemente, el paradigma de Programación lógica pura ha sido generalizado a un contexto más general de Programación lógica con restricciones (Constraint Logic Programming, CLP), un esquema genérico para extensiones conservativas a la programación lógica pura [12, 17]. El estilo CLP se muestra especialmente fecundo en el campo de la integración de lenguajes. La integración de la programación lógica y ecuacional en el marco de CLP resulta ser simple y elegante, especialmente por la garantía de una semántica análoga a la de la programación lógica pura. El lenguaje CLP(X) resultante de una instanciación del esquema no sólo hereda las propiedades semánticas más atractivas de la programación lógica (semántica declarativa por modelo mínimo, caracterización por punto fijo y semántica operacional equivalente) sino que, además, posee la ventaja de contar con una semántica algebraica que se define directamente sobre la estructura X con la que se parametriza el esquema. El concepto de estructura especifica el dominio sobre el que se efectúa la computación dando la interpretación semántica a funciones y relaciones y es el elemento clave para la definición semántica algebraica del lenguaje.

El lenguaje CLP(H/E) es una instancia del esquema CLP que usa ecuaciones para expresar restricciones entre símbolos de función. La estructura con la que se parametriza el esquema es el algebra cociente H/E, i.e. la partición más fina inducida por una teoría de la igualdad E sobre el Universo de Herbrand H para el programa. El único símbolo de predicado para las restricciones es el =, que se interpreta como igualdad semántica en el dominio.

Una cuestión fundamental a afrontar en el diseño de un lenguaje CLP es la selección de los algoritmos adecuados para la verificación de la solubilidad de las restricciones. En H/E este problema es sólo (semi)- decidible. Como núcleo del mecanismo de resolución de restricciones que semidecide la solubilidad de las mismas, en [1, 2] se define un procedimiento de narrowing [13, 24], cuyo uso presenta como inconveniente la posibilidad de no terminación de éste cuando la restricción no es satisfacible. Como consecuencia, un paso de derivación CLP(H/E) puede conducir a computaciones que entran en ciclo sin producir ninguna respuesta y es para evitar esta dificultad por lo que en este trabajo se considera una versión perezosa del lenguaje. La idea de la evaluación perezosa está estrechamente relacionada con la de hacer todo lo que es seguro en cada momento, evitando el análisis de situaciones peligrosas.

∗Este trabajo ha sido parcialmente subvencionado por CICYT TIC 92-0793 y realizado mientras la primera autora está disfrutando de una beca de Investigación de la Consellería de Cultura, Educació i Ciència de la Generalitat Valenciana.

‡Departamento de Sistemas Informáticos y Computación, Universidad Politécnica de Valencia, Camino de Vera s/n, Apdo. 22012, 46020 Valencia, Spain. e-mail: mjrg(jpiris)(maria)@dsic.upv.es

La organización del trabajo es como sigue. Con la intención de ofrecer un trabajo autocontenido, en la sección segunda se revisan algunas nociones y resultados básicos sobre sistemas de reescritura condicionales y unificación semántica. También se reformulan algunos conceptos básicos del marco conceptual CLP en términos de transiciones y de configuraciones para facilitar el posterior uso de la aproximación estructural de Plotkin a la definición semántica operacional de CLP(H/E) y se revisa la definición de la sintaxis del lenguaje. En la sección tercera formalizamos, utilizando la aproximación de Plotkin, nuestra propuesta de mecanismo computacional perezoso, que hace uso de un conjunto de transformaciones sintácticas para optimizar los cálculos [10, 23]. En la sección cuarta se presenta un intérprete Prolog para el lenguaje. Finalmente se establecen algunas conclusiones y se incluye, como anexo, un ejemplo de ejecución. Asumimos en el lector un conocimiento básico de la programación lógica [22], programación lógica con restricciones (CLP) [17, 12], ecuaciones y sistemas de reescritura condicionales [20] y unificación semántica [27]. En [4] se estudia la aplicación del lenguaje CLP(H/E) al prototipado automático de aplicaciones de bases de datos.

2 Preliminares

Por Σ, Π y V (posiblemente con subíndices) denotamos, respectivamente, colecciones disjuntas numerables de símbolos de función, símbolos de predicado y símbolos de variable con sus signaturas. τ(Σ ∪ V) y τ(Σ) denotan, respectivamente, los conjuntos de términos y términos sin variables (términos básicos) construidos sobre Σ y V. Un (Π, Σ)-átomo es una expresión de la forma p(t_{1}, …, t_{n}) donde p ∈ Π es n-ario y t_{i} ∈ τ(Σ ∪ V), i = 1, …, n. Una (Π, Σ)-restricción es un conjunto (posiblemente vacío) de (Π, Σ)- átomos. El símbolo ˜ denotará una secuencia finita de símbolos. τ(Σ) suele ser llamado el Universo de Herbrand (H) sobre el alfabeto Σ.

Una Σ-ecuación s = t es un par de términos s, t ∈ τ(Σ ∪ V). Una Σ-teoría ecuacional de Horn E consiste en un conjunto finito de cláusulas de Horn ecuacionales, de la forma e ← e_{1}, e_{2}, …, e_{n}, n ≥ 0, donde e, e_{1}, e_{2}, …, e_{n} son Σ-ecuaciones. Una teoría ecuacional de Horn E puede verse como un sistema de reescritura R donde las reglas son las cabezas y las condiciones son los respectivos cuerpos. Representamos las ocurrencias de un término como secuencias, posiblemente vacías, de naturales; t/u es el subtérmino de t a la ocurrencia u; t[u ← r] es el término t con el subtérmino a la ocurrencia u reemplazado por r; V(t) denota el conjunto de variables de un término t [20].

Sea E una teoría ecuacional de Horn. Se dice que el término s se reescribe al término t, s →_{R} t, si existe una (variante de una) cláusula (l = r ⇐ s_{1} = t_{1}, …, s_{n} = t_{n}) en E, una ocurrencia u de s y una

sustitución θ tales que s/u = lθ, t = s[u ← rθ] y ∀i. 1 ≤ i ≤ n. ∃γ_{i} tal que s_{i}θ →∗_{R} γ_{i} ∧ t_{i}θ →∗_{R} γ_{i}.

Se dice que dos términos s y t son convergentes, s ↓_{R} t, si existe un término ω tal que s →∗_{R} ω ∧ t →∗_{R} ω. La relación →_{R} se dice que es confluente si para todo término s_{1}, s_{2}, s_{3} tales que s_{1} →∗_{R} s_{2} ∧ s_{1} →∗_{R} s_{3}, existe un término s tal que s_{2} →∗_{R} s ∧ s_{3} →∗_{R} s. La relación →_{R} es noetheriana si no existe una cadena infinita s_{1} →_{R} s_{2} →_{R} s_{3} →_{R} … de reescrituras. Una teoría ecuacional de Horn se dice que es canónica sii la relación →_{R} es confluente y noetheriana.

Cada teoría ecuacional de Horn E genera una relación de congruencia más fina =_{E} (llamada E-igualdad) sobre τ(Σ ∪ V) (la menor teoría que contiene todos los pares s = t tales que^{1} E ⊧ s = t). Se dice que E es una presentación o axiomatización de la teoría de la igualdad =_{E} y, por abuso, se habla a veces de la teoría de la igualdad E para denotar la teoría axiomatizada por E. Denotaremos como H/E la partición más fina τ(Σ)/=_{E} inducida por =_{E} sobre el conjunto de términos básicos τ(Σ).

Se dice que dos términos s, t son E-unificables (o E-iguales) sii existe una sustitución σ tal que sσ y tσ están en la congruencia =_{E}, i.e. tal que E ⊧ sσ = tσ. La sustitución σ es llamada un E-unificador de s y t. Se llama E-unificación al proceso de resolver una ecuación bajo la teoría ecuacional E. Ya que el proceso es sólo semidecidible, un algoritmo de E-unificación puede verse como un procedimiento de semidecisión para verificar la solubilidad de restricciones ecuacionales sobre el cociente H/E. Cada instancia de un E-unificador representa una solución sobre este cociente. Las aproximaciones de mayor significación al problema de computar el conjunto de E-unificadores de dos términos son tres: flat SLD resolución [6, 11, 28], conjuntos completos de transformaciones [10, 13, 23] y paramodulación [25] o formas especiales de ésta, tales como superposición [9] o narrowing [15, 24].

1En lo que sigue asumimos que las interpretaciones obedecen los axiomas de la igualdad. Consecuentemente, los conceptos de satisfacibilidad y consecuencia lógica están definidos con respecto a estos axiomas

Sea E una teoría ecuacional de Horn. Un símbolo de función f ∈ Σ se dice que es irreducible sii no existe ninguna cláusula (l = r ← e_{1}, e_{2}, …, e_{n}.) ∈ E tal que l ∈ V ni f ocurre como el símbolo de función más externo en l; en cualquier otro caso f es un símbolo de función definido. En teorías donde se hace la distinción anterior, la signatura Σ queda particionada como Σ = C ⨄ F, donde C es el conjunto de símbolos de función irreducibles y F es el conjunto de símbolos de función definidos. A continuación revisamos las nociones básicas de CLP [17].

Sea Π = Π_{C} ∪ Π_{B}, con Π_{C} ∩ Π_{B} = Ø. Un (Π, Σ)-programa es un conjunto de cláusulas de la forma: H ← c□. o H ← c□B_{1}, …, B_{n}., donde c es una (Π_{C}, Σ)-restricción finita (posiblemente vacía), y H (la cabeza) y B_{1}, …, B_{n} (el cuerpo), n ≥ 0, son (Π_{B}, Σ)-átomos. Un objetivo es una cláusula de programa sin cabeza.

Dada una estructura X [17], se dice que una restricción c es X -soluble (en símbolos X ⊧ ˜∃c) sii existe una X -valuación θ (una valoración sobre el soporte de X) tal que X ⊧ cθ. Se dice entonces que θ es una X -solución de c. También se dice que c es satisfacible.

La semántica declarativa de un programa CLP puede verse tanto en términos de consecuencia lógica como con un estilo algebraico. La respuesta a un objetivo G no es una sustitución, sino una conjunción de restricciones c tal que: (P,ℑ) ⊧ (∀) (c ⇒ G) (versión lógica) y P ⊧_{X} (∀) (c ⇒ G) (versión algebraica), donde P es un programa CLP, X la estructura y ℑ es una teoría que axiomatiza X [17]. La teoría CLP impone restricciones sobre X, ℑ y sus relaciones para establecer equivalencias entre las semánticas.

Sea P un programa CLP(X) y G = ← c□A_{1}, …, A_{n}. un objetivo. Definimos una configuración como el par C = ⟨← c □ A_{1}, …, A_{n}⟩. Sea G_{0} =← c_{0}□B̃. un objetivo inicial. La configuración C_{0} = ⟨← c_{0} □ B̃⟩ es una configuración inicial. Una configuración terminal C tiene la forma C = ⟨← c □ ⟩, donde c representa la restricción computada correspondiente a esa derivación.

Un intérprete (ansioso) de un lenguaje CLP(X) se basa en una generalización de la regla de SLDresolución utilizada en programación lógica convencional y en un algoritmo apropiado para resolver restricciones en el dominio de computación correspondiente. Intuitivamente, una computación CLP (ansiosa) puede verse como una secuencia de pasos de reducción de objetivos en la que se acumulan restricciones, posiblemente simplificadas (previa comprobación de su satisfacibilidad). La computación termina con un conjunto satisfacible de restricciones como respuesta^{2}.

La regla estándard que describe un paso de (P, X)-computación se define del siguiente modo [1, 2, 17]:

\frac{\begin{matrix}∃ n variantes de cláusulas en P (H_{j} ← c′_{j}□B̃_{j}., j = 1, …, n) ∧ \\ c̃ = \{c′_{1}, c′_{2}, …, c′_{n}, A_{1} = H_{1}, …, A_{n} = H_{n}\} ∧ X ⊧ ˜∃(c_{i} ∪ c̃) \end{matrix}}{⟨← c_{i}□A_{1}, …, A_{n}⟩ →_{CLP (X)} ⟨← c_{i} ∪ c̃ □B̃_{1}, …, B̃_{n}⟩}

Cuando la condición X ⊧ ˜∃(c_{i}∪c̃) se elimina de la premisa de la regla se obtiene un intérprete perezoso para el lenguaje CLP comparable al que se describe en [12]. En [12] se asume además que un procedimiento de simplificación de restricciones se aplica en cada paso. Este procedimiento es capaz de detectar, en ocasiones, la insatisfacibilidad de la restricción.

3 Semántica Operacional (perezosa) para CLP(H/E)

CLP(H/E) es un lenguaje diseñado para realizar la integración de la programación lógica y ecuacional en el marco de la programación lógica con restricciones. Informalmente, un programa CLP(H/E) consta de dos conjuntos de cláusulas de Horn definidas. Uno de ellos, la parte relacional, contiene sólo cláusulas cuya cabeza es un átomo (no ecuacional) y cuyo cuerpo puede contener tanto átomos como restricciones (ecuacionales). La parte funcional contiene sólamente cláusulas constituidas enteramente por ecuaciones (cláusulas de Horn ecuacionales o, equivalentemente, ecuaciones condicionales). Formalmente, sea Π_{C} = {=}, Π = Π_{C} ∪ Π_{B} y Π_{C} ∩ Π_{B} = Ø. Definimos un (Π, Σ)-programa CLP(H/E) como un (Π, Σ)-programa extendido con una Σ-teoría ecuacional de Horn canónica E.

Ejemplo 3.1. El siguiente conjunto de cláusulas es un programa CLP(H/E). (p_{1}) p(f(Z)) ← □ q(Z). (p_{2}) q(a). (e_{1}) f(a) = a. (e_{2}) f(d(X)) = f(X). (e_{3}) g(X) = Y ← f(X) = Y.

2Debido a que las restricciones no se resuelven completamente en cada paso de computación se debe notar que, en el caso particular de la estructura H/E, esta forma de resolución evita el problema de la posible infinitud del número de resolventes entre una cláusula de programa y una cláusula objetivo que se presenta en las definiciones clásicas de resolución ecuacional (donde, a causa de la posible infinitud del conjunto de E-unificadores de un par de términos, el espacio de búsqueda de la resolución puede no sólo ser infinito en profundidad sino también en amplitud) [13].

Es inmediato que un mecanismo computacional impaciente (i.e. ansioso) para CLP(H/E) presenta como inconveniente la posibilidad de entrar en ciclo sin producir ninguna respuesta cuando se intenta probar la solubilidad de la restricción acumulada. El siguiente ejemplo ilustra este hecho.

Ejemplo 3.2. Consideremos,e.g., el programa del ejemplo 3.1 con el objetivo inicial G_{0} =← □p(b). La configuración CLP(H/E) inicial es C_{0} = ⟨← □p(b)⟩. Considerando la cláusula (p_{1}), la nueva restricción c̃_{1} es c̃_{1} = { b = f(Z) }.

El intérprete ansioso para CLP(H/E) debería decidir la satisfacibilidad de la restricción c̃_{1} antes de efectuar el correspondiente paso de computación. El intento de E-unificar la restrición (irresoluble) c̃_{1} utilizando la regla (e_{1}) fallaría al derivar la ecuación (ground) irresoluble {b = a}. Sin embargo la derivación b = f(Z) →_{{Z/d(X)}(e_{2})} b = f(X) →_{{X/d(X′)}(e_{2})} b = f(X′) → … es infinita por aplicación de la regla (e_{2}).

3.1 Derivaciones perezosas

En este apartado se formaliza un mecanismo computacional perezoso como semántica operacional del lenguaje CLP(H/E) para evitar el problema de la no posible terminación de un paso de computación CLP(H/E) ansioso cuando la restricción acumulada no es satisfacible. Nuestra noción de computación perezosa es similar a la noción de resolución perezosa presentada en [13] y a la noción de reducción de objetivos que se define en [12], donde la solubilidad de las restricciones no se exige en cada paso. Es evidente, no obstante, que una estrategia ”demasiado” perezosa detectaría la irresolubilidad de las restricciones ”demasiado” tarde, produciendo una explosión inaceptable del árbol de derivaciones CLP. La capacidad para detectar la insatisfacibilidad de las restricciones es muy importante para podar caminos superfluos del árbol y evitar así computaciones innecesarias. En lo que sigue formalizamos la idea de un simplificador (incremental) de restricciones que también analiza la insatisfacibilidad de las mismas. En este contexto incrementalidad significa que no es necesario repetir todo el trabajo realizado en el paso de computación previo cuando se añade incrementalmente una nueva restricción.

Definición 3.1.1 (relación de transición ⟶_{LCLP (H/E)}). Sea c una restricción. Supongamos que c puede escribirse de la forma c_{1} ∪ c_{2} (cualquiera de las cuales puede ser vacía) donde c_{1} es equivalente a un conjunto de ecuaciones en forma resuelta θ̂_{1} [21]. Entonces llamamos representación de c al par ⟨ θ̂_{1}, c_{2} ⟩^{3}. En lo que sigue no haremos distinción entre restricciones y su representación. Usaremos el terminal fail para representar restricciones irresolubles. La regla que describe un paso de computación perezosa para CLP(H/E) a partir de una configuración ⟨ ← c_{i} □ A_{1}, …, A_{n} ⟩ viene dada por:

\frac{\begin{matrix}∃ n variantes de cláusulas en P (H_{j} ← c′_{j}□B̃_{j}., j = 1, …, n) ∧ \\ c̃ = \{c′_{1}, c′_{2}, …, c′_{n}, A_{1} = H_{1}, …, A_{n} = H_{n}\} ∧ \\ c_{i+1} = Simplificación(c_{i}, c̃) ∧ c_{i+1} ≠ fail \end{matrix}}{⟨ ← c_{i}□A_{1}, …, A_{n} ⟩ ⟶_{LCLP (H/E)} ⟨ ← c_{i+1}□B̃_{1}, …, B̃_{n} ⟩}

donde la función Simplificación(c_{i}, c̃) en la premisa de la regla reduce la restrición c_{i} ∪ c̃ a una forma (más simple) equivalente mediante un conjunto apropiado de transformaciones, que se describirá posteriormente, sin comprobar su solubilidad en la estructura H/E, i.e. sin estudiar el problema de la E-unificabilidad de las ecuaciones. El efecto de la simplificación es reducir el espacio de búsqueda de las restricciones disminuyendo, consecuentemente, el indeterminismo. La restricción c_{i+1} resultante del proceso de simplificación equivale lógicamente a la restricción c_{i} ∪ c̃ original en el sentido de que tiene las mismas soluciones sobre la estructura H/E. Si la vuelta de la función es fail, la restricción c_{i} ∪ c̃ es irresoluble.

Una configuración terminal C tiene la forma C = ⟨← c □ ⟩. Si la restricción c es E-unificable entonces representa la restricción respuesta computada correspondiente a esa derivación.

La corrección y completitud de este cálculo es consecuencia inmediata de los resultados en [12, 17], que se aplican a cualquier lenguaje que puede formalizarse como una instancia del esquema.

3La restricción vacía se representa por ⟨ ⟩.

3.2 Conjunto de Transformaciones Sintácticas

En la premisa de la regla que describe un paso de computación perezosa ⟶_{LCLP (H/E)} se evalúa la función Simplificación(c_{i}, c̃), que reduce la restricción c_{i}∪c̃ a una forma (más simple) equivalente. A continuación se describe en forma de reglas de inferencia el conjunto de transformaciones que definen esta función.

Definición 3.2.1 (relación de transición →_{Simpl}). Sea θ una sustitución. Sea E un conjunto de ecuaciones. Definimos una Simpl-configuración como un par T = ⟨ θ̂, E ⟩^{4}. Se define la relación →_{Simpl} entre restricciones mediante el siguiente sistema de transición.

(1) Regla de eliminación de ecuaciones triviales:

\frac{x ∈ V}{⟨ θ̂ , (\{x = x\} ∪ E) ⟩ →_{Simpl} ⟨ θ̂ , E ⟩}

(2) Regla de reordenación:

\frac{x ∈ V ∧ t ∉ V}{⟨ θ̂ , (\{t = x\} ∪ E) ⟩ →_{Simpl} ⟨ θ̂ , (\{x = t\} ∪ E) ⟩}

(3) Regla de eliminación de variables:

\frac{x ∈ V ∧ data(t) ∧ x ∉ V(t)}{⟨ θ̂ , (\{x = t\} ∪ E) ⟩ →_{Simpl} ⟨ θ̂.\{X/t\} , E\{X/t\} ⟩}

(4) Regla de descomposición de términos:

\frac{f ∈ C}{⟨ θ̂ , (\{f(s_{1}, …, s_{n}) = f(t_{1}, …, t_{n})\} ∪ E) ⟩ →_{Simpl} ⟨ θ̂ , (\{s_{1} = t_{1}\} ∪ … ∪ \{s_{n} = t_{n}\} ∪ E) ⟩}

(5) Regla de reescritura de términos condicional (CTR)^{5} :

\frac{(λ = ρ ⇐ ẽ) ∈ E ∧ e/u = λσ ∧ e′ = e[u ← ρσ] ∧ sσ ↓_{R} tσ ∀(s = t) ∈ ẽ}{⟨ θ̂ , (e ∪ E) ⟩ →_{Simpl} ⟨ θ̂ , (e′ ∪ E)⟩}

(6) Reglas de fallo:

\frac{f , g ∈ C ∧ f ≠ g}{⟨ θ̂ , (\{f(s_{1}, s_{2}, …, s_{n}) = g(t_{1}, t_{2}, …, t_{m})\} ∪ E) ⟩ →_{Simpl} fail}

\frac{x ∈ V ∧ data(t) ∧ x ∈ V(t) ∧ t ≠ X}{⟨ θ̂ , (\{x = t\} ∪ E) ⟩ →_{Simpl} fail}

siendo data(t) la relación definida como:

data(t) si (t ∈ C) ∨ (t ∈ V) ∨ (t = f(t_{1}, … t_{2}) ∧ f ∈ C ∧ (∀i, 1 ≤ i ≤ n, data(t_{i})))

Definición 3.2.2 (Simpl-configuración terminal T). Definimos el conjunto de Simpl-configuraciones terminales de la siguiente forma: { ⟨ θ̂ , E ⟩ / ⟨ θ̂ , E ⟩ ↛_{Simpl} } ∪ {fail}.

Es conocido que cada regla del cálculo →_{Simpl} transforma un conjunto de ecuaciones θ̂ ∪ E en otro conjunto θ̂′ ∪ E′ con el mismo conjunto de H/E-soluciones [13]. Si el cálculo termina en fail el conjunto de ecuaciones original es irresoluble. Claramente, el cálculo →_{Simpl} siempre termina para teorías ecuacionales canónicas y es independiente del orden en que hayan sido aplicadas las reglas^{6} [13]. Se debe notar la incrementalidad en el proceso de simplificación de las restricciones gracias a la representación adoptada.

4Denotamos con θ̂ la representación ecuacional {x_{1} = t_{1}, …, x_{n} = t_{n}} de la sustitución θ = {x_{1}/t_{1}, …, x_{n}/t_{n}}.

5Las variables de la cláusula (λ = ρ ⇐ ẽ) se asumen estandarizadas aparte.

6Para la terminación de la regla de reescritura condicional el sistema de reescritura debe ser decreciente en el sentido de [19, 24]. Esta propiedad es más fuerte que la de terminación y asegura la decibilidad de la relación →_{R} para sistemas de reescritura condicionales.

Definición 3.2.3 (Comportamiento del cálculo →_{Simpl}). Sea T_{0} = ⟨ θ̂ , (c ∪ c̃θ) ⟩. Definimos el comportamiento de la relación →_{Simpl} como la función:

Simplificación(⟨ θ̂ , c ⟩, c̃) = \{ \begin{matrix}⟨ θ̂′ , c′ ⟩ & si T_{0} →∗_{Simpl} ⟨ θ̂′ , c′ ⟩ \\ fail & si T_{0} →∗_{Simpl} fail \end{matrix}

El siguiente ejemplo ilustra cómo el mecanismo anteriormente descrito evita el problema de la posible no terminación de un paso de computación CLP(H/E) ansiosa.

Ejemplo 3.2.4. Consideremos el programa CLP(H/E) definido en el ejemplo 3.1. con el objetivo inicial G_{0} =← □p(b). La configuración CLP(H/E) inicial es C_{0} = ⟨← □p(b)⟩. Considerando la cláusula (p_{1}), la nueva restricción c̃_{1} es c̃_{1} = { b = f(Z) }.

El intérprete ansioso para CLP(H/E) no es capaz de producir una respuesta para el objetivo, sin embargo, teniendo en cuenta que Simplificación( ⟨ ⟩, {b = f(Z)}) = ⟨ ∅ , {b = f(Z)} ⟩ = c′_{1}, el mecanismo computacional perezoso descrito en la sección 3.1 puede probar la transición C_{0} ⟶_{LCLP (H/E)} ⟨c′_{1}□ q(Z) ⟩

Considerando ahora la cláusula (p2), la nueva restricción es c̃_{2} = {Z = a}. Teniendo en cuenta que ⟨ ∅ , ({b = f(Z)} ∪ {Z = a}) ⟩ →_{Simpl (3)} ⟨ {Z = a} , {b = f(a)} ⟩ →_{Simpl (5)} ⟨ {Z = a} , {b = a} ⟩ →_{Simpl (6^{i})} fail se tiene que c′_{2} = Simplificación(⟨ ∅ , {b = f(Z)} ⟩, {Z = a}) = fail y, como consecuencia, no es posible probar la correspondiente transición ⟶_{LCLP (H/E)}. El objetivo G_{0} fracasa, por tanto, finitamente.

Se debe notar también que nuestro concepto de derivación perezosa recupera la capacidad de computar funciones que no posee el intérprete CLP(H/E) ansioso que se obtiene como instancia de la definición estándar presentada en la sección 2.

Ejemplo 3.2.5. Sea el siguiente programa CLP(H/E) que define el número de elementos de una lista:

(e_{1}) n elementos(λ) = 0. (e_{2}) n elementos(X.T) = 1+n elementos(T). Consideremos el objetivo inicial G_{0} = ← n elementos(a.b.c) = X □. El intérprete (ansioso) que se describe en la sección 2 comprueba la satisfacibilidad de la restricción en el objetivo G_{0} y devuelve la propia restricción como respuesta. El intérprete que se describe en esta sección simplifica la restricción n elementos(a.b.c) = X computando la restricción respuesta X = 3.

3.3 Optimización del cálculo →_{Simpl}

A continuación presentamos una optimización del cálculo de simplificación de restricciones que está basado en la idea de convergencia de operadores (operator joinability) que se describe en [8]. En lo que sigue extendemos dicha noción al caso de sistemas de reescritura condicionales. En [3] se redefine este concepto en el marco formal de la teoría de la Interpretación Abstracta.

Sea R un sistema de reescritura de términos sobre la signatura Σ. Construimos un sistema de reescritura R′ derivado de R de la siguiente forma:

• Para cada r = (f(t_{1}, t_{2}, …, t_{n}) → g(s_{1}, s_{2}, …, s_{m}) ⇐ ẽ) ∈ R, se construye otra regla r′ = (f → g ⇐ out(ẽ)). Se añade al sistema de reescritura abstracto R’ cada instancia r′ρ de r′, donde ρ = {X_{1}/f_{1}, …, X_{n}/f_{n}}, siendo {X_{1}, …, X_{n}} las variables de la regla r′ y f_{1}, …, f_{n} ∈ Σ.

• Para cada r = (f(t_{1}, t_{2}, …, t_{n}) → X ⇐ ẽ) ∈ R, X ∈ V se construye la regla r′ = (f → X ⇐ out(ẽ)). Se añade al sistema de reescritura abstracto R’ cada instancia r′ρ de r′, donde ρ = {X_{1}/f_{1}, …, X_{n}/f_{n}}, siendo {X_{1}, …, X_{n}} las variables de la regla r′ y f_{1}, …, f_{n} ∈ Σ, f_{1} ≠ f.

donde out(ẽ) = {out(t) = out(s) | (t = s) ∈ ẽ} siendo out(t) el símbolo más externo de t si t ∉ V y t en cualquier otro caso.

La noción de convergencia de operadores es una noción decidible que puede ser implementada, e.g., mediante un sencillo proceso que construye el grafo de la relación →_{R′} de acuerdo con las reglas del sistema de reescritura R′. Dos símbolos de función f, g ∈ Σ son convergentes en R′, f ↓_{R′} g, si los caminos en el grafo que parten de los vértices correspondientes tienen, al menos, un vértice común [26]. Se debe notar que el conjunto de vértices de cada grafo es finito puesto que el número de reglas en R′ lo es.

Proposición 3.3.1 ([8]). Una ecuación f(t̃) = g(s̃) es satisfacible en R sólo si f ↓_{R′} g.

El cálculo →_{Simpl} puede reforzarse haciendo uso del resultado anterior con la introducción de la siguiente regla:

\frac{f ↓̸_{R′} g}{⟨ θ̂ , (\{f(s_{1}, s_{2}, …, s_{n}) = g(t_{1}, t_{2}, …, t_{m})\} ∪ E) ⟩ →_{Simpl} fail}

Ejemplo 3.3. Sea (P, E) un programa CLP(H/E) definido por las siguientes reglas: (p_{1}) p(b(Z)) ← □ q(Z). (p_{2}) q(0). (e_{1}) a(f(X)) = c(X). (e_{2}) b(f(X)) = d(X).

Sea G_{0} = ← □ p(a(X)) el objetivo inicial. La configuración inicial es C_{0} = ⟨← □ p(a(X)) ⟩. Utilizando la regla (p_{1}) del programa se tiene la restricción acumulada c̃ = { a(X) = b(Z) }. La inconsistencia de c̃ sólo puede reconocerse tras detectar la no convergencia de los operadores más externos a y b, i.e. a ↓̸_{R} b, respecto a las reglas del sistema derivado R′ = { a →_{R′} c, b →_{R′} d }. El cálculo →_{Simpl} original no detecta esta inconsistencia dado que ninguna de las reglas de transformación es aplicable a c̃.

4 Un intérprete Prolog (perezoso) para CLP(H/E)

En esta sección se presenta un intérprete Prolog (perezoso) para programas CLP(H/E). El intérprete ha sido implementado en BIM-Prolog e instalado sobre estaciones SUN-3/80.

El intérprete se define, esencialmente, mediante cuatro predicados: solve/3, ics/3, simplify/5 e inwing/3. El primero de estos predicados conduce las transiciones del nivel CLP(H/E) del intérprete. Los otros dos realizan el segundo nivel del sistema, simplificando (incrementalmente) las restricciones y detectando, en su caso, su insatisfacibilidad. El predicado inwing/3 define un procedimiento de narrowing condicional básico que se puede utilizar para comprobar la satisfacibilidad de las restricciones en cada configuración terminal.

4.1 El nivel →_{LCLP}

En la definición del modelo operacional del lenguaje se adoptó la regla de computación estándar del modelo CLP, en la que todos los átomos existentes en el objetivo se seleccionan simultáneamente [16]. Esta regla es, canónicamente, justa pero poco compatible con una interpretación eficiente. La adopción de Prolog como lenguaje de implementación ha impulsado a utilizar sus mecanismos (en particular el de ”backtracking”) para programar cómodamente la búsqueda. La implementación que se describe es, por tanto, una aproximación al modelo operacional del lenguaje.

En virtud de la propiedad de independencia de regla de computación podemos redefinir la relación de transición ⟶_{LCLP (H/E)} entre configuraciones de la siguiente forma:

\frac{\begin{matrix}(H ← c′□B̃.) ∈ P ∧ c̃ = \{c′, A_{i} = H\} ∧ \\ c′ = Simplificación(c, c̃) ∧ c′ ≠ fail \end{matrix}}{⟨← c□A_{1}, …, A_{n}⟩ ⟶_{LCLP (H/E)} ⟨← c′□A_{1}, …, A_{i−1}, B̃, A_{i+1}, …, A_{n}⟩}

donde se asume presente una regla de computación que selecciona, como subobjetivo a reducir, el átomo A_{i}, 1 ≤ i ≤ n, y una regla de búsqueda que determina qué cláusula de programa utilizar. En la implementación se utilizan las reglas estándar left-to-right y top-to-bottom en profundidad de Prolog.

Las cláusulas de programa se almacenan como cláusulas unit: clause (Head,Body,ConstrBody) correspondientes a una regla del programa Head:- ConstrBody □ Body., donde ConstrBody y Body son, respectivamente, la parte ecuacional y relacional del cuerpo de la cláusula.

Los argumentos del predicado solve/3 son: la lista de átomos a resolver, el estado de partida del simplificador de restricciones y el estado con que termina.

   solve([],ICS state,ICS state).
   solve([Goal|Restgoal],PrevICS state,NewICS state):-
       solve(Goal,PrevICS state,TempICS state),
   solve(Restgoal,TempICS state,NewICS state).
   solve(Goal,PrevICS state,NewICS state):-
       flatgoal(Goal,Flatgoal,Listeqs), clause (Flatgoal,Body,ConstrBody),
       append(Listeqs,ConstrBody,TildeConstr),

ics(PrevICS state,TildeConstr,TempICS state),
solve(Body,TempICS state,NewICS state).

El procedimiento flatgoal/3 realiza un aplanamiento del subobjetivo Goal, sustituyendo cada uno de sus argumentos por una nueva variable y añadiendo la ecuación que expresa la igualdad entre ambos a la lista de restricciones Listeqs.

flat goal(Goal,Goal,[]).
flat goal(Goal,Flat goal,[Eq|Rest eq]):-
Eq=..[=-,Arg goal,New vble], Goal=..[Pred goalArg goal|Rest arg goal],
Partial goal=..[Pred goal|Rest arg goal],
flat goal(Partial goal,Flat part goal,Rest eq),
Flat part goal=..[Pred goal|Args flat part goal],
Args flat goal=[New vble|Args flat part goal],
Flat goal=..[Pred goal|Args flat goal].

El núcleo del procedimiento solve/3 es el predicado ics/3, que define el segundo nivel del sistema.

4.2 El simplificador de restricciones →_{T RANS}

Los argumentos de ics/3 son: el estado de partida, la nueva restricción c̃ a acumular y el estado resultante que incorpora la restricción (simplificada) acumulada.

ics(PrevICS state,Tildeconstr,NewICS state):-
PrevICS state=(Constr,Hat theta), NewICS state=(Constr prima,Hat theta prima),
apply sust(Tildeconstr,Hat theta,Tilde hat constr),
append(Constr,Tilde hat constr,Tempconstr),
simplify(Hat theta,Tempconstr,Hat theta prima,Constr prima,Fail), Fail.

El predicado simplify/5 es el núcleo del simplificador. simplify/5 implementa las reglas del sistema →_{T RANS} descritas en 3.2. El quinto argumento del predicado simplify/5 informa de la detección de insatisfacibilidad.

simplify(Prev theta,Prevconstr,New theta,NewConstr,Fail):-
apply rules(Prev theta,Prevconstr,New theta,NewConstr,Fail),
(Fail, update(solv(yes)); update(solv(no))), !.

El predicado apply rules/5 aplica las reglas de transformación sintácticas a un conjunto de restricciones.

apply rules(Prev theta,Prevconstr,New theta,NewConstr,Fail):-
apply rules (Prev theta,Prevconstr,New theta,NewConstr ,Fail,[], ),
(Fail,take off(NewConstr ,NewConstr);true).
apply rules (Prev theta,[],Prev theta,Rest ,true,L,Rest):-
append(Rest,L,Rest ), !.
apply rules (Prev theta,Constr,N theta,R constr,Fail,L,NL):-
trans rule(Prev theta,Constr,(Rule used,N Constr),New theta,Fail ,L,NL ),
(Fail, \+(Rule used=none),
apply rules (New theta,N Constr,R constr,N theta,Fail,NL ,NL);
Fail=Fail ), !.
trans rule(Theta,Constr,(1,NConstr),Theta,true,L,L):-
Constr=[=-(Left,Right)|RestC], Left==Right, NConstr=RestC, !.
trans rule(Theta,Constr,(2,NConstr),Theta,true,L,L):-
Constr=[=-(Left,Right)|RestC], nonvar(Left), var(Right),
NConstr=[=-(Right,Left)|RestC], !.
trans rule(Theta,Constr,(3,NConstr),New theta,true,L,NL
Constr=[=-(Left,Right)|RestC], var(Left), data(Right),

takevbles(Right,Var Right), \+(in(Left,Var Right)), difieren(L,Left,Right,E2,NL ),
apply(Left,Right,RestC,R), append(R,E2,NConstr),
append(NL ,[=-(Left,Right)],NL ),
compose sust(Theta,[=-(Left,Right)],New theta), !.
trans rule(Theta,Constr,(4,NConstr),Theta,true,L,L):-
Constr=[=-(Left,Right)|RestC], nonvar(Left), nonvar(Right),
functor(Left,F1,A1), functor(Right,F2,A2),
irreducibles(F1,A1), irreducibles(F2,A2)
F1=F2, A1=A2, Left=..[F1|Args1], Right=..[F2|Args2],
joinargs(Args1,Args2,Listarest), append(Listarest,RestC,NConstr), !.
trans rule(Theta,Constr,(5,NConstr),Theta,true,L,L):-
Constr=[=-(Left,Right)|RestC], normal form(Left,Right,LeftN,RightN),
(\+(Left=LeftN) ; \+(Right=RightN)),
append([=-(LeftN,RightN)],RestC,NConstr), !.
trans rule(Theta,Constr,(5,NConstr),Theta,true,L,NL):-
Constr=[=-(Left,Right)|RestC],
normal form(Left,Right,LeftN,RightN),
LeftN==Left, RightN==Right,
(var(Right), append(L,[=$(Right,Left)],NL);
append(L,[=$(Left,Right)],NL)), !.
trans rule( ,Constr,('6i',unsatisfiable constraint), ,fail,L,L):-
Constr=[=-(Left,Right)|Rest], nonvar(Left), nonvar(Right),
functor(Left,F1,A1), functor(Right,F2,A2),
irreducibles(F1,A1), irreducibles(F2,A2)
(F1\ ==F2; A1\ ==A2), !.
trans rule( ,Constr,('6ii',unsatisfiable constraint), ,fail,L,L):-
Constr=[=-(Left,Right)|Rest], var(Left), data(Right),
takevbles(Right,Var Right), in(Left,Var Right), !.
trans rule(Hat theta,Constraint,(none,Constraint),Hat theta,true,L,L):- !.
difieren(L,Left,Right,E2,NL):- take eqs(L,NLL,E),
aplicaciones(E,Left,Right,E2,New), apply(Left,Right,NLL,N),
append(N,New,NL), !.
aplicaciones([],Left,Right,[],[]):- !.
aplicaciones([E1|Rest],Left,Right,E,Rest2):- apply(Left,Right,[E1],E2),
[E1]\ ==E2, aplicaciones(Rest,Left,Right,R,Rest2),
append(E2,R,E), !.
aplicaciones([E1|Rest],Left,Right,R,Rest2):- E1=..[=-,L,R],
aplicaciones(Rest,Left,Right,R,R2),
append([=$(L,R)],R2,Rest2], !.
take eqs([=$(L ,R)|R ],L,[=-(L ,R)|R ]):- take eqs(R ,L,R ).
take eqs([E|R],[E|L],R ]):- take eqs(R,L,R ), !.
take eqs([],[],[]).
take off([],[]).
take off([=$(L,R)|R ],[=-(L,R)|RR]):- take off(R ,RR), !.
take off([E|R],[E|R ]):- take off(R,R ), !.

El predicado apply sust/3 aplica un conjunto de sustituciones a un término.

apply sust(G,[],G):- !.
apply sust(G,[=-(L,R)|T],G ):-
sust(L,R,G,GG), apply sust(GG,T,G ), !.
sust(L,R,T,R):- L==T, !.
sust(L,R,T,T):- (var(T);ground(T)), !.
sust(L,R,T,T ):- T=..[F|A], sust a(L,R,A,As), T =..[F|As], !.

sust a( , ,[],[]).
sust a(L,R,[A|RA],[As|RAs]):-
    sust(L,R,A,As), sust a(L,R,RA,RAs), !.

El predicado compose sust/3 realiza la composición de dos sustituciones.

compose sust(T,[],T):- !.
compose sust([],S,S):- !.
compose sust(T,S,NT):- comp1(T,S,T1), extract var(T,VT),
    comp2(VT,S,NS), append(T1,NS,NT), !.
comp1([], ,[]):- !.
comp1([H|T],[=-(V1,T1)|Rest],[HS|R]):-
    sust(V1,T1,H,Hs), V1\ ==TS, !, comp1(Rest,T,R), !.
comp2( ,[],[]):- !.
comp2(VT,[=-(V,T)|R],NS):- in(V,VT), !, comp2(VT,R,NS), !
comp2(XT,[X|R],[X|NS]):- comp2(VT,R,NS), !.

El predicado extract var/2 extrae las variables de los pares de una sustitución.

extract var([],[]):- !.
extract var([=-(X, )|Rest],[X|R]):- extract var(Rest,R), !.

El predicado normal form/4 reduce los argumentos de una ecuación a su forma canónica.

normal form(T,S,TN,SN):-rewrite(T,TN),rewrite(S,SN),!.
rewrite(TC,TC):- write(TC),nl, var(TC),!.
rewrite(TC,TR):- TC=..[F|Arg],rewrite arg(Arg,Narg),
    TC1=..[F|Narg],rewrite term(TC1,TR).
rewrite term(TC,TR):- TC=..[F|Args m],functor(TC,F,N A),
    functor(TC prima,F,N A),rwr(TC prima,R, ,T),
    TC prima=..[F|Args prima], test(Args m,Args prima),
    Args prima = Args m, list est(T,L),call condition(L),rewrite(R,TR).
rewrite term(T,T).
rewrite arg([],[]).
rewrite arg([A1|Arg],[AR|ArgR]):-rewrite(A1,AR),rewrite arg(Arg,ArgR).
call condition([=-(I,D)|Rc]):-!,normal form(I,D,N,N), call condition(Rc),!.
call condition( ).
test([],[]):-!.
test([X|Rx],[Y|Ry]):-test term(X,Y),test(Rx,Ry),!.
test term(X,Y):-nonvar(X),nonvar(Y),X=..[F|Ax],Y=..[F|Ay],test(Ax,Ay),!.
test term(X,Y):-var(Y).
list est([],''):- !.
list est([X|[]],X):- !.
list est([H|T],E):- list est(T,E1), E=(H,E1), !.

4.3 El algoritmo de narrowing condicional

Las cláusulas de la teoría ecuacional están almacenadas como cláusulas Prolog con la siguiente forma =-(Left,Right):- Condition. Siguiendo las ideas de [6] se ha programado un procedimiento init/0 que computa el conjunto de ocurrencias no variables de las partes derechas de las cabezas de las cláusulas de la teoría ecuacional:

   init :- clause(=-(L,R),C), occ(R,OR), assertz(rwr(L,R,OR,C)),fail
   init.
   occ(T,0) :- var(T), !.
   occ(T,[1|Ann]):- T=..[F|ARG], occ1(ARG,Ann).
   occ1([],[]).
   occ1([TH|TT],[A|Ann]):- occ(TH,A), occ1(TT,Ann).

El procedimiento inwing/2 implementa un procedimiento de narrowing condicional con regla de computación left-to-right y regla de búsqueda top-to-bottom en profundidad.

   =-(T,S):- inwing(T,S).
   inwing(T,S) :- occ(T,OT), occ(S,OS), !,
       narred(T,OT,TR), narred(S,OS,SR), TR=SR.
   narred(T,O,T):- !.
   narred(TC,[1|Oarg],TR):- TC=..[F|Arg], narrarg(Arg,Oarg,Narg),
       TC1=..[F|Narg], narrterm(TC1,TR).
   narrterm(T,T).
   narrterm(TC,TR):- rwr(TC,R,OR,T), call(T), narred(R,OR,T).
   narrarg([],[].[]).
   narrarg([A1|Arg],[O1|Oarg],[AR|ArggR]):-
       narred(A1,O1,AR), narrarg(Arg,Oarg,ArgR).

5 Conclusiones

En este trabajo hemos formalizado un mecanismo computacional perezoso como semántica operacional del lenguaje CLP(H/E) que retrasa el problema de la E-unificación de las restricciones hasta alcanzar un configuración terminal. Nuestra idea de computación perezosa es semejante a la noción de resolución perezosa de [14] y a la de reducción de objetivos que se define en [12]. Este modo de computación evita el problema de la posible no terminación de un paso de computación estándar [16] motivado por la indecibilidad del problema de la satisfacibilidad ecuacional. El intérprete propuesto en este trabajo es capaz de calcular todas las respuestas que puede obtener el intérprete impaciente. Como ventaja adicional se consigue un progreso parcial, en cuanto a simplificación de la restricción respuesta computada, en cada paso de computación CLP. Esto es posible gracias a la incorporación de un conjunto de transformaciones sintácticas que, basadas en algunas reglas clásicas para el tratamiento de la unificación en teorias ecuacionales [7, 10, 14, 23] son capaces, en ocasiones, de detectar la insatisfacibilidad de la restricción.

Agradecimientos

Agradecemos profundamente la labor de nuestros revisores, cuyas valiosas indicaciones nos han permitido mejorar la presentación de este trabajo.

Referencias bibliográficas

[1] M. Alpuente and M. Falaschi. Incremental Constraint Satisfaction for Equational Logic Programming. In J. Maluszynski and M. Wirsing, editors, Proc. of PLILP’91, volume 528 of Lecture Notes in Computer Science, pages 111–122. Springer-Verlag, Berlin, 1991.

[2] M. Alpuente, M. Falaschi, and G. Levi. Incremental Constraint Satisfaction for Equational Logic Programming. Theoretical Computer Science. to appear. Extended abstract in Proc. ILPS’91 Workshop on Defeasible Reasoning and Constraint Solving, pages 47-75. San Diego, Ca., Oct. 1991.

[3] M. Alpuente, M. Falaschi, and F. Manzo. Analyses of Inconsistency for Incremental Equational Logic Programming. In Proc. of PLILP’92, Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1992.

[4] M. Alpuente and M.J. Ramírez. An Equational Constraint Logic Approach to Conceptual Modelling. In Proc. of DEXA’92, pages 26-31. Springer-Verlag, Wien New York, 1992.

[5] M. Bellia and G. Levi. The relation between logic and functional languages: a survey. Journal of Logic Programming, 3:217–236, 1986.

[6] P. Bosco, E. Giovannetti, and C. Moiso. Narrowing vs. SLD-resolution. Theoretical Computer Science, 59:3–23, 1988.

[7] H.J. Bürckert. Lazy E-unification - a method to delay alternative solutions. Technical report, Université de Nancy, France, 1987.

[8] N. Dershowitz and J. Sivakumar. Solving Goals in Equational Languages. In S. Kaplan and J.Joaunnaud, editors, Proc. First Int’l Workshop on Conditional Term Rewriting, volume 308 of Lecture Notes in Computer Science, pages 45–55. Springer-Verlag, Berlin, 1987.

[9] L. Fribourg. Slog: a logic programming language interpreter based on clausal superposition and rewriting. In Proc. Second IEEE Int’l Symp. on Logic Programming, pages 172–185. IEEE, 1985.

[10] J.H. Gallier and W. Snyder. A general complete E-unification procedure. In P. Lescanne, editor, Rewriting Techniques and Applications, volume 256 of Lecture Notes in Computer Science, pages 216–227. Springer-Verlag, Berlin, 1987.

[11] E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel Leaf: A Logic plus Functional Language. Journal of Computer and System Sciences, 42, 1991.

[12] M. Höhfeld and G. Smolka. Definite relations over constraint languages. Technical report, IBM Deutschland GmbH, Stuttgart, 1988.

[13] S. Hölldobler. Foundations of Equational Logic Programming, volume 353 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin, 1989.

[14] S. Hölldobler. Conditional equational theories and complete sets of transformations. Theoretical Computer Science, 75:85–110, 1990.

[15] H. Hussman. Unification in conditional-equational theories. Technical report, Fakultät für Mathematik und Informatik, Universität Passau, 1986.

[16] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. Technical report, Department of Computer Science, Monash University, 1986.

[17] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. Fourteenth Annual ACM Symp. on Principles of Programming Languages, pages 111–119. ACM, 1987.

[18] J. Jaffar, J.-L. Lassez, and M.J. Maher. A logic programming language scheme. In D. de Groot and G. Lindstrom, editors, Logic Programming, Functions, Relations and Equations, pages 441–468. Prentice Hall, Englewood Cliffs, NJ, 1986.

[19] S. Kaplan. Fair conditional term rewriting systems: unification, termination and confluence. In H.-J. Kreowski, editor, Recent Trends in Data Type Specification, volume 116 of Informatik-Fachberichte, pages 136–155. Springer-Verlag, Berlin, 1986.

[20] J.W. Klop. Term rewriting systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, I. Oxford University Press, 1991.

[21] J.-L. Lassez, M.J. Maher, and K. Marriott. Unification Revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587–625. Morgan Kaufmann, Ca., 1988.

[22] J.W. Lloyd. Foundations of logic programming. Springer-Verlag, Berlin, 1987. second edition.

[23] A. Martelli, C. Moiso, and G.F. Rossi. An algorithm for unification in equational theories. In Proc. IEEE Symp. on Logic Programming, pages 180–186. IEEE, 1986.

[24] A. Middeldorp and E. Hamoen. Counterexamples to completeness results for basic narrowing. To appear in Proc. Third Int’l Conf. on Algebraic and Logic Programming, 1992.

[25] P. Padawitz. Computing in Horn Clause Theories, volume 16 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, Berlin, 1988.

[26] M.J. Ramis, J. Piris, and M. Alpuente. Derivaciones perezosas en programación lógica con restricciones ecuacionales. In Proc. XVIII Conferencia Latinoaméricana de Informática PANEL’92, pages 1008-1015. Las Palmas de Gran Canaria, 1992

[27] J.H. Siekmann. Universal unification. In 7th Int’l Conf. on Automated Deduction, volume 170 of Lecture Notes in Computer Science, pages 1–42. Springer-Verlag, Berlin, 1984.

[28] H. Tamaki. Semantics of a Logic Programming Language with a Reducibility Predicate. In Proc. First IEEE Int’l Symp. on Logic Programming, pages 259–264. IEEE, 1984.

[29] P. Veloso, J. Castilho and A. Furtado. Systematic Derivation of Complementary Specifications. In Proc. 7th Int’l Conf. on Very Large Data Bases VLDB’81, Cannes, pages 309-421. IEEE Computer Society Press, 1981.

A Anexo

Ejemplo A.1. knapsack 0/1 [2]

P = { (p_{1})  knapsack(M, L, W)  ← addweight(M) = W □ sublist(M, L).

(p_{2}) sublist([ ], Z). (p_{3}) sublist([X | Y], [X | Z]) ← □ sublist(Y, Z). (p_{4}) sublist(Y, [X | Z]) ← □ sublist(Y, Z). }

E = { (e_{1}) 0 + y = y.

(e_{2}) s(x) + y = s(x + y). (e_{3}) weight(a) = s(s(s(0))). (e_{4}) weight(b) = s(s(0)). (e_{5}) weight(c) = s(s(0)). (e_{6}) addweight([ ]) = 0. (e_{7}) addweight([X | Y]) = weight(X) + addweight(Y). }

En la siguiente tabla se compara el comportamiento de:

• un intérprete eager (no incremental), que utiliza un procedimiento de narrowing condicional básico como núcleo del constraint solver que (semi-)decide la solubilidad de las restricciones, y

• varios intérpretes lazy, que retrasan el problema de la E-unificabilidad de las ecuaciones hasta haber resuelto completamente el resto de átomos en el objetivo.

Las abreviaturas empleadas en la tabla son las siguientes:

E  intérprete eager, sin optimizaciones.
MM  intérprete lazy, con reglas Martelli-Montanari + reescritura condicional (CTR)
MM + Dz  MM + regla non-joinability Dershowitz [3].
MM + Dz + aN MM + Dz + regla abstract Narrowing [3].
iEA  intérprete lazy incremental, con iEA como solver [3].

Los intérpretes MM + Dz + aN e iEA incorporan una regla de narrowing abstracto optimizado, en el que cada nodo del árbol se simplifica antes de un paso de narrowing (detectándose, posiblemente, su insatisfacibilidad). Para la simplificación se utiliza un conjunto →_{Simpl} de reglas formado por las reglas de Martelli-Montanari, reescritura condicional (CTR) y la regla de non-joinability de Dershowitz. Para los benchmarks eliminamos a veces la regla CTR para potenciar la mejora producida por la incrementalidad en la construcción del árbol.

Los tiempos de la tabla se dan en segundos sobre una SUN 3/80 workstation con 16 Mbytes de RAM.

Λ \underline{Tabla de Tiempos I}

g_{1}  no  ∞  no  0.48  no  0.58
no  ∞  no  ∞
g_{5}  X = addw([a, b])  2.30  X = 5  2.86  X = 5  2.40
g_{6}^{7}  no  3.20  no  ∞  no  0.96

E  MM  MM + Dz Goal  answer  CPU  answer  CPU  answer  CPU g_{2}^{7}  no  0.41  no  ∞  no  0.42 g_{3}^{8}  no  ∞  Y + s(0) = 0  0.18  Y + s(0) = 0  0.30 g_{4}  M = [a]  1.72  M = [a]  2.00  M = [a]  2.48 g_{5},g_{2}  no  33.52  no  ∞  no  17.72 g_{5},g_{6}  no  16.32  no  ∞  no  20.98

Λ \underline{Tabla de Tiempos I (cont.)}

MM + Dz + aN  iEA
CTR ∉ →_{Simpl}  CTR ∈ →_{Simpl}  CTR ∉ →_{Simpl}  CTR ∈ →_{Simpl}
Goal  answer  CPU  answer  CPU  answer  CPU  answer  CPU
g_{1}  no  32.12  no  0.50  no  30.72  no  0.46
g_{2}  no  3.10  no  0.42  no  3.22  no  0.36
g_{3}^{8}  no  3.22  no  0.94  no  3.50  no  1.08
g_{4}  M = [a]  3.24  M = [a]  2.82  M = [a]  3.76  M = [a]  3.56
g_{5}  X = addw([a,b])  2.52  X = 5  2.58  X = addw([a,b])  2.62  X = 5  2.46
g_{6}  no  1.42  no  1.00  no  1.47  no  1.16
g_{5},g_{2}  no  53.22  no  18.82  no  50.98  no  15.40
g_{5},g_{6}  no  25.72  no  21.48  no  22.38  no  19.04

Goals:

g_{1} : knapsack([a|M], [a, b, c], s(0)) c_{0_{1}} : s(0) = addweight([a|M]) Unsolvable
g_{2} : knapsack([ ], [a, b, c], weight(Y)) c_{0_{2}} : weight(Y) = addweight([ ]) Unsolvable
g_{3} : knapsack([ ], [a, b, c], Y + s(0)) c_{0_{3}} : Y + s(0) = addweight([ ]) Unsolvable
g_{4} : knapsack(M, [a, b, c], s(s(s(0)))) c_{0_{4}} : s(s(s(0))) = addweight(M) Solvable
g_{5} : knapsack([a, b], [a, b, c], X)  c_{0_{5}} : X = addweight([a, b])  Solvable
g_{6} : knapsack([b], [ ], s(s(0)))  c_{0_{6}} : s(s(0)) = addweight([b])  Solvable

Ejemplo A.2. [3]

P = {

p_{1}) p(X) ⇐ h(f(X)) = Y, f(Z) = c(W) □.
p_{2})  q(X) ⇐ f(g(X)) = c(0), h(f(Y)) = s(0) □.
p_{3})  qq(X) ⇐ c(f(X)) = f(c(Y))  □.
p_{4})  m(X) ⇐ f(X) = c(g(h(Y)))  □. }

R = {  R_{A} = {
r_{1})  h(0)  → s(0).  r_{1_{A}})  h(0)  → s(0).
r_{2})  h(c(0)) → 0.  r_{2_{A}})  h(c(0)) → 0.
r_{3})  h(f(X)) → X ⇐ g(X) = X.  r_{3_{A}})  h(f(X)) → X ⇐ g(X) = X.
r_{4})  f(0)  → c(0).  r_{4_{A}})  f(0)  → c(0).
r_{5})  f(c(X)) → c(f(X)).  r_{5_{A}})  f(c(X)) → c(⊥).
r_{6})  g(0)  → 0.}  r_{6_{A}})  g(0)  → 0. }

Tabla de Tiempos II

E  MM + Dz^{8}  MM + Dz + aN  iEA
Goal  answer  CTR ∉ →_{Simpl} CTR ∈ →_{Simpl}  CTR ∉ →_{Simpl} CTR ∈ →_{Simpl}
p(X)  Y=h(f(X))  0.38  0.26  0.86  0.76  0.94  0.88
q(X)  no  ∞  ∞  12.70  5.08  12.00  5.18
qq(X)  c(f(X))=f(c(Y)) 0.38  0.32  0.38
f(X)=f(Y)  0.22  0.28  0.40
m(X), q(Z)  no  ∞  ∞  3343.52  351.78  3306.94  339.74
m(X), qq(Z) f(X)=c(g(h(Y)))
c(f(Z))=f(c(X1)) 0.78 5.50 2.38

f(X)=c(g(h(Y)))

f(Z)=f(X1) 0.54 12.50 2.48
m(X), p(Z)  f(X)=c(g(h(Y)))
X1=h(f(Z))  0.80  0.58  46.32  40.42  3.20  2.99

7El intérprete perezoso MM entra en un camino de derivación CLP infinita por aplicación de la cláusula de programa (p_{4}) mientras el intérprete impaciente, basado en narrowing, detecta la irresolubilidad de la restricción y tiene un espacio de búsqueda finito.

8Los intérpretes perezosos MM y MM + Dz computan una restricción simplificada (irresoluble) en tiempo finito. Sin embargo el procedimiento de narrowing, que se utiliza al final de cada derivación para (semi-)decidir qué respuestas computadas son correctas, entra en ciclo sin reconocer su insatisfacibilidad. Los intérpretes MM + Dz + aN e iEA reconocen el fallo en un tiempo finito.

Ejemplo A.3. Agencia de Empleo [4]

% SPEC agbd

% IRREDUCIBLES

%  a  / 0
%  b  / 0
%  nil  / 0
%  apply  / 2
%  offer  / 3
%  hire  / 3

% FUNCTIONS

%  fire  / 3
%  freepos  / 2
%  pcapply  / 2
%  pcoffer  / 3
%  pchire  / 3
%  pcfire  / 3

% PREDICATES

%  iscand  / 2
%  isemployee  / 2
%  worksfor  / 3
%  haspos  / 2

% RELATIONAL CLAUSES^{9}

iscand(X,apply(Z,T))  ← X=Z, pcapply(Z,T)  □.
iscand(X,apply(Z,T))  ← ¬(X=Z), pcapply(Z,T)  □ iscand(X,T).
iscand(X,offer(W,M,T))  ← pcoffer(W,M,T)  □ iscand(X,T).
iscand(X,hire(Z,W,T))  ← ¬(X=Z), pchire(Z,W,T)  □ iscand(X,T).
isemployee(X,apply(Z,T))  ← ¬(X=Z), pcapply(Z,T)  □ isemployee(X,T).
isemployee(X,offer(W,M,T))  ← pcoffer(W,M,T)  □ isemployee(X,T).
isemployee(X,hire(Z,W,T))  ← X=Z, pchire(Z,W,T)  □.
isemployee(X,hire(Z,W,T))  ← ¬(X=Z), pchire(Z,W,T)  □ isemployee(X,T).
worksfor(X,Y,apply(Z,T))  ← ¬(X=Z), pcapply(Z,T)  □ worksfor(X,Y,T).
worksfor(X,Y,offer(W,N,T))  ← pcoffer(W,N,T)  □ worksfor(X,Y,T).
worksfor(X,Y,hire(Z,W,T))  ← X=Z, Y=W, pchire(Z,W,T)  □.
worksfor(X,Y,hire(Z,W,T))  ← ¬(X=Z), pchire(Z,W,T)  □ worksfor(X,Y,T).
haspos(Y,apply(Z,T))  ← pcapply(Z,T)  □ haspos(Y,T).
haspos(Y,offer(W,N,T))  ← Y=W, pcoffer(W,N,T)  □.
haspos(Y,offer(W,N,T))  ← ¬(Y=W), pcoffer(W,N,T)  □ haspos(Y,T).
haspos(Y,hire(Z,W,T))  ← Y=W, freepos(Y,T)>1,pchire(Z,W,T) □.
haspos(Y,hire(Z,W,T))  ← ¬(Y=W), pchire(Z,W,T)  □ haspos(Y,T).

9El tratamiento de la negación en CLP(H/E) es ecuacional. La información negativa se incorpora en forma de reglas de reescritura que se utilizan para reducir las restricciones a false. Las expresiones ¬P en las reglas siguientes debe entenderse, por tanto, como la versión azucarada de P = false.

% EQUATIONAL CLAUSES

apply(Z,T) = T  ← ¬pcapply(Z,T).
offer(W,M,T) = T  ← ¬pcoffer(W,M,T).
hire(X,Y,T) = T  ← ¬pchire(X,Y,T).
fire(X,Y,apply(Z,T)) = apply(Z,fire(X,Y,T))  ← pcapply(Z,T), pcfire(X,Y,apply(Z,T)).
fire(X,Y,offer(W,M,T)) = offer(W,M,fire(X,Y,T)) ← pcoffer(W,M,T), pcfire(X,Y, offer(W,M,T)).
fire(X,Y,hire(Z,W,T)) = T  ← X=Z, W=Y, pchire(Z,W,T), pcfire(X,Y,hire(Z,W,T)).
fire(X,Y,hire(Z,W,T)) = hire(Z,W,fire(X,Y,T))  ← ¬(X=Z), pchire(Z,W,T), pcfire(X,Y,hire(Z,W,T)).
fire(X,Y,T) = T  ← ¬pcfire(X,Y,T).

freepos(Y,nil) = 0.

freepos(Y,apply(Z,T)) = freepos(Y,T)  ← pcapply(Z,T).
freepos(Y,offer(W,N,T)) = freepos(Y,T)+N  ← Y=W, pcoffer(W,N,T).
freepos(Y,offer(W,N,T)) = freepos(Y,T)  ← ¬(Y=W), pcoffer(W,N,T).
freepos(Y,hire(Z,W,T)) = freepos(Y,T)-1  ← Y=W, pchire(Z,W,T).
freepos(Y,hire(Z,W,T)) = freepos(Y,T)  ← ¬(Y=W), pchire(Z,W,T).

pcapply(X,nil).

¬pcapply(X,apply(Z,T))  ← X=Z, pcapply(Z,T).
pcapply(X,apply(Z,T)) = pcapply(X,T)  ← ¬(X=Z), pcapply(Z,T).
pcapply(X,offer(W,M,T)) = pcapply(X,T)  ← pcoffer(W,M,T).
¬pcapply(X,hire(Z,W,T))  ← X=Z, pchire(Z,W,T).
pcapply(X,hire(Z,W,T)) = pcapply(X,T)  ← ¬(X=Z), pchire(Z,W,T).
pcoffer(W,M,T)  ← M>0.
¬pcoffer(W,M,T)  ← ¬(M>0).
pchire(X,Y,T) = pchire (X,Y,T)  ← freepos(Y,T) > 0.
¬pchire(X,Y,T)  ← ¬freepos(Y,T) > 0.

¬pchire (X,Y,nil).

pchire (X,Y,apply(Z,T))  ← X=Z, pcapply(Z,T).
pchire (X,Y,apply(Z,T)) = pchire (X,Y,T)  ← ¬(X=Z), pcapply(Z,T).
pchire (X,Y,offer(W,M,T)) = pchire (X,Y,T)  ← pcoffer(W,M,T).
¬pchire (X,Y,hire(Z,W,T))  ← X=Z, pchire (Z,W,T).
pchire (X,Y,hire(Z,W,T)) = pchire (X,Y,T)  ← ¬(X=Z), pchire (Z,W,T).

¬pcfire(X,Y,nil).

¬pcfire(X,Y,apply(Z,T))  ← X=Z, pcapply(Z,T).
pcfire(X,Y,apply(Z,T)) = pcfire(X,Y,T)  ← ¬(X=Z), pcapply(Z,T).
pcfire(X,Y,offer(W,N,T)) = pcfire(X,Y,T)  ← pcoffer(W,N,T).
pcfire(X,Y,hire(Z,W,T))  ← X=Z, Y=W, pchire(Z,W,T).
pcfire(X,Y,hire(Z,W,T)) = pcfire(X,Y,T)  ← ¬(X=Z), pchire(Z,W,T).

% ENDSPEC

Tabla de Tiempos III Goals:

E  MM + Dz + aN  iEA Goal  answer  CTR ∉ →_{Simpl} CTR ∈ →_{Simpl}  CTR ∉ →_{Simpl} CTR ∈ →_{Simpl} g_{1}  no  1.20  0.72  0.68  0.74  0.74 g_{2}  no  2.72  6.84  3.12  6.68  3.20 g_{3}  X=a  0.26  1.22  0.52  1.40  0.78

no  3.80  7.08  5.06  7.38  5.80 g_{4}  X=a  0.26  1.22  0.54  1.42  0.78

no  4.10  6.72  5.30  7.08  5.80 g_{5}  X=a  0.36  1.60  0.58  1.58  0.90

X=b  1.28  6.84  3.38  8.42  4.62 no  5.04  18.16  13.18  21.62  13.94 g_{6}  X=a  0.42  1.42  0.64  1.60  0.94

Y=a X ≠ a  1.38  7.74  4.32  8.22  4.78

no  11.40  19.34  14.44  21.58  14.82 g_{4},g_{2}  no  oveflow  19.36  11.06  19.02  10.62

g_{1} : iscand(a, nil) g_{2} : iscand(a, apply(b, nil)) g_{3} : iscand(X, apply(a, nil)) g_{4} : iscand(a, apply(X, nil)) g_{5} : iscand(X, apply(a, apply(b, nil))) g_{6} : iscand(a, apply(X, apply(Y, nil)))

Conclusiones:

• Comparación Eager / Lazy

– Los intérpretes lazy computan todas las respuestas que puede obtener el intérprete eager.

– Las reglas de simplificación y fallo de los intérpretes lazy son capaces, en ocasiones, de detectar la insatisfacibilidad de la restricción evitando el posible problema de la no terminación de un paso de derivación eager (ver tabla I, goal g_{1}, ∞ ÷ 0.48).

– Como ventaja adicional, se consigue un progreso parcial, en cuanto a simplificación de la restricción respuesta computada, en cada paso de derivación CLP. Se recupera la capacidad de computar funciones propia de todo lenguaje ecuacional (ver tabla I, goal g_{5}, X = addweight([a, b]) ÷ X = 5).

– El retraso del test de solubilidad puede, sin embargo, producir un espacio de búsqueda (para la resolución lazy CLP) infinito, cuando el espacio de la resolución eager CLP era finito (ver tabla I, goal g_{6}, 3.20 ÷ ∞).

• Comparación MM / MM + Dz / MM + Dz + aN

– No podemos establecer un resultado general para la mejora en eficiencia producida por la incorporación de la regla de narrowing abstracto ya que depende fuertemente de los ejemplos seleccionados.

∗ Si las reglas de MM ya reconocían el fallo, simplemente no hay sobrecarga en tiempo (ver tabla I, goal g_{1}, 0.48 ÷ 0.58).

∗ En el caso en que sólo la regla de narrowing abstracto sea capaz de detectar el fallo, se consigue una mejora decisiva en los tiempos (ver tabla I, goal g_{3}, ∞ ÷ 0.94).

∗ En caso de no detectar fallo, el resultado variará para cada programa en particular, dependiendo de la relación entre el tiempo invertido en intentar la detección del fallo, y el comportamiento del procedimiento de narrowing que analizara la misma restricción. En el caso general, la sobrecarga no es muy grande, mientras puede evitar una derivación infinita y/o el riesgo de computar respuestas incorrectas.

• Comparación MM + Dz + aN / iEA

– La construcción incremental del árbol de búsqueda puede ser una buena optimización. Ha conseguido mejorar significativamente los tiempos (ver tabla II, goal (m(X), p(Z)), 46.32÷3.20 y 40.42 ÷ 2.99). La bondad de la técnica depende del ratio entre la reducción del espacio de búsqueda debida a la poda y la sobrecarga debida a la computación de la función merge. La estrategia resulta efectiva en los casos en que las restricciones no se demuestran irresolubles con las reglas de MM + Dz y los grafos de narrowing abstracto presentan suficientes ramas de fallo a la izquierda de la primera rama de éxito. Para este caso, la exploración incremental del grafo de narrowing abstracto para las restricciones acumuladas tiene un coste menor que el que se requiere para explorar el grafo completo en cada paso de computación. La mejora se aprecia tanto más cuantas menos variables comparten las restricciones. Cuando el narrowing es normalizante el efecto puede resultar inapreciable.