Design and implementation of a modular interface to integrate CLP and tabled execution

Abstract

Logic programming (LP) is a family of high-level programming languages which provides high
expressive power. With LP, the programmer writes the properties of the result and / or executable
specifications instead of detailed computation steps.
Logic programming systems which feature tabled execution and constraint logic programming
have been shown to increase the declarativeness and efficiency of Prolog, while at the same time
making it possible to write very expressive programs. Tabled execution avoids infinite failure in
some cases, while improving efficiency in programs which repeat computations. CLP reduces the
search tree and brings the power of solving (in)equations over arbitrary domains.
Similarly to the LP case, CLP systems can also benefit from the power of tabling. Previous implementations
which take ful advantage of the ideas behind tabling (e.g., forcing suspension, answer
subsumption, etc. wherever it is necessary to avoid recomputation and terminate whenever possible)
did not offer a simple, well-documented, easy-to-understand interface. This would be necessary
to make the integratation of arbitrary CLP solvers into existing tabling systems possible. This
clearly hinders a more widespread usage of the combination of both facilities.
In this thesis we examine the requirements that a constraint solver must fulfill in order to be interfaced
with a tabling system. We propose and implement a framework, which we have called
Mod TCLP, with a minimal set of operations (e.g., entailment checking and projection) which the
constraint solver has to provide to the tabling engine.
We validate the design of Mod TCLP by a series of use cases: we re-engineer a previously existing
tabled constrain domain (difference constraints) which was connected in an ad-hoc manner
with the tabling engine in Ciao Prolog; we integrateHolzbauer’s CLP(Q) implementationwith Ciao
Prolog’s tabling engine; and we implement a constraint solver over (finite) lattices. We evaluate its
performance with several benchmarks that implement a simple abstract interpreter whose fixpoint
is reached by means of tabled execution, and whose domain operations are handled by the
constraint over (finite) lattices, where TCLP avoids recomputing subsumed abstractions.---ABSTRACT---La programación lógica con restricciones (CLP) y la tabulación son extensiones de la programación
lógica que incrementan la declaratividad y eficiencia de Prolog, al mismo tiempo que
hacen posible escribir programasmás expresivos.
Las implementaciones anteriores que integran completamente ambas extensiones, incluyendo
la suspensión de la ejecución de objetivos siempre que sea necesario, la implementación de inclusión
(subsumption) de respuestas, etc., en todos los puntos en los que sea necesario para evitar
recomputaciones y garantizar la terminación cuando sea posible, no han proporcionan una interfaz
simple, bien documentada y fácil de entender. Esta interfaz es necesaria para permitir integrar
resolutores de CLP arbitrarios en el sistema de tabulación. Esto claramente dificulta un uso más
generalizado de la integración de ambas extensiones.
En esta tesis examinamos los requisitos que un resolutor de restricciones debe cumplir para ser
integrado con un sistema de tabulación. Proponemos un esquema (y su implementación), que
hemos llamadoMod TCLP, que requiere un reducido conjunto de operaciones (en particular, y entre
otras, entailment y proyección de almacenes de restricciones) que el resolutor de restricciones
debe ofrecer al sistema de tabulación.
Hemos validado el diseño de Mod TCLP con una serie de casos de uso: la refactorización de un
sistema de restricciones (difference constraints) previamente conectado de un modo ad-hoc con
la tabulación de Ciao Prolog; la integración del sistema de restricciones CLP(Q) de Holzbauer; y
la implementación de un resolutor de restricciones sobre retículos finitos. Hemos evaluado su
rendimiento con varios programas de prueba, incluyendo la implementación de un intérprete
abstracto que alcanza su punto fijo mediante el sistema de tabulación y en el que las operaciones
en el dominio son realizadas por el resolutor de restricciones sobre retículos (finitos) donde TCLP
evita la recomputación de valores abstractos de las variables ya contenidos en llamadas anteriores.