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.