To appear in Theory and Practice of Logic Programming (TPLP)

1

arXiv:cs/0601071v1 [cs.PL] 16 Jan 2006

Constraint Functional Logic Programming over
Finite Domains
ANTONIO J. FERNÁNDEZ ∗
Dpto. de Lenguajes y Ciencias de la Computación,
Universidad de Málaga, Spain
E-mail: afdez@lcc.uma.es

TERESA HORTALÁ-GONZÁLEZ†,
FERNANDO SÁENZ-PÉREZ † and RAFAEL DEL VADO-VÍRSEDA ‡
Dpto. de Sistemas Informáticos y Programación
Universidad Complutense de Madrid, Spain
E-mails: {teresa,fernan,rdelvado}@sip.ucm.es
submitted 15 July 2004; revised 1 August 2005; accepted 13 January 2006

Abstract
In this paper, we present our proposal to Constraint Functional Logic Programming over
Finite Domains (CF LP (FD) ) with a lazy functional logic programming language which
seamlessly embodies finite domain (FD) constraints. This proposal increases the expressiveness and power of constraint logic programming over finite domains (CLP (FD) ) by
combining functional and relational notation, curried expressions, higher-order functions,
patterns, partial applications, non-determinism, lazy evaluation, logical variables, types,
domain variables, constraint composition, and finite domain constraints.
We describe the syntax of the language, its type discipline, and its declarative and operational semantics. We also describe T OY(FD), an implementation for CF LP (FD) , and a
comparison of our approach with respect to CLP (FD) from a programming point of view,
showing the new features we introduce. And, finally, we show a performance analysis which
demonstrates that our implementation is competitive with respect to existing CLP (FD)
systems and that clearly outperforms the closer approach to CF LP (FD) .
KEYWORDS: Constraint Logic Programming, Functional Logic Programming, Finite Domains.

1 Introduction
Constraint logic programming (CLP ) (Jaffar and Maher 1994) was born from a
desire to have both a better problem expression and performance than logic pro∗ This author was partially supported by Spanish MCyT under contracts TIN2004-7943-C04-01
and TIN2005-08818-C04-01.
† The work of this author has been supported by the Spanish project PR 48/01-9901 funded by
UCM.
‡ The work of this author has been partially supported by the Spanish National Project MELODIAS (TIC2002-01167).

2 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
gramming (LP ). Its success lies in that it combines the declarativeness of LP with
the efficiency of the constraint programming (CP ) paradigm. The essential component of the CLP schema is that it can be parameterized by a computational
domain so that different domains determine different instances of the schema. Constraint Programming over finite domains (CP (F D)) (Marriot and Stuckey 1998;
Henz and Müller 2000) has emerged as one of the most exciting paradigms of programming in recent decades. There are several reasons for the interest that CP (F D)
has raised: (1) the strong theoretical foundations (Tsang 1993; Apt 2003; Frühwirth and Abdennadher 2003)
that make CP a sound programming paradigm; (2) CP (F D) is a heterogeneous
field of research ranging from theoretical topics in mathematical logic to practical
applications in industry (particularly, problems involving heterogeneous constraints
and combinatorial search) and (3) CP is based on posing constraints, which are basically true relations among domain variables. For this last reason, the declarative
languages seem to be more appropriate than imperative languages to formulate F D
constraint problems. In particular, one of the most successful instances of CP (F D)
is CLP (F D) .
Another well-known instance of declarative programming (DP ) is functional programming (F P ). The basic operations in functional languages are defined using
functions which are invoked using function applications and put together using
function composition. F P gives great flexibility, different from that provided by
(C)LP , to the programmer, because functions are first-class citizens, that is, they
can be used as any other object in the language (i.e., results, arguments, elements
of data structures, etc). Functional languages provide evident advantages such as
declarativeness, higher-order functions, polymorphism and lazy evaluation, among
others. To increase the performance, one may think of integrating F D constraints
into F P (as already done in LP ). However, literature lacks proposals in this sense
and the reason seems to lie in the relational nature of F D constraints, which do
not fit well in F P . In spite of this limitation, it seems clear that the integration of
F D constraints into F P is interesting not only for F P but also for discrete constraint programming, as the constraint community may benefit from the multiple
advantages of F P .
More recently, functional logic programming (F LP ) emerges with the aim to
integrate the declarative advantages from both F P and LP . F LP gives rise to
new features which cannot be found neither in F P nor in LP (Hanus 1994). F LP
has not the inherent limitations of F P and thus it is an adequate framework
for the integration of functions and constraints. To our best knowledge, the first
proposal for a constraint functional logic programming scheme (CF LP ) that attempts to combine constraint logic programming and functional logic programming
is (Darlington et al. 1992). The idea behind this approach can be roughly described
by the equation CF LP (D) = CLP (F P (D)), intended to mean that a CF LP language over the constraint domain D is viewed as a CLP language over an extended
constraint domain F P (D) whose constraints include equations between expressions
involving user defined functions, which will be solved via narrowing. Further, the
CF LP scheme proposed by F.J. López-Fraguas in (López-Fraguas 1992) tried to
provide a declarative semantics such that CLP (D) programs could be formally

Constraint Functional Logic Programming over Finite Domains

3

understood as a particular case of CF LP (D) programs. In the classical approach
to CLP semantics, a constraint domain is viewed as a first-order structure D,
and constraints are viewed as first-order formulas that can be interpreted in D.
In (López-Fraguas 1992), CF LP (D) programs were built as sets of constrained
rewriting rules. In order to support a lazy semantics for the user defined functions,
constraint domains D were formalized as continuous structures, with a Scott domain
(Gunter and Scott 1990) as a carrier, and a continuous interpretation of function
and predicate symbols. The resulting semantics had many pleasant properties, but
also some limitations. In particular, defined functions had to be first-order and deterministic, and the use of patterns in function definitions had to be simulated by
means of special constraints.
In a recent work (López-Fraguas et al. 2004a), a new generic scheme CF LP (D)
has been proposed, intended as a logical and semantic framework for lazy Constraint
Functional Logic Programming over a parametrically given constraint domain D,
which provides a clean and rigorous declarative semantics for CF LP (D) languages
as in the CLP (D) scheme, overcoming the limitations of the older CF LP (D)
scheme (López-Fraguas 1992). CF LP (D) programs are presented as sets of constrained rewriting rules that define the behavior of possibly higher-order and/or
non-deterministic lazy functions over D. The main novelties in (López-Fraguas et al. 2004a)
were a new formalization of constraint domains for CF LP , a new notion of interpretation for CF LP (D) programs, and a new Constraint Rewriting Logic CRW L(D)
parameterized by a constraint domain, which provides a logical characterization of
program semantics. Further, (López-Fraguas et al. 2004b) has formalized an operational semantics for the new generic scheme CF LP (D) proposed in (López-Fraguas et al. 2004a).
This work presented a constrained lazy narrowing calculus CLN C(D) for solving goals for CF LP (D) programs, which was proved sound and strongly complete
with respect to CRW L(D)’s semantics. These properties qualified CLN C(D) as
a convenient computation mechanism for declarative constraint programming languages. More recently, (del Vado-Vı́rseda 2005) presented an optimization of the
CLN C(D) calculus by means of definitional trees (Antoy 1992) to efficiently control
the computation. This new constrained demanded narrowing calculus CDN C(D)
preserves the soundness and completeness properties of CLN C(D) and maintains
the good properties shown for needed and demand-driven narrowing strategies
(Loogen et al. 1993; Antoy et al. 2000; del Vado-Vı́rseda 2003). These properties
adequately render CDN C(D) as a concrete specification for the implementation of
the computational behavior in existing CF LP (D) systems such as T OY (Caballero et al. 1997)
and Curry (Hanus 1999).
The main contributions of the paper are listed below:
• The paper describes the theoretical foundations for the CF LP (F D) language, i.e., a concrete instance of the general scheme CF LP (D) presented in
(López-Fraguas et al. 2004a; López-Fraguas et al. 2004b). First, this instance
includes an explicit treatment of a type system for constraints as well as for
programs, goals and answers. Second, it also presents a new formalization of
the constraint finite domain F D for CF LP that includes a succinct declara-

4 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
tive semantics (similarly as done for CLP ) for an enough-expressive primitive
constraints set. Finally, it provides the formal specification of a finite domain
constraint solver defined over those primitive constraints that constitutes the
theoretical basis for the implementation of correct propagation solvers.
• The paper presents an operational semantics for finite domain constraint solving on declarative languages using a new constraint lazy narrowing calculus
CLN C(F D), consisting of a natural and novel combination of lazy evaluation and F D constraint solving that does not exist, to our knowledge, in any
declarative constraint solver (see (López-Fraguas et al. 2004b) and Section 5).
This operational semantics is defined with respect to a constraint rewriting
logic over a F D setting that makes it very different from the operational
behavior of CLP (F D) languages.
• The paper presents T OY(F D) from a programming point of view, which is
the first CF LP (F D) system that provides a wide set of F D constraints comparable to existing CLP (F D) systems and which is competitive with them,
as shown with performance results. Also, the advantages of combining F D
constraints into F LP are highlighted via examples. Our system is therefore a
contribution for increasing the expressiveness and efficiency of F LP by using
F D constraints and a state-of-the-art propagation solver.
The structure of the paper is as follows. Section 2 presents our CF LP (F D)
language by describing its type discipline, patterns and expressions, finite domains,
and constraint solvers. In Section 3, we provide a constraint lazy narrowing calculus
over F D domains (CLN C(F D)) along with the notions of well-typed programs,
admissible goals, and correct answers. Next, Section 4 describes our implementation
of CF LP (F D): T OY(F D), highlighting the advantages obtained from embodying
constraints into a functional logic language with respect to CLP (F D) , and comparing the performance of our CF LP (F D) system with other declarative constraint
systems. Section 5 discusses related work and, finally, Section 6 summarizes some
conclusions and points out future work.

2 The CF LP (F D) Language
We propose a constraint functional logic programming language over finite domains
which is a pure declarative language, typed, lazy, and higher-order, and that provides support for constraint solving over finite domains. CF LP (F D) aims to the
integration of the best features of existing functional and logic languages into F D
constraint solving.
In this section, we present the basis of our CF LP (F D) language about syntax,
type discipline, and declarative semantics. We also formalize the notion of a constraint finite domain and specify the expected behavior that a F D constraint solver
attached to our CF LP (F D) language must hold.

Constraint Functional Logic Programming over Finite Domains

5

2.1 Polymorphic Signatures
We assume a countable set TVar of type variables α, β, . . . and a countable ranked
S
alphabet T C = n∈N T C n of type constructors C ∈ T C n . Types τ ∈ Type have
the syntax τ ::= α | C τ1 . . . τn | τ → τ ′ | (τ1 , . . . , τn ).
By convention, C τ n abbreviates C τ1 . . . τn , “→” associates to the right, τ n → τ
abbreviates τ1 → · · · → τn → τ , and the set of type variables occurring in τ is
written tvar(τ ). A type τ is called monomorphic iff tvar(τ ) = ∅, and polymorphic
otherwise. (τ1 , . . . , τn ) is a type intended to denote n-tuples. A type without any
occurrence of “→” is called a datatype. Datatype definitions declare new (possibly
polymorphic) constructed types and determine a set of data constructors for each
type. Our CF LP (F D) language provides predefined types such as [A] (the type of
polymorphic lists, for which Prolog notation is used), bool (with constants true and
f alse), int for integer numbers, char (with constants a, b, . . . ) or success (with
constant ⊤).
A polymorphic signature over T C is a triple Σ = hT C, DC, F Si, where DC =
S
S
n
n
n∈N F S are ranked sets of data constructors and evaluable
n∈N DC and F S =
function symbols. Evaluable functions can be further classified into domain dependent primitive functions P F n ⊆ F S n and user defined functions DF n = F S n \
P F n for each n ∈ N.
Each n-ary c ∈ DC n comes with a principal type declaration c :: τ n → C αk ,
where n, k ≥ 0, α1 , . . . , αk are pairwise different, τi are datatypes, and tvar(τi ) ⊆
{α1 ,. . . , αk } for all 1 ≤ i ≤ n. Also, every n-ary f ∈ F S n comes with a principal
type declaration f :: τ n → τ , where τi , τ are arbitrary types. For any polymorphic
signature Σ, we write Σ⊥ for the result of extending DC 0 in Σ with a special
data constructor ⊥, intended to represent an undefined value that belongs to every
type. We also assume that DC 0 includes the three constants mentioned above
true, f alse :: bool, and ⊤ :: success, which are useful for representing the results
returned by various primitive functions. As notational conventions, in the rest of
the paper, we use c, d ∈ DC, f, g ∈ F S and h ∈ DC ∪ F S, and we define the arity
of h ∈ DC n ∪ F S n as ar(h) = n.

2.2 Expressions, Patterns and Substitutions
In the sequel, we always assume a given polymorphic signature Σ, often not made
explicit in the notation. We introduce the syntax of applicative expressions and
patterns, which is needed for understanding the construction of constraint finite
domains and constraint finite domain solvers. We assume a countably infinite set
Var of (data) variables X, Y, . . . and the integer set Z of primitive elements 0, 1,
−1, 2, −2, . . . , mutually disjoint and disjoint from TVar and Σ. Primitive elements
are intended to represent the finite domain specific set of integer values.
An expression e ∈ Exp⊥ (Z) has the syntax e ::= ⊥ | u | X | h | (e e′ ) |
(e1 , . . . , en ) where u ∈ Z, X ∈ Var, h ∈ DC ∪ F S, (e e′ ) stands for the application
operation which applies the function denoted by e to the argument denoted by
e′ and (e1 , . . . , en ) represents tuples with n components. The set of data variables

6 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
occurring in e is written var(e). Moreover, e is called linear iff every X ∈ var(e)
has a single occurrence in e, ground iff var(e) = ∅ and total iff is an expression
with no occurrences of ⊥. Partial patterns t ∈ P at⊥ (Z) ⊂ Exp⊥ (Z) are built as
t ::= ⊥ | u | X | c t1 . . . tm | f t1 . . . tn where u ∈ Z, X ∈ Var, c ∈ DC with
m ≤ ar(c), and f ∈ F S with n < ar(f ). Notice that partial applications (i.e.,
application to less arguments than indicated by the arity) of c and f are allowed as
patterns, which are then called higher-order patterns (González-Moreno et al. 99b),
because they have a functional type. We define the information ordering ⊑ as the
least partial ordering over P at⊥ (Z) satisfying the following properties: ⊥ ⊑ t for
all t ∈ P at⊥ (Z) and h tm ⊑ h t′m whenever these two expressions are patterns and
ti ⊑ t′i for all i ∈ {1, . . . , m}.
As usual, we define (data) substitutions σ ∈ Sub⊥ (Z) as mappings σ : Var →
P at⊥ (Z) extended to σ : Exp⊥ (Z) → Exp⊥ (Z) in the natural way. By convention,
we write ε for the identity substitution, eσ instead of σ(e) and σθ for the composition of σ and θ. We define the domain dom(σ) of a substitution σ in the usual way.
A substitution σ such that σσ = σ is called idempotent. For any set of variables
X ⊆ Var we define the restriction σ ↾ X as the substitution σ ′ such that dom(σ ′ )
= X and σ ′ (X) = σ(X) for all X ∈ X . We use the notation σ =X θ to indicate
that σ ↾ X = θ ↾ X , and we abbreviate σ =Var\X θ as σ =\X θ. Type substitutions
can be defined similarly, as mappings σt : TVar → Type with a unique extension
σ̂t : Type → Type, denoted also as σt . The set of all type substitutions is denoted as
TSubst. Most of the concepts and notations for data substitutions (such as domain,
composition, etc.) make sense also for type substitutions, and we will freely use
them when needed.
2.3 Well-typed Expressions
Inspired by Milner’s type system (Damas and Milner 1982) we now introduce the
notion of well-typed expression. We define a type environment as any set T of type
assumptions X :: τ for data variables s.t. T does not include two different assumptions for the same variable. The domain dom(T ) of a type environment is the set
of all the data variables that occur in T . For any variable X ∈ dom(T ), the unique
type τ s.t. (X :: τ ) ∈ T is denoted as T (X). The notation (h :: τ ) ∈var Σ is
used to indicate that Σ includes the type declaration h :: τ up to a renaming of
type variables. Type judgements (Σ, T ) ⊢W T e :: τ with e ∈ Exp⊥ (Z) are derived
by means of the following type inference rules:
(Σ, T ) ⊢W T
(Σ, T ) ⊢W T
(Σ, T ) ⊢W T
(Σ, T ) ⊢W T
(Σ, T ) ⊢W T

u :: int, for every u ∈ Z.
X :: τ , if T (X) = τ .
h :: τ σt , if (h :: τ ) ∈var Σ⊥ , σt ∈ TSubst.
(e e′ ) :: τ , if (Σ, T ) ⊢W T e :: (τ ′ → τ ), (Σ, T ) ⊢W T e′ :: τ ′ ,
for some τ ′ ∈ Type.
(e1 , . . . ,en ) :: (τ1 , . . . ,τn ), if ∀i ∈ {1, . . . ,n} : (Σ, T ) ⊢W T ei :: τi .

An expression e ∈ Exp ⊥ is called well-typed iff there exist some type environment
T and some type τ , such that the type judgement (Σ, T ) ⊢W T e :: τ can be derived.

Constraint Functional Logic Programming over Finite Domains

7

Expressions that admit more than one type are called polymorphic. A well-typed
expression always admits a so-called principal type (PT) that is more general than
any other. A pattern whose PT determines the PTs of its subpatterns is called
transparent.

2.4 The Constraint Finite Domain F D
Adopting the general approach of (López-Fraguas et al. 2004a; López-Fraguas et al. 2004b),
a constraint finite domain F D can be formalized as a structure with carrier set DZ ,
consisting of ground patterns built from the symbols in a polymorphic signature Σ
and the set of primitive elements Z. Symbols in Σ are intended to represent data
constructors (e.g., the list constructor), domain specific primitive functions (e.g.,
addition and multiplication over Z) satisfying monotonicity, antimonotonicity and
radicality properties (see (López-Fraguas et al. 2004a) for details), and user defined
functions. Requiring primitives to be radical, which just means that for given arguments, they are expected to return a total result, unless the arguments bear too
few information for returning any result different from ⊥. As we will see in the next
subsection, it is also possible to instantiate this notion of constraint finite domain
by adding a new formal specification of a constraint finite domain solver SolveF D
as the theoretical basis of our operational semantics and implementation.
Assuming then a constraint finite domain F D, we define first the syntax and
semantics of constraints over F D used in this work. In contrast to CLP (F D), our
constraints can include now occurrences of user defined functions and can return
any value of the Type set.
• Primitive constraints have the syntactic form p tn →! t , being p ∈ P F n a
primitive function symbol and t1 , . . . , tn , t ∈ P at⊥ (Z) with t total.
• Constraints have the syntactic form p en →! t , with p ∈ P F n , e1 , . . . , en ∈
Exp⊥ (Z) and t ∈ P at⊥ (Z) total.
In the sequel, we use the notation P Con(F D) for the set of all the primitive constraints π over F D. We reserve the capital letter Π for sets of primitive constraints,
often interpreted as conjunctions. The semantics of primitive constraints depends
on the notion of valuation V al(F D) over F D, defined as the set of substitutions of
ground patterns for variables. The set of solutions of π ∈ P Con(F D) is a subset
SolF D (π) ⊆ V al(F D) that satisfy π in F D in the sense of (López-Fraguas et al. 2004a).
Analogously, the set of solutions of Π ⊆ P Con(F D) is defined as SolF D (Π) =
T
σ with
π∈ Π SolF D (π). Moreover, we define the set of solutions of a pair Π
σ) = SolF D (Π) ∩ Sol(σ), where Sol(σ) is the set of
σ ∈ Sub⊥ (Z) as SolF D (Π
valuations η such that Xη ≡ tη for each X 7→ t ∈ σ.
The next definition presents a possible specific polymorphic signature with finite domain constraints constituted by a minimum set of primitive function symbols with their corresponding declarative semantics. By means of this signature,
our CF LP (F D) language allows the management of the usual finite domain constraints defined over Z in CLP (F D) and also equality and disequality constraints

8 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
defined over P at⊥ (Z) in a similar way as done in (González-Moreno et al. 99b).
Definition 1
Consider the following usual primitive operators and relations defined over Z:
⊗Z :: int → int → int, where ⊗ ∈ {+, −, ∗, /}
≍Z :: int → int → bool, where ≍ ∈ {=, 6=, <, ≤, >, ≥}.
Table 1. Primitive Function Symbols in F D and their Declarative Interpretation
Strict Equality
(on patterns)

seq :: α → α → bool
seq F D : DZ × DZ → {true, f alse, ⊥}
seq F D t t → true, ∀t ∈ DZ total
seq F D t1 t2 → f alse, ∀t1 , t2 ∈ DZ . t1 , t2 have no common upper
bound w.r.t. the information ordering ⊑
seq F D t1 t2 → ⊥, otherwise

Less or Equal
(on integers)

leq :: int → int → bool
leq F D : DZ × DZ → {true, f alse, ⊥}
leq F D u1 u2 → true, if u1 , u2 ∈ Z and u1 ≤Z u2
leq F D u1 u2 → f alse, if u1 , u2 ∈ Z and u1 >Z u2
leq F D u1 u2 → ⊥, otherwise

Operators
(on integers)

⊗ :: int → int → int
⊗F D : DZ × DZ → DZ
⊗F D u1 u2 → u1 ⊗Z u2 , if u1 , u2 ∈ Z
⊗F D u1 u2 → ⊥, otherwise

Finite Domains

domain :: int → [int] → bool
domainF D : DZ × DZ → {true, f alse, ⊥}
domainF D u [u1 , . . . , un ] → true,
if ∀i ∈ {1, . . . , n−1}.ui ≤Z ui+1 and ∃i ∈ {1, . . . , n}.u =Z ui
domainF D u [u1 , . . . , un ] → f alse,
if ∃i ∈ {1, . . . , n−1}.ui >Z ui+1 or ∀i ∈ {1, . . . , n}.u 6=Z ui
domainF D u [u1 , . . . , un ] → ⊥, otherwise

Variable Labeling

indomain :: int → success
indomainF D : DZ → {⊤, ⊥}
indomainF D u → ⊤, if u ∈ Z
indomainF D u → ⊥, otherwise

Table 1 shows the set of primitive functions p ∈ P F n with their corresponding
type declarations and their declarative interpretation pF D ⊆ DZn × DZ considered
in our constraint finite domain F D (we use the notation pF D tn → t to indicate that
(tn , t) ∈ pF D ). We note that all our primitive functions satisfy the aforementioned
properties.


Constraint Functional Logic Programming over Finite Domains

9

The function indomain is the basis for a labeling (enumeration or search) strategy,
which is crucial in constraint solving efficiency. labeling is applied when no more
constraint propagation is possible, and its basic step consists of selecting a variable
X with a non-empty, non-singleton domain, selecting a value u of this domain,
and assigning u to X. We note that in our framework, various labeling strategies
(variable and value selection) have all the same declarative semantics, but they may
differ in their operational behavior and therefore in efficiency as it happens in the
CLP (F D) setting (more details can be found in Section 4.5.1). In the rest of the
paper, when opportune, we use the following notations:
• t == s abbreviates seq t s →! true and t \ = s abbreviates seq t s →! f alse
(the notations = and 6= can be understood as a particular case of the notations
== and \ = when these are applied to integers and/or integer variables).
• a ≤ b abbreviates leq a b →! true (and analogously for the other comparison
primitives <, > and ≥).
• a ⊗ b ≍ c abbreviates a ⊗ b →! r, r ≍ c.
• u ∈ D abbreviates domain u D →! true and u1 , . . . , un ∈ D abbreviates
u1 ∈ D ∧ . . . ∧ un ∈ D. Analogously, u ∈
/ D abbreviates domain u D →! f alse
and u1 , . . . , un ∈
/ D abbreviates u1 ∈
/ D ∧ . . . ∧ un ∈
/ D.
• domain [u1 , . . . , un ] a b with a, b ∈ Z (a ≤ b) abbreviates u1 , . . . , un ∈ [a .. b],
where [a .. b] represents the integer list [a, a + 1, . . . , b − 1, b] that intuitively
represents the integer interval [a,b].
• labeling L [u1 , . . . , un ] abbreviates and extends indomain u1 →! ⊤ ∧ . . . ∧
indomain un →! ⊤ with a list L of predefined constants that allow to specify
different labeling strategies.
Using these notations, a primitive constraint store S ⊆ P Con(F D) can be expressed
as a finite conjunction of primitive constraints of the form t == s, t \ = s, u ∈ D,
u∈
/ D, a ⊗ b ≍ c, domain [u1 , . . . , un ] a b and/or labeling L [u1 , . . . , un ] where t, s
are total patterns, ui , u, a, b, c ∈ Z ∪ Var, and L, D are total patterns representing
a variable or a list.
2.5 Constraint Solvers over F D
The design of a suitable operational semantics over finite domains for goal solving
in CF LP (F D) combines constrained lazy narrowing with constraint solving over
a given constraint finite domain F D. The central notion of lazy narrowing can be
found in the literature, e.g., (Middeldorp and Okui 1998; Middeldorp et al. 2002).
In this subsection, we describe the expected behavior of a constraint solver over the
finite constraint domain F D w.r.t. the semantics given in the previous subsection,
as the basis of our goal solving mechanism.
Definition 2
A constraint solver over a given constraint domain F D is a function named SolveF D
expecting as parameters a finite primitive constraint store S ⊆ P Con(F D) in the
sense of Definition 1 and a finite set of variables χ ⊆ Var called the set of protected variables. The constraint solver is expected to return a finite disjunction of

10 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
Wk
k alternatives: SolveF D (S, χ) = i=1 (Si σi ), where each Si ⊆ P Con(F D) and
each σi ∈ Sub⊥ (Z) is a total idempotent substitution satisfying the following requirements: no alternative can bind protected variables, for each alternative either
all the protected variables disappear or some protected variable becomes demanded
(i.e., no solution can bind these variables to an undefined value), no solution is lost
by the constraint solver, and the solution space associated to each alternative is inSk
cluded in one of the input constraint stores (i.e., SolF D (S) = i=1 SolF D (Si σi )).
In the case k = 0, the disjunction is understood as failure and SolF D (S) = ∅ (that
means failure detection).

(López-Fraguas et al. 2004b) describes a constraint solver defined on the domain
Hseq in which the constraints considered are just those for the strict (dis)equality
on pure patterns (i.e. those patterns constructed over an empty set of primitive elements). Now, in this paper, we extend this solver to the constraint domain F D in
which we consider Z as the set of primitive elements. We follow this approach and asWk
sume that the solver SolveF D will behave as follows: SolveF D (S, χ) = i=1 (Si σi )
Wk
iff S ε ⊢⊢∗χ i=1 (Si σi ) 6⊢⊢χ , where the relation ⊢⊢χ expresses a solver resolution
step, and S ε 6⊢⊢χ indicates that S is in solved form w.r.t. the action of the constraint solver in the sense of Definition 2. Moreover, the relation ⊢⊢χ manipulates
disjunctions by combining them as follows:
W
W
if Si σi ⊢⊢χ j (Sj σj )
. . . ∨ Si σi ∨ . . . ⊢⊢χ . . . ∨ j (Sj σj ) ∨ . . .
Tables 2-5 show the sets of rules that define the relation ⊢⊢χ . These rules extend and complement those presented in (López-Fraguas et al. 2004b) specifically
to work with finite domain constraints defined on the set of integer patterns. For
clarity, we omit the corresponding failure rules, which can be easily deduced from
our tables.
Table 2 captures the operational behavior of the constraint solver SolveF D to
manage constraints of the form seq, leq or domain when these return a variable
as a result. The result variable is instantiated to each of its possible values (i.e.,
true and f alse) giving rise to different alternatives for each of the possibilities and
propagating the corresponding bind to the remaining alternatives.
Table 2. General Rules for the Constraint Solver
seq t s →! R, S

σ ⊢⊢χ (t == s, Sθ1

leq a b →! R, S

σ ⊢⊢χ (a ≤ b, Sθ1

domain u [u1 , . . . , un ] →! R, S

σθ1 ) ∨ (t \ = s, Sθ2
σθ1 ) ∨ (a > b, Sθ2

σ ⊢⊢χ (u ∈ [u1 , . . . , un ], Sθ1
(u ∈
/ [u1 , . . . , un ], Sθ2

σθ2 )
σθ2 )
σθ1 ) ∨
σθ2 )

(For the 3 rules) only if R ∈
/ χ; with θ1 = {R 7→ true} and θ2 = {R 7→ f alse}

Constraint Functional Logic Programming over Finite Domains

11

Observe that, by applying the rules shown in Table 2, all the constraints based
on the primitive seq are proposed as explicit constraints in form of strict equality
or strict disequality. Then, the solver distinguishes several cases depending on the
syntactic structure of the (integer) patterns used as arguments. Table 3 shows
the rules to cover these cases that reproduce the process of syntactic unification
between equalities and disequalities as it is done in the classical syntactic unification
algorithms (see for example (Fernández 1992)).
Table 3. Rules for Strict (Dis)-Equality
u == u, S
σ ⊢⊢χ S
σ, if u ∈ Z
X == t, S
σ ⊢⊢χ t == t, Sθ
σθ, if X ∈
/ χ ∪ var(t), var(t) ∩ χ = ∅, θ = {X 7→ t}
σ ⊢⊢χ t1 == s1 , . . . , tn == sn , S σ
(h t1 . . . tn ) == (h s1 . . . sn ), S
′
Z ′
u \ = u′ , S
σ ⊢⊢χ S
σ, if u,
W u ∈ Z, and u 6= Wun
X \ = (h t1 . . . tn ), S
σ ⊢⊢χ ( i (Sθi
σθi )) ∨ ( k=1 (Uk \ = tk θ, Sθ
σθ))
if X ∈
/ χ, var(h t1 . . . tn )∩ χ 6= ∅, θi = {X 7→ hi Y mi }, with hi 6= h, and
θ = {X 7→ h U n }, Y mi , U n are new fresh variables.
(h t1 . . . tn ) \ = u, S
σ ⊢⊢χ S
σ if u ∈ Z
σ ⊢⊢χ (t1 \ = s1 , S
σ) ∨ . . . ∨ (tn \ = sn , S
σ)
(h t1 . . . tn ) \ = (h s1 . . . sn ), S
(h t1 . . . tn ) \ = (h′ s1 . . . sm ), S
σ ⊢⊢χ S
σ, if h 6= h′ or m 6= n

In addition to the rules for the strict (dis)equality over integer patterns, the solver
has also to consider, by contrast to the solver given in (López-Fraguas et al. 2004b),
new rules for the particular treatment of the primitive constraints (specific for F D)
defined over the primitive elements in Z. These rules are shown in Table 4.
Table 4. Rules for the Specific Primitive Constraints of F D
u ≤ u′ , S
u > u′ , S
a ⊗ b ≍ c, S
a ⊗ b = X, S

σ ⊢⊢χ S
σ ⊢⊢χ S

σ, if u, u′ ∈ Z, and u ≤Z u′
σ, if u, u′ ∈ Z, and u >Z u′

σ ⊢⊢χ S
σ, if a, b, c ∈ Z and a ⊗Z b ≍Z c
σ ⊢⊢χ Sθ
σθ, if X ∈
/ χ, a, b ∈ Z and θ = {X 7→ a ⊗Z b}

Moreover, the solver also has to cover the domain and indomain classical constraints in finite domain constraint programming languages, to respectively fix the
domain of the constrained variables and label them according to their corresponding
domain (Dechter 2003). Table 5 shows the new rules that consider these cases.
After applying the constraint solver SolveF D , a primitive constraint store S ⊆
P Con(F D) is expressed in solved form as a finite conjunction of primitive constraints of the form (we use the notations given in Section 2.4) X == t, X \ = t,

12 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
Table 5. Rules for Finite Domain and Variable Labeling
u ∈ [u1 , . . . , un ], S
u∈
/ [u1 , . . . , un ], S

σ ⊢⊢χ S
σ ⊢⊢χ S

σ, if u, ui ∈ Z ∪ Var and ∃i ∈ {1, . . . , n}. ui ≡ u.
σ, if u, ui ∈ Z and ∀i ∈ {1, . . . , n}. ui 6=Z u.

W
labeling [. . .] [X], X ∈ [u1 , . . . , un ], S
σ ⊢⊢χ n
σθi ),
i=1 (Sθi
if X ∈
/ χ, and ∀i ∈ {1, . . . , n}, ui ∈ Z and θi = {X 7→ ui }
σ ⊢⊢χ S
σ, if u ∈ Z
labeling [. . .] [u], S

u ∈ D and a ⊗ b ≍ c where X ∈ Var, t is a total pattern, u, a, b, c ∈ Z ∪ Var and
D is a total pattern defining a list of variables and/or integers.
Example 1
We illustrate the operational semantics of our finite domain constraint solver providing a constraint solver derivation from the initial constraint store {seq X (s K)
→! R, A + B < Z} and taking into account the set of protected variables {Z}.
We describe in detail the rules applied by the constraint solver and, at each goal
transformation step, we underline which subgoal is selected:
ε ⊢⊢{Z}
seq X (s K) →! R, A + B < Z
({X == s K, A + B < Z}
({X \ = s K, A + B < Z}

{R 7→ true}) ∨
{R 7→ f alse}) ⊢⊢{Z}

• ({X == s K, A + B < Z}
{R 7→ true}) ⊢⊢{Z}
{R 7→ true, X 7→ s K}) ⊢⊢{Z}
({s K == s K, A + B < Z}
{R 7→ true, X 7→ s K}) 6⊢⊢{Z}
({K == K, A + B < Z}
• ({X \ = s K, A + B < Z}
{R 7→ f alse}) ⊢⊢{Z}
({A + B < Z}
{R 7→ f alse, X 7→ 0}) ∨
{R 7→ f alse, X 7→ s M }) 6⊢⊢{Z}
({A + B < Z, M \ = K}
Therefore, the constraint solver returns the following solved forms:
SolveF D ({ seq X (s K) →! R, A + B < Z }, {Z} ) =
({A + B < Z, K == K}
{R 7→ true, X 7→ s K}) ∨
({A + B < Z}
{R 7→ f alse, X 7→ 0}) ∨
{R 7→ f alse, X 7→ s M })
({A + B < Z, M \ = K}
As shown in Tables 2-5, our new constraint solver for the finite domain F D with
strict equality and disequality has been designed to hold all the initial assumptions
required in the general framework CF LP for constraint solvers (see Definition 2).
It can be formally proved by means of the following result.
Theorem 1
Let S ⊆ P Con(F D) be a primitive constraint store, σ ∈ Sub⊥ (Z) an idempotent
total substitution and χ ⊆ Var a set of protected variables. If S σ satisfies the reWk
quirements of Definition 2 and S σ ⊢⊢χ
σi ), then SolF D (S σ) =
i=1 (Si

Constraint Functional Logic Programming over Finite Domains

13

Sk

SolF D (Si σi ), where dom(σi ) ∩ var(Si ) = ∅ and χ ∩ (dom(σi ) ∪ ran(σi ))
σ ⊢⊢χ fails then SolF D (S
σ) = ∅.
= ∅ for all 1 ≤ i ≤ k. Moreover, if S
i=1

The proof of this theorem (see Appendix A) can be done distinguishing several cases from the declarative semantics of each primitive function symbol given
in Table 1 and the requirements of each constraint solver rule in Tables 2-5. According to this result, the relation ⊢⊢χ preserves the requirements of a constraint
solver and the constraint solver steps fail only in case of an unsatisfiable constraint
store. Therefore, if we repeatedly apply this result from an initial constraint store
and a set of protected variables in order to compute a constraint store in solved
form, we directly obtain the correctness of our finite domain constraint solver w.r.t.
CF LP (F D)’s semantics.
3 The CLN C(F D) Calculus
This section describes a lazy narrowing calculus with constraints defined on the
finite domain F D (the Constraint Lazy Narrowing Calculus CLN C(F D) for short)
for the solving of goals from programs. Since we have proved in the previous section
that our finite domain constraint solver holds the properties required in the general
framework, this calculus can be obtained as a simplified instantiation of the general
scheme for CF LP described in (López-Fraguas et al. 2004b), and used in this work
as the formal foundation of the operational semantics in T OY(F D).
In order to understand the main ideas of our operational semantics, we first give a
precise definition for the class of well-typed programs, admissible goals and correct
answers we are going to work with.
3.1 Programs, Goals and Answers
Our well-typed CF LP (F D)-programs are sets of constrained rewriting rules that
define the behavior of possibly higher-order and/or non-deterministic lazy functions
over F D, called program rules. More precisely, a program rule R for a defined
function symbol f ∈ DF n with an associated principal type τ1 → . . . → τn → τ
has the form f t1 . . . tn = r ⇐ C and is required to satisfy the conditions listed
below:
1. t1 . . . tn is a linear sequence of transparent patterns and r ∈ Exp⊥ (Z) is a
total expression.
2. C is a finite set of total constraints (in the form of Definition 1), intended to
be interpreted as conjunction, and possibly including occurrences of defined
function symbols.
3. There exists some type environment T with domain var(R) which well-types
the defining rule in the following sense:
(a)
(b)
(c)
(d)

For 1 ≤ i ≤ n: (Σ, T ) ⊢W T ti :: τi .
(Σ, T ) ⊢W T r :: τ .
For each (e == e′ ) ∈ C: ∃µ ∈ Type s.t. (Σ, T ) ⊢W T e :: µ :: e′ .
For each (e \ = e′ ) ∈ C: ∃µ ∈ Type s.t. (Σ, T ) ⊢W T e :: µ :: e′ .

14 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
(e) For each (u ∈ D) ∈ C: (Σ, T ) ⊢W T u :: int, D :: [int].
(f) For each (a ⊗ b ≍ c) ∈ C: (Σ, T ) ⊢W T a, b, c :: int
where (Σ, T ) ⊢W T e :: τ :: e′ denotes (Σ, T ) ⊢W T e :: τ, (Σ, T ) ⊢W T e′ :: τ .
The left-linearity condition required in item 1 is quite common in functional
and functional logic programming. As in constraint logic programming, the conditional part of a program rule needs no explicit occurrences of existential quantifiers.
Another distinguished feature of our language is that no confluence properties are
required for the programs, and therefore functions can be non-deterministic, i.e.
return several values for given (even ground) arguments.
Example 2
The following example illustrates the previous definition of typed CF LP (F D)programs by showing some constrained program rules which will be used for lazy
evaluation of infinite lists in the next subsections.
take :: int → [α] → [α]
(T1) take 0 Xs
= []
(T2) take N [ ]
= []
(T3) take N [X | Xs] = [X|take (N - 1) Xs]
check list :: [int] → int
(CL1) check list [ ]
(CL2) check list [X|Xs]
(CL3) check list [X|Xs]
(CL4) check list [X|Xs]

=
=
=
=

0
1
2
4

⇐ N >0
⇐N>0

⇐ domain [X] 1 2
⇐ domain [X] 3 4
⇐ domain [X] 5 7

generateFD :: int → [int]
(G1) generateFD 0 = [ ]
(G2) generateFD N = [X | generateFD N]

⇐ N > 0, domain [X] 0 N-1

from :: int → [int]
(F) from N = [N | from (N+1)]
According to (López-Fraguas et al. 2004b), we define goals for this kind of proC
S
σ, where the symbol must be
grams in the general form G ≡ ∃U . P
interpreted as conjunction, U is the finite set of so-called existential variables of the
goal G, P is a multiset of so-called productions of the form e1 → t1 , . . . , en → tn ,
where ei ∈ Exp⊥ (Z) and ti ∈ P at⊥ (Z) are totals for all 1 ≤ i ≤ n (the set of produced variables of G is defined as the set of variables occurring in t1 . . . tn ), C is a
finite conjunction of constraints (possibly including occurrences of defined function
symbols), S is a finite conjunction of primitive constraints in the form of Definition 1, called constraint store, and σ is an idempotent substitution called answer
C
S) = ∅.
substitution such that dom(σ) ∩ var(P
Additionally, we say that a goal G is an admissible goal iff it is well-typed: satisfies
the same admissibility criteria given above for programs for each constraint in C

Constraint Functional Logic Programming over Finite Domains

15

and S, and the same conditions of compatible types for each production in P and
each binding in σ given in (González-Moreno et al. 99b). Moreover, it must hold
the so-called goal invariants given in (López-Fraguas et al. 2004b): each produced
variable is produced only once, all the produced variables must be existential, the
transitive closure of the relation between produced variables must be irreflexive,
and no produced variable enters the answer substitution. An admissible goal is
called a solved goal iff P and C are empty and S is in solved form w.r.t. the action
of the constraint solver in the sense of Definition 2.
Similarly to (González-Moreno et al. 99a; González-Moreno et al. 99b; del Vado-Vı́rseda 2003),
the CLN C(F D) calculus uses a notion of demanded variable to deal with lazy evaluation.
Definition 3
Let G be an admissible goal. We say that X ∈ var(G) is a demanded variable iff
1. X is demanded by the constraint store S of G, i.e. µ(X) 6= ⊥ holds for every
µ ∈ SolF D (S) (for practical use, the calculation of this kind of demanded
variables in F D can be easily done extending the rules given in the appendix
of (López-Fraguas et al. 2004b) in the line of our rules shown in Tables 2-5).
/ Var or k > 0
2. X is demanded by a production (Xak → t) ∈ P such that, t ∈
and t is a demanded variable in G.
Example 3
We suppose an admissible goal with only the primitive constraint seq X (s K)
→! R in the associated constraint store S. We note that K is not a demanded
variable by S, because µ = {X 7→ 0, K 7→ ⊥, R 7→ f alse} ∈ SolF D (S) (clearly,
seq F D µ(X) (s K)µ → µ(R) = f alse where µ(X) = 0 and (s K)µ = s (µ(K)) =
s (⊥) have no common upper bound w.r.t. the information ordering ⊑, according
to Table 1) but µ(K) = ⊥. However, X and R are both demanded variables by
S (according to the radicality property, any µ ∈ SolF D (S) must satisfy µ(R) total
and then µ(R) 6= ⊥ and consequently µ(X) 6= ⊥). In this situation, if we have
also a production F 1 → X in the produced part of the goal involving a higherorder variable F , automatically F is also a demanded variable (by a production
but not by the constraint store S). Moreover, we note that it is also possible to
have a variable F demanded by both the constraint store (for example, if we add
the primitive constraint F == ⊕ 2 to S) and a production (for example, F 1 → 3
instead of F 1 → X). In this case, F is demanded twice, supplying more relevant
and precise information for goal solving in the produced part and the constraint
store of the goal.
Finally, we describe the notion of correct answer that we want to compute from
goals and programs in our CF LP (F D)-framework. Since the calculus CLN C(F D)
is semantically based on the Constraint ReWriting Calculus CRW L(F D), that
represents a concrete instance over the constraint domain F D of the constraint
rewriting logic described in (López-Fraguas et al. 2004a), this logic can be also used
as a logical characterization of our program semantics. On the basis of this logic,

16 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
we define our concept of correct answer with respect to an admissible goal G and
θ, where Π ⊆ P Con(F D)
a given CF LP (F D)-program as a pair of the form Π
and θ ∈ Sub⊥ (Z) is an idempotent substitution such that dom(θ) ∩ var(Π) = ∅,
fulfilling the same semantic conditions given in (López-Fraguas et al. 2004b) w.r.t.
CRW L(D)’s semantics.
The following example shows a correct answer for the admissible goal with only
take 3 (generateF D 10) == List
and the CF LP (F D)a strict equality
program given in Example 2:
{X1 , X2 , X3 ∈ [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]} ✷ {List 7→ [X1 , X2 , X3 ]}
Analogously, it is also possible to prove that M ∈ [1..2] and M ∈ [3..4] (both of
them with an empty substitution) are correct answers for the admissible goal with
only a user defined finite domain constraint
check list (f rom M ) < 3
.
We will see in the next subsection how to compute all of these answers by means
of the constrained lazy narrowing over F D.
3.2 Constrained Lazy Narrowing over F D
The calculus CLN C(F D) can be obtained as a particular instantiation from the
general CLN C(D) calculus because we have proved that our finite domain constraint solver satisfies the requirements given in the general framework. Therefore,
the calculus CLN C(F D) can be described as a set of transformation rules for admissible goals of the form G ⊢⊢ G′ , specifying one of the possible ways of performing
one step of goal solving. In this sense, derivations are sequences of ⊢⊢-steps where
successful derivations will eventually end with a solved goal and failing derivations
end with an inconsistent goal . We have two classes of goal transformation rules:
rules for constrained lazy narrowing by means of productions, and rules for constraint solving and failure detection.
The goal transformation rules concerning productions are the same rules given
in (López-Fraguas et al. 2004b) for general productions and are designed with the
aim of modeling the behavior of constrained lazy narrowing with sharing, but now
involving only the primitive functions over finite domains given in Definition 1,
possibly higher-order defined functions and functional variables.
The goal transformation rules concerning constraints can also be used to combine (primitive or used defined) finite domain constraints with the action of our
constraint finite domain solver. As the main novelty, we note that only primitive
constraints are sent to the F D constraint solver. This is because non-primitive
constraints are first translated to primitive ones by replacing the non-primitives
arguments by new fresh variables before executing constraint solving and by registering new productions between the non-primitive arguments and the new variables
for lazy evaluation. Moreover, the constraint solver must protect all the produced
variables of the goal in order to respect the constrained lazy evaluation and the
admissibility conditions of goals. Additionally, the usual failure rules can also be
used for failure detection in constraint solving and failure detection in the syntactic
unification of the produced part of the goal.

Constraint Functional Logic Programming over Finite Domains

17

Finally, we note that since Theorem 1 proves the correctness of our finite domain
constraint solver w.r.t. the general framework, the main properties of the lazy narrowing calculus CLN C(F D), soundness and completeness w.r.t. the declarative semantics of CRW L(F D), follows directly from the general results of (López-Fraguas et al. 2004b).
Obviously, these properties qualify CLN C(F D) as a convenient computation mechanism for constraint functional logic programming over finite domains and provide a formal foundation for our CF LP (F D) implementation T OY(F D). From
the viewpoint of efficiency, a computation strategy for CLN C(F D) using definitional trees (Antoy 1992) has been proposed recently in (del Vado-Vı́rseda 2005)
and (Estévez-Martín and del Vado-Vı́rseda 2005) for ensuring only needed narrowing steps and extend the efficient properties shown in (Loogen et al. 1993; Antoy et al. 2000;
del Vado-Vı́rseda 2003) guiding and avoiding don’t know choices of constrained program rules over F D.
3.3 Example of Goal Resolution by Using CLN C(F D)
This section is closed with a simple example which illustrates the process of goal
solving via the narrowing calculus CLN C(F D) and our finite domain constraint
solver SolveF D . We compute all the answers from the goal check list (f rom M )
<3
using the CF LP (F D)-programs given in Example 2. Its resolution corresponds to the following sequence of goal transformation rules in (López-Fraguas et al. 2004b)
where, at each goal transformation step, we underline which subgoal is selected. ⊢⊢R
indicates that the rule R in that work is applied.
check list (f rom M ) < 3
∃X. check list (f rom M ) → X

ε ⊢⊢AC
X<3

ε ⊢⊢DF

At this point, we note that X is a variable demanded by the constraint store and
we have several alternatives due to don’t know choice of the program rule check list:
∃X. check list (f rom M ) → X
X<3
ε ⊢⊢DF(CL1)
∃X. f rom M → [ ], 0 → X
X<3
ε ⊢⊢SP{X7→0}
0<3
ε ⊢⊢CS{∅}
(SolveF D ({0 < 3}, ∅) = ∅
f rom M → [ ]
f rom M → [ ]
ε ⊢⊢DF(F)
ε ⊢⊢CF 
[M | f rom (M + 1)] → [ ]

ε)

The application of the first program rule for check list leads to a failure derivation
without answer. We apply now the second program rule of check list:
∃X. check list (f rom M ) → X
X<3
ε ⊢⊢DF(CL2)
∃X ′ , Xs′ , X. f rom M → [X ′ |Xs′ ], 1 → X
domain [X ′ ] 1 2
X<3
ε ⊢⊢SP{X7→1}
′
′
′
′
domain [X ′ ] 1 2
1<3
ε ⊢⊢AC
∃X , Xs . f rom M → [X |Xs ]
∃X ′ , Xs′ . f rom M → [X ′ |Xs′ ]
1 < 3, domain [X ′ ] 1 2
ε ⊢⊢DF(F)
′
′
′
1 < 3, domain [X ′ ] 1 2
ε ⊢⊢DC
∃X , Xs . [M | f rom (M + 1)] → [X |Xs′ ]

18 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
∃X ′ , Xs′ . M → X ′ , f rom (M + 1) → Xs′
1 < 3, domain [X ′ ] 1 2
ε ⊢⊢SP{X′ 7→M}
′
′
∃Xs . f rom (M + 1) → Xs
1 < 3, domain [M ] 1 2
ε ⊢⊢EL
1 < 3, domain [M ] 1 2
ε ⊢⊢CS(∅)
M ∈ [1..2]
ε, because
ε
SolveF D ({1 < 3, domain [M ] 1 2}, ∅) = {M ∈ [1..2]}
Therefore, we obtain the first computed answer Π1
θ1 ≡ {M ∈ [1..2]}
Analogously, we can apply the third program rule of check list:
∃X. check list (f rom M ) → X
M ∈ [3..4]
ε

X <3

ε.

ε ⊢⊢∗DF(CL3)

θ2 ≡ {M ∈ [3..4]} ε. No more
and we obtain the second computed answer Π2
answers can be computed, because if we apply the fourth program rule of check list
we have again a failing derivation:
∃X. check list (f rom M ) → X
X<3
ε ⊢⊢DF(CL4)
domain [X ′ ] 5 7
X < 3
ε
∃X ′ , Xs′ , X. f rom M → [X ′ |Xs′ ], 4 → X
⊢⊢SP{X7→4}
domain [X ′ ] 5 7
4<3
ε ⊢⊢AC
∃X ′ , Xs′ . f rom M → [X ′ |Xs′ ]
′
′
′
′
4 < 3, domain [X ′ ] 5 7
ε ⊢⊢SF{X′ ,Xs′ } 
∃X , Xs . f rom M → [X |Xs ]
because SolveF D ({4 < 3, domain [X ′ ] 5 7}, {X ′, Xs′ }) = ∅
A detailed explanation of the computation of these answers using definitional
trees in CLN C(F D) to efficiently guide and avoid don’t know choices of constrained
program rules can be found in (Estévez-Martín and del Vado-Vı́rseda 2005). Moreover, we will see in the next section that these are exactly the same answers computed by our CF LP (F D) implementation T OY(F D).
4 T OY(F D)
So far, we have introduced the theoretical framework. Now, in this section we introduce T OY(F D), a CF LP (F D) implementation that extends the T OY system
to deal with F D constraints, highlight its advantages, and show its performance.
4.1 Introducing T OY(F D)
In this section, we describe T OY(F D) from a programming point of view, briefly
describing its concrete syntax and some predefined F D constraints.
4.1.1 An Overview of T OY(F D)
T OY(F D) programs consist of datatypes, type alias, infix operator definitions, and
rules for defining functions. The syntax is mostly borrowed from Haskell with the remarkable exception that variables and type variables begin with upper-case letters,
whereas constructor symbols and type symbols begin with lower-case. In particular,
functions are curried and the usual conventions about associativity of application

Constraint Functional Logic Programming over Finite Domains

19

hold. As usual in functional programming, types are inferred, checked and, optionally, can be declared in the program. To illustrate the datatype definitions, we
present the following examples using the concrete syntax of T OY :
• data nat = zero | suc nat, to define the naturals, and
• the Boolean predefined type as data bool = false | true;
A T OY(F D) program P is a set of defining rules for the function symbols
in its signature. Defining rules for a function f have the syntactic basic form
f t1 . . . tn = r <== C and, informally, its intended meaning is that a call to
f can be reduced to r whenever the actual parameters match the patterns ti , and
the conditions in C are satisfied. T OY(F D) also allows predicates (defined similarly as in logic programming) where predicates are viewed as a particular kind of
functions, with type p :: τ n → bool. As a syntactic facility, we can use clauses as
a shorthand for defining rules whose right-hand side is true. This allows to write
Prolog-like predicate definitions, so that a clause p t1 . . . tn : − C abbreviates
a defining rule of the form p t1 . . . tn = true <== C. With this sugaring in
mind and some obvious changes (like currying elimination) it should be clear that
(pure) CLP (F D) -programs can be straightforwardly translated to CF LP (F D) programs.
4.1.2 Simple Programming Examples

Table 6 shows introductory programming examples in T OY that do not make use of
the extension over F D, together with some goals and their outcomes (López-Fraguas and Sánchez-Hernández 1999).
Note that infix constraint operators are allowed in T OY(F D) , such as // to
build the expression X // Y, which is understood as // X Y. The goal (a) in
the table sorts a list, in a pure functional computation. The answer for the goal (b)
involves a syntactic disequality. In goal (c), F is a higher-order logic variable, and
the obtained values for this variable are higher-order patterns (permut, sort,...).
4.1.3 F D Constraints in T OY(F D)
Table 7 shows a small subset of the F D constraints supported by T OY(F D) ,
which are typical instances found in CP systems, and covers adequately the primitive constraints summarized in Table 1. In Table 7, int is a predefined type for
integers, and [τ ] is the type ‘list of τ ’. The datatype labelType is a predefined type
which is used to define many search strategies for finite domain variable labeling
(Fernández et al. 2004).
Relational constraint operators are applied to integers and return a Boolean
value. Arithmetical constraint operators are applied to and return integer values
(the set of primitive elements). They can be combined with relational constraint
operators to build (non)linear (dis)equations as constraints. Moreover, reified constraints1 can be implemented by equating a Boolean variable to a Boolean constraint, for all of the constraints built from the operators in this table and the
1

Reified constraints reflect the entailment of a constraint in a Boolean variable. In general,

20 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
Table 6. T OY Programming Basic Examples
% Non-deterministic choice of one of two values
infixr 40 //
X // Y = X
X // Y = Y
% Non-deterministic insertion of an element into a list
insert X [] = [X]
insert X [Y|Ys] = [X,Y|Ys] // [Y|insert X Ys]
% Non-deterministic generation of list permutations
permut [] = []
permut [X|Xs] = insert X (permut Xs)
% Testing whether a list of numbers is sorted
sorted [] = true
sorted [X] = true
sorted [X,Y|Ys] = sorted [Y|Ys] <== X <= Y
% Lazy ‘generate-and-test’ permutation sort. ’check’ calls ’sorted’ which demands its
% argument, which is lazily, non-deterministically generated by ’permut’. As soon as
% the test fails, ’permut’ stops the generation and tries another alternative
sort Xs = check (permut Xs)
check Xs = Xs <== sorted Xs == true
Goal
(a) sort [4,2,5,1,3] == L
(b) sort [3,2,1] /= L
(c) F [2,1,3] == [1,2,3]

Answers
L == [1,2,3,4,5]; no more solutions
L /= [1,2,3] ; no more solutions
F == permut; F == sort; . . .

contraint domain (see Example 4). Due to the functional component, we can apply
this technique to equate Boolean expressions to Boolean constraints, as well. Both
relational and arithmetical constraint operators are syntactically distinguished (by
prefixing them with #) from standard relational operators in order to denote its
different operational behavior. Whereas a standard arithmetical operator demands
its arguments, an arithmetical constraint does not. The membership constraint
domain restricts a list of variables (its first argument) to have values in an integer
interval (defined by its two next integer arguments) whenever its return value is
true, whereas it restricts these variables to have values different from the interval
when its return value is false. The enumeration constraint labeling assigns values to the variables in its input integer list according to the options specified with
the argument of type list of labelType. In this list, search strategies, such as firstconstraints in reified form allow their fulfillment to be reflected back in an F D variable. For
example, X = (Y + Z > V ) constrains X to true as soon as the disequation is known to be true
and to f alse as soon as the disequation is known to be false. On the other hand, constraining X
to true imposes the disequation, and constraining X to f alse imposes its negation. Usually, in
CLP (F D) languages, the Boolean values f alse and true directly correspond to the numerical
values 0 and 1, respectively.

Constraint Functional Logic Programming over Finite Domains

21

Table 7. A Subset of Predefined F D Constraints in T OY(F D)
RELATIONAL CONSTRAINT OPERATORS
(# =), (#\ =) :: int → int → bool
(#<), (#<=), (#>), (#>=) :: int → int → bool
ARITHMETICAL CONSTRAINT OPERATORS
(#+), (#−), (#∗), (#/) :: int → int → int
MEMBERSHIP CONSTRAINTS
domain :: [int] → int → int → bool
ENUMERATION CONSTRAINTS
labeling :: [labelType] → [int] → bool
COMBINATORIAL CONSTRAINTS
all different :: [int] → bool

(Strict Equality)
(Less or Equal)
(Operators)
(Finite Domains)
(Variable Labeling)
(Global Constraints)

fail (see Section 4.5.1), as well as optimization options for finding minimum and
maximum values for cost functions can be specified. The combinatorial constraint
all different ensures different values for the elements in its list argument and
is an example of the set of global constraints (for which an efficient propagation
algorithm has been developed) supported by T OY(F D) .
We do neither mention nor explain all the predefined constraints in detail and
encourage the interested reader to visit the link proposed in (Fernández et al. 2004)
for a more detailed explanation. We emphasize that all the pieces of code in this
paper are executable in T OY(F D) and the answers for example goals correspond
to actual executions of the programs.
4.1.4 Simple Examples with F D Constraints
Example 4
Below, we show the resolution at the T OY(F D) command line level of a simple
goal that does not involve labeling.
TOY(FD)> domain [X, Y] 10 20, X #<= Y == L
yes
L == true, X in 10..20, Y in 10..20;
yes
L == false, X in 11..20, Y in 10..19;
no
Also note that this CF LP (F D) implementation only inform about a limited
outcome, which consists of: (1) substitutions of the form Variable == Pattern,
(2) disequality constraints Variable /= Pattern, (3) disjunctions D of constraints
Variable in IntegerRange (these constraints denote the possible values a variable might take, as in common constraint systems; i.e., they do not state D, but
negated D), and (4) success information: yes and no stand for success and failure,
respectively. Finally, ‘;’ separates the solutions which has been explicitly requested
by the user. Primitive constraints in the finite domain constraint store are not
shown.

22 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
Example 5
We show a T OY(F D) program involving labeling to solve the classical N-queens
problem whose objective is to place N queens on an N × N chessboard so that
there are no threatening queens.
include "misc.toy"
include "cflpfd.toy"
queens :: int -> [labelType] -> [int]
queens N Label = L <== length L == N, domain L 1 N,
constrain_all L, labeling Label L
constrain_all :: [int] -> bool
constrain_all [] = true
constrain_all [X|Xs] = true <== constrain_between X Xs 1,
constrain_all Xs
constrain_between :: int -> [int] -> int -> bool
constrain_between X [] N = true
constrain_between X [Y|Ys] N = true <== no_threat X Y N,
constrain_between X Ys (N+1)
no_threat:: int -> int -> int -> bool
no_threat X Y I = true <== X #\= Y, X #+ I #\= Y, X #- I #\= Y
The intended meaning of the functions should be clear from their names and definitions, provided that length L returns the length of the list L. The first two lines
are needed to include predefined functions such as length and domain. An example
of solving at the command prompt, where ff stands for the first-fail enumeration
strategy (see Section 4.5.1), is
TOY(FD)> queens 15 [ff] == L
yes
L == [1,3,5,14,11,4,10,7,13,15,2,8,6,9,12]
Example 6
We present a T OY(F D) program using syntactic sugaring for predicate-like functions that solves the well-known CLP (F D) program Send+More=Money.
smm :: int -> int -> int -> int -> int -> int -> int -> int
-> [labelType] -> bool
smm S E N D M O R Y Label :domain [S,E,N,D,M,O,R,Y] 0 9, S #> 0, M #> 0,
all_different [S,E,N,D,M,O,R,Y], add S E N D M O R Y,
labeling Label [S,E,N,D,M,O,R,Y]
add :: int -> int -> int -> int -> int -> int -> int -> int -> bool

Constraint Functional Logic Programming over Finite Domains

23

add S E N D M O R Y :- 1000#*S #+ 100#*E #+ 10#*N #+ D
#+ 1000#*M #+ 100#*O #+ 10#*R #+ E
#= 10000#*M #+ 1000#*O #+ 100#*N #+ 10#*E #+ Y
For our simple T OY(F D) programs, some examples of goals and answers which
can be computed by T OY(F D) are shown in Table 8.
Table 8. Examples of Goal Solving
Goal

Answers

domain [A,B] 1 (1+2), A#>B,
all different [A,B], labeling [ ] [A,B]

A==2,B==1; A==3,B==1;
A==3,B==2; no more solutions

domain [X,Y,Z] 1 10,
2 #* X #+ 3 #* Y #+ 2 #< Z

X in 1..2,Y==1,Z in 8..10;
no more solutions

domain [X,Y,Z] 1 5, X #> Y,
2 #* Y #> Z #+ 4, X #>= Z

X in 4..5,Y in 3..4,Z in 1..3;
no more solutions

smm S E N D M O R Y [] == T

S==9,E==5,N==6,D==7,M==1,O==0,
R==8,Y==2,T==true;
no more solutions

queens 5 [] == [M,A,E,Y,B],
smm S E N D M O R Y []

M==1,A==3,E==5,Y==2,B==4,S==9,
N==6,D==7,O==0,R==8;
no more solutions

4.2 CF LP (F D) vs. CLP (F D)
It is commonly acknowledged that CLP (F D) is a successful declarative approach;
hence, we discuss the advantages of CF LP (F D) , focusing on the T OY(F D) implementation, with respect to CLP (F D). This section explains why the addition
of F P features enhances the CLP setting. When necessary, we illustrate different
features of CF LP (F D) by means of examples. Further programming examples in
pure functional logic programming and CF LP (F D) can be found, respectively, in
(López-Fraguas and Sánchez-Hernández 1999) and (Fernández et al. 2004).
4.2.1 CF LP (F D) ⊃ CLP (F D)
As already pointed out, besides other features, CF LP (F D) provides the main
characteristics of CLP (F D), i.e., F D constraint solving, non-determinism and relational form. Moreover, CF LP (F D) provides a sugaring syntax for LP predicates

24 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
and thus, as already commented, any pure CLP (F D)-program can be straightforwardly translated into a CF LP (F D)-program. In this sense, CLP (F D) may be
considered as a strict subset of CF LP (F D) with respect to problem formulation.
As a direct consequence, our language is able to cope with a wide range of applications (at least with all those applications that can be formulated with a CLP (F D)
language). We will not insist here on this matter, but prefer to concentrate on the
extra capabilities of CF LP (F D) with respect to CLP (F D).
4.2.2 CF LP (F D) \ CLP (F D)
Due to its functional component, CF LP (F D) adds further expressiveness to
CLP (F D) as allows the declaration of functions and their evaluation in the F P
style. In the following, we enumerate and discuss other features not present (or
unusual) in the CLP (F D) paradigm.
Types. Our language is strongly typed and thus involves all the well-known advantages of a type checking process, enhancing program development and maintenance. Each F D constraint has associated, like any function, a type declaration,
which means that a wrong use can be straightforwardly detected in the typical type
checking process.
Functional Notation. It is well-known that functional notation reduces the number of variables with respect to relational notation, and thus, CF LP (F D) increases
the expressiveness of CLP (F D) as it combines relational and functional notation.
For instance, in CLP (F D) the constraint conjunction N=2, X ∈ [1,10-N] cannot
be expressed directly and must be written adding a third component, as N=2, Max
is 10-N, domain([X],1,Max) that uses an extra variable. However, T OY(F D)
expresses that constraint directly as N==2, domain [X] 1 (10-N).
Currying. Again, due to its functional component, T OY(F D) allows curried functions (and thus constraints); for instance, see the application of curried F D constraint (3#<)/1 in Example 7 later in this section.
Higher-Order and Polymorphism. In T OY(F D) functions are first-class citizens, which means that a function (and thus an F D constraint) can appear in any
place where data do. As a direct consequence, an F D constraint may appear as
an argument (or even as a result) of another function or constraint. The functions
managing other functions are called higher-order (HO) functions. Also, polymorphic
arguments are allowed in CF LP (F D).
Example 7
A traditional example of a polymorphic HO function is
map :: (A -> B) -> [A] -> [B]
map F [] = []
map F [X|Xs] = [(F X) | (map F Xs)]

Constraint Functional Logic Programming over Finite Domains

25

that receives both a function F and a list as arguments and produces a list resulting
from applying the function to each element in the list. Now, suppose that X and
Y are F D variables ranging in the domain [0..100] (expressed, for instance, via the
constraint domain [X,Y] 0 100). Then, the goal map (3#<) [X,Y] returns the
Boolean list [true,true] resulting from evaluating the list [3#<X,3#<Y], and X
and Y are also restricted to have values in the range [4,100] as the constraints
3#<X and 3#<Y are sent to the constraint solver. Note also the use of the curried
function (3#<).
Laziness. In contrast to logic languages, functional languages support lazy evaluation, where function arguments are evaluated to the required extend (the call-byvalue used in LP vs. the call-by-need used in F P ). Strictly speaking, lazy evaluation
may also correspond to the notion of only once evaluated in addition to only required
extent (Peyton-Jones 1987). T OY(F D) increases the power of CLP (F D) by incorporating a novel mechanism that combines lazy evaluation and F D constraint
solving, in such a way that only the demanded constraints are sent to the solver.
This is a powerful mechanism that opens new possibilities for F D constraint solving.
For example, in contrast to CLP (F D), it is possible to manage infinite structures.
Example 8
Consider the recursive functions take and generateFD from Example 2. An eager evaluation of the following goal does not terminate as it tries to completely
evaluate the second argument, yielding to an infinite computation. However, a lazy
evaluation generates just the first 3 elements of the list, as shown below:
TOY(FD)> take 3 (generateFD 10) == List
yes
List == [ _A, _B, _C ]

_A, _B, _C in 0..9

In general, lazy narrowing avoids computations which are not demanded, therefore saving computation time. Example 9 contains a formulation of the typical magic
series (or sequences) problem (Van Hentenryck 1989). This example highlights the
expressive power of T OY(F D) by solving multiple problem instances that can be
described and solved via lazy evaluation of infinite lists.
Example 9
Let S = (s0 , s1 , ...,sN −1) be a non-empty finite series of non-negative integers.
The series S is said N-magic if and only if there are si occurrences of i in S, for
all i ∈ {0,...,N-1}. Below, we propose a T OY(F D) program to calculate magic
series where the function generateFD is as defined in Example 2.
lazymagic :: int -> [int]
lazymagic N = L <== take N (generateFD N) == L,
constrain L L 0 Cs, sum L (#=) N,
scalar_product Cs L (#=) N, labeling [ff] L
constrain :: [int] -> [int] -> int -> [int] -> bool
constrain [] A B [] = true

26 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
constrain [X|Xs] L I [J|Js] = true <== I==J, count I L (#=) X,
constrain Xs L (I+1) Js
sum/3, scalar product/4 and count/4 are predefined HO constraints (Fernández et al. 2004),
that accept a relational F D constraint operator with type int → int → bool as
argument (e.g., the constraint #=). sum L C N means that the summation of the
elements in the list L is related through C with the integer N (in the example, the
summation is constrained to be equal to N). scalar product and count stand for
scalar product and element counting under the same parameters as sum.
A goal lazymagic N, for some natural N, returns the N-magic series where the
condition take N (generateFD N) is evaluated lazily as (generateFD N) produces
an infinite list. More interesting is to return a list of different solutions starting from
N. This can be done using a recursive definition to produce the infinite list of magic
series (from N) as shown below.
magicfrom :: int -> [[int]]
magicfrom N = [lazymagic N | magicfrom (N+1)]
Now, it is easy to generate a list of magic series by lazy evaluation. For example,
the following goal generates a 3-element list containing, respectively, the solution
to the problems of 7-magic, 8-magic and 9-magic series.
TOY(FD)> take 3 (magicfrom 7) == L
yes
L == [ [ 3, 2, 1, 1, 0, 0, 0 ],
[ 4, 2, 1, 0, 1, 0, 0, 0 ],
[ 5, 2, 1, 0, 0, 1, 0, 0, 0 ] ]
More expressiveness is shown by mixing curried functions, HO functions and function composition (another nice feature from the functional component of T OY(F D)).
For example, consider the T OY(F D) code shown below:
from :: int -> [int]
from N = [N | from (N+1)]
(.):: (B -> C) -> (A -> B) -> (A -> C)
(F . G) X = F (G X)
lazyseries :: int -> [[int]]
lazyseries = map lazymagic . from
where (.)/2 defines the composition of functions. Observe that lazyseries curries the
composition (map lazymagic) . from. Then, it is easy to generate the 3-element
list shown above by just typing the goal
TOY(FD)> take 3 (lazyseries 7) == L
This simple example gives an idea of the nice features of CF LP (F D) that combines F D constraint solving, management of infinite lists and lazy evaluation, curried notation of functions, polymorphism, HO functions (and thus HO constraints),
composition of functions and a number of other characteristics that increase the
potentialities with respect to CLP (F D).

Constraint Functional Logic Programming over Finite Domains

27

4.3 Correctness of the CFLP(FD) Implementation
In this section, we briefly discuss the correctness of our T OY(F D) implementation
with respect to our CF LP (F D) framework.
T OY(F D) integrates, as a host language, the higher-order lazy functional logic
language T OY (López-Fraguas and Sánchez-Hernández 1999) and, as constraint
solver, the efficient F D constraint solver of SICStus Prolog (Carlsson et al. 1997).
Under the condition of considering just an empty set of protected variables, the SICStus Prolog finite domain solver always satisfies the conditions for constraint solvers
required in Section 2.5. Since the CLN C(F D) calculus is strongly complete (see
(López-Fraguas et al. 2004b)) in the sense that the choice of goal transformation
rules can be a don’t care choice, in practice, we can choose a suitable demand-driven
strategy: our F D constraint solver is only applied at the end of the process of goal
solving, when we have an empty set of protected variables (as we have done in the
example in Section 3.3) or when protected variables are not relevant. This strategy
can be performed in the CLN C(F D) calculus in the line of (del Vado-Vı́rseda 2005)
as well as in T OY(F D) in the line of (Estévez-Martín and del Vado-Vı́rseda 2005).
Therefore, we can conclude that our operational semantics with this strategy covers
adequately the T OY(F D) implementation.
Additionally, we have run a number of tests in the implementation and have
compared the derivations produced by the calculus CLN C(F D) to the traces obtained from debugging in T OY(F D), and the results show that these are effectively
identical by following an adequate demand-driven strategy in CLN C(F D). For instance, the CF LP (F D) program shown in Example 2 corresponds almost directly
to a T OY(F D) program, and the solving of the goal check list (f rom M ) < 3
in T OY(F D) is shown below (see (Estévez-Martín and del Vado-Vı́rseda 2005) for
more details).

Toy(FD)> check_list (from M) < 3
yes
M in 1..2
Elapsed time: 0 ms.
more solutions (y/n/d) [y]?
yes
M in 3..4
Elapsed time: 0 ms.
more solutions (y/n/d) [y]?
no.
Elapsed time: 0 ms.
Note that the computed answers correspond exactly to those obtained in the goal
solving process described in Section 3.3 via the narrowing calculus CLN C(F D).

28 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
4.4 Notes about the Implementation
In T OY(F D), F D constraints are evaluated internally by using mainly two predicates: hnf(E,H), which specifies that H is one of the possible results of narrowing
the expression E into head normal form, and solve/1, which checks the satisfiability of constraints (of rules and goals) before the evaluation of a given rule. This
predicate is, basically, defined as follows2 :
(1)
(2)
(3)
(4)

solve((ϕ, ϕ′ ))
solve(L == R)
solve(L / = R)
solve(L#♦ R)

(5) solve(C A1 . . . An )

:−
:−
:−
:−
:−

solve(ϕ), solve(ϕ′ ).
hnf(L, L′ ), hnf(R, R′ ), equal(L′ , R′ ).
hnf(L, L′ ), hnf(R, R′ ), notequal(L′ , R′ ).
hnf(L, L′ ), hnf(R, R′ ), {L′ #♦R′ }.
where ♦ ∈ {=, \=, <, <=, >, >=}.
hnf(A1 , A′1 ), . . . , hnf(An , A′n ), {C(A′1 , . . . , A′n )}.
where C is any constraint returning a Boolean.

The interaction with the constraint solver (i.e., SICStus F D constraint solver in
the current T OY(F D) version) is reflected in the last two clauses: every time an
F D constraint appears, the solver is eventually invoked with a goal {G} where G
is the translation of the F D constraint from T OY(F D) to SICStus Prolog. Head
normal forms are required for constraint arguments in order to allow the solver to
solve the constraint.

4.5 Performance
As far as we know, T OY(F D) was the first F LP system integrating a F D constraint system. However, we know about the existence of an implementation of
the F LP language Curry (Hanus 1999) that supports a limited set of F D constraints (Hanus M. (editor) 2005). This implementation, called PAKCS, provides
the following constraints:
(1) a set of arithmetical operations {*#,+#,-#,=#,/=#,<#,<=#,>#,>=#},
(2) a membership constraint domain /3,
(3) some global constraints3 and
(4) an enumeration constraint labeling /1 that also provides searching options.
In this section, we compare the performance of T OY(F D) with that of the
Curry2Prolog compiler, which is the most efficient implementation of Curry inside
PAKCS (version 1.7.1 of December 2005).
In addition, for evaluating if T OY(F D) is competitive with respect to existing
CLP (F D) systems, we have also considered four well-known CLP (F D) systems:
1. The version 3.12.1 of April 2005 of the F D constraint solver of SICStus Prolog (Carlsson et al. 1997; SICStus Prolog 2005). This solver was included in
order to measure the overhead due to the management of functional logic

2
3

The code does not correspond exactly to the implementation, which is the result of many
transformations and optimizations.
Exactly, those named in this paper, i.e. all different/1, count/4, scalar product/4 and sum/3.

Constraint Functional Logic Programming over Finite Domains

29

expressions, which are compiled to SICStus Prolog in T OY(F D), and, therefore, including all the stuff needed to handle the F LP characteristics such as
laziness and higher-order functions.
2. The GNU Prolog system (version 1.2.16) (Diaz and Codognet 2001; GNU Prolog 2005),
which is a free Prolog compiler that includes one of the most efficient finite
domain constraint solver. This solver is based on the concept of indexicals
(Codognet and Diaz 1996) and it has been demonstrated that it has a performance comparable to commercial systems.
3. SWI-Prolog (version 5.4.x) (Wielemaker 2003; SWI-Prolog 2005) that it is an
emergent and very promising Prolog system that provides an integer domain
constraint solver implemented with attributed variables.
4. Ciao Prolog (version 1.10#5 of August 2004) which is a full multi-paradigm
programming environment for developing programs in the Prolog language
and in several other languages which are extensions and modifications of
Prolog in several interesting and useful directions. Ciao Prolog provides a
package, based upon the indexical concept, to write and evaluate constraint
programming expressions over finite domains in a Ciao program.
4.5.1 Labeling
Constraint solving can be implemented with a combination of two processes: constraint propagation and labeling (i.e., search) (Dechter 2003). The labeling process
consists of (1) choosing a variable (variable ordering) and (2) assigning to the variable a value which belongs to its domain (value ordering). The variable ordering
and the value ordering used for the labeling can considerably influence the efficiency
of the constraint solving when only one solution to the problem is required. It has
little effect when the search is for all solutions. In this study, we consider two labelings, the naı̈ve labeling that chooses the leftmost variable of a list of variables and
then selects the smallest value in its domain, and the first-fail labeling that uses
a principle (Haralick and Elliot 1980) which says that to succeed, try first where
you are the most likely to fail. This principle recommends the choice of the most
constrained variable, which often means (for the finite domain) choosing a variable
with the smallest domain. The naı̈ve labeling assures that both variable and value
ordering are the same for all the systems and hence (although less efficient) is better
for comparing the different systems when only one solution is required.
4.5.2 The Benchmarks
We have used a wide set of benchmarks4 and, for the sake of fairness, whenever it
was possible, we used exactly the same formulation of the problems for all systems
as well as the same F D constraints. The benchmarks used are:
• cars: solve a car sequencing problem with 10 cars (Dincbas et al. 1988). This
benchmark deals with 100 Boolean variables (i.e., finite domain variables
4

All the programs used in the comparison are available at http://www.lcc.uma.es/∼afdez/cflpfd/.

30 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda

•
•
•
•

•
•

•

•

ranging over [0,1]), 10 finite domain variables ranging over [1,6], 6 atmost
constraints, 50 element constraints, and 49 linear disequations.
equation 10: a system of 10 linear equations with 7 variables ranging over
[0,10].
equation 20: a system of 20 linear equations with 7 variables ranging over
[0,10].
magic series (N): calculate a series of N numbers such that each of them is
the number of occurrences in the series of its position in the series (Codognet and Diaz 1996).
optimal Golomb ruler (N): find an ordered set of n distinct non-negative
integers, called marks, a1 < ... < an , such that all the differences ai − aj
(i > j) are distinct and an is minimum (Shearer 1990).
queens (N): place N queens on a N × N chessboard such that no queen
attacks each other (Van Hentenryck 1989).
pythagoras: calculate the proportions of a triangle by using the Pythagorean
theorem. This problem involves 3 variables ranging over [1,1000], and 7 disequality (non-linear) equations.
sendmore: a cryptoarithmethic problem with 8 variables ranging over [0,9],
with one linear equation, 2 disequations and 28 inequality constraints (or
alternatively one all different constraint imposed over the whole set of constrained variables). It consists of solving the equation SEN D + M ORE =
M ON EY .
suudoku: the problem is to fill partially filled 9x9 squares of 81 squares such
that each row and column are permutations of [1,...,9], and each 3x3 square,
where the leftmost column modulo 3 is 0, is a permutation of [1,...,9].

The programs equation 10, equation 20 and sendmore test the efficiency of
the systems to solve linear equation problems. The programs cars and suudoku
check the efficiency of specialized constraints such as the all different constraint.
The pythagoras problem deals with non-linear equations.
The queens and magic series programs are scalable and therefore useful to test
how the systems work for bigger instances of the same problem. Note that both
the number of variables and the number of values for each variable grow linearly
with the parameter N in the examples. That is, given a value N , at least N F D
variables must be declared with domains that range between 0 or 1 and N .
The search for optimal Golomb rulers is an extremely difficult task as it
is a combinatorial problem whose bounds grow geometrically with respect to the
solution size (Shearer 1990). This (also scalable) benchmark allows us to check the
optimization capabilities of the system.
4.5.3 Results
All the benchmarks were performed on the same Linux machine (under Fedora Core
system, 2.69-1667) with an Intel(R) Pentium 4 processor running at 2.40 GHz and
with a RAM memory of 512 Mb. For the sake of brevity, we only provide the results
for first solution search.

Constraint Functional Logic Programming over Finite Domains

31

Table 9. T OY(F D) vs. C(F)LP Systems: Naı̈ve Labeling
Benchmark

T OY(FD)

PAKCS

SICStus

SWI

GNU

Ciao

cars
equation10
equation20
magic(64)
magic(100)
magic(150)
magic(200)
magic(300)
pythagoras
queens(8)
queens(16)
queens(20)
queens(24)
queens(30)
sendmore
suudoku

5
20
35
265
910
2700
5970
18365
50
10
180
4030
8330
1141760
0
10

N
50
60
340
980
3180
6540
22750
80
20
200
4200
8400
1141940
5
20

5
10
10
(430) 260
(1520) 900
(4770) 2560
(10870) 5690
(RE) 17780
20
10
170
3930
8120
1069750
0
10

N
590
1185
N (OGS)
N (OGS)
N (OGS)
N (OGS)
N (OGS)
940
110
38720
1064130
??
??
15
60

1
2
4
134
901
(SO) 4894
(SO) 14570
(SO) 68020
10
1
11
216
460
67745
0
1

N
N
N
N
N
N
902
31
6873
190435
576625
??
14
51

Table 10. Speed-Up of T OY(F D) wrt. other C(F)LP Systems for Naı̈ve Labeling
Benchmark

PAKCS

SICStus

SWI

GNU

Ciao

cars
equation10
equation20
magic (64)
magic (100)
magic (150)
magic (200)
magic (300)
pythagoras
queens (8)
queens (16)
queens (20)
queens (24)
queens (30)
sendmore
suudoku

∞
2.50
1.71
1.28
1.07
1.17
1.09
1.23
1.60
2.00
1.11
1.04
1.00
1.00
≥ 5.00
2.00

1 00
0.50
0.28
(1.62) 0.98
(1.67) 0.98
(1.76) 0.98
(1.82) 0.99
(∞) 0.96
0.40
1.00
0.94
0.97
0.97
0.93
≥ 1.00
1.00

∞
29.50
33.85
∞
∞
∞
∞
∞
18.80
11.00
215.11
264.05
(?)
(?)
≥ 15.00
6.00

0.20
0.10
0.11
0.50
0.99
1.81
2.44
3.70
0.20
0.10
0.06
0.05
0.05
0.05
1.00
0.10

∞
∞
∞
∞
∞
∞
∞
∞
18.04
3.12
38.18
42.25
69.22
(?)
≥ 14.00
5.10

(∞)
(∞)
(∞)

≥

Table 9 shows the results using naı̈ve labeling. The meaning for the columns is
as follows. The first column gives the name of the benchmark used in the comparison, and the next six columns show the running (elapsed) time (measured in
milliseconds) to find the first answer of the benchmark for each system.
Table 10 shows the results shown in Table 9 in terms of the speed-up of T OY(F D)

32 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
Table 11. T OY(F D) vs. C(F)LP systems: First-Fail Labeling
Benchmark

T OY(FD)

PAKCS

SICStus

SWI

GNU

Ciao

cars
equation10
equation20
magic (64)
magic (100)
magic (150)
magic (200)
magic (300)
magic (400)
magic (500)
pythagoras
queens (8)
queens (16)
queens (20)
queens (24)
queens (30)
sendmore
suudoku

0
20
30
90
220
470
870
1835
3420
5510
50
10
20
45
40
150
0
10

N
50
55
150
310
690
1480
3610
10050
13100
80
15
50
75
80
190
5
20

0
10
15
(320) 80
(1090) 195
(3440) 465
(7950) 850
(RE) 1820
(RE) 3370
(RE) 5250
10
5
8
10
15
25
0
10

N
N
N
N
N
N
N
N
N
N
N
N
N
N
N
N
N
N

0
3
4
18
53
(SO) 52
(SO) 125
(SO) 568
(SO) 1088
(SO) 1830
10
1
2
3
4
6
0
1

N
N
N
N
N
N
N
N
N
N
N
N
N
N
N
N
N
N

with respect to the rest of the systems (that is, the result of dividing the time of a
given system by the time of T OY(F D)).
Table 11 shows the results of solving the same benchmarks by using first-fail
labeling. Note that the current versions of SWI Prolog and Ciao Prolog do not
provide first-fail labeling. Also, Table 12 shows the speed-up corresponding to the
results in Table 11 and again displays the performance of T OY(F D) with respect
to the rest of the systems. The meaning for the columns is as in Table 10, but a
last column is added in order to show the speed-up of T OY(F D) using first-fail
labeling with respect to the same system with naı̈ve labeling.
Tables 13 and 14 display corresponding results for optimization. Particularly,
Table 13 shows the (elapsed) time measured in milliseconds to solve the optimization
problem considered in the benchmarking process, whereas Table 14 shows the speedup of our system with respect to the rest of the systems.
In these tables, all numbers represent the average of ten runs. The symbol ??
means that we did not receive a solution for the benchmark in a reasonable time
and (?) indicates a non-determined value. The symbol N in the PAKCS, SWI Prolog
and Ciao Prolog columns mean that we could not formulate the benchmark because
of insufficient provision for constraints.
Also the notation OGS in the SWI column indicates that we received an error of
Out Of Global Stack and, consequently, no answer was returned. In the GNU Prolog
column, the notation (SO) number means that, in the first execution of the program
no answer was calculated because a Stack Overflow error was raised, and that, after
increasing significantly the corresponding (cstr and trail) environment variables, in

Constraint Functional Logic Programming over Finite Domains

33

Table 12. Speed-Up of T OY(F D) wrt. other C(F)LP Systems for First-Fail Labeling
Benchmark

PAKCS

SICStus

SWI

GNU

Ciao

T OY(FD)
(naı̈ve)

cars
equation10
equation20
magic (64)
magic (100)
magic (150)
magic (200)
magic (300)
magic (400)
magic (500)
pythagoras
queens (8)
queens (16)
queens (20)
queens (24)
queens (30)
sendmore
suudoku

∞
2.50
1.83
1.66
1.40
1.46
1.70
1.96
2.93
2.37
1.60
1.50
2.50
1.66
2.00
1.26
≥ 5.0
2.00

≥ 1.00
0.50
0.50
(3.55) 0.88
(4.95) 0.88
(7.31) 0.98
(9.13) 0.97
(∞) 0.99
(∞) 0.98
(∞) 0.95
0.20
0.50
0.40
0.22
0.37
0.16
≥ 1.00
1.00

∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞

≥ 1.00
0.15
0.13
0.20
0.24
(∞) 0.11
(∞) 0.14
(∞) 0.30
(∞) 0.31
(∞) 0.33
0.20
0.10
0.10
0.06
0.10
0.04
≥ 1.00
0.10

∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞
∞

≥ 5.00
1.00
1.16
2.94
4.13
5.74
6.86
10.00
(?)
(?)
1.00
1.00
9.00
89.55
208.25
7611.73
≥ 1.00
1.00

Table 13. T OY(F D) vs. C(F)LP Systems: Optimization Benchmarks
Benchmark

T OY(FD)

PAKCS

SICStus

SWI

GNU

Ciao

golomb(8)
golomb(10)
golomb(12)

360
26230
5280170

350
27500
5453220

280
25730
5208760

N
N
N

86
8595
2162863

N
N
N

further executions we obtained an answer in the (average) time indicated by number.
The notation RE in the SICStus Prolog column indicates that we also did not
compute an answer because a Resource Error by Insufficient Memory was returned.
The dash (-) in the Ciao Prolog column means that we received an incorrect answer
for this benchmark5 .
As already declared, whenever possible we maintained the same formulation for
all the benchmarks in each system. However, this was not always possible in the
magic series benchmark. In the T OY(F D), PAKCS and SICStus Prolog systems,
this problem was coded by using specific constraints (i.e., count/4, sum/3 and
scalar product/4 - see formulation in Example 9). However, the GNU Prolog system
5

This event seems to be caused by a bug existing in the F D constraint package.

34 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
Table 14. Speed-Up of T OY(F D) wrt. other C(F)LP Systems for Optimization
Benchmarks
Benchmark

SICStus

PAKCS

SWI

GNU

Ciao

golomb(8)
golomb(10)
golomb(12)

0.77
0.98
0.98

0.97
1.04
1.03

∞
∞
∞

0.23
0.32
0.40

∞
∞
∞

lacks these constraints and, therefore, we used a classical formulation that requires
to use reified constraints (Codognet and Diaz 1996). This classical formulation is
somewhat different in T OY(F D) since reification applies to Boolean types (whilst
in GNU Prolog, as in general in CLP (F D) languages, the Boolean values f alse and
true correspond to the numerical values 0 and 1 respectively). On the other hand,
it was not possible in PAKCS as reified constraints are not available in this system.
However, since SICStus Prolog allows reified constraints, the two formulations were
considered in this system. Then, in the SICStus column and for the magic series
benchmark row, we show between parentheses the (elapsed solving) time associated
with the reified constraints-based formulation followed by the time associated to
the alternative formulation based on the use of specific constraints.
In the speed-up tables, in those cases in which for a particular system either a
problem could not be expressed (e.g., for PAKCS, SWI Prolog or Ciao Prolog), or
an error was returned avoiding to compute a first answer, or an incorrect answer
was returned, we use the symbol ∞ to express that our system clearly outperforms
that system since our system provides constraint support to formulate a solution
for the benchmark and compute an answer. Also, a result ≥ x.00 indicates that
T OY(F D) computed an answer in 0.0 milliseconds and thus no speed-up can be
calculated; in these cases, x.00 indicates that T OY(F D) is, at least, x times faster
than the compared system.

4.5.4 Analysis of the Results
The third column in Tables 10 and 12, and column 2 in Table 14 show that, in
general, our implementation behaves closely to that of SICStus Prolog in both
constraint satisfaction and constraint optimization (in fact, this is not surprising as
current version of T OY(F D) uses SICStus Prolog F D solver) except for solving
linear equations (in these cases it is between two and four times slower). The reason
seems to be in the transformation process previous to the invocation of the F D
solver. Expressions have to be transformed into head normal form, which means
that their arguments are also transformed into head normal form (see Section 4.4).
Thus, there seems to be an overhead when expressions (such as those for linear
equations) involve a high number of arguments and sub-expressions. This may be
the same reason argued to explain the slow-down of T OY(F D) in the solving of

Constraint Functional Logic Programming over Finite Domains

35

the queens benchmark via first-fail labeling, although no appreciable slow-down was
shown in the solving via naı̈ve labeling.
PAKCS is between one and three times slower than our implementation. This
is quite interesting as the PAKCS implementation is fairly efficient and is also
based on the SICStus Prolog F D library. Perhaps the reason of this slowdown with
respect to T OY(F D) is that PAKCS implements an alternative operational model
that also supports concurrency, and this model introduces some kind of overhead
in the solving of goals.
T OY(F D) also performs reasonably well compared to the other CLP (F D) systems. It clearly outperforms both Ciao Prolog’s and SWI Prolog’s constraint solvers
which are far, in their current versions, from the efficiency of T OY(F D) in the solving of constraint satisfaction problems (for fairness, we have to say that these results
cannot be extrapolated to the whole Ciao Prolog and SWI Prolog systems which
are quite efficient; in fact, the integer bounds constraint solver of SWI Prolog seems
to be a rather non-optimized simple integer constraint solver that probably will be
largely improved in future versions. This same argument can be applied to the finite
domain constraint solving package currently existing in the Ciao Prolog system that
seems to be non-mature yet). With respect to GNU Prolog’s constraint solver, our
system behaves acceptably well if we take into account that this solver has shown
an efficiency comparable to commercial systems. Except for the N-queens benchmark (that seems to be particularly optimized for GNU solver) our system is in
the same order of efficiency. Moreover, it even behaves better on scalable problems
when the size of the problem increases (e.g., in the magic series problem with naı̈ve
labeling). In this sense, again with the exception of the N-queens problem, as the
instance of the problem increases, the performance of T OY(F D) becomes closer
to that of GNU Prolog (this result is confirmed for both constraint satisfaction and
constraint optimization).
Further, with regard to the comparison to the other CF LP (F D) system, we have
to say that PAKCS provides a small set of global constraints (i.e., exactly four) as
mentioned in Section 4.5, whereas T OY(F D) also gives support to specialized constraints for particular problems such as scheduling and placements problems. Moreover, PAKCS does not provide F D constraints that help users to recover statistics
of the constraint solving process (e.g., number of domain prunings, entailments detected by a constraint, backtracks due to inconsistencies, constraint resumptions,
etc) which is very useful in practice, as T OY(F D) does. (For the sake of fairness,
we mention again that PAKCS supports the concurrent evaluation of constraints
which is also very convenient in practice.)
Based on the results shown in this Section, we can assure that T OY(F D) is
the first pure CF LP (F D) system that provides a wide set of F D constraints that
makes it really competitive compared to existing CLP (F D) systems. These results
encourage us to continue working on our approach, and we hope to further improve
the results in a close future by means of introducing further optimizations.

36 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
5 Related Work
In addition to already cited related work, in this section we discuss some more related work. As already said, most of the work to integrate constraints in the declarative programming paradigm has been developed on LP (Codognet and Diaz 1996;
Carlsson et al. 1997). However, there exist some attempts to integrate constraints in
the functional logic framework. For instance, (Arenas et al. 1996; López-Fraguas and Sánchez-Hernández 1999)
show how to integrate both linear constraints over real numbers and disequality
constraints in the F LP language T OY. Also, (Lux 2001) describes the addition of
linear constraints over real numbers to the F LP language Curry (Hanus 1999). Our
work is guided to the F D constraint, instead of real constraints (although they are
preserved), which allows to use non-linear constraints and adapts better to a range
of F D applications.
With respect to F D, the closer proposal to ours is that described in (Antoy and Hanus 2000)
that indicated how the integration of F D constraints in F LP could be carried out.
As already indicated, PAKCS is an implementation that follows these indications.
T OY(F D) may also be considered from a multiparadigmatic view that means
to combine constraint programming with another paradigms in one setting. In this
context, there are some similarities with the language Oz (Van Roy et al. 2003;
Van Roy and Haridi 2004) as this provides salient features of F P such as compositional syntax and first-class functions, and features of LP and constraint programming including logic variables, constraints, and programmable search mechanisms.
However, Oz is quite different to T OY(F D) because of a number or reasons: (1)
Oz does not provide main features of classical functional languages such as explicit types or curried notation; (2) functional notation is provided in Oz as a syntactic convenience; (3) The Oz computation mechanism is not based on rewriting
logic as that of T OY(F D) ; (4) Oz supports a class of lazy functions based on a
demand-driven computation but this is not an inherent feature of the language (as
in T OY(F D) ) and functions have to be made lazy explicitly (e.g., via the concept
of futures); (5) functions and constraints are not really integrated, that is to say,
they do not have the same category as in T OY(F D) (i.e., constraints are functions) and both coexist in a concurrent setting, and (6) Oz programs follow a far
less concise program syntax than T OY(F D). In fact, Oz generalizes the CLP and
concurrent constraint programming paradigms to provide a very flexible approach
to constraint programming very different to our proposal for CF LP (F D).
Also, LIFE (Aït-kaci and Podelski 1993) is an experimental language aiming to
integrate logic programming and functional programming but, as Oz, the proposal
is quite different to T OY(F D) as firstly, it is considered in the framework of
object-oriented programming, and, secondly, LIFE enables the computation over
an order-sorted domain of feature trees by allowing the equality (i.e., unification)
and entailment (i.e., matching) constraints over order-sorted feature terms.
There exist other constraint systems that share some aspects with
T OY(F D) although they are very different. One of those systems is FaCiLe
(Barnier and Brisset 2001), a constraint programming library that provides constraint solving over integer finite domains, HO functions, type inference, strong

Constraint Functional Logic Programming over Finite Domains

37

typing, and user-defined constraints. However, despite these similarities, FaCiLe is
very different to T OY(F D) as it is built on top of the functional language OCaml
that provides full imperative capabilities and does not have a logical component;
also OCaml is a strict language, as opposed to lazy ones. In fact, as Oz , it allows
the manipulation of potentially infinite data structures by explicit delayed expressions, but laziness is not an inherent characteristic of the resolution mechanism as in
T OY(F D). Moreover, FaCiLe is a library and thus it lacks programming language
features.
Other interesting systems are OPL (Van Hentenryck 1999) and AMPL (Fourer et al. 1993)
that cannot be compared to our work because they are algebraic languages which
therefore are not general programming languages. Moreover, these languages do
not benefit neither from complex terms and patterns nor from non-determinism as
T OY(F D) does.
Finally, we mention here another CF LP scheme proposed in the Phd Thesis
of M. Marin (Marin 2000). This approach introduces CF LP (D, S, L), a family of
languages parameterized by a constraint domain D, a strategy S which defines the
cooperation of several constraint solvers over D, and a constraint lazy narrowing calculus L for solving constraints involving functions defined by user given constrained
rewriting rules. This approach relies on solid work on higher-order lazy narrowing calculi and has been implemented on top of Mathematica (Marin et al. 1999;
Marin et al. 2000). Its main limitation from our viewpoint is the lack of declarative
semantics.
Generally speaking, T OY(F D) is, from its nature, different to all the constraints
systems discussed above since T OY(F D) is a pure F LP language that combines
characteristics of pure LP and pure F P paradigms, and its operational mechanism is
the result of combining the operational methods of logic languages (i.e., unification
and resolution) and functional languages (i.e., rewriting).

6 Conclusions and Future Work
In this paper we have presented CF LP (F D), a functional logic programming approach to F D constraint solving. CF LP (F D) is not only a declarative alternative
to CLP (F D) but also extends its capabilities with new characteristics unusual or
not existing in CLP (F D) such as functional and curried notation, types, curried
and higher-order functions (e.g., higher-order constraints), constraint composition,
higher-order patterns, lazy evaluation and polymorphism, among others. As a consequence, CF LP (F D) provides better tools, when compared to CLP (F D), for a
productive declarative programming as it implicitly enables more expressivity, due
to the combination of functional, relational and curried notation as well as type
system. Moreover, lazy evaluation allows the use of structures hard to manage in
CLP (F D), such as infinite lists.
A CF LP (F D) language is also presented by describing its syntax, type discipline
and both declarative and operational semantics. F D constraints are integrated as
functions to make them first-class citizens and allow their use in any place where a

38 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
data can (e.g., as arguments of functions). This provides a powerful mechanism to
define higher-order constraints.
We have also reported an implementation of the CF LP (F D) proposal which
connects a F LP language to a F D constraint solver, that provides both lazy computation and F D constraint solving. The F D solver is required to hold termination,
soundness and completeness properties. T OY(F D) is our implementation of the
CF LP (F D) language previously described, that connects the functional logic language T OY to the efficient F D constraint solver of SICStus Prolog. The result is
that T OY(F D) is a lazy functional logic system with support for F D constraint
solving.
We have also explained the most important contributions by showing the extra
capabilities of CF LP (F D) with respect to CLP (F D) . This comparison points out
the main benefits of integrating F LP and F D in a declarative language.
Moreover, we have also shown that constraint solving in T OY(F D) is fairly
efficient as, in general, behaves closely to SICStus Prolog, which means that the
wrapping of SICStus Prolog by T OY does not increase significantly the computation time. In addition, T OY(F D) clearly outperforms existing CLP (F D) systems
such as SWI Prolog and Ciao Prolog and also is competitive with respect to GNU
Prolog, one of the most efficient CLP (F D) systems. Furthermore, T OY(F D) is
around one and three times faster than PAKCS, its closer CF LP (F D) implementation. Practical applications of T OY(F D) can be found in (Fernández et al. 2002;
Fernández et al. 2003).
Throughout the paper it should have been clear that one inherent advantage of
the CF LP (F D) approach is that it enables to solve all the CLP (F D) applications
as well as other problems closer to the functional setting.
We claim that the integration of F D constraints into a F LP language receive
benefits from both worlds, i.e., taking functions, higher-order patterns, partial applications, non-determinism, lazy evaluation, logical variables, and types from F LP
and domain variables, constraints, and propagators from the F D constraint programming.
In addition, we claim that the idea of interfacing a F LP language and constraint solvers can be extended to other kind of interesting constraint systems, such
as non-linear constraints, constraints over sets, or Boolean constraints, to name a
few. Observe that T OY(F D) can be thought of as a constraint solving procedure
integrated into a sophisticated, state-of-the-art execution mechanism for lazy narrowing. Operationally speaking, T OY(F D) compiles CF LP (F D)-programs into
Prolog-programs in a system equipped with a constraint solver. This makes both
lazy evaluation and constraint solving be inherent features of the system.

Acknowledgment
We thank the anonymous reviewers for their useful comments and suggestions that
helped us to improve this paper.

Constraint Functional Logic Programming over Finite Domains

39

References
Aït-kaci, H. and Podelski, A. 1993.
Towards a meaning of LIFE.
Journal of Logic Programming 16, 3, 195–234.
A preliminary version appeared in
(Maluszynski and Wirsing 1991), pp:255-274.
Antoy, S. 1992. Definitional trees. In 3rd International Conference on Algebraic and
Logic Programming (ALP’92). Number 632 in LNCS. Springer-Verlag, Volterra, Italy,
143–157.
Antoy, S., Echahed, R., and Hanus, M. 2000. A needed narrowing strategy. J.
ACM 47, 4, 776–822.
Antoy, S. and Hanus, M. 2000. Compiling multi-paradigm declarative programs into
prolog. In 3rd International Workshop on Frontiers of Combining Systems (FroCoS’2000), H. Kirchner and C. Ringeissen, Eds. Number 1794 in LNCS. Springer,
Nancy, France, 171–185.
Apt, K. 2003. Principles of constraint programming. Cambridge University Press.
Arenas, P., Hortalá, M., López-Fraguas, F., and Ullán, E. 1996. Real constraints
within a functional logic language. In Joint Conference on Declarative Programming
(APPIA-GULP-PRODE’96), P. Lucio, M. Martelli, and M. Navarro, Eds. Donostia-San
Sebastian, Spain.
Barnier, N. and Brisset, P. 2001. FaCiLe: a functional constraint library. ALP Newsletter 14, 2 (May).
Caballero, R., López-Fraguas, F., and Sánchez, J. 1997. User’s manual for T OY.
Technical report SIP-5797, Universidad Complutense de Madrid, Dpto. Lenguajes, Sistemas Informáticos y Programación.
Carlsson, M., Ottosson, G., and Carlson, B. 1997. An open-ended finite domain
constraint solver. In 9th International Symposium on Programming Languages: Implementations, Logics and Programs (PLILP’97), U. Montanari and F. Rossi, Eds. Number
1292 in LNCS. Springer-Verlag, Southampton, UK, 191–206.
Codognet, P. and Diaz, D. 1996. Compiling constraints in clp(FD). The Journal of
Logic Programming 27, 3, 185–226.
Damas, L. and Milner, R. 1982. Principal type-schemes for functional programs. In
Ninth ACM Symposium on Principles of Programming Languages (POPL’82). ACM
Press, Albuquerque, New Mexico, 207–212.
Darlington, J., Guo, Y., and Pull, H. 1992. A new perspective on the integration
of functional and logic languages. In International Conference on Fifth Generation
Computer Systems (FGCS’92), I. Staff, Ed. IOS Press, Tokyo, Japan, 682–693.
Dechter, R. 2003. Constraint processing. Morgan Kaufmann.
del Vado-Vı́rseda, R. 2003. A demand-driven narrowing calculus with overlapping definitional trees. In ACM SIGPLAN Conference on Principles and Practice of Declarative
Programming (PPDP’03). ACM Press, Uppsala, Sweden, 213–227.
del Vado-Vı́rseda, R. 2005. Declarative constraint programming with definitional trees.
In 5th International Workshop on Frontiers of Combining Systems (FroCoS’05). Lecture
Notes in Computer Science, vol. 3717. Springer, Vienna, Austria, 184–199.
Diaz, D. and Codognet, P. 2001. Design and implementation of the GNU prolog system.
Journal of Functional and Logic Programming 2001, 6 (October).
Dincbas, M., Simonis, H., and Van Hentenryck, P. 1988. Solving the car-sequencing
problem in constraint logic programming. In 8th European Conference on Artificial
Intelligence (ECAI’88), Y. Kodratoff, Ed. Pitmann Publishing, London, Munich, Germany, 290–295.
Estévez-Martín, S. and del Vado-Vı́rseda, R. 2005. Designing an efficient computation strategy in cf lp(FD) using definitional trees. In 2005 ACM SIGPLAN workshop

40 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
on Curry and functional logic programming (WCFLP ’05). ACM Press, New York, NY,
USA, 23–31.
Fernández, A. J., Hortalá-González, M. T., and Sáenz-Pérez, F. 2002. A constraint functional logic language for solving combinatorial problems. In Research and
Development in Intelligent Systems XIX, A. P. M. Bramer and F. Coenen, Eds. BCS
Conference Series. Springer-Verlag, Cambridge, England, 337–350.
Fernández, A. J., Hortalá-González, M. T., and Sáenz-Pérez, F. 2003. Solving
combinatorial problems with a constraint functional logic language. In 5th International
Symposium on Practical Aspects of Declarative Languages (PADL’2003), P. Wadler and
V. Dahl, Eds. Number 2562 in LNCS. Springer-Verlag, New Orleans, Louisiana, USA,
320–338.
Fernández, A. J., Hortalá-González, T., and Sáenz-Pérez, F. 2004. TOY(FD):
System, Sources and user manual. Available at http://toy.sourceforge.net/.
Fernández, M. 1992. Narrowing based procedures for equational disunification. Applicable Algebra in Engineering Communication and Computing 3, 1–26.
Fourer, R., Gay, D., and Kernighan, B. 1993. AMPL: A modeling language for
mathematical programming. Scientific Press.
Frühwirth, T. and Abdennadher, S. 2003. Essentials of constraint programming.
Cognitive Technologies Series. Springer.
GNU Prolog. 2005. http://pauillac.inria.fr/∼diaz/gnu-prolog/.
González-Moreno, J., Hortalá-González, M., López-Fraguas, F., and
Rodrı́guez-Artalejo, M. 99a. An approach to declarative programming based
on a rewriting logic. The Journal of Logic Programming 40, 1 (July), 47–87.
González-Moreno, J., Hortalá-González, M., and Rodrı́guez-Artalejo, M. 99b.
Polymorphic types in functional logic programming. In 4th International Symposium on Functional and Logic Programming (FLOPS’99), A. Middeldorp and T. Sato,
Eds. Number 1722 in LNCS. Springer-Verlag, Tsukuba, Japan, 1–20. Also published
in a special issue of the Journal of Functional and Logic Programming, 2001. See
http://danae.uni-muenster.de/lehre/kuchen/JFLP.
Gunter, C. and Scott, D. 1990. Semantic domains. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, J. van Leeuwen, Ed. Elsevier
and The MIT Press, 633–674.
Hanus, M. 1994. The integration of functions into logic programming: a survey. The
Journal of Logic Programming 19-20, 583–628. Special issue: Ten Years of Logic Programming.
Hanus, M. 1999.
Curry: a truly integrated functional logic language.
http://www.informatik.uni-kiel.de/∼curry/.
Hanus M. (editor). 2005.
PAKCS 1.7.1, User manual (version of December 2005).
The Portland Aachen Kiel Curry System. Available from
http://www.informatik.uni-kiel.de/∼pakcs/.
Haralick, R. and Elliot, G. 1980. Increasing tree search efficiency for constraint
satisfaction problems. Artificial Intelligence 14, 263–313.
Henz, M. and Müller, T. 2000. An overview of finite domain constraint programming.
In 5th Conference of the Association of Asia-Pacific Operational Research Societies.
Singapore.
Jaffar, J. and Maher, M. 1994. Constraint logic programming: a survey. The Journal
of Logic Programming 19-20, 503–581.
Loogen, R., López-Fraguas, F. J., and Rodrı́guez-Artalejo, M. 1993. A demand
driven computation strategy for lazy narrowing. In 5th International Symposium on Programming Language Implementation and Logic Programming PLILP’93, M. Bruynooghe

Constraint Functional Logic Programming over Finite Domains

41

and J. Penjam, Eds. Lecture Notes in Computer Science, vol. 714. Springer, Tallinn,
Estonia, 184–200.
López-Fraguas, F. 1992. A general scheme for constraint functional logic programming. In 3rd International Conference on Algebraic and Logic Programming (ALP’92),
H. Kirchner and G. Levi, Eds. Number 632 in LNCS. Springer-Verlag, Volterra, Italy,
213–227.
López-Fraguas, F., Rodríguez-Artalejo, M., and del Vado-Vírseda, R. 2004a.
Constraint functional logic programming revisited. In 5th International Workshop on
Rewriting Logic and its Applications (WRLA’2004). Barcelona, Spain. An extended
and revised version has also been published in Elsevier ENTCS series 117:5–50, 2005.
López-Fraguas, F., Rodríguez-Artalejo, M., and del Vado-Vírseda, R. 2004b.
A lazy narrowing calculus for declarative constraint programming. In 6th ACMSIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’04). ACM Press, Verona, Italy, 43–54.
López-Fraguas, F. and Sánchez-Hernández, J. 1999. T OY: A multiparadigm declarative system. In 10th International Conference on Rewriting Techniques and Applications, P. Narendran and M. Rusinowitch, Eds. Number 1631 in LNCS. Springer-Verlag,
Trento, Italy, 244–247.
Lux, W. 2001. Adding linear constraints over real numbers to Curry. In 5th International Symposium on Functional and Logic Programming (FLOPS’2001), A. Middeldorp, H. Kuchen, and K. Ueda, Eds. Number 2024 in LNCS. Springer-Verlag, Tokyo,
Japan, 185–200.
Maluszynski, J. and Wirsing, M., Eds. 1991. Programming Language Implementation
and Logic Programming, 3rd International Symposium, PLILP’91, Passau, Germany,
August 26-28, 1991, Proceedings. Lecture Notes in Computer Science, vol. 528. Springer.
Marin, M. 2000. Functional logic programming with distributed constraint solving. Ph.D.
thesis, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz.
Marin, M., Ida, T., and Schreiner, W. 1999. CFLP: a mathematica implementation of
a distributed constraint solving system. In 3rd International Mathematical Symposium
(IMS’99). Computational Mechanics Publications. WIT Press, Hagenberg, Austria, 23–
25.
Marin, M., Ida, T., and Suzuki, T. 2000. Cooperative constraint functional logic
programming.
In International Symposium on Principles of Software Evolution
(IPSE’2000), T. Katayama, T. Tamai, and N. Yonezaki, Eds. IEEE, Kanazawa, Japan,
223–230.
Marriot, K. and Stuckey, P. J. 1998. Programming with constraints. The MIT Press,
Cambridge, Massachusetts.
Middeldorp, A. and Okui, S. 1998. Deterministic lazy narrowing calculus. Journal of
Symbolic Computation 25, 6, 733–757.
Middeldorp, A., Suzuki, T., and Hamada, M. 2002. Complete selection functions for
a lazy conditional narrowing calculus. Journal of Functional and Logic Programming 3.
Peyton-Jones, S. 1987. The implementation of functional programming languages. Prentice Hall, Englewood Cliffs, N.J.
Shearer, J. 1990. Some new optimum golomb rulers. IEEE Transactions on Information
Theory 36, 183–184.
SICStus Prolog. 2005. http://www.sics.se/isl/sicstus.
SWI-Prolog. 2005. http://www.swi-prolog.org/.
Tsang, E. 1993. Foundations of constraint satisfaction. Academic Press, London and
San Diego.

42 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
Van Hentenryck, P. 1989. Constraint satisfaction in logic programming. The MIT
Press, Cambridge, MA.
Van Hentenryck, P. 1999. The OPL optimization programming language. The MIT
Press, Cambridge, MA.
Van Roy, P., Brand, P., Duchier, D., Haridi, S., Henz, M., and Schulte, C. 2003.
Logic programming in the context of multiparadigm programming: the Oz experience.
Theory and Practice of Logic Programming 3, 6 (November), 717–763.
Van Roy, P. and Haridi, S. 2004. Concepts, techniques and models of computer programming. The MIT Press, Cambridge, MA.
Wielemaker, J. 2003. An overview of the SWI-Prolog programming environment. In
Proceedings of the 13th International Workshop on Logic Programming Environments,
F. Mesnard and A. Serebenik, Eds. Katholieke Universiteit Leuven, Heverlee, Belgium,
1–16. CW 371.

Appendix A [Proof of Theorem 1] in Page 12
The proof of theorem 1 can be done distinguishing several cases from the declarative
semantics of each primitive function symbol given in Table 1 and the requirements
of each constraint solver rule or failure rule in Tables 2-5:
Rules of Table 2
σ ⊢⊢χ
We examine for example the first rule in Table 2: seq t s →! R, S
(t == s, Sθ1
σθ1 ) ∨ (t \ = s, Sθ2
σθ2 ) with R ∈
/ χ, θ1 = {R 7→ true}
and θ2 = {R 7→ f alse} (the rest of rules in Table 2 are analogous). We prove that
σ) = SolF D (t == s, Sθ1
σθ1 ) ∪ SolF D (t \ = s, Sθ2
SolF D (seq t s →! R, S
σθ2 ):
⊆) Let η ∈ SolF D (seq t s →! R, S
σ). By definition of SolF D we have η ∈
σ). Since η ∈ SolF D (seq t s →! R) we
SolF D (seq t s →! R) and η ∈ SolF D (S
obtain seq F D tη sη → η(R) with η(R) total. According to Table 1, η(R) must be
only true or f alse. We distinguish two cases:
• If η(R) = true then trivially η ∈ SolF D (seq t s →! true) or equivalently
η ∈ SolF D (t == s). Moreover, since η(R) = true = (true)η we have η ∈
Sol(θ1 ) and then θ1 η = η (because η(θ1 (R)) = (true)η = η(R) and η(θ1 (X))
= η(X) for all X 6= R). Then, since η ∈ SolF D (S
σ) we also have θ1 η ∈
σ), or equivalently η ∈ SolF D (Sθ1
σθ1 ). We can conclude η ∈
SolF D (S
SolF D (t == s, Sθ1
σθ1 ).
• If η(R) = f alse, using an analogous reasoning, we can also conclude η ∈
σθ2 ).
SolF D (t \ = s, Sθ2
Therefore, η ∈ SolF D (t == s, Sθ1
⊇) Let η ∈ SolF D (t == s, Sθ1
tinguish again two cases:
• If η ∈ SolF D (t == s, Sθ1

σθ1 ) ∪ SolF D (t \ = s, Sθ2
σθ1 ) ∪ SolF D (t \ = s, Sθ2

σθ2 ).
σθ2 ). We dis-

σθ1 ) then, by definition of SolF D we have η ∈

Constraint Functional Logic Programming over Finite Domains

43

σθ1 ) (or equivalently, η ∈ SolF D (Sθ1 )
SolF D (t == s) and η ∈ SolF D (Sθ1
and η ∈ SolF D (σθ1 )). Since η ∈ SolF D (σθ1 ) and R ∈
/ dom(σ) (by initial
hypothesis, seq t s →! R, S
σ satisfy the requirements of Definition 2)
we deduce η ∈ Sol(θ1 ) and then η(R) = (true)η = true. But then, η ∈
SolF D (seq t s →! R) because seq F D tη sη → η(R) = true and we have η
∈ SolF D (t == s). Moreover, θ1 η = η (because η(θ1 (R)) = (true)η = η(R)
and η(θ1 (X)) = η(X) for all X 6= R) and we can also obtain η ∈ SolF D (S
σ) because η ∈ SolF D (Sθ1
σθ1 ), or equivalently, θ1 η ∈ SolF D (S
σ).
σ).
Therefore, η ∈ SolF D (seq t s →! R, S
• If η ∈ SolF D (t \ = s, Sθ2
σθ2 ), using an analogous reasoning, we can also
conclude η ∈ SolF D (seq t s →! R, S
σ).
The remaining conditions of the theorem for this rule trivially hold because of the
σ satisfies the requirements of Definition 2,
initial hypothesis seq t s →! R, S
and because of the conditions of the rule R ∈
/ χ.
Rules of Table 3
σ ⊢⊢χ S
σ with u ∈ Z.
We examine the first rule in Table 3: u == u, S
In this case, trivially SolF D (u == u, S
σ) = SolF D (u == u) ∩ SolF D (S
σ)
σ) = SolF D (S
σ). The remaining conditions of the
= V al(F D) ∩ SolF D (S
theorem trivially holds by initial hypothesis. We examine now the second rule in
Table 3: X == t, S
σ ⊢⊢χ t == t, Sθ
σθ with X ∈
/ χ ∪ var(t), var(t) ∩ χ =
σ) = SolF D (t == t, Sθ
∅ and θ = {X 7→ t}. We prove that SolF D (X == t, S
σθ):
⊆) Let η ∈ SolF D (X == t, S σ). By definition of SolF D we have η ∈ SolF D (X ==
σ). Since η ∈ SolF D (X == t) we obtain seq F D η(X) tη →
t) and η ∈ SolF D (S
true. According to Table 1 we obtain η(X) = tη with tη total and then η ∈ Sol(θ).
In this situation, trivially η ∈ SolF D (t == t). Moreover, since η ∈ Sol(θ), we deduce θη = η (because η(θ(X)) = tη = η(X) and η(θ(Y )) = η(Y ) for all Y 6= X).
Then, since η ∈ SolF D (S
σ), we also have θη ∈ SolF D (S
σ), or equivalently
σθ). Therefore, we can conclude η ∈ SolF D (t == t, Sθ
σθ).
η ∈ SolF D (Sθ
⊇) Let η ∈ SolF D (t == t, Sθ
σθ). By definition of SolF D we have η ∈
SolF D (t == t) and η ∈ SolF D (Sθ
σθ) (or equivalently, η ∈ SolF D (Sθ) and
η ∈ SolF D (σθ)). Since η ∈ SolF D (σθ) and X ∈
/ dom(σ) (by initial hypothesis,
σ satisfies the requirements of Definition 2) we deduce η ∈ Sol(θ)
X == t, S
and then η(X) = tη. But then, η ∈ SolF D (X == t) because η ∈ SolF D (t == t) and
seq F D η(X) tη → true with η(X) = tη total. Moreover, θη = η (because η(θ(X))
= tη = η(X) and η(θ(Y )) = η(Y ) for all Y 6= X) and we can obtain η ∈ SolF D (S
σ) because η ∈ SolF D (Sθ
σθ), or equivalently, θη ∈ SolF D (S
σ). Therefore
σ).
η ∈ SolF D (X == t, S
The remaining conditions of the theorem for this rule trivially hold because of

44 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
σ satisfies the requirements of Definition 2,
the initial hypothesis X == t, S
and because of the conditions of the rule X ∈
/ χ ∪ var(t) and var(t) ∩ χ = ∅.
Finally, we examine the main rule in Table 3 for strict disequality (the rest of rules
W
σ ⊢⊢χ ( i (Sθi
σθi ))
in Table 3 are analogous or more simples): X \ = h tn , S
Wn
σθ)) with X ∈
/ χ, var(h tn ) ∩ χ 6= ∅, θi = {X 7→ hi
∨ ( k=1 (Uk \ = tk θ, Sθ
Y mi } with hi 6= h, and θ = {X 7→ h U n } with Y mi , U n new fresh variables. We
S
σ) = ( i SolF D (∃Y mi . (Sθi
σθi )) ) ∪ (
prove that SolF D (X \ = h tn , S
Sn
Sol
(∃U
.
(U
\
=
t
θ,
Sθ
σθ))
):
F
D
n
k
k
k=1
⊆) Let η ∈ SolF D (X \ = h tn , S
σ). By definition of SolF D we have η ∈
σ). Since η ∈ SolF D (X \ = h tn ) we
SolF D (X \ = h tn ) and η ∈ SolF D (S
obtain seq F D η(X) (h tn )η → f alse. According to Table 1, η(X) and (h tn )η =
h tn η have no common upper bound w.r.t. the information ordering ⊑, and we can
distinguish two cases:
• η(X) = hi smi with hi 6= h. Since Y mi are new variables, we can define η ′
=\Y m η such that η ′ (Yk ) = sk for all 1 ≤ k ≤ mi and η ′ (Z) = η(Z) for all
i

Z ∈
/ Y mi . Clearly, η ′ (X) = η(X) = hi smi = hi η ′ (Ymi ) = (hi Y mi )η ′ and
then η ′ ∈ Sol(θi ). Moreover, θi η ′ =\Y m η because η ′ (θi (X)) = (hi Y mi )η ′
i

/
= hi η ′ (Ymi ) = hi smi = η(X) and η ′ (θi (Z)) = η ′ (Z) = η(Z) for all Z ∈
{X} ∪ Y mi . Since η ∈ SolF D (S
σ) and Y mi are new variables in S
σ,
σ), or equivalently, η ′ ∈ SolF D (Sθi
σθi ).
we also have θi η ′ ∈ SolF D (S
Finally, since there exists η ′ =\Y m η with Y mi new variables such that η ′ ∈
i

SolF D (Sθi
σθi ) we can deduce η ∈ SolF D (∃Y mi . (Sθi
σθi )) for any i
such that hi 6= h.
• η(X) = h sn with a pattern sk (1 ≤ k ≤ n) such that sk and tk η have no
common upper bound w.r.t. the information ordering ⊑ (i.e., seq F D sk tk η
→ f alse). Since U n are new variables, we can define η ′ =\U n η such that
η ′ (Uk ) = sk for all 1 ≤ k ≤ n and η ′ (Y ) = η(Y ) for all Y ∈
/ U n . Clearly,
η ′ (X) = η(X) = h sn = h η ′ (Un ) = (h U n )η ′ and then η ′ ∈ Sol(θ). Moreover,
θη ′ =\U n η because η ′ (θ(X)) = (h U n )η ′ = h η ′ (Un ) = h sn = η(X) and
η ′ (θ(Y )) = η ′ (Y ) = η(Y ) for all Y ∈
/ {X} ∪ U n . Therefore, there exists 1 ≤
FD ′
′
k ≤ n such that seq
η (Uk ) tk θη → f alse because η ′ (Uk ) = sk and tk θη ′
= tk η (since U n are new variables, var(tk ) ∩ U n = ∅) and we can deduce η ′
σ), or equivalently
∈ SolF D (Uk \ = tk θ). On the other hand, η ∈ SolF D (S
θη ′ ∈ SolF D (S
σ), because U n are again new variables in S
σ. We can
′
′
also conclude η ∈ SolF D (Sθ σθ). Finally, since there exists η =\U n η with
U n new variables such that η ′ ∈ SolF D (Uk \ = tk θ, Sθ
σθ), we obtain η ∈
σθ)) (1 ≤ k ≤ n).
SolF D (∃U n . (Uk \ = tk θ, Sθ
S
Sn
⊇) Let η ∈ ( i SolF D (∃Y mi . (Sθi
σθi )) ) ∪ ( k=1 SolF D (∃U n . (Uk \ = tk θ,
Sθ
σθ)) ). We distinguish again two cases:
σθi )) for any i such that hi 6= h. By definition of
• η ∈ SolF D (∃Y mi . (Sθi
SolF D , there exists η ′ =\Y m η such that η ′ ∈ SolF D (Sθi
σθi ) (or equivai
′
′
′
lently, η ∈ SolF D (Sθi ) and η ∈ SolF D (σθi )). Since η ∈ SolF D (σθi ) and X

Constraint Functional Logic Programming over Finite Domains

45

∈
/ dom(σ) (by initial hypothesis, X \ = h tn , S σ satisfies the requirements
of Definition 2), we deduce η ′ ∈ Sol(θi ) and then η ′ (X) = (hi Y mi )η ′ =
hi η ′ (Ymi ). Moreover, since η ′ =\Y m η, we also deduce θi η ′ =\Y m η because
i

i

η ′ (θi (X)) = (hi Y mi )η ′ = η ′ (X) = η(X) and η ′ (θi (Z)) = η ′ (Z) = η(Z) for
all Z ∈
/ {X} ∪ Y mi . In this situation, seq F D η ′ (X) (h tn )η ′ → f alse, because
′
η (X) = (hi Y mi )η ′ = hi η ′ (Ymi ) and (h tn )η ′ = h tn η ′ with hi 6= h have
no common upper bound w.r.t. the information ordering ⊑. Therefore, η ′ ∈
SolF D (X \ = h tn ), and we also have η ∈ SolF D (X \ = h tn ) because Y mi
are new variables in X \ = h tn and η ′ =\Y m η. On the other hand, since
i

σθi ), or equivalently θi η ′ ∈ SolF D (S
σ), and Y mi are
η ′ ∈ SolF D (Sθi
new variables in S
σ, we obtain η ∈ SolF D (S
σ) because θi η ′ =\Y m η.
i
σ).
Therefore, η ∈ SolF D (X \ = h tn , S
• η ∈ SolF D (∃U n . (Uk \ = tk θ, Sθ σθ)) (1 ≤ k ≤ n). By definition of SolF D ,
there exists η ′ =\U n η such that η ′ ∈ SolF D (Uk \ = tk θ, Sθ
σθ) (1 ≤ k
≤ n). By definition of SolF D again we have η ′ ∈ SolF D (Uk \ = tk θ) and η ′
σθ) (or equivalently, η ′ ∈ SolF D (Sθ) and η ′ ∈ SolF D (σθ)).
∈ SolF D (Sθ
′
Since η ∈ SolF D (σθ) and X ∈
/ dom(σ) (by initial hypothesis, X \ = h tn ,
σ satisfies the requirements of Definition 2) we deduce η ′ ∈ Sol(θ) and
S
then η ′ (X) = (h U n )η ′ = h η ′ (Un ). Moreover, since η ′ =\U n η, we also deduce
θη ′ =\U n η because η ′ (θ(X)) = (h U n )η ′ = η ′ (X) = η(X) and η ′ (θ(Z)) =
η ′ (Z) = η(Z) for all Z ∈
/ {X} ∪ U n . Since η ′ ∈ SolF D (Uk \ = tk θ), and
according to Table 1, we have seq F D η ′ (Uk ) tk θη ′ → f alse where η ′ (Uk )
and tk θη ′ = tk η (because var(tk ) ∩ U n = ∅) have no common upper bound
w.r.t. the information ordering ⊑. In this situation, we also have seq F D η(X)
(h tn )η → f alse because η(X) = (h U n )η ′ = h η ′ (Un ), (h tn )η = h tn η, and
clearly η(X) and (h tn )η have no common upper bound w.r.t. the information
ordering ⊑ (there exists 1 ≤ k ≤ n such that η ′ (Uk ) and tk η have no common
upper bound w.r.t. the information ordering ⊑). Therefore, η ∈ SolF D (X \ =
σθ), or equivalently θη ′ ∈
h tn ). On the other hand, since η ′ ∈ SolF D (Sθ
SolF D (S
σ), and U n are new variables in S
σ, we obtain η ∈ SolF D (S
σ) because θη ′ =\U n η. Therefore, η ∈ SolF D (X \ = h tn , S
σ).
The remaining conditions of the theorem for this rule trivially hold because of the
initial hypothesis X \ = h tn , S
σ satisfies the requirements of Definition 2, and
because of the conditions of the rule X ∈
/ χ, var(h tn ) ∩ χ 6= ∅, and Y mi , U n are
new fresh variables.
Rules of Table 4
We examine the first rule in Table 4: u ≤ u′ , S
σ ⊢⊢χ S
σ with u, u′ ∈ Z
Z
′
′
and u ≤ u . In this case, trivially SolF D (u ≤ u , S
σ) = SolF D (u ≤ u′ ) ∩
σ) = V al(F D) ∩ SolF D (S
σ) = SolF D (S
σ). The remaining
SolF D (S
conditions of the theorem trivially hold by the initial hypothesis. We examine now
the main rule in Table 4 (the rest of rules are analogous or more simples): a ⊗ b =
σ ⊢⊢χ Sθ
σθ with X ∈
/ χ, a, b ∈ Z and θ = {X 7→ a ⊗Z b}. We prove
X, S

46 A.J. Fernández,T. Hortalá-González,F. Sáenz-Pérez and R. del Vado-Vı́rseda
that SolF D (a ⊗ b = X, S

σ) = SolF D (Sθ

σθ):

⊆) Let η ∈ SolF D (a ⊗ b = X, S
σ). By definition of SolF D we have η ∈
σ). Since η ∈ SolF D (a ⊗ b = X) we obtain
SolF D (a ⊗ b = X) and η ∈ SolF D (S
⊗F D a b → a ⊗Z b, seq F D (a ⊗Z b) η(X) → true where a, b, a ⊗Z b ∈ Z. According
to Table 1, we obtain η(X) = a ⊗Z b = (a ⊗Z b)η and then η ∈ Sol(θ). Moreover,
we deduce θη = η because η(θ(X)) = (a ⊗Z b)η = a ⊗Z b = η(X) and η(θ(Y )) =
σ) we also have θη ∈ SolF D (S
σ), or
η(Y ) for all Y 6= X. Since η ∈ SolF D (S
σθ).
equivalently, η ∈ SolF D (Sθ
⊇) Let η ∈ SolF D (Sθ
σθ). By definition of SolF D we have η ∈ SolF D (Sθ)
and η ∈ SolF D (σθ). Since by initial hypothesis a ⊗ b = X, S
σ satisfies the
requirements of Definition 2, we have X ∈
/ dom(σ) and then η ∈ Sol(θ) (i.e., η(X)
= (a ⊗Z b)η = (a ⊗Z b) ∈ Z, where a, b ∈ Z). But then ⊗F D a b → a ⊗Z b, seq F D
(a ⊗Z b) η(X) → true, and therefore η ∈ SolF D (a ⊗ b = X). Moreover, θη = η
because η(θ(X)) = (a ⊗Z b)η = a ⊗Z b = η(X) and η(θ(Y )) = η(Y ) for all Y 6=
σθ), or equivalently θη ∈ SolF D (S
σ), we obtain η ∈
X. Since η ∈ SolF D (Sθ
σ). Therefore, η ∈ SolF D (a ⊗ b = X, S
σ).
SolF D (S
The remaining conditions of the theorem for this rule trivially hold because of
σ satisfies the requirements of Definition 2,
the initial hypothesis a ⊗ b = X, S
and because of the conditions of the rule X ∈
/ χ.
Rules of Table 5
We examine the first rule in Table 5: u ∈ [u1 , . . . , un ], S
σ ⊢⊢χ S
σ with
u, ui ∈ Z ∪ Var and ∃i ∈ {1, . . . , n}. ui ≡ u. In this situation, and according to
Table 1, we have SolF D (u ∈ [u1 , . . . , un ]) = V al(F D): η ∈ SolF D (u ∈ [u1 , . . . ,
un ]) implies that domainF D uη [u1 η, . . . , un η] → true where ∀i ∈ {1, . . . , n−1}.
ui η ≤Z ui+1 η and ∃i ∈ {1, . . . , n}. uη =Z ui η. It holds for all η ∈ V al(F D) beσ satisfies the requirements of
cause of the initial hypothesis u ∈ [u1 , . . . , un ], S
Definition 2 (i.e., [u1 , . . . , un ] represents an increasing integer list), and because of
the conditions of this rule (i.e., ∃i ∈ {1, . . . , n}. ui ≡ u). Then, trivially SolF D (u
∈ [u1 , . . . , un ], S
σ) = SolF D (u ∈ [u1 , . . . , un ]) ∩ SolF D (S
σ) = V al(F D) ∩
σ) = SolF D (S
σ). The remaining conditions of the theorem for this
SolF D (S
rule trivially hold by the initial hypothesis. The second rule in Table 5 is completely
analogous: SolF D (u ∈
/ [u1 , . . . , un ]) = V al(F D) because u, ui ∈ Z, ∀i ∈ {1, . . . , n}.
ui 6=Z u, and according to Table 1, domainF D uη [u1 η, . . . , un η] → f alse holds for
all η ∈ V al(F D).
Finally, we examine the main rule for labeling in Table 5: labeling [. . .] [X], X
Wn
σ ⊢⊢χ i=1 (Sθi
σθi ) with X ∈
/ χ, and ∀i ∈ {1, . . . , n}, ui
∈ [u1 , . . . , un ], S
∈ Z, θi = {X 7→ ui }. We prove that SolF D (labeling [. . .] [X], X ∈ [u1 , . . . , un ], S
Sn
σ) = i=1 SolF D (Sθi
σθi ):

Constraint Functional Logic Programming over Finite Domains

47

σ). By definition
⊆) Let η ∈ SolF D (labeling [. . .] [X], X ∈ [u1 , . . . , un ], S
of SolF D we have η ∈ SolF D (labeling [. . .] [X], X ∈ [u1 , . . . , un ]) and η ∈ SolF D (S
σ). Then, indomainF D η(X) → ⊤, domainF D η(X) [u1 , . . . , un ] → true because
ui ∈ Z for all 1 ≤ i ≤ n. According to Table 1, we deduce η(X) ∈ Z, ∀i ∈ {1, . . . ,
n−1}. ui ≤Z ui+1 and ∃i ∈ {1, . . . , n}. η(X) =Z ui . Therefore, η(X) = ui = ui η and
then η ∈ Sol(θi ) (1 ≤ i ≤ n). Moreover, we have θi η = η because η(θi (X)) = ui η =
σ) we
ui = η(X) and η(θi (Y )) = η(Y ) for all Y 6= X. Finally, since η ∈ SolF D (S
can conclude θi η ∈ SolF D (S σ) or equivalently η ∈ SolF D (Sθi σθi ) (1 ≤ i ≤ n).
⊇) Let η ∈ SolF D (Sθi
σθi ) (1 ≤ i ≤ n). By definition of SolF D we have η
∈ SolF D (Sθi ) and η ∈ SolF D (σθi ). By the initial hypothesis labeling [. . .] [X], X ∈
σ satisfies the requirements of Definition 2, we have X ∈
/ dom(σ)
[u1 , . . . , un ], S
and then η ∈ Sol(θi ) (i.e., η(X) = ui η = ui due to ui ∈ Z). Moreover, we have
θi η = η because η(θi (X)) = ui η = ui = η(X) and η(θi (Y )) = η(Y ) for all Y 6=
σθi ), or equivalently, θi η ∈ SolF D (S
σ), we
X. Then, since η ∈ SolF D (Sθi
σ). Finally, we prove that η ∈ SolF D (labeling [. . .] [X], X
deduce η ∈ SolF D (S
∈ [u1 , . . . , un ]). Since η(X), ui ∈ Z for all 1 ≤ i ≤ n, [u1 , . . . , un ] is an increasing
integer list by the initial hypothesis, and there exists 1 ≤ i ≤ n such that η(X) =
ui ∈ Z, according to Table 1 we can deduce domainF D η(X) [u1 , . . . , un ] → true.
Moreover, since η(X) ∈ Z, trivially indomainF D η(X) → ⊤ according again to
Table 1. Then, indomainF D η(X) → ⊤, domainF D η(X) [u1 , . . . , un ] → true, and
we can conclude that η ∈ SolF D (labeling [. . .] [X], X ∈ [u1 , . . . , un ]). Therefore,
σ).
η ∈ SolF D (labeling [. . .] [X], X ∈ [u1 , . . . , un ], S
The remaining conditions of the theorem for this rule trivially hold because of
σ satisfies the rethe initial hypothesis labeling [. . .] [X], X ∈ [u1 , . . . , un ], S
quirements of Definition 2, and because of the conditions of the rule X ∈
/ χ. The
last rule for labeling follows a trivial reasoning because SolF D (labeling [. . .] [u]) =
V al(F D) if u ∈ Z. According to Table 1, indomainF D uη → ⊤ for all η ∈ V al(F D).
σ) = SolF D (labeling [. . .] [u]) ∩ SolF D (S
Therefore, SolF D (labeling [. . .] [u], S
σ) = V al(F D) ∩ SolF D (S
σ) = SolF D (S
σ). The remaining conditions of
the theorem are also trivial by initial hypothesis.
Failure Rules
Finally, we suppose any arbitrary failure rule such that S
σ ⊢⊢χ f ail and we
σ) = ∅. First, we note that any failure rule must have the
prove that SolF D (S
σ ⊢⊢χ f ail with conditions such that SolF D (S1 )
following syntactic form: S1 , S2
= ∅. For example, consider the failure rule associated to Table 4: u ≤ u′ , S
σ
′
Z ′
′
⊢⊢χ f ail with u, u ∈ Z and u > u . Clearly, SolF D (u ≤ u ) = ∅. In this situation,
SolF D (S1 , S2
σ) = SolF D (S1 ) ∩ SolF D (S2
σ) = ∅ ∩ SolF D (S2
σ) = ∅. 

