Lazy Derivations in Equational Constraint Logic Programming
Author
María José Ramis, Javier Piris and María Alpuente
Abstract
El lenguaje
CLP(H/E) es una instancia del esquema CLP que
resuelve ecuaciones bajo una teoría de la igualdad presentada como
una teoría ecuacional de Horn E. 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,
hemos definido 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.
Keywords
Equational constraint logic programming,
term rewriting systems, equational unification, lazy resolution.