A Fully Sound Goal Solving Calculus for the Cooperation of Solvers in the CFLP Scheme
Sonia Estévez Martín, Antonio J. Fernández, Maria Teresa Hortalá González, Mario Rodrı́guez Artalejo, Rafael del Vado Vírseda · Electronic Notes in Theoretical Computer Science · 2007
The C F L P scheme for Constraint Functional Logic Programming has instances C F L P ( D ) corresponding to different constraint domains D . In this paper, we propose an amalgamated sum construction for building coordination domains C , suitable to represent the cooperation among several constraint domains D 1 , … , D n via a mediatorial domain M . Moreover, we present a cooperative goal solving calculus for C F L P ( C ) , based on lazy narrowing, invocation of solvers for the different domains D i involved in the coordination domain C , and projection operations for converting D i constraints into D j constraints with the aid of mediatorial constraints (so-called bridges) supplied by M . Under natural correctness assumptions for the projection operations, the cooperative goal solving calculus can be proved fully sound w.r.t. the declarative semantics of C F L P ( C ) . As a relevant concrete instance of our proposal, we consider the cooperation between Herbrand, real arithmetic and finite domain constraints.