Under consideration for publication in Theory and Practice of Logic Programming

1

arXiv:cs/0511090v2 [] 14 Jan 2006

Integration of Declarative and Constraint
Programming
PETRA HOFSTEDT and PETER PEPPER
Technische Universität Berlin, Sekr. FR 5-13, Franklinstr. 28/29, D-10587 Berlin
(e-mail: {ph,pepper}@cs.tu-berlin.de)
submitted 18 December 2003; revised 20 February 2005, 25 November 2005; accepted 13
January 2006

Abstract
Combining a set of existing constraint solvers into an integrated system of cooperating
solvers is a useful and economic principle to solve hybrid constraint problems. In this paper
we show that this approach can also be used to integrate different language paradigms
into a unified framework. Furthermore, we study the syntactic, semantic and operational
impacts of this idea for the amalgamation of declarative and constraint programming. To
appear in Theory and Practice of Logic Programming (TPLP).
KEYWORDS: declarative languages, constraints, cooperative constraint solving, language
integration, multiparadigm constraint programming languages

1 Introduction
Declarative programming languages base on the idea that programs should be as
close as possible to the problem speciﬁcation and domain. In particular, the semantics of the computation does not depend on the concepts of time and state.
Programs of these languages usually consist of directly formulated mathematical
objects, i. e. of predicates and functions in logic and functional (logic) languages
resp. which are used to describe properties of problems and required solutions.
Our point of view is to consider declarative programming as constraint programming: Syntactically this is evident. Logic languages are based on predicates, and
goals (on these predicates) are constraints. For functional languages the underlying equality relations can be regarded as constraints as well. But this point of
view also applies to the (operational) semantics: the evaluation of expressions in
logic and functional languages consists of their stepwise transformation to a normal
form, while particular knowledge is collected (in the form of substitutions). This
corresponds to a stepwise propagation of constraints.
This kind of consideration opens an interesting potential: In (Hofstedt 2000b)
a framework for cooperating constraint solvers has been introduced which allows
the integration of arbitrary solvers and the handling of hybrid constraints. Considering declarative programming as constraint programming and looking at the

2

Petra Hofstedt and Peter Pepper

language evaluation mechanisms as constraint solvers we are able to integrate these
solvers into this framework. Within the framework it is then possible to extend the
declarative languages by constraint systems and, thus, to build constraint languages
customised for a given set of requirements for a comfortable modelling and solving
of many problems. The paper elaborates this approach.
We start with a recapitulation of necessary concepts and elements of the syntax and semantics of declarative languages in Sect. 2. Section 3 reintroduces the
framework for cooperating solvers of Hofstedt (2000b). In Sect. 4 we examine the
integration of a functional logic language and consider the approach w. r. t. a logic
language. We conclude our paper with a discussion of the gains and perspectives of
the approach in Sect. 5 and compare it with related work.

2 Declarative Programming Languages
Declarative languages are roughly distinguished into functional, logic, and constraint programming languages.
All declarative languages base on the concepts of signatures and terms.
Definition 2.1. A signature Σ = (S, F, R) consists of a set S of sorts, a set F of
S-sorted function symbols and a set R of S-sorted predicate symbols. R contains
in particular equality symbols for every sort s ∈ S and the predicate symbols true
and f alse.
By T (F, X) we denote the usual set of free F -terms, short: terms, over the set
X of S-sorted variables. Variable-free terms are called ground terms. Expressions
r(t1 , . . . , tn ) with terms ti and a predicate symbol r ∈ R as outermost symbol are
called predicate terms. By T (Σ, X) we denote the set of terms and predicate terms.
Given a Σ-structure D we obtain the usual notions of the value of a ground term
t in D and of the validity of a predicate term p in D, denoted as D  p. ✁
In connection with the evaluation of programs the well-known notions of substitutions and uniﬁers play a central role. We brieﬂy recall their main aspects.
Definition 2.2. By t[t′ ] we denote a term t with a distinguished subterm t′ . (This
can be formally deﬁned using either positions or contexts.)
A substitution σ is a sort-preserving association {x1 = t1 , . . . , xm = tm } from
variables xi ∈ X to terms ti ∈ T (F, X). (Since it ﬁts more nicely into our overall
framework and therefore simpliﬁes some of the later presentations, we write substitutions here as special equations.) The application of a substitution σ to a term or
predicate term e is denoted as σ(e).
A unifier of two terms or predicate terms t and t′ is a substitution σ which makes
them equal: σ(t) = σ(t′ ). The most general uniﬁer is denoted as mgu(t, t′ ).
The composition of some substitutions σ and φ is deﬁned by (σ ◦ φ)(x) = σ(φ(x))
for all x ∈ X. A substitution σ is idempotent, if σ ◦ σ = σ holds.
The parallel composition ↑ of idempotent substitutions is deﬁned as in (Palamidessi 1990),
i. e. (σ ↑ φ) = mgu(σ, φ). (Since we consider substitutions as special equations, mgu
is deﬁned for them.) ✁

Integration of Declarative and Constraint Programming

3

Starting from the foundation T (Σ, X) we build a hierarchy of language paradigms.
constraint functional (logic)
functional logic
functional

constraint logic
constraint

logic

T (Σ, X)
In the following we brieﬂy sketch the syntax and the underlying ideas of this
hierarchy. In the subsequent sections we will then address the much more important
issues of the semantic and operational integration of the diﬀerent paradigms.
Functional programming. The realm of functional programming languages (examples are haskell (Hudak et al. 2000) and opal (Didrich et al. 1994)) is inhabited by a plethora of syntactic variations. For our conceptual treatment we can
constrain this to a minimal core that is as close as possible to the other kinds of
languages that we are treating here. In the following, we distinguish two (disjoint)
subsets of the set F of function symbols of the signature Σ: the set ∆ ⊆ F of
constructors of the underlying data types and the set Φ ⊆ F of defined functions.
Definition 2.3. A functional program P over Σ is given by a ﬁnite set of rules of
the form (called pattern-based definitions)
f (t1 , . . . , tn ) → t
where f ∈ Φ is a deﬁned function and the parameter terms ti ∈ T (∆, X) are linear
constructor terms, i. e. are built up from constructors and variables such that every
variable occurs only once. The right-hand side t ∈ T (F, X ′ ) is an arbitrary F -term,
restricted to those variables X ′ ⊆ X that actually occur on the left-hand side. ✁
The evaluation of a functional program P reduces a given ground term e using the
rules of P until a normal form is obtained (Field and Harrison 1988). Each reduction step picks some function call f (e′1 , . . . , e′n ), that is, a subterm of e[f (e′1 , . . . , e′n )],
which can be uniﬁed with the left-hand side of some rule f (t1 , . . . , tn ) → t. The
resulting uniﬁer σ = mgu(f (t1 , . . . , tn ), f (e′1 , . . . , e′n )) is then applied to the righthand side t to derive the new term e[σ(t)].
Since there may be diﬀerent applicable rules for a chosen subterm caused by
overlapping left-hand sides, the rule selection strategy – e. g. ﬁrst-ﬁt or best-ﬁt – of
the language ensures a deterministic rule choice.
Moreover, there are diﬀerent reduction strategies for picking a redex in each
step, for example leftmost-innermost, leftmost-outermost, lazy, etc. These strategies lead to quite diﬀerent semantics as has already been studied extensively in
(Manna 1974). These diﬀerences are mainly reﬂected in the model-theoretic interpretation of the equality t1 = t2 of the functional domain. For the following

4

Petra Hofstedt and Peter Pepper

illustrating examples an intuitive understanding of equality will do. A thorough
elaboration will be given in Sect. 4.
Example 2.1. The following functional program provides rules for the addition of
natural numbers which are represented by the constructors 0 and s.
add(0,X)
→X
add(s(X),Y) → s(add(X,Y))

(1)
(2)

This leads e. g. to the following evaluation sequence, where the reduced subterms
are underlined:
add(s(0),s(s(0))) ❀(2) s(add(0,s(s(0)))) ❀(1) s(s(s(0))) ✁
Since we will use it later on, we present a second example here. It comes from
the realm of resistors and their composition.
Example 2.2. For describing the composition of resistors we have three constructor
functions: a simple resistor, sequential composition, and parallel composition. The
laws of physics entail the program rules:
rc(simple(X)) → X
rc(seq(R1, R2)) → rc(R1) + rc(R2)
rc(par(R1, R2)) → 1/(1/rc(R1) + 1/rc(R2))
This allows e. g. the following evaluation:
rc(par(simple(300), simple(600))) ❀ 1/(1/rc(simple(300))+1/rc(simple(600)))
❀ 1/(1/300 + 1/600) ❀ 200 ✁
Functional logic programming. Functional logic programming was originally
developed as an extension of functional languages by concepts of logic languages, cf.
(Reddy 1985; Loogen 1995). However, they can as well be considered as embedding
functional concepts into a logic language, which is indicated by the dashed connection in the above diagram. Typical representatives are babel (Moreno-Navarro and Rodrı́guez-Artalejo 1992)
and curry (Hanus et al. 2003).
Syntactically, a functional logic program looks like a functional program. The
diﬀerence lies in the evaluation mechanism. Whereas functional programs only allow
the reduction of ground terms to normal forms, functional logic programs also allow
the solving of equations using residuation (Aı̈t-Kaci and Nasr 1989) and narrowing
(Hanus 1994).
A narrowing step is a transition e[l′ ] ❀l→r,σ σ(e[r]), where l → r is a rule from
the program P and l′ is a non-variable term (i. e. l′ ∈
/ X) such that σ = mgu(l′ , l).
Example 2.3. We again use the above addition example. In order to solve the
equation add(s(A), B) = s(s(0)), we apply narrowing. The chosen subterm is underlined.
add(s(A),B) = s(s(0)) ❀(2),{X1=A,Y1=B} s(add(A,B)) = s(s(0))
❀(1),{A=0,X2=B} s(B) = s(s(0))
Thus, a solution of the initial equation is given by the substitution σ(A) = 0 and

Integration of Declarative and Constraint Programming

5

σ(B) = s(0) which is computed by uniﬁcation of s(B) and s(s(0)) after the last
narrowing step. ✁
We need to ensure conﬂuence of the rewrite system which is essential for completeness. Thus, the rules of functional logic programs usually must satisfy particular
conditions, e. g. linearity of the left-hand sides, no free variables in the right-hand
sides and (weak) nonambiguity for lazy languages, cf. (Hanus 1994).
An overview of functional logic programming languages is given in (Hanus 1994),
where the following assessment is made: “In comparison with pure functional languages, functional logic languages have more expressive power due to the availability
of features like function inversion, partial data structures, and logic variables. In
comparison with pure logic languages, functional logic languages have a more efﬁcient operational behaviour since functions allow more deterministic evaluations
than predicates.”
It should not come as a surprise that the aforementioned semantic intricacies of
functional languages carry over to functional logic programming, leading to notions
such as innermost narrowing and the like, cf. (Hanus 1994). But there are more
severe problems, which are often ignored in the literature. Consider the example
from (Hanus 1994).
Example 2.4. Consider the following program
f(X) → a
g(a) → a
For the equation f(g(X)) = a innermost narrowing yields the substitution {X = a} as
the only solution, whereas outermost narrowing provides the identity substitution
{} as solution. However, this depends on the language semantics. In most functional
languages the function g would be considered undeﬁned for all arguments but a
(since there are no patterns for the other cases). And in a call-by-value semantics
this would entail that {X = a} is the only solution. This illustrates that call-by-name
or call-by-need semantics is incompatible with innermost strategies (Manna 1974).
These observations will play a role in our later considerations in Sect. 4. ✁
Logic programming. By contrast to functional programming, logic programming
is based on predicate terms.
Definition 2.4. A logic program P is a set of rules of the form
q0 (t0,1 , . . . , t0,m ) :- q1 (t1,1 , . . . , t1,n ), . . . , qk (tk,1 , . . . , tk,r ), k ≥ 0.
where the qi (. . .) are predicate terms and they are called atoms. The borderline
case k = 0, which has no conditions, is called a fact. ✁
The evaluation of a logic program is based on resolution. One starts with a goal
(R1 ∧ . . . ∧ Rl ), which is a conjunction of atoms, and adds its negation (¬R1 ∨ . . . ∨
¬Rl ) to the set of rules. Then one has to ﬁnd a refutation, that is, a sequence of
resolution steps which ends with the empty clause ✷.
′
A resolution step on a goal G = (R1′ ∧ . . . ∧ Rm
) and a program P takes one
′
subgoal Ri and a new variant r = (Q : − Q1 , . . . , Qn .), n ≥ 0, of a rule of P

6

Petra Hofstedt and Peter Pepper

such that Ri′ and Q can be uniﬁed with most general uniﬁer σ. The result of the
′
resolution step G ❀σ,r G′ is the new goal G′ = (σ(R1′ ) ∧ . . . ∧ σ(Ri−1
) ∧ σ(Q1 ) ∧
′
′
. . . ∧ σ(Qn ) ∧ σ(Ri+1 ) ∧ . . . ∧ σ(Rm )).
If a refutation can be computed, i. e. P  ∃(R1 ∧ . . . ∧ Rl ) holds, then the computation yields an answer substitution φ (as composition of the uniﬁers computed
in the resolution steps) such that P  ∀ φ(R1 ∧ . . . ∧ Rl ) holds. For a detailed
description of logic programming and its well-known representative prolog see for
example (Nilsson and Maluszyński 1995).
Constraint programming. Here problems are speciﬁed by means of constraints,
that is, ﬁrst order formulas which express conditions or restrictions describing properties of objects and relations between them. Constraints come from constraint
systems:
Definition 2.5. Let Σ = (S, F, R) be a signature such that R contains at least a
predicate symbol =s for every sort s ∈ S. Let X be a set of Σ-variables. Let D be a
Σ-structure with equality, i. e. for every predicate symbol =s there is an according
predicate which is an equivalence relation and fulﬁls the following requirements:
For all f ∈ F , r ∈ R and all terms ti , t′i ∈ T (F, X) of appropriate sorts si :
If for all i: D  ∀(ti =si t′i ), then
• D  ∀(f (t1 , . . . , tn ) =s f (t′1 , . . . , t′n )), when f (t1 , . . . , tn ) and f (t′1 , . . . , t′n ) are
both deﬁned, or both terms are undeﬁned,
• D  ∀(r(t1 , . . . , tm ) ↔ r(t′1 , . . . , t′m )), when r(t1 , . . . , tn ) and r(t′1 , . . . , t′n ) are
both deﬁned, or both terms are undeﬁned.
A basic constraint is of the form r(t1 , . . . , tm ), where r ∈ R and ti ∈ T (F, X).
The set of basic constraints over Σ is denoted by Constraint. It contains the two
distinct constraints true and f alse with D  true and D 2 f alse.
A constraint system is a 4-tuple ζ = (Σ, D, X, Cons), where {true, f alse} ⊆
Cons ⊆ Constraint. ✁
Example 2.5. A typical example are constraint systems for linear arithmetic with
constraints that are equalities and inequalities, e. g. X + 2 ∗ Y = 7 and X ≤ 3.5.
In this realm the signature Σ usually contains the function symbols +, −, ∗, / and
the relation symbols =, ≥, ≤. ✁
The evaluation of constraints is handled by constraint solvers. These are sophisticated algorithms for particular application domains, for example the simplex
algorithm for linear arithmetic. Constraint solvers can not only check the satisﬁability of constraints but can also compute entailed constraints, projections and even
solutions. A solution of a constraint is a valuation which satisﬁes it.
In order to allow more convenient programming, constraint systems can be embedded into an appropriate language, which provides concepts like recursion, encapsulation and abstraction. This leads to constraint logic and constraint functional
(logic) programming.

Integration of Declarative and Constraint Programming

7

Constraint logic programming. Logic programs are extended by constraints
such that the right-hand side of a rule may not only contain atoms but also constraints from an arbitrary constraint system. Consequently, the evaluation mechanism of logic languages, viz. resolution, has to be extended by mechanisms for
collecting constraints and checking their satisﬁability using appropriate constraint
solvers (Jaﬀar et al. 1998).
The ﬁrst and also the most typical language which has been extended by constraints, was the logic programming language prolog; the initial motivation was
to overcome the limitations of the expressive power of the language when reasoning
about arithmetic. A typical and comfortable constraint logic programming system
is ECLi PSe (Cheadle et al. 2003).
Constraint functional (logic) programming. Functional (logic) languages can
be extended further by guarding the rules with sets of constraints.
Definition 2.6. A constraint functional (logic) program P over Σ is given by a
ﬁnite set of rules of the form
f (t1 , . . . , tn ) → t where G
where – as in functional logic programs – f ∈ Φ, ti ∈ T (∆, X) and t ∈ T (F, X).
But now we have in addition a set G of (basic) constraints over Σ and X. ✁
For example, toy(F D) (Fernández et al. 2003) and toy(R) (Hortalá-González et al. 1997)
allow ﬁnite domain constraints and real arithmetic constraints, resp.
An example of a constraint functional logic program and its evaluation will be
considered informally in Sect. 3.1. The evaluation mechanism is discussed in detail
and formally in Sect. 4.

3 Cooperating Constraint Solvers
The basic architecture of a simple constraint solving system is a solver algorithm
CS associated to a constraint store C and a constraint pool ; both are sets of (basic)
constraints (see Figure 1 (a)).
• Initially the constraint store of a solver is empty, more precisely: it contains
only the constraint true; the constraint pool contains the constraints to solve.
• By the so-called constraint propagation the solver adds constraints from the
pool to its store while ensuring that the constraints in the store remain satisﬁable. In this way the set of possible valuations for the variables of the
constraint store is successively narrowed.
• If the solver detects an inconsistency, the corresponding constraint is rejected.
When constraints from different realms shall be used together, one has two possibilities. Either one programs a new solver that is capable of handling all kinds
of constraints. Or one takes several existing solvers, one for each realm, and coordinates them by some mediating program. The former approach usually generates
more eﬃcient solvers, but the amount of implementation work becomes prohibitive,

8

Petra Hofstedt and Peter Pepper
constraint pool
constraint pool

control

meta constraint solver

constraint
solver CS
constraint
solver CS1

...

constraint
solver CSk

store C
store C1
(a)

store Ck
(b)

Fig. 1. General architecture for (cooperating) constraint solvers
when more and more kinds of constraints shall be integrated. Therefore we focus
on the second approach, which is more ﬂexible and more economic.
In (Hofstedt 2000a) a framework for cooperating constraint solvers has been introduced and formally described, including cooperation strategies for the solvers. In
(Hofstedt 2001) termination and conﬂuence, as well as soundness and completeness
restrictions are examined. An implementation of our system meta-s is described in
(Frank et al. 2003a; Frank et al. 2003b).
Figure 1 (b) shows the architecture of our system for cooperating solvers. In the
following let L with µ, ν ∈ L denote the set of indices of constraint systems.
• The stores Cν of the individual constraint solvers CSν hold the constraints
which have been propagated so far. Initially they are all empty.
• The constraint pool is again the set of constraints that still need to be considered. Initially it contains the whole constraint problem to be solved.
• The meta solver coordinates the work of the individual solvers. It distributes
the constraints from the pool to the appropriate solvers, which put them
into their stores by constraint propagation and use them for their local computation (see the function tell ν below). Conversely, constraints in the local
stores may be projected to the pool in order to make them available as new
information to other solvers (see the functions proj ν→µ below).
The process of sequent propagations and projections ends, when no more information exchange takes place. Then the contents of the stores and of the pool together
represent the result: it may indicate, whether the initial constraint conjunction was
unsatisﬁable or not; moreover, restrictions of the solution space are provided by
means of projections of the stores. The restrictions may even provide a full solution
of the problem.
Details of the cooperation and communication of the involved solvers are determined by the cooperation strategy of the solvers. A cooperation strategy may inﬂuence the solution process with regard to diﬀerent criteria. The solver cooperation
system meta-s which implements our ideas provides a ﬂexible strategy deﬁnition

Integration of Declarative and Constraint Programming

9

framework. One can prescribe particular search strategies, one can formulate choice
heuristics for constraints with respect to their gestalt and their domains, one can
specify the order of propagation and projection and so forth. For this system it
has been shown in (Frank et al. 2003a) that appropriate strategies for solver cooperation can yield comfortable performance improvements for various kinds of
constraint problems.
At the heart of our approach are the requirements for the interfaces by which the
solvers are integrated into the system. There are essentially two kinds of operations
that constitute this interface (cf. Sect. 3.2 and 3.3):
• For every solver CSν there is a function tell ν for propagating constraints from
the pool to the store Cν .
• For every pair of solvers CSν , CSµ there is a function proj ν→µ for providing
information from the store Cν to the solver CSµ (via the constraint pool).
Note that this entails the translation into the other solver’s signature.
3.1 An Example
To give a better intuition about the working of our approach, we present a small
example. It is taken from the realm of constraint functional logic programming and
illustrates the interaction of a functional logic language with a ﬁnite domain solver
and a solver for interval arithmetic.
Example 3.1. The following program1 describes resistors from a certain set {300 Ω,
. . . , 3000 Ω}, as well as the formulas for the sequential and parallel composition
of resistors. The formulation is a mixture of functional logic programming and
constraint programming. The ﬁrst constraint uses the membership test ∈F D from a
constraint system for ﬁnite domains, and the other two constraints use the equality
=A from a constraint system over rational arithmetic. The equality =F L comes
from the functional logic resolution mechanism.
rc(simple(X)) → X where X ∈F D {300, 600, 900, 1200, . . ., 2700, 3000}
rc(seq(R1, R2)) → Z where X + Y =A Z, X =F L rc(R1), Y =F L rc(R2)
rc(par(R1, R2)) → Z where 1/X + 1/Y =A 1/Z, X =F L rc(R1), Y =F L rc(R2)
Note that the various subterms (including equations) in this program are all
homogeneous, that is, they are in T (Σ, X) for the signature of one of the underlying
solvers. This is possible in general: by introducing auxiliary variables we can always
turn hybrid terms into homogeneous terms; this is called ﬂattening of terms and
constraints, resp. Again, this relies on an appropriate semantic deﬁnition of the
functional logic equality =F L (which will be discussed in Sect. 4).
In the following we sketch the way, in which our approach may handle the above
program. For the time being, the treatment is on a more intuitive basis. The formalisation of the various steps will be given subsequently. We use the following
1

We use so-called extra variables in the rules, i. e. variables which occur in the body but not in
the head. We discuss the issue of completeness in presence of extra variables briefly in Sect. 4.1.

10

Petra Hofstedt and Peter Pepper

notation to illustrate the snapshots from the evaluation, where the three stores
CF L , CF D and CA belong to the functional logic language solver, the ﬁnite domain
solver, and the arithmetic solver, resp.
ConstraintP ool
store of CSF L

store of CSF D

store of CSA

(1) Suppose we want to compose two resistors in parallel and need a combined resistance of 200 Ω. The question is, which resistors do we have to pick from our set. This
question is formalizable in our program as the equation rc(par(RA, RB)) =F L 200.
This leads to the following initial conﬁguration.
rc(par(RA, RB)) =F L 200
true

true

true

(2) We apply the third rule (using narrowing) and reach the following system state.
Z =F L 200,

1/X + 1/Y =A 1/Z,

true

X =F L rc(RA),

true

Y =F L rc(RB)
true

(3) When there are several constraints in the pool, the particular cooperation strategy of the system decides, which constraint to choose next for propagation, here
e. g. the goal 1/X + 1/Y =A 1/Z. We propagate it (using the function tell A ) to the
arithmetic solver CSA . This is followed by a propagation of Z =F L 200 to the store
of CSF L . (In the pertinent stores we can omit the index of the equality symbol.)
X =F L rc(RA),
Z = 200

Y =F L rc(RB)

true

1/X + 1/Y = 1/Z

(4) Next, the system chooses the goal X =F L rc(RA) for a narrowing step based on
the rules of our program (using the function tell F L ). This leads to a disjunction of
three possibilities:
RA =F L simple(X) ∧ X ∈F D {300, 600, . . . , 3000}
∨ RA =F L seq(R1, R2) ∧ (X1 + Y1 =A X) ∧ X1 =F L rc(R1) ∧ Y1 =F L rc(R2)
∨ RA =F L par(R1, R2) ∧ (1/X2 + 1/Y2 =A 1/X) ∧ X2 =F L rc(R1) ∧ Y2 =F L rc(R2)
Due to the disjunction, we have to form three instances of our conﬁguration, each
representing one of the choices. For lack of space we only present the derivation of
the ﬁrst alternative here.
RA =F L simple(X),
Z = 200

X ∈F D {300, . . . , 3000},
true

Y =F L rc(RB)
1/X + 1/Y = 1/Z

Note that the store CF L did not change in this step. The application of a program
rule causes a replacement of the chosen constraint by new ones according to the

Integration of Declarative and Constraint Programming

11

right-hand side of the rule. In contrast, an enhancement of the store happens at the
propagation of constraints which do not contain deﬁned functions any more, as we
will see in Step (6).
(5) Now we apply the same process to the second goal Y =F L rc(RB), again pursuing
only the ﬁrst variant.
RA =F L simple(X), X ∈F D {300, . . .}, RB =F L simple(Y), Y ∈F D {300, . . . , 3000}
Z = 200

true

1/X + 1/Y = 1/Z

(6) Next we propagate all the constraints of the pool to their associated stores.
true
RA = simple(X)
RB = simple(Y)
Z = 200

X ∈ {300, . . . , 3000}
Y ∈ {300, . . . , 3000}

1/X + 1/Y = 1/Z

(7) At this point a system without solver cooperation would terminate the computation and not draw any further conclusions.
But our system enables solver cooperation. For the continuation of our example
we assume that the cooperation strategy of the system now forces the ﬁnite domain
solver to project its store by generating bounds for the variables using the function
proj F D→A .2 This is followed by a projection of CF L for the variable Z common to
CF L and CA .
(Z =A 200),
RA = simple(X)
RB = simple(Y)
Z = 200

(300 ≤A X),

(X ≤A 3000),

X ∈ {300, . . . , 3000}
Y ∈ {300, . . . , 3000}

(300 ≤A Y),

(Y ≤A 3000)

1/X + 1/Y = 1/Z

(8) The new constraints in the pool are now amenable to treatment by the arithmetic solver. Therefore the meta solver propagates them (using tell A ) to this solver.
Using its computational capabilities, the arithmetic solver can derive more accurate
bounds:
true
RA = simple(X)
RB = simple(Y)
Z = 200
2

X ∈ {300, . . . , 3000}
Y ∈ {300, . . . , 3000}

1/X + 1/Y = 1/200, Z = 200
(300 ≤ X), (X ≤ 600)
(300 ≤ Y), (Y ≤ 600)

Actually, our implementation meta-s (Frank et al. 2003a) distinguishes between weak projection generating only constraint conjunctions and strong projection which is allowed to project
disjunctions as well (first proposed in (Hofstedt 2001)). Using different kinds of projections we
are able to realise a variant of the Andorra principle (Costa et al. 1991; Warren 1988) which
proved to be very advantageous w. r. t. efficiency. The generation of bounds in our example
represents a weak projection.

12

Petra Hofstedt and Peter Pepper

(9) In the following steps the arithmetic solver’s improved bounds can be projected
back to the pool, from where they are propagated to the ﬁnite domain solver, which
then narrows down its choices.
true
RA = simple(X)
RB = simple(Y)
Z = 200

X ∈ {300, 600}
Y ∈ {300, 600}

1/X + 1/Y = 1/200, Z = 200
(300 ≤ X), (X ≤ 600)
(300 ≤ Y), (Y ≤ 600)

(10) At this point we need strong projection (cf. footnote (2)) by which the ﬁnite
domain solver puts a disjunction of equations
(X =A 300 ∧ Y =A 300) ∨ . . . ∨ (X =A 600 ∧ Y =A 600)
into the pool. Each of these four conjunctions can again be propagated to the
arithmetic solver. Two of them will lead to solutions, but the other two propagations
lead to inconsistencies in the arithmetic solver and are therefore discarded. One
successful ﬁnal conﬁguration is:
true
RA = simple(300)
RB = simple(600)
Z = 200

X = 300
Y = 600

Z = 200
X = 300
Y = 600

The solution {RA = simple(300), RB = simple(600)} can be extracted from the
constraint store CF L of the solver CSF L . ✁
This small example already demonstrates the important role of cooperation
strategies for the eﬃciency of the computation. For example, the ability to control the order of weak and strong projections allows a considerable restriction of
the set of variable assignments before an explicit search for solutions is initiated for
the remaining alternatives. Suppose that we had applied the strong projection at an
earlier point. This would have caused a search across all 100 alternatives of resistor
combinations, i. e. (X =A 300 ∧ Y =A 300), . . . , (X =A 3000 ∧ Y =A 3000). As a matter of fact, it is in general a good strategy to delay the introduction of disjunctions
as long as possible for the sake of eﬃciency. This is suggested by experiences with
the KIDS system (Westfold and Smith 2001).
Based on the intuitive insights provided by this example we will now look more
deeply into the precise deﬁnitions of the propagation function tell ν and the projection function proj ν→µ .
3.2 Constraint Propagation (tell ν )
As can be seen e. g. in Step (3) of the above example, the function tell ν , ν ∈ L,
takes a constraint c ∈ Consν (i. e. a basic constraint of the constraint system of
solver CSν ) from the pool and adds it to the constraint store Cν , which leads to a

Integration of Declarative and Constraint Programming

13

tell ν : Consν × Storeν −→ {true, f alse} × Storeν × DCConsν with
1. if tell ν (c, Cν ) = (true, Cν′ , c′′ ), then
(a) Dν  ∀((Cν ∧ c) ←→ (Cν′ ∧ c′′ )),
(b) Dν  ∀(Cν′ −→ Cν ),
(c) Dν  ∃Cν′ ,
2. if tell ν (c, Cν ) = (f alse, Cν′ , c′′ ), then
Cν′ = Cν , c′′ = f alse, Dν  ¬∃(Cν ∧ c).

Fig. 2. Interface function tell ν , ν ∈ L, (requirements)
new store Cν′ . There may also be a remaining part c′′ of c, which is put back into
the pool (but this happens rarely in practice).
√
Example 3.2. Suppose we have the constraint X = Y in the pool. This may be
used to put the constraint X = Y2 into the store of some solver, while keeping the
constraint Y ≥ 0 in the pool. ✁
Figure 2 shows the requirements for the function tell ν .3 The function returns
three values. The ﬁrst one is a Boolean indicator of the success or failure. The
second one is the modiﬁed store. And the third one is the remaining constraint
c′′ ∈ DCConsν , which is put back into the pool. By DCConsν we denote the set of
disjunctions of constraint conjunctions.
When the solver successfully propagates a constraint c to a store Cν (Case 1),
then it must be ensured that the (overall) knowledge of the store and the constraint
is neither lost nor increased (a). It is only possible to add constraints to a store,
but not to delete them. Thus, the new constraint store Cν′ must imply the old one
(b). Of course, the new store Cν′ has to be satisﬁable in the domain Dν of CSν as it
is a constraint store (c). In Example 3.1, e. g. in Steps (3) and (4), tell A and tell FL
have been applied according to this deﬁnition.
This ﬁrst case also covers the situation that a solver is not able to handle a
certain constraint c, i. e. if the solver is incomplete. In this case the store Cν does
not change and c = c′′ remains in the pool.4
Figure 3 visualises the state change of the system when a solver performs a
successful constraint propagation. The left side shows the system before the propagation, the right side afterwards. When we propagate c to Cν by tell ν (c, Cν ), c
is deleted from the pool and propagated to the store Cν . The resulting new store
Cν′ and the remaining constraint c′′ may in general be disjunctions of constraint
W
conjunctions, e. g. c′′ = i∈{1,...,n} c(i) . Since store and pool are sets of basic constraints, this causes a splitting of the system as shown in Figure 3.
3

4

In (Hofstedt 2000a) two forms of successful propagation are distinguished, which is necessary
for general solvers to ensure termination of the system. For the “language solvers” considered
in this paper this is simplified.
Again, to ensure termination of the overall system, this particular case must be detected by
the overall machinery and the treatment of the constraint must be suspended. We omit this
technical detail in favour of readability.

14

Petra Hofstedt and Peter Pepper
c0 , . . . , c(1) , . . . , cr

c0 , . . . c, . . . , cr

...

MCS

MCS

... CSν ... CSµ ...

... CSν ... CSµ ...

Cν

...

Cµ

...

...

′
Cν

...

tell(c, Cν ) = (true, Cν′ , c′′ ), W
where c ∈ Consν and c′′ = i∈{1,...,n} c(i) .

Cµ

......
c0 , . . . , c(n) , . . . , cr

...
...

MCS
... CSν ... CSµ ...

′
Cν

...

Cµ

...

Fig. 3. Application of the interface function tell
If tell ν (c, Cν ) fails (Case 2) because c and Cν are contradictory, then f alse is
added to the constraint pool and Cν does not change (not shown in Figure 3).
Example 3.3. The interface function tell A of our rational arithmetic solver CSA
could work as follows (see e. g. Step (10) in Example 3.1):
Given the store C = (1/X+1/Y =A 1/200) the propagation tell A ((X =A 300), C) =
(true, C ′ , true) yields – after some computation by the solver CSA – a new simpliﬁed store C ′ = (X =A 300 ∧ Y =A 600). On the other hand, tell A ((Y >A 600), C ′ ) =
(f alse, C ′ , f alse) represents a failing propagation. ✁
For each concrete solver CSν the user must provide a suitable function tell ν .
However, constraint propagation is mainly based on the satisﬁability test which is
the main operation of a constraint solver. Moreover, the requirements in Figure 2
are chosen in such a way that they allow an easy integration of many existing
solvers into the cooperating system, taking particular properties of solvers (like
their incompleteness (cf. Case 1) or an existing entailment test) into consideration.
Examples for such concrete propagation functions will be shown in Sect. 4 for
the special cases of functional logic and logic languages, when they are viewed as
solvers.
3.3 Projection of Constraint Stores (proj ν→µ )
Projection is used for information exchange between constraint solvers CSν and
CSµ , ν 6= µ, µ, ν ∈ L, via the constraint pool.
Figure 4 shows the requirements for the function proj ν→µ . The function proj ν→µ
takes a set of common variables of the two solvers and the local store Cν and returns
(a disjunction of conjunctions of) constraints to the pool. proj ν→µ (X, Cν ) = c
describes a projection of a store Cν w. r. t. common variables (i. e. X ⊆ Xν ∩ Xµ )
to provide constraints c of another solver CSµ . It provides knowledge implied by
the store Cν . Projection does not change the stores but only extends the pool by
the projected constraints.
To ensure that ﬁnally no solution is lost, a projection c must provide every
satisfying valuation of the current store Cν . That is, proj ν→µ must be deﬁned

Integration of Declarative and Constraint Programming

15

proj ν→µ : ℘(Xν ∩ Xµ ) × Storeν → DCConsµ , where Vars(proj ν→µ (X, Cν )) = Y ⊆ X,
must be sound, i. e. for every valuation σν for the variables of Y must hold:
If (Dν , σν )  ∃
∃

Y

Y

Cν , then (Dµ , σν )  proj ν→µ (X, Cν ), where

Cν denotes the existential closure of formula Cν except for the variables of Y .

Fig. 4. Interface function proj ν→µ , µ 6= ν, µ, ν ∈ L, (requirements)
in such a way that every solution σν of Cν is a solution of its projection c in Dµ
(soundness).
Example 3.4. Consider the arithmetic solver CSA and the ﬁnite domain solver
CSF D . Let CF D = (X ∈F D {300, . . . , 3000} ∧ Y ∈F D {300, . . . , 3000}) hold. Deﬁne
proj F D→A (as a weak projection, cf. footnote (2)) such that
proj F D→A ({X}, CF D ) = ((X ≥A 300) ∧ (X ≤A 3000)).

This corresponds to Step (7) of Example 3.1. ✁

As in the case of tell ν the function proj ν→µ has to be concretely programmed for
every pair of given solvers. For many pairs of solvers it is possible to automatically
provide simple projection functions generating equality constraints which at least
express variable bindings. Often it is also suﬃcient to provide actual projection
functions only for particular pairs of solvers and to reduce superﬂuous communication.
Examples of projection functions will also be shown in Sect. 4 in connection with
constraint functional logic and constraint logic languages.

3.4 Semantics
In (Hofstedt 2001) we deﬁne reduction systems describing solver collaborations
based on the interface functions tell ν and proj ν→µ . The reduction systems work on
so-called conﬁgurations which consist of representations of the current constraint
pool and the associated stores, which together represent the state of the system.
Hofstedt (2001) gives a detailed discussion of the termination, conﬂuence, soundness and completeness of the reduction systems.
Based on the signatures and Σ-structures of the incorporated constraint systems
we build combined constraint systems by their disjoint unions. Clearly, for those
sorts and function and predicate symbols that are common to diﬀerent systems the
corresponding carrier sets, functions and predicates must be identical. This applies
in particular to the semantics of the equality symbol (on shared sorts).
It is shown that – using our method – no solutions are lost. If the system fails
then the given constraint problem is unsatisﬁable. Furthermore, we discuss the
situation of suspended constraints remaining in the pool due to the incompleteness
of solvers. If all incorporated solvers are complete and the reduction relation is
terminating, then for a satisﬁable constraint problem the method can be guaranteed
to be successful.

16

Petra Hofstedt and Peter Pepper

The soundness and completeness results do not depend on the particular cooperation strategy of the solvers.
The (obvious) fact that the completeness of the overall system depends on the
completeness of the individual solvers will play a role in connection with functional
logic languages.

4 Combination of Declarative and Constraint Programming
As a particular application, our system of cooperating solvers allows the integration
of diﬀerent host languages by treating them as constraint solvers. As a matter of
fact, it even makes it possible to work quite ﬂexibly with diﬀerent evaluation strategies, that is, diﬀerent operational semantics. A good point in case are functional
(logic) languages, which have very diﬀerent semantics depending on the chosen
evaluation mechanisms. As mentioned in Sect. 2, this has already been elaborated
in the textbook (Manna 1974) for functional languages; for the realm of functional
logic programming the pertinent issues are described in (Hanus 1994; Hanus 1995).
The feasibility of this idea is based on two main observations: First, the evaluation
of expressions in declarative languages consists of their stepwise transformation to
a normal form while particular knowledge (in the form of substitutions) is collected.
Second, this way of proceeding is similar to a stepwise propagation of constraints
to a store, which is simpliﬁed in doing so.
In the following, we consider the integration of a functional logic language and
of a logic language, resp., into the system of cooperating solvers. Syntactically, we
extend the languages by constraints, but their evaluation mechanisms are nearly
unchanged: they are only extended by a mechanism for collecting constraints of the
other constraint solvers.
A four-step process. The integration of a declarative language into our system
of cooperating solvers requires four activities.
1. The inherent constraints of the language have to be identiﬁed.
2. Conversely, the constraints from the other domains have to be integrated into
the syntax of the language.
3. The language evaluation mechanism (e. g. reduction or resolution) has to be
extended by gathering constraints from the other domains.
4. Finally one needs to carefully deﬁne the interface functions tell . and proj .→.
of the new language solver.
4.1 A Functional Logic Language as Constraint Solver
The introduction of constraints into the rules of a functional logic language yields
constraint functional logic programming. We follow our four step process. Recall
that the basic syntactic construct is
f (t1 , . . . , tn ) → t where G
where G is a set of constraints, including constraints from other domains. Moreover,

Integration of Declarative and Constraint Programming

17

all constraints in G are homogeneous, that is, are built from the signature of one
solver, including equalities t1 =FL t2 of the functional logic language.
(1) Identifying language constraints. Functional logic languages are based on equalities between terms. In order to state precisely what this means, we have to look
more closely into the semantic models of these languages, cf. e. g. (Manna 1974;
Winskel 1993; Broy et al. 1987). It has to be ensured that the operational semantics
induced by our cooperating solvers is compatible with the mathematical semantics
of the language under consideration.
Recall that the semantic value of a term t in the model D is denoted by JtKD ; when
D is obvious from the context, we omit it and just write JtK. We are dealing with
partial functions; according to the traditional convention we write “⊥” (pronounced
“bottom”) to express partiality: JtK = ⊥ means: t has no proper semantic value.
We note in passing that there are two kinds of partiality, both of which can be
subsumed under the element ⊥. One is nontermination of evaluations, the other is
the lack of matching rules. For example, if there is no rule for X/0 – independent
of the responsible solver – then we have Jt/0K = ⊥. The following discussion is
exempliﬁed with nontermination but it applies to both cases.
Example 4.1. Consider the following superﬁcial example over the natural numbers
with constructors 0 and s . (To ease reading we write s without parentheses.)
f(0, Y) → 0
f(s X, Y) → f(X, f(s X, Y))
We consider a functional logic solver CSFL working in cooperation with others and
we use again the notation from Example 3.1 to illustrate the snapshots from the
evaluation. The formalisation of the interface functions for CSFL will be given and
explained in more detail subsequently.
Start from the constraint Z =F L f(0, f(s 0, s 0)) in the pool.
Z =F L f(0, f(s 0, s 0))
true

true

true

In a call-by-name semantics we ﬁrst reduce the outermost f using the ﬁrst rule of
the program. This immediately yields the result: Z =F L 0. Semantically this means
JZK = Jf(0, f(s 0, s 0))Kcbn = J0K.
In a call-by-value semantics we ﬁrst reduce the innermost f using the second rule:
Z =F L f(0, f(0, f(s 0, s 0))). As one can immediately see, this reduction process
will never terminate, that is, there will always be an equation Z =F L ti in the
pool (with longer and longer right-hand sides ti ). Semantically this means JZK =
Jf(0, f(s 0, s 0))Kcbv = ⊥. ✁
What does this mean for the introduction of variables? Recall that we need
auxiliary variables for the homogeneity of the constraints for diﬀerent solvers, i. e.
we need to ﬂatten constraints and terms. To see the pertinent problems, we modify

18

Petra Hofstedt and Peter Pepper

the above example by introducing several auxiliary variables. Moreover, we add a
further function g.
f(0, Y) → 0
f(s X, Y) → f(X, W) where W =F L f(s X, Y)
g(X)
→ 0 where f(s X, s X) =F L 0
Let us ﬁrst consider the operational semantics. We start from
Z =F L g(0)
true

true

true

After the ﬁrst two steps this leads to the following situation:
Z =F L 0, f(0, W) =F L 0, W =F L f(s 0, s 0)
true

true

true

In the next steps we may propagate Z =F L 0 and evaluate the two calls of f:
W =F L f(0, W′ ), W′ =F L f(s 0, s 0)
Z=0

true

true

This may continue into the following conﬁguration:
W(i) =F L f(s 0, s 0)
Z = 0, W = 0, W′ = 0, . . .

true

true

This process will obviously continue forever, creating more and more auxiliary variables W(j) .
Let us compare this w. r. t. the original (not ﬂattened) deﬁnition of the function
f in Example 4.1 and the two kinds of mathematical semantics that we consider
here.
• Under call-by-value semantics, the result is JZK = Jg(0)K = ⊥.
• Under call-by-name semantics the result is JZK = Jg(0)K = J0K.
Note that the auxiliary variables W, W′ , . . . do not appear at all in the solution
space of the mathematical semantics, since they are only internal artefacts of the
computation process.
Coming back to the operational semantics, we can only look up the value of Z in
the store, when the computation is ﬁnished, that is, when the pool is empty. In the
above example this will never happen; therefore we will never be able to extract
the value Z = 0 from the store. This means that Z has no value, i. e. JZK = ⊥.
In other words: Without further precautions, the introduction of variables is only
compatible with call-by-value semantics.
How could we implement call-by-name semantics and still allow the introduction
of variables? A simple solution consists of the introduction of a dependency relation

Integration of Declarative and Constraint Programming

19

between variables. In our example, W′ would depend on W, because it occurs in
the term on the right-hand side of W. As soon as the pertinent rule would reduce
W =F L f(0, W′ ) to W =F L 0, the dependent variable W′ would be eliminated from the
pool. Moreover, the order of evaluation would have to follow the dependencies.
As can be seen from this sketch, our method of handling hybrid constraints by
ﬂattening is more naturally related to call-by-value semantics, but with a little eﬀort
other semantic principles such as call-by-name can be accommodated as well.
We note in passing that these considerations do not only apply to functional logic
solvers, but to all kinds of solvers. Consider for example an arithmetic solver with
the rule 0 ∗ X = 0. If we multiply the term g(0) from the above example by 0 we
obtain from Z = 0 ∗ g(0) the two constraints Z = 0 ∗ X1 , X1 =F L g(0), which leads to
Z = 0, X1 =F L g(0). Again, the diﬀerences between call-by-name and call-by-value
can be captured by introducing a dependency of the variable X1 on Z.
Remark on strict equality. From a semantic point of view it is unsatisfactory that we
express undeﬁnedness only operationally by the fact that the pool does not become
empty. In a denotational setting, one would prefer to represent this situation also
as ⊥. This brings strict equality into the game.
In discussions about mathematical semantics there are usually two kinds of equality: Under strong equality we have e. g. (⊥ =D ⊥) = true and (⊥ =D 3) = f alse.
And strict equality has the property Jt1 = t2 K =D ⊥ if Jt1 K =D ⊥ or Jt2 K =D ⊥.
Strong equality obeys the laws of classical two-valued logic, but it is in general not
decidable. Strict equality is a “normal” operator in the language but the semantics
leads to all problems of three-valued logic. Neither equality is “better” than the
other, they just serve diﬀerent purposes.
Call-by-value semantics evidently conforms nicely to strict equality. In our above
example we have JZK = Jg(0)K = Jf(s 0, s 0)K = . . . = ⊥. Therefore every pool
contains some equality of the kind JW(i) = f(s 0, s 0)K and thus JW(i) = ⊥K, which –
under strict equality – is ⊥. Finally, we must consider conjunctions as strict such
that the whole conﬁguration is ⊥. This exactly reﬂects the fact that our computation
does not terminate.5 The overall system remains semantically consistent, since a
“wrong” equation such as Z = 0 is in conjunction with ⊥ and therefore does no
harm. As a matter of fact, the overall conﬁguration just moves in each step from
one representation of the value ⊥ to another representation of the value ⊥.
The same considerations apply to call-by-name semantics. Here we have the situation that e. g. Jf(0, ⊥)K = 0. Therefore an equality like f(0, W) = 0, where both
terms are diﬀerent from ⊥, has the same truth value under both kinds of equality.
However, if we encounter a function that is nonterminating even under call-by-name
semantics, then we need again the strict equality in order to represent the overall
nontermination by ⊥.
The fact that the operational semantics requires additional means such as dependencies among variables is independent of the kind of equality. If one considers the
5

The formal disjunctions that reflect the various branches of the evaluation need a different
semantic treatment in order to accommodate the inherent nondeterminism.

20

Petra Hofstedt and Peter Pepper

above example, the computation is consistent, since it simply keeps adding valid
equalities of the kind W(i) = 0 to the store. All we need is a mechanism to stop it
from doing this forever.
(2) Extending the language by constraints of other domains. The syntax of the
language also contains the constraints from the other domains (occurring in the part
. . . where G of the rules). Therefore they are also part of the language constraints.
To get a clean separation of concerns we also have to ﬂatten hybrid terms from
diﬀerent domains. Suppose, for example, that we had given the third rule of our
program in the hybrid form
rc(par(R1, R2)) → Z where 1/rc(R1) + 1/rc(R2) =A 1/Z
Then we would need to put this into the separated form
rc(par(R1, R2)) → Z where 1/X + 1/Y =A 1/Z,

X =FL rc(R1),

Y =FL rc(R2)

(3) Extending the language evaluation mechanism by gathering constraints. Functional logic languages are based on narrowing. Therefore we consider this evaluation
mechanism as constraint solver CSFL . But in addition to performing the narrowing
steps, the solver must also collect constraints from other domains (occurring in the
part . . . where G).
The basic concept of a narrowing step with constraints can be described as follows:
Let e be an equation with a distinguished non-variable subterm t, that is, e[t] with
t∈
/ X. Let (l → r where G) be a rule from the program such that σ = mgu(t, l)
uniﬁes the subterm t with the left-hand side l of the rule. Then the narrowing step
yields the new equation σ(e[r]) together with the rewritten constraint σ(G), we
write: e[t] ❀σ (σ(e[r]), σ(G)).
The extensive discussion of the previous pages has shown the various possibilities
for choosing evaluation strategies and their impacts on the semantics.
(4) Defining the interface functions tell FL and proj FL→ν of the particular language
solver. This ﬁnal step has to integrate the eﬀects of narrowing and constraint collection with the other solvers.
Propagation. Figure 5 illustrates how the interface function tell FL is used to simulate a narrowing step with constraints, and Figure 6 gives the formal deﬁnition of
the pertinent requirements. To ease the presentation we suppose that all functional
logic equalities are in the form Y =FL t with variable Y and term t. This can always
be achieved with the help of auxiliary variables.
Like all solvers, CSFL propagates constraints to its store CFL thereby checking
the satisﬁability of CFL in conjunction with the new constraints. Therefore the
function tell FL incorporates the principle of narrowing.
In the light of the preceding discussion on ﬂattening we assume that all constraints which get into the pool (either as part of the initial problem to solve or
as results of propagations or projections) are decomposed with the help of auxiliary variables such that all subterms of the form f (t1 , . . . , tn ), where f is a deﬁned

Integration of Declarative and Constraint Programming

...

. . . , Y =FL t, . . .

. . . , σi , Y =FL ti , σi (Gi ), . . .

MCS

MCS

... CSFL ... CSν ...

... CSFL ... CSν ...

CFL
=φ

...

Cν

...

...

CFL

...

21

...
...

. . . , σj , Y =FL tj , σj (Gj ), . . .

MCS

Cν

... CSFL ... CSν ...

Program:
li → ri where Gi
lj → rj where Gj
...

and it holds:
φ(t) ❀σi (ti , σi (Gi )) and
φ(t) ❀σj (tj , σj (Gj )).

...

CFL

...

Cν

...

Fig. 5. Application of the interface function tell FL (see also Figure 6)
function, are extracted. The deﬁnition of tellFL therefore only needs to consider
narrowing steps on outermost terms. The distinction between call-by-value and
call-by-name must therefore be based on the aforementioned dependency relation
among variables.
We have to distinguish two kinds of constraints Y =FL t (see Figure 6):
(1) When the term t still contains deﬁned functions, a narrowing step is applied
as part of tell FL . This is only reﬂected by a change of the constraint pool. The store
does not change in this case. Note that due to the ﬂattening t contains exactly one
deﬁned function f , and this function is the outermost symbol in t. Moreover, since
the substitution φ deﬁned in Figure 6 only contains constructor terms, t̂ = φ(t)
retains this property.
(2) When the term t is a constructor term then the constraint Y =FL t is added
to the store if possible. Thereby, the satisﬁability test is realised by the parallel
composition ↑ of substitutions.
This integration of the narrowing into the propagation sometimes leads to earlier
bindings of variables and thus to a faster recognition of unsuccessful computations.
The price to be paid is that the solver CSFL is amalgamated into the function
tell FL – and with it all its problems.
Example 4.2. To elucidate the interface deﬁnition we use our running example
from Sect. 3.1. In Step (2) of this example we applied the only matching rule
rc(par(R1, R2)) → Z where 1/X + 1/Y =A 1/Z,

X =FL rc(R1),

Y =FL rc(R2)

to the initial conﬁguration. We split the equation in the pool into two equations
using an auxiliary variable such that the pool reads:
Z1 =F L rc(par(RA, RB)),

Z1 =F L 200

We pick the ﬁrst term and apply tell FL as described in Figure 6. Note that we
have the special situation, where the store CFL = φ is still empty such that t̂ =
φ(rc(par(RA, RB))) = rc(par(RA, RB)).
The narrowing step for the term with (a new instance of) the rule uniﬁes the

22

Petra Hofstedt and Peter Pepper

tell FL : Let P be a functional logic program with constraints, let CFL = φ be the current
constraint store of CSFL . (Recall that the constraint store CFL is nothing but a substitution φ from variables to constructor terms, which is written in the form of equations
and thus can be treated like constraints.) Let c = (Y =FL t) be the constraint to be
propagated. Let t̂ = φ(t).
Finally, we use the following notion: A rule p = (lp → rp where Gp ) applies to t̂, if for
t̂ 6∈ X there is a unifier σp = mgu(t̂, lp ).
We need to distinguish the following cases
1. Let t̂ contain defined functions; that is, t̂ is of the form f (. . .) with f being the only
defined function (due to the maximal flattening). If the set Pc ⊆ P of applicable
rules is nonempty, then
W
tell FL (c, CFL ) = (true, CFL ,
p∈Pc (σp ∧ (Y =FL σp (rp )) ∧ σp (Gp ))).

2. Let t̂ be a constructor term, i. e. t̂ ∈ T (∆, XFL ).

(a) If ({Y = t} ↑ CFL ) 6= ∅, then
tell FL (c, CFL ) = (true, {Y = t} ↑ CFL , true).
(b) If ({Y = t} ↑ CFL ) = ∅, then
tell FL (c, CFL ) = (f alse, CFL , f alse).

Fig. 6. Interface function tell FL
subterm rc(par(RA, RB)) – which happens to be the full term – with the left-hand
side rc(par(R1, R2)) of the rule. Since this matching exists, we have Case 1 of
Figure 6. The resulting most general uniﬁer is the substitution σ = {R1 = RA, R2 =
RB}. Applied to the rule this substitution yields the instantiated right-hand side Z
and constraints 1/X + 1/Y =A 1/Z, X =FL rc(RA), Y =FL rc(RB). This is put back
into the pool:
R1 =F L RA, R2 =F L RB, Z1 =F L Z, 1/X + 1/Y =A 1/Z, X =F L rc(RA),
Y =F L rc(RB), Z1 =F L 200
If there is more than one applicable rule, we get a number of newly built constraint
pools.
Applying tell FL to the two constraints R1 =F L RA and R2 =F L RB leads to
Case 2.(a) of Figure 6. As a result the store CFL then contains these constraints (a
substitution). The remaining constraints in the pool are as follows:
Z1 =F L Z, Z1 =F L 200, 1/X + 1/Y =A 1/Z, X =F L rc(RA), Y =F L rc(RB).
Note, that Example 3.1 displays simpliﬁed forms for brevity. ✁
Projection. Since the constraint store CFL only contains substitutions, the projection is trivial. It generates equality constraints representing them. For example,
in Step (7) the constraint Z =A 200 is transferred from CFL to the pool using
proj F L→A .
The speciﬁcation of the function proj F L→ν is given in Figure 7. (Note, that the
equalities in the result φ|X are indexed ν to express the fact that they now belong
to the domain of the solver CSν .)

Integration of Declarative and Constraint Programming

23

proj F L→ν : The projection of a store CF L = φ w. r. t. a constraint system ζν and a set
of variables X ⊆ XF L ∩ Xν makes the substitutions for x ∈ X explicit:
n
proj F L→ν (X, φ) = φ|X if φ 6= ∅
true otherwise.

Fig. 7. Interface function proj F L→ν , ν ∈ L
Completeness and other aspects. Since the interface functions tell F L and proj F L→ν
of our functional logic language solver fulﬁl the requirements given in Sect. 3, the
soundness and completeness results of the cooperation framework hold for the integration of a functional logic language – however, only relative to the completeness
of the narrowing strategy encoded within tell FL .
It is well known that narrowing is in principle a complete and sound method
for theories presented by conﬂuent and terminating rewrite systems. But in connection with functional logic languages and in particular in the presence of extra variables the issue of completeness becomes more intricate. This problem has
been investigated by several authors, among others (Middeldorp and Hamoen 1994;
Suzuki et al. 1995; Hanus 1995). These papers discuss slightly diﬀerent syntactic
criteria, which guarantee that certain narrowing strategies (e. g. lazy or needed
narrowing) are sound and complete.
Evidently, these criteria carry over to the narrowing strategy that we embed into
our function tell FL . For lack of space we cannot go into details here. Suﬃce it to
say that, for example, our program rule
rc(par(R1, R2)) → Z where 1/X + 1/Y =A 1/Z,

X =FL rc(R1),

Y =FL rc(R2)

contains the three extra variables X, Y and Z and is in the class 3-CTRS of (Middeldorp and Hamoen 1994).
But the syntactic form also meets the requirements of being orthogonal, properly
oriented and right-stable (Suzuki et al. 1995), which guarantees that the program
is level-conﬂuent. (These conditions essentially state that the variables are in a nice
left-to-right order.)
As a matter of fact, the rule is also constructor-based and functional in the
sense of (Hanus 1995), since the variables R1 and R2 in the guarding constraints
occur in the left-hand side and the variable Z of the right-hand side is deﬁned by
the guarding constraints. This also entails the completeness of lazy and needed
narrowing. But Hanus imposes a further requirement: the equality =FL has to be
strict (which allows to consider it as an equality (Y ≡ t) =FL true). Since we only
put substitutions with constructor terms into the store CFL , this works in our
approach as well. (This is similar to the language curry (Hanus et al. 2003).)
However, there is one further issue! The above quoted requirements refer to the
functional logic equalities in the guard G. But our rules have a more general form:
f (t1 , . . . , tn ) → r where c1 , . . . , cm , u1 =FL v1 , . . . , uk =FL vk
Only the equalities ui =FL vi (with ui being a constructor term, possibly only a
variable) belong to the functional logic solver. The cj are constraints from other
domains.

24

Petra Hofstedt and Peter Pepper

This raises the question: How do these constraints c1 , . . . , cm from the other
domains ﬁt into the picture? Let us consider our standard example
rc(par(R1, R2)) → Z where 1/X + 1/Y =A 1/Z,

X =FL rc(R1),

Y =FL rc(R2)

Without the ﬁrst constraint, the variable Z would not occur in the guard and thus
the rule would not even be 3-CTRS (and thus no completeness results could be
given at all). On the other hand, all constraints ci do not contain any of the deﬁned
functions and therefore do not participate in any kind of narrowing strategy. So,
from the point of view of narrowing, a variable like Z can be treated like a constant.
If one of the other solvers ﬁnds a solution, e. g. Z = 200 in our example, then the
corresponding substitution is put into the store CFL . This way the associated value
is guaranteed to be a ground constructor term and thus does not interfere with the
narrowing strategies.
This illustrates again the – evident – fact that the completeness of the overall
system, and thus also of its narrowing part, depends on the completeness of all
participating solvers.
4.2 A Logic Language as Constraint Solver
The integration of a logic language into the system of cooperating solvers yields a
constraint logic programming language. Since this is actually simpler than the case
of functional logic languages, we only sketch it here brieﬂy.
(1 & 2) Identifying language constraints and extending the language by constraints
of other domains. It is widely accepted that logic programming can be interpreted
as constraint programming over the Herbrand universe. The appropriate constraint
solving mechanism CSL is resolution.
The goals according to a given constraint logic program P are the natural constraints of a logic language solver. Furthermore, the set ConsL of constraints of this
solver must contain equality constraints Y =L t between variables and terms to
represent substitutions.6
We extend the syntax of the language by constraints of other constraint systems
which yields the typical CLP syntax, cf. e. g. (Jaﬀar and Lassez 1987). Thus, the
set ConsL must furthermore include all constraints of the incorporated solver(s).
(3 & 4) Extending the language evaluation mechanism by gathering constraints and
defining the interface functions of the particular language solver. For the integration
of CSL into the system the interface functions tell L and proj L→ν must be deﬁned.
Step (3), i. e. gathering constraints during resolution, is realised by the extension
of the resolution step from atoms to the whole body including the constraints of
other domains.
6

Not all CLP systems support equalities on the syntactical level. Rather they only generate them
internally in the solver. In our system, they are explicitly visible.

Integration of Declarative and Constraint Programming

25

tell L : Let P be a constraint logic program, let CL = φ be the current store of CSL .
1. Let R = p(t1 , . . . , tm ) be the constraint (goal) which is to be propagated. Let
R̂ = φ(R). We use the following notion: A rule p = (Qp :- rhsp ) applies to R̂, if
there is a unifier σp = mgu(R̂, Qp ).
(a) If the set PR ⊆ P of applicable
W rules is nonempty, then
tell L (R, CL ) = (true, CL ,
p∈PR (σp ∧ σp (rhsp ))).

(b) If there is no applicable rule in P , then
tell L (R, CL ) = (f alse, CL , f alse).

2. Let c = (Y =L t) be the constraint which is to be propagated.
(a) If ({Y = t} ↑ CL ) 6= ∅, then
tell L (c, CL ) = (true, {Y = t} ↑ CL , true).
(b) If ({Y = t} ↑ CL ) = ∅, then
tell L (c, CL ) = (f alse, CL , f alse).

Fig. 8. Interface function tell L
Propagation. The propagation function tell L emulates resolution steps (including
gathering constraints). Its formal deﬁnition is given in Figure 8. Case 1.(a) represents a resolution step on a goal R as a successful propagation, where for every
applicable rule we get a newly created constraint pool and, thus, a new instantiation of the architecture. If there is no applicable rule for a goal, i. e. Case 1.(b),
the propagation fails (in contrast to the functional logic solver considered before,
undeﬁnedness of a predicate is regarded as failure here).
Similar to the deﬁnition of tellF L the remaining cases describe the propagation
of equality constraints by parallel composition of substitutions (Case 2).
Projection. As before, the projection function provides constraints representing the
substitution from the store which has been computed during resolution. The definition of the projection function proj L→ν is the same as for the functional logic
language solver given in Figure 7, where the index F L is replaced by L to denote
the origin of the projection.
Since the interface functions tell L and proj L→ν fulﬁl the requirements given in
Sect. 3, the soundness and completeness results of the cooperation framework hold
for the integration of a logic language.

5 Conclusion and Related Work
This paper describes a general approach for the integration of declarative languages
and constraint systems. This essentially means to treat their evaluation mechanisms
together with programs as constraint solvers. This is done in four general steps:
1.
2.
3.
4.

Identifying language constraints,
Extending the language by constraints of other domains,
Extending the language evaluation mechanism by gathering constraints,
Deﬁning the interface functions of the particular language solver.

26

Petra Hofstedt and Peter Pepper

The most important aspect of our approach is that the overall system for cooperating solvers allows the handling of hybrid constraints over diﬀerent domains.
Gains and perspectives. Our general framework for cooperating solvers provides
mechanisms for the deﬁnition of cooperation strategies. Similar to CLP(X) (Jaﬀar and Lassez 1987)
and CFLP(X) (López-Fraguas 1992), which are covered by our approach, the framework can thus be instantiated by three parameters: a strategy deﬁnition S, a set
X of constraint systems and a host language Y. In this way, our approach enables
the building of constraint languages customised for a given set of requirements for
a comfortable modelling and the solution of many problems.
For example, if one needs a convenient language to express search problems with
special constraints over ﬁnite and/or further domains, the user chooses a logic language and according constraint systems. For problems which allow or require a
more deterministic modelling one may decide to build a constraint language based
on a functional or functional logic language. In a similar way one can imagine to
combine a database language with constraints (Kanellakis et al. 1995) or a particular special-purpose language or system, such as an expert system, a geographical
information system, or a planning system. Of course, the user is responsible for a
sound speciﬁcation of the language constraints and the deﬁnition of the interface
functions.
The meta-solver system meta-s (Frank et al. 2003b; Frank et al. 2003a) implements our ideas. Even though meta-s provides programming constructs for its
integration into other applications, which may even be imperative languages, the
true integration of imperative languages according to our approach is an open question and a topic of future research. The main reason is that declarative languages
abstract from real-world issues such as time and state while imperative languages
are time-dependent which complicates their integration also for our approach.
The choice of an appropriate cooperation strategy plays an important role for
the eﬃciency of the cooperating system (Frank et al. 2003a).
The deﬁnition of solver cooperation strategies is also very interesting in the case
of language solvers. This will allow for example to switch from depth-ﬁrst search
to breadth-ﬁrst search or an evaluation mechanism based on the Andorra principle
(Costa et al. 1991; Warren 1988) using a logic language without reimplementing
the evaluation mechanisms. The system meta-s already oﬀers predeﬁned strategy
patterns for these search strategies which can be reﬁned by problem-dependent
knowledge or user knowledge about the program.
If the user is able to deﬁne cooperation strategies for the solvers and the language(s) or to reﬁne them on the base of predeﬁned strategy patterns (as given in
our implementation), she/he can also employ problem-dependent knowledge and
user knowledge, e. g. about the termination of particular predicates, to guide the
computation.
First results (Frank et al. 2004) on the integration of language solvers into the
meta-solver framework meta-s according to the described approach conﬁrm our
theoretical considerations.

Integration of Declarative and Constraint Programming

27

Finally, the approach opens a further interesting perspective: A simple approach
for the combination of diﬀerent languages consists of the deﬁnition of an explicit
interface and providing language constructs for initialising subcomputations in the
particular languages. In this way one reaches a loose coupling and interaction of
programs written in diﬀerent languages.
Our cooperation framework bases on a similar idea: It provides a meta mechanism which takes care of the strategy of the cooperating solvers and provides the
constraint pool for maintaining and managing common data and constraints. Besides this the main concept is the uniform solver interface which allows to integrate
declarative languages as solvers as shown above. Using this interface it is not only
possible to integrate constraint solvers and language evaluation mechanisms but
also to integrate language evaluation mechanisms among each other by appropriate interface deﬁnitions. This ﬁnally yields a language interaction according to the
above sketched interface model.
Related Work. López-Fraguas (1992) considered a general scheme CFLP(X) for
constraint functional logic programming. The scheme is based on lazy functional
logic languages and allows beside conditions constraints in the guards of the rules.
Using our cooperation approach, we achieve a covering of the CFLP(X) and CLP(X)
(Jaﬀar and Lassez 1987) approaches. In (Hortalá-González et al. 1997) and (Fernández et al. 2003),
extending CFLP(X), functional logic programming is integrated with real arithmetic and ﬁnite domain constraints respectively. The lazy functional logic languages
toy(R) and toy(F D) are the respective implementations. Lux (2001) integrates
linear constraints over real numbers into the functional logic language curry in a
similar way.
open cflp by Kobayashi et al. (2003) combines a functional logic host language
with collaborating equational solvers which may be distributed in an open environment. It provides the user with a declarative strategy deﬁnition for the cooperating solvers basing upon a set of basic operators. However, the strategy language of
meta-s gives ﬁner control over the individual collaboration steps because of its well
considered solver interface on the one hand and its structural pattern-matching and
constraint rewriting facilities which provide a ﬁner and more intuitive control for
strategy deﬁnition on the other hand.
While our approach pursues the idea to integrate languages into a system of cooperating solvers the approaches (López-Fraguas 1992; Hortalá-González et al. 1997;
Fernández et al. 2003; Kobayashi et al. 2003; Lux 2001) come from the opposite
point of view and extend the functional logic program evaluation by constraint
evaluation.
In contrast to the other approaches our framework allows the integration of several constraint systems. The user can integrate desired domains and solvers which
satisfy the interface requirements as discussed in Sect. 3. The opportunity to integrate diﬀerent host languages and constraint systems also distinguishes our approach from other existing systems of cooperating solvers (for example (Hong 1994;
Monfroy 1996; Rueher 1995)) that usually have one ﬁxed host language (a logic language).

28

Petra Hofstedt and Peter Pepper

Furthermore both, the above mentioned languages and the cooperative systems,
mainly have a ﬁxed order of evaluation of constraints and functional expressions
resp. In contrast, an integration according to our ideas using the meta-s system
allows the user to either deﬁne its own strategies or to reﬁne existing strategy
patterns in a simple way. The usefulness of diﬀerent cooperation strategies has been
proven for usual solvers (e. g. on arithmetic, see (Frank et al. 2003b)). As well, ﬁrst
results for the integration of a logic language into meta-s conﬁrm their usefulness
for language solvers (Frank et al. 2004).
oz (Müller et al. 1995) supports (constraint) logic, functional and object-oriented
programming styles within one (as well ﬁxed) language. The computation in oz is
based on the concept of computation spaces (Schulte 2002) which consist of a constraint store containing only basic constraints and propagators (for more complex
constraints) manipulating them. Similar to our framework, computation spaces can
be used to describe solver cooperations and search strategies. However, this relies
on all solvers sharing the same store format and hence is not satisfying for the main
goal of our approach, i. e. the cooperation of black box solvers independent of their
implementation.
Acknowledgement. We want to thank our colleague Stephan Frank for many valuable
comments and his assistance in preparing the manuscript. Our particular thanks goes to
the reviewers who provided detailed and insightful comments that helped to improve the
paper considerably.

References
Aı̈t-Kaci, H. and Nasr, R. 1989. Integrating Logic and Functional Programming. Lisp
and Symbolic Computation 2, 1, 51–89.
Broy, M., Wirsing, M., and Pepper, P. 1987. On the Algebraic Definition of Programming Languages. ACM Transactions on Programming Languages and Systems 9, 1
(January), 54–99.
Cheadle, A. M., Harvey, W., Sadler, A. J., Schimpf, J., Shen, K., and Wallace,
M. G. 2003. ECLi PSe . An Introduction. Tech. Rep. IC-PARC-03-1, Centre for Planning
and Resource Control, Imperial College London.
Costa, V. S., Warren, D. H., and Yang, R. 1991. Andorra-I: A Parallel Prolog System
that Transparently Exploits both And- and Or-Parallelism. In Third ACM SIGPLAN
Symposium on Principles and Practice of Parallel Programming – PPOPP. SIGPLAN
Notices, vol. 26 (7). ACM Press, 83–93.
Didrich, K., Fett, A., Gerke, C., Grieskamp, W., and Pepper, P. 1994. OPAL:
Design and Implementation of an Algebraic Programming Language. In International
Conference on Programming Languages and System Architectures, J. Gutknecht, Ed.
LNCS, vol. 782. Springer, 228–244.
Fernández, A., Hortalá-Gonzáles, T., and Sáenz-Pérez, F. 2003. Solving Combinatorial Problems with a Constraint Functional Logic Language. In Practical Aspects of
Declarative Languages, 5th International Symposium – PADL, V. Dahl and P. Wadler,
Eds. LNCS, vol. 2562. Springer, 320–338.
Field, A. and Harrison, P. 1988. Functional Programming. Addison-Wesley.
Frank, S., Hofstedt, P., and Mai, P. R. 2003a. A Flexible Meta-solver Framework for
Constraint Solver Collaboration. In Advances in Artificial Intelligence, 26th German

Integration of Declarative and Constraint Programming

29

Conference on Artificial Intelligence – KI 2003, A. Günter, R. Kruse, and B. Neumann,
Eds. LNCS, vol. 2821. Springer, Kiel, Germany, 520–534.
Frank, S., Hofstedt, P., and Mai, P. R. 2003b. Meta-S: A Strategy-oriented MetaSolver Framework. In 16th International Florida Artificial Intelligence Research Society
Conference – FLAIRS, I. Russell and S. M. Haller, Eds. The AAAI Press, St. Augustine,
Florida, 177–181.
Frank, S., Hofstedt, P., and Reckmann, D. 2004. Strategies for the Efficient Solution
of Hybrid Constraint Logic Programs. In Third Workshop on Multiparadigm Constraint
Programming Languages – MultiCPL, S. Muñoz-Hernández, J. M. Gómez-Perez, and
P. Hofstedt, Eds. Saint-Malo, France, 103–117.
Hanus, M. 1994. The Integration of Functions into Logic Programming: From Theory to
Practice. Journal of Logic Programming 19/20, 583–628.
Hanus, M. 1995. On Extra Variables in (Equational) Logic Programming. In Twelfth
International Conference on Logic Programming. MIT Press, 665–679.
Hanus, M., Antoy, S., Kuchen, H., López-Fraguas, F. J., Lux, W., MorenoNavarro, J. J., and Steiner, F. 2003. Curry: An Integrated Functional Logic Language. Report. Version 0.8 of April 15, 2003.
Hofstedt, P. 2000a. Better Communication for Tighter Cooperation. In First International Conference on Computational Logic – CL. LNCS, vol. 1861. Springer, 342–358.
Hofstedt, P. 2000b. Cooperating Constraint Solvers. In Sixth International Conference
on Principles and Practice of Constraint Programming – CP. LNCS, vol. 1894. Springer,
520–524.
Hofstedt, P. 2001. Cooperation and Coordination of Constraint Solvers. Ph.D. thesis,
Dresden University of Technology.
Hong, H. 1994. Confluency of Cooperative Constraint Solvers. Tech. Rep. 94–08, Research
Institute for Symbolic Computation, Linz, Austria.
Hortalá-González, T., López-Fraguas, F., Sánchez-Hernández, J., and UllánHernández, E. 1997. Declarative Programming with real Constraints. Tech. Rep. SIP
5997, Universidad Complutense de Madrid.
Hudak, P., Peterson, J., and Fasel, J. H. 2000.
A Gentle Introduction
to Haskell 98.
Tech. rep., Yale University, Department of Computer Science.
http://www.haskell.org/tutorial/, visited 2005-11-18.
Jaffar, J. and Lassez, J.-L. 1987. Constraint Logic Programming. In 14th ACM
Symposium on Principles of Programming Languages – POPL. ACM Press, 111–119.
Jaffar, J., Maher, M., Marriott, K., and Stuckey, P. 1998. The Semantics of
Constraint Logic Programs. Journal of Logic Programming 37, 1-3, 1–46.
Kanellakis, P., Kuper, G., and Revesz, P. 1995. Constraint Query Languages. Journal
of Computer and System Sciences 51, 1, 26–52.
Kobayashi, N., Marin, M., and Ida, T. 2003. Collaborative Constraint Functional Logic
Programming System in an Open Environment. IEICE Transactions on Information
and Systems E86-D, 1, 63–70.
Loogen, R. 1995. Integration funktionaler und logischer Programmiersprachen. Oldenbourg.
López-Fraguas, F.-J. 1992. A General Scheme for Constraint Functional Logic Programming. In Algebraic and Logic Programming – ALP, H. Kirchner and G. Levi, Eds.
LNCS, vol. 632. Springer, 213–227.
Lux, W. 2001. Adding Linear Constraints over Real Numbers to Curry. In Functional and
Logic Programming, 5th International Symposium – FLOPS, H. Kuchen and K. Ueda,
Eds. LNCS, vol. 2024. Springer, 185–200.
Manna, Z. 1974. Mathematical Theory of Computation. McGraw-Hill.

30

Petra Hofstedt and Peter Pepper

Middeldorp, A. and Hamoen, E. 1994. Completeness Results for Basic Narrowing.
Applicable Algebra in Engineering, Communication and Computing 5, 213–253.
Monfroy, E. 1996. Solver Collaboration for Constraint Logic Programming. Ph.D. thesis,
Centre de Recherche en Informatique de Nancy. INRIA.
Moreno-Navarro, J. and Rodrı́guez-Artalejo, M. 1992. Logic Programming
with Functions and Predicates: The Language BABEL. Journal for Logic Programming 12, 3&4, 191–223.
Müller, M., Müller, T., and Van Roy, P. 1995. Multiparadigm Programming in Oz.
In Workshop on Visions for the Future of Logic Programming, D. Smith, O. Ridoux,
and P. V. Roy, Eds. Portland, Oregon.
Nilsson, U. and Maluszyński, J. 1995. Logic, Programming and Prolog. John Wiley &
Sons Ltd.
Palamidessi, C. 1990. Algebraic Properties of Idempotent Substitutions. In Automata,
Languages and Programming – ICALP, M. Paterson, Ed. LNCS, vol. 443. Springer,
386–399.
Reddy, U. 1985. Narrowing as the Operational Semantics of Functional Languages. In
IEEE Symposium on Logic Programming. 138–151.
Rueher, M. 1995. An Architecture for Cooperating Constraint Solvers on Reals. In
Constraint Programming: Basics and Trends, A. Podelski, Ed. LNCS, vol. 910. Springer,
231–250.
Schulte, C. 2002. Programming Constraint Services. LNCS, vol. 2302. Springer.
Suzuki, T., Middeldorp, A., and Ida, T. 1995. Level-Confluence of Conditional Rewrite
Systems with Extra Variables in Right-Hand Sides. In 6th International Conference on
Rewriting Techniques and Applications. LNCS, vol. 914. Springer, 179–193.
Warren, D. H. 1988. The Andorra Principle. Presented at the Gigalips Workshop,
Swedish Institute of Computer Science (SICS), Stockholm, Sweden.
Westfold, S. J. and Smith, D. R. 2001. Synthesis of Efficient Constraint Satisfaction
Programs. In Knowledge Engineering Reviews. Special Issue on AI and OR. Kestrel
Institute Technical Report KES.U.01.7.
Winskel, G. 1993. Formal Semantics of Programming Languages. MIT Press.

