1

arXiv:0807.3451v3 [cs.PL] 10 Jan 2009

A Non-Termination Criterion for Binary
Constraint Logic Programs
ÉTIENNE PAYET and FRED MESNARD
IREMIA - LIM - université de la Réunion, France
(e-mail: {epayet,fred}@univ-reunion.fr)

Note: this paper has been accepted for publication in Theory and Practice of Logic
Programming (TPLP).
Abstract
On the one hand, termination analysis of logic programs is now a fairly established research
topic within the logic programming community. On the other hand, non-termination analysis seems to remain a much less attractive subject. If we divide this line of research into
two kinds of approaches: dynamic versus static analysis, this paper belongs to the latter.
It proposes a criterion for detecting non-terminating atomic queries with respect to binary
CLP rules, which strictly generalizes our previous works on this subject. We give a generic
operational definition and an implemented logical form of this criterion. Then we show
that the logical form is correct and complete with respect to the operational definition.
KEYWORDS: constraints, constraint logic programming, non-termination.

1 Introduction
On the one hand, termination analysis of logic programs is a fairly established research topic within the logic programming community, see the following surveys:
(De Schreye and Decorte 1994; Mesnard and Ruggieri 2003). Various termination
analyzers are now available via web interfaces and we note that the Mercury compiler, designed with industrial goals in mind, includes a termination analysis (described in (Speirs et al. 1997)) available as a compiler option.
On the other hand, non-termination analysis seems to remain a much less attractive subject. We can divide this line of research into two kinds of approaches:
dynamic versus static analysis. In the former one, (Bol et al. 1991) sets up some
solid foundations for loop checking, while (Shen et al. 2001) presents some recent
work. The main idea is to prune infinite derivations at runtime (some finite derivations may also be pruned by some loop checkers). In the latter approach, which
includes the work we present in this article, one tries to compute at compile-time
queries which admit at least one infinite derivation. One of the earliest works on the
static approach is described in (De Schreye et al. 1989) where the authors present
an algorithm for detecting non-terminating atomic queries with respect to (w.r.t.)
a binary clause of the form p(s̃) ← p(t̃). The condition is described in terms of rational trees, while we aim at generalizing non-termination analysis for the generic

2

É. Payet and F. Mesnard

CLP(X) framework. Non-termination has also been studied in other paradigms,
such as Term Rewrite Systems (Waldmann 2004; Giesl et al. 2005; Zantema 2005;
Waldmann 2007; Zankl and Middeldorp 2007; Payet 2008); the technique described
in (Payet 2008) is close to that of this paper. In (Gupta et al. 2008), non-termination
of C programs is considered and in (Godefroid et al. 2005; Sen et al. 2005) some
techniques are provided that detect crashes, assertion violation and non-termination
in C programs.
Our analysis shares with the work on termination analysis which is presented
in (Codish and Taboch 1999) a key component: the binary unfoldings of a logic
program (Gabbrielli and Giacobazzi 1994), which transform a finite set of definite
clauses into a possibly infinite set of facts and binary definite clauses. Some termination analyses compute a finite over-approximation of the binary unfolding semantics, over a constraint domain such as CLP(N ). In contrast, the non-termination
analysis we have presented in (Payet and Mesnard 2006) starts from a finite subset
BP of the binary unfoldings of the concrete program P ; of course, a larger subset
may increase the precision of the analysis ((Payet and Mesnard 2006) provides some
experimental evidence). This non-termination analysis first detects patterns of nonterminating atomic queries from the binary recursive clauses and then propagates
this non-termination information to compute classes of atomic queries for which we
have a finite proof that there exists at least one infinite derivation w.r.t. BP . The
equivalence between the termination of a logic program and that of its binary unfoldings (Codish and Taboch 1999) is a corner stone of the analysis; it allows us to
conclude that any atomic query belonging to the identified above classes admits an
infinite left derivation w.r.t. P . The basic idea in (Payet and Mesnard 2006) relies
on checking, for each recursive clause in BP , that the body is more general than
the head; if this test succeeds, we can conclude that the head is an atomic query
which has an infinite derivation w.r.t. BP . A key observation consists in considering neutral argument positions i.e. argument positions of the predicate symbols
defined in P that do not have any effect on the derivation process when they are
filled with a term that satisfies a given condition. The subsumption test presented
in (Payet and Mesnard 2006) only considers the arguments that are in the nonneutral positions and checks that the arguments in the neutral positions satisfy
their associated condition. This extension of the classical subsumption test considerably increases the power of the approach in the sense that it allows one to
compute more classes of non-terminating atomic queries.
The initial motivation in (Payet and Mesnard 2006) was to complement termination analysis with non-termination inside the logic programming paradigm in
order to detect optimal termination conditions expressed in a language describing classes of queries. Although we obtained interesting experimental results, the
overall approach remains quite syntactic, with an ad hoc flavor and tight links to
some basic logic programming machinery such as the unification algorithm. So in
the present paper our aim is to generalize the approach to the constraint logic programming (CLP) setting and the main contribution of this work consists in a strict
generalization of the logical criterion defined in (Payet and Mesnard 2004).
The paper is organized as follows. In Section 2 we give some preliminary def-

Non-Termination of CLP

3

initions and in Section 3 we recall in CLP terms the subsumption test to detect
looping queries. In Section 4 we introduce the neutral argument positions; the operational definition we give (Section 4.3) is useless in practice, hence we propose
a sufficient condition for neutrality, expressed as a logical formula related to the
constraint binary clause under consideration (Section 4.4). For some constraint domains, we show that the condition is also necessary (Section 4.5). Depending on the
constraint theory, the validity of such a condition can be automatically decided. In
Section 4.6, we describe an algorithm that uses the logical formula of the sufficient
condition to compute neutral argument positions. Finally, in Section 5 we describe
our prototype and we conclude in Section 6. The detailed proofs of the results can
be found in the appendices at the end of the paper.
Notice that our approach consists in computing a finite subset BP of the binary
unfoldings of the program of interest and then in inferring non-terminating queries
using BP only; hence, we deliberately choose to restrict the analysis to binary CLP
rules and atomic CLP queries as the result we obtain can be lifted to full CLP.
2 Preliminaries
For any non-negative integer n, [1, n] denotes the set {1, . . . , n}. If n = 0, then
[1, n] = ∅. We recall some basic definitions about CLP, see (Jaffar et al. 1998) for
more details. From now on, we fix an infinite countable set V of variables together
with a signature Σ, i.e. a pair hF, Πi where F is a set of function symbols and Π
is a set of predicate symbols with F ∩ Π = ∅ and (F ∪ Π) ∩ V = ∅. Every element
of F ∪ Π has an arity which is the number of its arguments. We write f /n ∈ F
(resp. p/n ∈ Π) to denote that f (resp. p) is an element of F (resp. Π) whose arity
is n ≥ 0. A constant symbol is an element of F whose arity is 0.
A term is a variable, a constant symbol or an object of the form f (t1 , . . . , tn )
where f /n ∈ F , n ≥ 1 and t1 , . . . , tn are terms. An atomic proposition is an element
p/0 of Π or an object of the form p(t1 , . . . , tn ) where p/n ∈ Π, n ≥ 1 and t1 , . . . , tn
are terms. A first-order formula on Σ is built from atomic propositions in the usual
way using the logical connectives ∧, ∨, ¬, →, ↔ and the quantifiers ∃ and ∀. If φ is a
formula and W := {X1 , . . . , Xn } is a set of variables, then ∃W φ (resp. ∀W φ) denotes
the formula ∃X1 . . . ∃Xn φ (resp. ∀X1 . . . ∀Xn φ). We let ∃φ (resp. ∀φ) denote the
existential (resp. universal) closure of φ.
We fix a Σ-structure D, i.e. a pair hD, [·]i which is an interpretation of the
symbols in Σ. The set D is called the domain of D and [·] maps each f /0 ∈ F to
an element of D and each f /n ∈ F with n ≥ 1 to a function [f ] : Dn → D; each
p/0 ∈ Π to an element of {0, 1} and each p/n ∈ Π with n ≥ 1 to a boolean function
[p] : Dn → {0, 1}. We assume that the predicate symbol = is in Σ and is interpreted
as identity in D. A valuation is a mapping from V to D. Each valuation v extends
by morphism to terms. As usual, a valuation v induces a valuation [·]v of terms to
D and of formulas to {0, 1}.
Given a formula φ and a valuation v, we write D |=v φ when [φ]v = 1. We write
D |= φ when D |=v φ for all valuation v. Notice that D |= ∀φ if and only if D |= φ,
that D |= ∃φ if and only if there exists a valuation v such that D |=v φ, and that

4

É. Payet and F. Mesnard

D |= ¬∃φ if and only if D |= ¬φ. We say that a formula φ is satisfiable (resp.
unsatisfiable) in D when D |= ∃φ (resp. D |= ¬φ).
We fix a set L of admitted formulas, the elements of which are called constraints.
We suppose that L is closed under variable renaming, existential quantification and
conjunction and that it contains all the atomic propositions, the always satisfiable
formula true and the unsatisfiable formula false. We assume that there is a computable function solv which maps each c ∈ L to one of true or false indicating
whether c is satisfiable or unsatisfiable in D. We call solv the constraint solver.
Example 2.1 (Qlin )
The constraint domain Qlin has <, ≤, =, ≥, > as predicate symbols, +, −, ∗,
/ as function symbols and sequences of digits as constant symbols. Only linear
constraints are admitted. The domain of computation is the structure with the
set of rationals, denoted by Q, as domain and where the predicate symbols and
the function symbols are interpreted as the usual relations and functions over the
rationals. A constraint solver for Qlin always returning either true or false is
described in (Refalo and Hentenryck 1996).
Sequences of distinct variables are denoted by X̃, Ỹ or Z̃ and are sometimes
considered as sets of variables: we may write ∀X̃ , ∃X̃ or X̃ ∪ Ỹ . Sequences of (not
necessarily distinct) terms are denoted by s̃, t̃ or ũ. Given two sequences of n terms
s̃ := (s1 , . . . , sn ) and t̃ := (t1 , . . . , tn ), we write s̃ = t̃ either to denote the constraint
s1 = t1 ∧ · · · ∧ sn = tn or as a shorthand for “s1 = t1 and . . . and sn = tn ”. Given
a valuation v, we write v(s̃) to denote the sequence (v(s1 ), . . . , v(sn )) and [s̃]v to
denote the sequence ([s1 ]v , . . . , [sn ]v ).
The signature in which all programs and queries under consideration are included
is ΣL := hF, Π ∪ Π′ i where Π′ is the set of predicate symbols that can be defined
in programs, with Π ∩ Π′ = ∅.
An atom has the form p(t1 , . . . , tn ) where p/n ∈ Π′ and t1 , . . . , tn are terms. A
program is a finite set of clauses. A clause has the form H ← c ⋄ B where H and
B are atoms and c is a finite conjunction of atomic propositions such that D |= ∃c.
A query has the form hA | di where A is an atom and d is a finite conjunction
of atomic propositions. Given an atom A := p(t̃), we write rel (A) to denote the
predicate symbol p. Given a query Q := hA | di, we write rel (Q) to denote the
predicate symbol rel (A). The set of variables occurring in some syntactic objects
O1 , . . . , On is denoted Var (O1 , . . . , On ).
We consider the following operational semantics given in terms of derivations
from queries to queries. Let hp(ũ) | di be a query and p(s̃) ← c ⋄ q(t̃) be a fresh copy
of a clause r. When solv (s̃ = ũ ∧ c ∧ d) = true then
hp(ũ) | di =⇒hq(t̃) | s̃ = ũ ∧ c ∧ di
r

is a derivation step of hp(ũ) | di w.r.t. r with p(s̃) ← c ⋄ q(t̃) as its input clause. We
+
write Q =⇒ Q′ to summarize a finite number (> 0) of derivation steps from Q to
P

Q′ where each input clause is a variant of a clause from program P . Let Q0 be a
query. A sequence of derivation steps Q0 =⇒ Q1 =⇒ · · · of maximal length is called
r1

r2

Non-Termination of CLP

5

a derivation of P ∪ {Q0 } when r1 , r2 , . . . are clauses from P and the standardization
apart condition holds, i.e. each input clause used is variable disjoint from the initial
query Q0 and from the input clauses used at earlier steps. We say Q0 loops w.r.t.
P when there exists an infinite derivation of P ∪ {Q0 }.
3 Loop Inference with Constraints
In the logic programming framework, the subsumption test provides a simple way
to infer looping queries: if, in a logic program P , there is a clause p(s̃) ← p(t̃)
such that p(t̃) is more general than p(s̃), then the query p(s̃) loops w.r.t. P . In this
section, we extend this result to the constraint logic programming framework.
3.1 A “More General Than” Relation
A query can be viewed as a finite description of a possibly infinite set of atoms, the
arguments of which are values from D.
Example 3.1
In the constraint domain Qlin , the query Q := hp(X, Y ) | Y ≤ X + 2i describes the
set of atoms p(x, y) where x and y are rational numbers and X and Y can be
made equal to x and y respectively while the constraint Y ≤ X + 2 is satisfied. For
instance, p(0, 2) is an element of the set described by Q.
In order to capture this intuition, we introduce the following definition.
Definition 3.2 (Set Described by a Query)
The set of atoms that is described by a query Q := hp(t̃) | di is denoted by Set(Q)
and is defined as: Set (Q) = {p([t̃]v ) | D |=v d}.
Clearly, Set (hp(t̃) | di) = ∅ if and only if d is unsatisfiable in D. Moreover, two
variants describe the same set:
Lemma 3.3
Let Q and Q′ be two queries such that Q′ is a variant of Q. Then, Set (Q) = Set(Q′ ).
Notice that the operational semantics we introduced above can be expressed using
sets described by queries:
Lemma 3.4
Let Q be a query and r := H ← c ⋄ B be a clause. There exists a derivation step of
Q w.r.t. r if and only if Set(Q) ∩ Set(hH | ci) 6= ∅.
The “more general than” relation we consider is defined as follows:
Definition 3.5 (More General )
We say that a query Q1 is more general than a query Q when Set(Q) ⊆ Set(Q1 ).
Example 3.6
In Qlin , the query Q1 := hp(X, Y ) | Y ≤ X + 3i is more general than the query
Q := hp(X, Y ) | Y ≤ X + 2i. However, Q is not more general than Q1 ; for instance,
p(0, 3) ∈ Set (Q1 ) but p(0, 3) 6∈ Set(Q).

6

É. Payet and F. Mesnard
3.2 Loop Inference

Suppose we have a derivation step Q =⇒ Q1 where r := H ← c ⋄ B. Then, by
r

Lemma 3.4, Set(Q) ∩ Set(hH | ci) 6= ∅. Hence, if Q′ is a query that is more general
than Q, as Set(Q) ⊆ Set (Q′ ), we have Set(Q′ )∩Set (hH | ci) 6= ∅. So, by Lemma 3.4,
there exists a query Q′1 such that Q′ =⇒ Q′1 . The following lifting result says that,
r

moreover, Q′1 is more general than Q1 .

Theorem 3.7 (Lifting)
Consider a derivation step Q =⇒ Q1 and a query Q′ that is more general than Q.
r

Then, there exists a derivation step Q′ =⇒ Q′1 where Q′1 is more general than Q1 .
r

From this theorem, we derive two corollaries that can be used to infer looping
queries just from the text of a program.
Corollary 3.8
Let r := H ← c ⋄ B be a clause. If hB | ci is more general than hH | ci then hH | ci
loops w.r.t. {r}.
The intuition of Corollary 3.8 is that we have hH | ci =⇒ Q1 where Q1 is a variant of
r

hB | ci; hence, Q1 is more general than hH | ci; so, by the Lifting Theorem 3.7, there
exists a derivation step Q1 =⇒ Q2 where Q2 is more general than Q1 ; by repeatedly
r

using this reasonning, one can build an infinite derivation of {r} ∪ {hH | ci}.
Corollary 3.9
Let r := H ← c ⋄ B be a clause from a program P . If hB | ci loops w.r.t. P then
hH | ci loops w.r.t. P .
The intuition of Corollary 3.9 is that we have hH | ci =⇒ Q1 where Q1 is a variant of
r

hB | ci, which implies that Q1 is more general than hB | ci; as there exists an infinite
derivation ξ of P ∪ {hB | ci}, by successively applying the Lifting Theorem 3.7 to
each step of ξ one can construct an infinite derivation of P ∪ {Q1 }.
Example 3.10
Consider the following recursive clause r in Qlin :
p(N ) ← N ≥ 1 ∧ N = N1 + 1 ⋄ p(N1 )
The query Q1 := hp(N1 ) | N ≥ 1 ∧ N = N1 + 1i is more general than the query Q :=
hp(N ) | N ≥ 1 ∧ N = N1 + 1i (for instance, p(0) ∈ Set (Q1 ) but p(0) 6∈ Set(Q)). So,
by Corollary 3.8, Q loops w.r.t. {r}. Therefore, there exists an infinite derivation
ξ of {r} ∪ {Q}. Then, if Q′ is a query that is more general than Q, by successively
applying the Lifting Theorem 3.7 to each step of ξ, one can construct an infinite
derivation of {r} ∪ {Q′ }. So, Q′ also loops w.r.t. {r}.
4 Loop Inference Using Filters
The condition provided by Corollary 3.8 is rather weak because it fails at inferring
looping queries in some simple cases. This is illustrated by the following example.

Non-Termination of CLP

7

Example 4.1
Consider the following recursive clause r in Qlin :
p(N, T ) ← N ≥ 1 ∧ N = N1 + 1 ∧ T1 = 2 ∗ T ∧ T ≥ 1 ⋄ p(N1 , T1 )
Let c denote the constraint in r. The query hp(N, T ) | ci loops w.r.t. {r} because
only the first argument of p decreases in r and in this query it is unspecified.
But we cannot infer that hp(N, T ) | ci loops w.r.t. {r} from Corollary 3.8 as in r
hp(N1 , T1 ) | ci is not more general than hp(N, T ) | ci because of the second argument
of p: for instance, p(1, 1) ∈ Set(hp(N, T ) | ci) but p(1, 1) 6∈ Set(hp(N1 , T1 ) | ci).
In what follows, we extend the relation “is more general”. Instead of comparing
atoms in all positions using the “more general” relation, we distinguish some predicate argument positions for which we just require that a certain property must
hold, while for the other positions we use the “more general” relation as before.
Doing so, we aim at inferring more looping queries.
Example 4.2 (Example 4.1 continued )
Let us consider argument position 2 of predicate symbol p. In the clause r, the
projection of c on T is equivalent to T ≥ 1; this projection expresses the constraint
placed upon the second argument of p to get a derivation step with r. Notice that the
projection of c on T1 is equivalent to T1 ≥ 2, which implies T1 ≥ 1. Therefore, the
requirements on the head variable T propagates to the body variable T1 . Moreover,
the “piece” hp(N1 ) | ci of hp(N1 , T1 ) | ci is more general than the “piece” hp(N ) | ci
of hp(N, T ) | ci. Consequently, hp(N1 , T1 ) | ci is more general than hp(N, T ) | ci up
to the second argument of p which, in hp(N1 , T1 ) | ci, satisfies T1 ≥ 1, the condition
to get a derivation step with r. Hence, by an extended version of Corollary 3.8 we
could infer that hp(N, T ) | ci loops w.r.t. {r}.
4.1 Sets of Positions
A basic idea in Example 4.2 lies in identifying argument positions of predicate
symbols. Below, we introduce a formalism to do so.
Definition 4.3 (Set of Positions)
A set of positions, denoted by τ , is a function that maps each p/n ∈ Π′ to a subset
of [1, n].
Example 4.4
If we want to distinguish the second argument position of the predicate symbol p
defined in Example 4.1, we set τ := hp 7→ {2}i. If we do not want to distinguish
any argument position of p, we set τ ′ := hp 7→ ∅i.
Definition 4.5
Let τ be a set of positions. Then, τ is the set of positions defined as: for each
p/n ∈ Π′ , τ (p) = [1, n] \ τ (p).

8

É. Payet and F. Mesnard

Example 4.6
If we set τ := hp 7→ {2}i and τ ′ := hp 7→ ∅i where the arity of p is 2, then
τ = hp 7→ {1}i and τ ′ = hp 7→ {1, 2}i.
Using a set of positions τ , one can project syntactic objects:
Definition 4.7 (Projection)
Let τ be a set of positions.
• The projection of p ∈ Π′ on τ is the predicate symbol denoted by pτ . Its arity
is the number of elements of τ (p).
• Let p/n ∈ Π′ and t̃ := (t1 , . . . , tn ) be a sequence of n terms. The projection of
t̃ on τ (p), denoted by t̃τ (p) , is the sequence (ti1 , . . . , tim ) where {i1 , . . . , im } =
τ (p) and i1 < · · · < im .
• Let A := p(t̃) be an atom. The projection of A on τ , denoted by Aτ , is the
atom pτ (t̃τ (p) ).
• The projection of a query hA | di on τ , denoted by hA | diτ , is the query hAτ | di.
Example 4.8 (Example 4.4 continued )
The projection of the query hp(N, T ) | ci on τ (resp. τ ′ ) is the query hpτ (T ) | ci (resp.
the query hpτ ′ | ci).
Projection preserves inclusion and non-disjointness of sets described by queries:
Lemma 4.9 (Inclusion)
Let τ be a set of positions and Q and Q′ be two queries. If Set (Q) ⊆ Set(Q′ ) then
Set(Qτ ) ⊆ Set (Q′τ ).
Lemma 4.10 (Non-Disjointness)
Let τ be a set of positions and Q and Q′ be two queries. If Set (Q) ∩ Set(Q′ ) 6= ∅
then Set(Qτ ) ∩ Set(Q′τ ) 6= ∅.
4.2 Filters
A second idea in Example 4.2 consists in associating constraints with argument
positions (T ≥ 1 for position 2 in Example 4.2). We define a filter to be the combination of sets of positions with their associated constraint:
Definition 4.11 (Filter )
A filter, denoted by ∆, is a pair (τ, δ) where τ is a set of positions and δ is a function
that maps each p ∈ Π′ to a query of the form hpτ (t̃) | di where D |= ∃d.
Example 4.12
Consider τ := hp 7→ {2}i and τ ′ := hp 7→ ∅i. Let δ := h p 7→ hpτ (B) | B ≥ 1i i and
δ ′ := h p 7→ hpτ ′ | truei i. Then, ∆ := (τ, δ) and ∆′ := (τ ′ , δ ′ ) are filters.
Note that δ(p) is given in the form of a query hpτ (t̃) | di, instead of just a constraint
d, because we need to indicate that the entry points of d are the terms in t̃. Indeed,
the function δ is used to “filter” queries: we say that a query Q satisfies ∆ when the
set of atoms described by Qτ , the projection of Q on the positions τ , is included in
the set of atoms described by δ(rel (Q)), the query defined for Q’s predicate symbol
by ∆. More formally:

Non-Termination of CLP

9

Definition 4.13 (Satisfies)
Let ∆ := (τ, δ) be a filter and Q be a query. Let p := rel (Q). We say that Q satisfies
∆ when Set (Qτ ) ⊆ Set(δ(p)).
Now we come to the extension of the relation “more general than”. Intuitively,
hp(t˜′ ) | d′ i is ∆-more general than hp(t̃) | di if the “more general than” relation holds
for the elements of t̃ and t˜′ whose position is not in τ while the elements of t˜′ whose
position is in τ satisfy δ. More formally:
Definition 4.14 (∆-More General )
Let ∆ := (τ, δ) be a filter and Q and Q′ be two queries. We say that Q′ is ∆-more
general than Q when Q′τ is more general than Qτ and Q′ satisfies ∆.
Example 4.15
Consider the constraint c in the clause
p(N, T ) ← N ≥ 1 ∧ N = N1 + 1 ∧ T1 = 2 ∗ T ∧ T ≥ 1 ⋄ p(N1 , T1 )
of Example 4.1. The query Q1 := hp(N1 , T1 ) | ci is ∆-more general
 than Q :=
hp(N, T ) | ci for the filter ∆ := p 7→ {2} , p 7→ hpτ (B) | B ≥ 1i . However, Q1
is not ∆′ -more general than Q for the filter ∆′ := p 7→ ∅ , p 7→ hpτ ′ | truei ;
indeed, τ ′ (p) = ∅ implies that being ∆′ -more general is equivalent to being more
general and, by Example 4.1, Q1 is not more general than Q.
Lemma 4.16 (Transitivity)
For any filter ∆, the “∆-more general than” relation is transitive.
Notice that for any filter ∆ := (τ, δ) and any query Q, we have that Qτ is more
general than itself (because the “more general than” relation is reflexive), but Q may
not satisfy ∆. Hence, the “∆-more general than” relation is not always reflexive.
Example 4.17
Consider the constraint domain Qlin . Let p/1 ∈ Π′ and ∆ := (τ, δ) be the filter defined by τ := hp 7→ {1}i and δ := h p 7→ hpτ (X) | X ≥ 1i i. The query
Q := hp(0) | truei is not ∆-more general than itself because Set (Qτ ) = {pτ (0)} 6⊆
{pτ (x) | x is a rational and x ≥ 1} = Set(δ(p)). Hence, Q does not satisfy ∆.
The fact that reflexivity does not always hold is an expected property. Indeed,
suppose that a filter ∆ := (τ, δ) induces a “∆-more general than” relation that is reflexive. Then for any queries Q and Q′ , we have that Q′ is ∆-more general than Q if
and only if Qτ′ is more general than Qτ (because, as Q′ is ∆-more general than itself,
Q′ necessarily satisfies ∆). Hence, δ is useless in the sense that it “does not filter anything”. Filters equipped with such a δ were introduced in (Payet and Mesnard 2004)
where for any predicate symbol p, δ(p) has the form hpτ (X̃) | truei, where X̃ is a
sequence of distinct variables. In this paper, we aim at generalizing the approach
of (Payet and Mesnard 2004). Hence, we also consider functions δ that really filter
queries.

10

É. Payet and F. Mesnard
4.3 DN Filters: an Operational Definition

Let us now introduce a special kind of filters that we call “derivation neutral”. The
name “derivation neutral” stems from the fact that if in a derivation of a query Q,
we replace Q by a ∆-more general Q′ , then we get a “similar” derivation.
Definition 4.18 (Derivation Neutral )
Let r be a clause and ∆ be a filter. We say that ∆ is DN for r when for each
derivation step Q =⇒ Q1 , the query Q1 satisfies ∆ and for each query Q′ that is ∆r

more general than Q, there exists a derivation step Q′ =⇒ Q′1 where Q′1 is ∆-more
r
general than Q1 . This definition is extended to programs: ∆ is DN for P when it
is DN for each clause of P .
Derivation neutral filters lead to the following extended version of Corollary 3.8
(to get Corollary 3.8, take ∆ := (τ, δ) with τ (p) = ∅ for any p).
Theorem 4.19
Let r := H ← c ⋄ B be a clause. Let ∆ be a filter that is DN for r. If hB | ci is
∆-more general than hH | ci then hH | ci loops w.r.t. {r}.
Example 4.20
If the filter ∆ of Example 4.15 is DN for the clause r = p(N, T ) ← c ⋄ p(N1 , T1 )
of Example 4.1, then we can deduce that hp(N, T ) | ci loops w.r.t. {r} because
hp(N1 , T1 ) | ci is ∆-more general than hp(N, T ) | ci (see Example 4.15).
Computing a derivation neutral filter from the text of a program is not straightforward if we use the above definition. Section 4.4 presents a logical characterization
that we use in Section 4.6 to compute a filter that is DN for a given recursive clause.
4.4 A Logical Characterization of DN Filters
From now on, we suppose, without loss of generality, that a clause has the form
p(X̃) ← c ⋄ q(Ỹ ) where X̃ and Ỹ are disjoint sequences of distinct variables. Hence,
c is the conjunction of all the constraints, including unifications. We distinguish the
following set of variables that appear inside such a clause.
Definition 4.21
The set of local variables of a clause r := p(X̃) ← c ⋄ q(Ỹ ) is local vars(r) :=
Var(c) \ (X̃ ∪ Ỹ ).
In this section, we aim at characterizing DN filters in a logical way. To this end,
we define:
Definition 4.22 (sat )
Let Q := hp(t̃) | di be a query and s̃ be a sequence of terms of the same length
as t̃. Then, sat(s̃, Q) denotes a formula of the form ∃Var (Q′ ) (s̃ = t̃′ ∧ d′ ) where
Q′ := hp(t̃′ ) | d′ i is a variant of Q and variable disjoint with s̃.
Intuitively, sat (s̃, Q) holds when the terms in the sequence s̃ satisfy the constraint
d, the entry points of which are the terms in t̃. Clearly, the satisfiability of sat(s̃, Q)
does not depend on the choice of the variant of Q. The set that is described by a
query can then be characterized as follows:

11

Non-Termination of CLP

Lemma 4.23
Let Q be a query and p := rel (Q). Let ũ be a sequence of arity(p) terms and v be
a valuation. Then, p([ũ]v ) ∈ Set(Q) if and only if D |=v sat (ũ, Q).
Now we give a logical definition of derivation neutrality. As we will see later,
under certain circumstances, this definition is equivalent to the operational one we
gave above.
Definition 4.24 (Logical Derivation Neutral )
We say that a filter ∆ := (τ, δ) is DNlog for a clause r := p(X̃) ← c ⋄ q(Ỹ ) when


D |= c → ∀X̃τ (p) sat(X̃τ (p) , δ(p)) → ∃Y c and D |= c → sat (Ỹτ (q) , δ(q))
where Y = Ỹτ (q) ∪ local vars(r).
Example 4.25
In Qlin , the filter

p 7→ {2} , p 7→ hpτ (B) | B ≥ 1i



is DNlog for the clause

p(N, T ) ← N ≥ 1 ∧ N = N1 + 1 ∧ T1 = 2 ∗ T ∧ T ≥ 1 ⋄ p(N1 , T1 )
of Example 4.1. Indeed, X̃τ (p) = {T }, Ỹτ (q) = {T1 } and local vars(r) = {}. So, if
we let c denote the constraint in this clause, the formulas of Definition 4.24 turn
into


D |= c → ∀T T ≥ 1 → ∃T1 c and D |= c → T1 ≥ 1
which are true.
The first formula in Definition 4.24 has the following meaning. If one holds a
solution for constraint c, then, changing the value given to the variables of X̃
distinguished by τ to some value satisfying δ(p), there exists a value for the local
variables and the variables of Ỹ distinguished by τ such that c is still satisfied. This
formula expresses the fact that DNlog arguments (i.e. those distinguished by τ ) do
not interact in c with the other arguments. Intuitively, two variables X1 and X2
do not interact in a constraint c when the set of values assigned to (X1 , X2 ) by
all the solutions of c results from the exhaustive combination of the set of values
assigned to X1 by all the solutions of c and the set of values assigned to X2 by all
the solutions of c; more formaly, when



(v(X1 ), v(X2 )) | D |=v c = v(X1 ) | D |=v c × v(X2 ) | D |=v c .

Example 4.26
• In Example 4.25 above, the set of values assigned to (N, T ) by all the solutions
of c is {(a, b) | a ≥ 1, b ≥ 1}. We have {(a, b) | a ≥ 1, b ≥ 1} = {a | a ≥
1} × {b | b ≥ 1} where {a | a ≥ 1} is the set of values assigned to N by all
the solutions of c and {b | b ≥ 1} is the set of values assigned to T by all the
solutions of c. Hence, N and T do not interact.
• Now consider c = (X ≥ Z ∧ Z ≥ Y ). The set of values assigned to (X, Y ) by
all the solutions of c is {(a, b) | a ≥ b} and the set of values assigned to X
and to Y by all the solutions of c is Q. As {(a, b) | a ≥ b} =
6 Q × Q, we have
that X and Y do interact.

12

É. Payet and F. Mesnard

The second formula in Definition 4.24 means that any solution of c assigns to
the variables of Ỹ distinguished by τ a value that satisfies δ(q). This corresponds
to the intuition that neutral argument positions are sorts of “pipes” where one can
place any term satisfying δ with no effect on the derivation process.
The logical definition of derivation neutrality implies the operational one:
Theorem 4.27
Let r be a clause and ∆ be a filter. If ∆ is DNlog for r then ∆ is DN for r.
DNlog in Definition 4.24 consists of two formulas, say DNlog1 and DNlog2, where
DNlog2 requires Ỹτ (q) to always satisfy δ(q). One may think of a (perhaps more
natural) requirement, say DNlog12, resulting from “merging” DNlog1 and DNlog2:


D |= c → ∀X̃τ (p) sat(X̃τ (p) , δ(p)) → ∃Y (c ∧ sat (Ỹτ (q) , δ(q))) .
The point is that a filter satisfying DNlog12 is not necessarily DN (i.e. Theorem 4.27
does not hold for DNlog12). For instance, consider in Qlin the clause
r := p(X) ← X ≤ 3 ∧ 2 ≤ Y ⋄ p(Y )
and the filter ∆ := (τ, δ) with τ (p) = {1} and δ(p) = hpτ (X) | X ≤ 3i. Then,
DNlog2 i.e.
D |= c → sat(Ỹτ (q) , δ(q))
does not hold: we have Ỹτ (p) = {Y } and any valuation v with v(X) = 1 and
v(Y ) = 4 is a solution of the constraint c in r i.e. D |=v c; but, as 3 < v(Y ), we have
D 6|=v Y ≤ 3 i.e. D 6|=v sat (Ỹτ (p) , δ(p)); therefore, D 6|=v c → sat (Ỹτ (p) , δ(p)). Hence,
∆ is not DNlog for r. In the next section (see Theorem 4.29 and Example 4.30)
we prove that DNlog in Qlin is equivalent to DN. Therefore, ∆ is not DN for r.
On the other hand, DNlog12 holds as in this example it is equivalent to (we have
X̃τ (p) = {X} and Y = {Y }):


D |= c → ∀X X ≤ 3 → ∃Y (c ∧ Y ≤ 3) .
4.5 When DN Filters Are Also DNlog
DN filters are not always DNlog as illustrated by the following example.
Example 4.28
Suppose that Σ = {0, =, ≥} and D = DQlin . Consider
r := p(X1 , X2 ) ← X2 ≥ X1 ∧ X1 ≥ 0 ∧ Y1 = X1 ∧ Y2 = X2 ⋄ p(Y1 , Y2 ) .
Let c denote the constraint in r. Consider also a filter ∆ := (τ, δ) where τ (p) = {1}
and δ(p) = hpτ (X) | X ≥ 0i. Notice that given the form of Σ, one cannot write a
constraint that has only one solution different from 0; more precisely, for any terms
t1 and t2 and any constraint d 6= false:
p(0, 0) ∈ Set (hp(t1 , t2 ) | di) .
Whatever Q, if there is a derivation step Q =⇒ Q1 :
r

(1)

Non-Termination of CLP

13

• the query Q1 satisfies ∆ because c implies that Y1 ≥ 0,
• for any Q′ that is ∆-more general than Q, Set(hp(X1 , X2 ) | ci) ∩ Set (Q′ ) 6= ∅
because by (1) p(0, 0) ∈ Set (hp(X1 , X2 ) | ci) ∩ Set(Q′ ); hence, there exists a
derivation step Q′ =⇒ Q′1 . Notice that Q′1τ is more general than Q1 τ because
r

Qτ′ is more general than Qτ and c demands that Y2 = X2 ; moreover, Q′1
satisfies ∆ because c implies that Y1 ≥ 0; therefore, Q′1 is ∆-more general
than Q1 .
Consequently, ∆ is DN for r. However, ∆ is not DNlog for r because the first formula
of Definition 4.24 does not hold. Indeed, as X̃τ (p) = X1 , Ỹτ (p) = Y1 and Y = {Y1 },
this formula is equivalent to D |= c → ∀X1 [X1 ≥ 0 → ∃Y1 c]. Let v be a valuation
such that v(X1 ) = v(Y1 ) = v(X2 ) = v(Y2 ) = 0; then, D |=v c. Let v1 be a valuation
with v1 (X1 ) = 1 and v1 matches v on the other variables; then, D |=v1 X1 ≥ 0;
however, D |=v1 ∃Y1 c does not hold because c contains the constraint X2 ≥ X1
with v1 (X2 ) = 0 and v1 (X1 ) = 1 and it is not possible to change the value that v1
assigns to Y1 so that v1 (X2 ) ≥ v1 (X1 ). Therefore, D |=v c → ∀X1 [X1 ≥ 0 → ∃Y1 c]
does not hold.
The point in Example 4.28 is that the problematic values (for DNlog-ness) cannot
be captured by a query, hence they do not prevent
 ∆ from being DN. More precisely, we have p v(X1 ), v(X2 ) = p v(Y1 ), v(Y2 ) = p(0, 0) and the atom p(0, 0) is
captured by the query
hp(0, 0) | truei, i.e. Set (hp(0, 0) | truei) = {p(0, 0)}. However,

p v1 (X1 ), v1 (X2 ) = p(1, 0) and there exists no query Q with Set(Q) = {p(1, 0)}. If
we had considered r in the constraint domain Qlin then ∆ would not have been DN
as there exists Q1 such that hp(0, 0) | truei =⇒ Q1 , the query hp(1, 0) | truei is wellr

formed in Qlin and is ∆-more general than hp(0, 0) | truei1 , but there exists no query
Q′1 such that hp(1, 0) | truei =⇒ Q′1 . Hence, an idea for matching DN with DNlog
r

consists in considering domains where every sequence of values can be captured by
a query:
Theorem 4.29
If, for all atoms A whose arguments are elements of D, there exists a query Q such
that Set (Q) = {A}, then every filter that is DN for a clause r is also DNlog for r.
The intuition of the proof of Theorem 4.29 consists in mapping some sequences of
values (induced by the considered valuations) to queries that capture them and in
using the DN property to prove that DNlog-ness holds. More precisely, let r :=
p(X̃) ← c ⋄ q(Ỹ ) and ∆ := (τ, δ) be a filter that is DN for r. First, we have to prove
that


D |= c → ∀X̃τ (p) sat (X̃τ (p) , δ(p)) → ∃Y c .
Let v be a valuation such that D |=v c and v ′ be a valuation such that v ′ (V ) = v(V )
for all variable V 6∈ X̃τ (p) and D |=v′ sat (X̃τ (p) , δ(p)). Then, there exists a query
Q such that Set(Q) = {p([X̃]v )} and a query Q′ such that Set (Q′ ) = {p([X̃]v′ )}.
1

because hp(1, 0) | trueiτ = hpτ (0) | truei = hp(0, 0) | trueiτ and hp(1, 0) | trueiτ = hpτ (1) | truei
with Set(hpτ (1) | truei) = {pτ (1)} ⊆ Set(δ(p))

14

É. Payet and F. Mesnard

Intuitively, as D |=v c, there exists a derivation step Q =⇒ Q1 ; moreover, as v ′
r

matches with v on X̃τ (p) and as the sequence of values that v ′ assignes to X̃τ (p)
satisfies ∆, then Q′ is ∆-more general than Q. Therefore, as ∆ is DN for r, there
exists a query Q′1 such that Q′ =⇒ Q′1 and Q′1 is ∆-more general than Q1 ; using
r

these properties of Q′ and Q′1 , one can deduce that D |=v′ ∃Y c, where Y = Ỹτ (q) ∪
local vars(r). We also have to prove that
D |= c → sat(Ỹτ (q) , δ(q)) .
This is a consequence of the fact that for any derivation step Q =⇒ Q1 , the query
r

Q1 satisfies ∆ (because ∆ is DN for r).
Example 4.30
For any rational number x, there exists a term t constructed from the constant
and function symbols of Qlin such that [t]v = x for any valuation v. Therefore, for
each atom p(ã) where ã is a sequence of rational numbers, there exists a query Q
in Qlin of the form hp(t̃) | truei, where the elements of t̃ are constructed from the
constant and function symbols of Qlin , which is such that Set (Q) = {p(ã)}. Hence,
by Theorem 4.29, in Qlin DN is equivalent to DNlog.
4.6 Computing Looping Queries
For any filter ∆ := (τ, δ) and any clause r := p(X̃) ← c ⋄ q(Ỹ ), we let


• DNlog1(∆, r) := c → ∀X̃τ (p) sat (X̃τ (p) , δ(p)) → ∃Y c

• DNlog2(∆, r) := c → sat (Ỹτ (q) , δ(q))
denote the formulas in Definition 4.24.
A solution to compute a DNlog filter for a clause r := p(X̃) ← c ⋄ p(Ỹ ) is to
consider the projection of c on the elements of X̃ that we wish to distinguish and
to check that DNlog1 and DNlog2 hold for r and the corresponding filter ∆proj .
Formally, for any set of variables W , the projection of c onto W is denoted by ∃W c
and is the formula ∃Var (c)\W c. If DNlog1 and DNlog2 hold for r and ∆proj , then
∆proj is DNlog for r, hence it is DN for r by Theorem 4.27; so we can try the test of
Theorem 4.19 to get a query that loops w.r.t. {r}. Hence the following algorithm:
An algorithm to compute a looping query
Input: a clause r := p(X̃) ← c ⋄ p(Ỹ ).
1. For each m ⊆ [1, arity(p)] do:
2.
Set τ (p) := m, δ(p) := hpτ (X̃τ (p) ) | ∃X̃τ (p) ci and ∆proj := (τ, δ).
3.
If DNlog1(∆proj , r) and DNlog2(∆proj , r) hold then
4.
If hp(Ỹ ) | ci is ∆proj -more general than hp(X̃) | ci then
5.
return hp(X̃) | ci, which is a looping query w.r.t. {r}.

15

Non-Termination of CLP

This algorithm always finds a DNlog filter. Indeed, for m = ∅, the corresponding
filter ∆proj = (τ, δ) is such that X̃τ (p) is the empty sequence, so δ(p) = hpτ | ∃∅ ci
where ∃∅ c is equivalent to ∃Var (c) c i.e. to true because in the definition of a clause
(see Section 2) we suppose that c is satisfiable; therefore, DNlog1(∆proj , r) and
DNlog2(∆proj , r) hold as they are equivalent to c → (true → ∃local vars(r ) c) and
c → true respectively.
Four tests are performed by the above algorithm for each subset m of [1, arity(p)]:
does DNlog1(∆proj , r) hold and does DNlog2(∆proj , r) hold and, if these tests succeed, is hp(Ỹ ) | ciτ more general than hp(X̃) | ciτ and does hp(Ỹ ) | ci satisfy ∆proj ?
Actually, only three tests are necessary as we have:
Lemma 4.31
Let r := p(X̃) ← c ⋄ p(Ỹ ) be a clause and ∆ := (τ, δ) be a filter. Then, we have
D |= DNlog2(∆, r) if and only if hp(Ỹ ) | ci satisfies ∆.
Example 4.32
Let us consider the constraint domain Qlin and the recursive clause
r := p(X1 , X2 ) ← X1 ≥ X2 ∧ Y1 = X1 + 1 ∧ Y2 = X2 ⋄ p(Y1 , Y2 ) .
Let c be the constraint in r. Consider m := {1, 2}. The projection of c onto
{X1 , X2 } is the constraint X1 ≥ X2 hence the algorithm sets τ (p) := {1, 2} and
δ(p) := hp(X1 , X2 ) | X1 ≥ X2 i and ∆proj := (τ, δ). The formulas DNlog1(∆proj , r)
and DNlog2(∆proj , r) hold as they are respectively equivalent to
c → ∀X1 ∀X2 (X1 ≥ X2 → ∃Y1 ∃Y2 c)

and

c → Y1 ≥ Y2 .

So, ∆proj is DNlog for r. Moreover, as hp(Y1 , Y2 ) | ci is ∆proj -more general than
hp(X1 , X2 ) | ci, by Theorem 4.19 the query hp(X1 , X2 ) | ci loops w.r.t. {r}. Notice
that by Definition 4.18, every query that is ∆proj -more general than hp(X1 , X2 ) | ci
also loops w.r.t. {r}. Generally speaking, for any predicate symbol q/n, a set of
positions m ⊆ [1, n] can be seen as a finite representation of the set of queries
of the form hq(t1 , . . . , tn ) | di where for each i ∈ m, d constrains ti to a ground
term. For instance, hp(0, 0) | truei loops w.r.t. {r} as it is ∆proj -more general than
hp(X1 , X2 ) | ci; this query belongs to the class described by the set of positions {1, 2}
for p; therefore we say that this class is non-terminating because there exists a query
in this class that loops. As hp(0, X) | truei, hp(X, 0) | truei and hp(X, Y ) | truei are
more general than hp(0, 0) | truei, by the Lifting Theorem 3.7 these queries also loop
w.r.t. {r}; consequently, the classes described by the sets of positions {1}, {2} and
{} for p are non-terminating too. So, for every set of positions m for p, the class of
queries described by m is non-terminating.
Example 4.33
In Qlin again, now consider the recursive clause (slightly different from that in
Example 4.32)
r := p(X1 , X2 ) ← X1 ≤ X2 ∧ Y1 = X1 + 1 ∧ Y2 = X2 ⋄ p(Y1 , Y2 )
Let c be the constraint in r and v be a valuation with v(X1 ) = v(X2 ) = v(Y2 ) = 0
and v(Y1 ) = 1; then we have D |=v c.

16

É. Payet and F. Mesnard
• Consider m := {1, 2}. The projection of c onto {X1 , X2 } is X1 ≤ X2 hence
the algorithm sets τ (p) := {1, 2}, δ(p) := hp(X1 , X2 ) | X1 ≤ X2 i and ∆proj :=
(τ, δ). The formula DNlog2(∆proj , r) is equivalent to c → Y1 ≤ Y2 . We have
D |=v c and D 6|=v Y1 ≤ Y2 so D 6|=v c → Y1 ≤ Y2 . Therefore, DNlog2(∆proj , r)
does not hold, so ∆proj is not DNlog for r.
• Consider m := {1}. The projection of c onto {X1 } is equivalent to the
constraint true. The algorithm sets τ (p) := {1}, δ(p) := hpτ (X1 ) | truei
and ∆proj := (τ, δ). The formula DNlog1(∆proj , r) is equivalent to c →
∀X1 (true → ∃Y1 c) i.e. c → ∀X1 ∃Y1 c. We have D |=v c; if we change the
value assigned to X1 to 1, then X1 ≤ X2 (a subformula of c) does not hold
anymore and one cannot find any value for Y1 such that X1 ≤ X2 holds
again; therefore, we have D 6|=v ∀X1 ∃Y1 c so D 6|=v c → ∀X1 ∃Y1 c. Hence,
DNlog1(∆proj , r) does not hold, so ∆proj is not DNlog for r.
• Consider m := {2}. The projection of c onto {X2 } is equivalent to the
constraint true. The algorithm sets τ (p) := {2}, δ(p) := hpτ (X2 ) | truei
and ∆proj := (τ, δ). The formula DNlog1(∆proj , r) is equivalent to c →
∀X2 (true → ∃Y2 c) i.e. c → ∀X2 ∃Y2 c. We have D |=v c; if we change the
value assigned to X2 to −1, then X1 ≤ X2 (a subformula of c) does not
hold anymore and one cannot find any value for Y2 such that X1 ≤ X2 holds
again; therefore, we have D 6|=v ∀X2 ∃Y2 c so D 6|=v c → ∀X2 ∃Y2 c. Hence,
DNlog1(∆proj , r) does not hold, so ∆proj is not DNlog for r.
• Consider m := ∅. The projection of c onto ∅ is equivalent to the constraint
true. The algorithm sets τ (p) := ∅, δ(p) := hpτ | truei and ∆proj := (τ, δ).
Both DNlog1(∆proj , r) and DNlog2(∆proj , r) hold as they are equivalent to
c → (true → c) and c → true respectively. So, ∆proj is DNlog for r. As
hp(Y1 , Y2 ) | ci is ∆proj -more general than hp(X1 , X2 ) | ci, by Theorem 4.19
hp(X1 , X2 ) | ci loops w.r.t. {r}. This query allows us to conclude that the
class described by the set of positions {} for p is non-terminating.

Consequently, we get no information about the classes described by the sets of
positions {1, 2}, {1} and {2}. Actually, the class described by {1, 2} is terminating,
i.e. every query in this class does not loop; indeed, intuitively, when the arguments
of p in a query Q are fixed to some values in Q, we have a finite derivation of
{r} ∪ {Q} because in r the first argument of p strictly increases until it becomes
greater than the second argument. Hence, the class described by {1, 2} will not
be inferred by our approach. On the other hand, the query hp(1, X) | truei loops
w.r.t. {r}, which implies that the class described by {1} is non-terminating. Our
approach fails to infer this result as X1 and X2 interact in c via X1 ≤ X2 , so
there is no DNlog filter for r that distinguishes position 1 and not position 2 of p.
Hence, as DN and DNlog match in this example, the DN approach fails2 to infer
2

Note that the situation of this example is different from that of Example 4.32. Here, we cannot
infer the non-termination of the class described by {1} from the non-termination of the class
described by {}. Indeed, every element in the class described by {1} has the form hp(t1 , t2 ) | di
where d constrains t1 to a ground term; on the other hand, every element in the class described
by {} has the form hp(t′1 , t′2 ) | d′ i where t′1 and t′2 are not constrained to some ground terms;
hence hp(t1 , t2 ) | di is not more general than hp(t′1 , t′2 ) | d′ i.

Non-Termination of CLP

17

the non-termination of {1}. So, a limitation of the DN approach when DN and
DNlog match is the following: when two arguments interact, if there is no DNlog
filter that distinguishes both their positions, then it is not possible to infer nontermination of a class of queries described by a set containing one of these positions
and not the other. Notice that non-interaction of arguments is expressed by DNlog
and not necessarily by DN; when DNlog and DN do not match (see Theorem 4.29),
there are situations where DN arguments can interact with non-DN arguments. In
Example 4.28, the arguments of p at positions 1 and 2 interact via X2 ≥ X1 ; the
filter that we give in this example distinguishes position 1 but not position 2 of p
and it is DN for r.
5 An Implementation
We have implemented the analysis in SWI-Prolog (Wielemaker 2003) for CLP(Qlin ).
The prototype3 takes a recursive binary rule p(X̃) ← c ⋄ p(Ỹ ) as input and tries
to find a filter with the projection of the constraint c of the considered rule onto
its head variables X̃. For each possible set of positions, it computes the four logical
formulas corresponding to Definition 4.14 and Definition 4.24. As the number of
such sets is exponential w.r.t. the arity of the predicate p, our analysis is at least
exponential. These formulas are evaluated by a decision procedure for arbitrary
logical formulas over hQ; {0, 1}; {+}; {=, <}i. If they are true (note that Lemma
4.31 shows that some tests are redundant), the analyzer prints the corresponding
filter and computes a concrete looping query.
So the analyzer implements Theorem 4.19 with the help of Theorem 4.27. We
point out that the analysis can be automated for any constraint domain the theory
of which is decidable, e.g. logic programming with finite trees and logic programming with rational trees (Maher 1988).
Table 1 summarizes the result of the analysis of a set of handcrafted binary
rules. The symbol X indicates thoses examples that the analysis presented in
(Payet and Mesnard 2004) could not prove non-terminating.
6 Conclusion
In (Payet and Mesnard 2006) we have presented a technique to complement termination analysis with non-termination inside the logic programming paradigm. Our
aim was to detect optimal termination conditions expressed in a language describing
classes of queries. The approach was syntactic and linked to some basic logic programming machinery such as the unification algorithm. In (Payet and Mesnard 2004)
we have presented a first step at generalizing the work of (Payet and Mesnard 2006)
to the CLP setting. The logical criterion we gave only considers those filters, the
function δ of which does not filter anything i.e. δ maps any predicate symbol p to
hpτ (X̃) | truei.
This paper describes a generalization of (Payet and Mesnard 2006) to the CLP
3

available at http://personnel.univ-reunion.fr/fred/dev/DNlog4Q.zip

18

É. Payet and F. Mesnard

Table 1. Running the analyzer on a set of examples.
binary clause

τ

p(A) ← true ⋄ p(B)

{1}

hp(X) | truei

hp(0) | truei

p(A) ← A = B ⋄ p(B)

{1}

hp(X) | truei

hp(0) | truei

p(A) ← A = 0 ⋄ p(B)

∅

hp | truei

hp(A) | A = 0i

p(A) ← A = 0 ∧ B = 0 ⋄ p(B)

∅

hp | truei

hp(A) | A = 0i

δ

p(A) ← A = 0 ∧ B = 1 ⋄ p(B)

looping query

none found

p(A) ← A ≥ 0 ∧ B = 1 ⋄ p(B)

{1}

hp(X) | X ≥ 0i

hp(0) | truei

X

p(A) ← A ≥ 0 ∧ B ≥ 1 ⋄ p(B)

{1}

hp(X) | X ≥ 0i

hp(0) | truei

X

p(A) ← A ≥ 0 ∧ B ≥ −1 ⋄ p(B)

∅

hp | truei

hp(A) | A ≥ 0i

p(A) ← A ≥ 1 ∧ B ≤ 0 ⋄ p(B)

none found

p(A) ← A = B + 1 ∧ B ≥ 0 ⋄ p(B)

∅

hp | truei

hp(A) | A ≥ 1i

p(A, B) ← A = C + 1 ∧ C ≥ 0
⋄ p(C, D)

{2}

hp(Y ) | truei

hp(A, 0) | A ≥ 1i

p(A, B) ← A = C + 1 ∧ C ≥ 0
∧B = D ⋄ p(C, D)

{2}

hp(Y ) | truei

hp(A, 0) | A ≥ 1i

p(A, B) ← A = C + 1 ∧ C ≥ 0
∧B + 1 = D ⋄ p(C, D)

{2}

hp(Y ) | truei

hp(A, 0) | A ≥ 1i

p(A, B) ← A = C + 1 ∧ C ≥ 0
∧B + 1 = D ∧ D ≥ 0
⋄ p(C, D)

{2}

hp(Y ) | Y ≥ −1i

hp(A, −1) | A ≥ 1i

p(A, B) ← A = C + 1 ∧ C ≥ 0
∧B = D + 1 ∧ D ≥ 0
⋄ p(C, D)

∅

hp | truei

hp(A, B)|A ≥ 1
∧B ≥ 1i

p(A, B) ← A ≥ B ∧ C = A + 1
∧D = B ⋄ p(C, D)

{1,2}

hp(X, Y ) | X ≥ Y i

hp(0, 0) | truei

p(A, B) ← A ≤ B ∧ C = A + 1
∧D = B ⋄ p(C, D)

∅

hp | truei

hp(A, B) | A ≤ Bi

pow2(A, B, C) ←
A=D+1∧D ≥0
∧E = 2 ∗ B ∧ B ≥ 1
∧F = C ∧ C ≥ 2
⋄ pow2(D, E, F )

{2, 3}

hpow2(Y, Z)|
Y ≥ 1 ∧ Z ≥ 2i

hpow2(A, 1, 2)|
A ≥ 1i

X

X

X

Non-Termination of CLP

19

setting. It presents a criterion, both in an operational and a logical form, to infer
non-terminating atomic queries with respect to a binary CLP clause. This criterion is generic in the constraint domain; its logical form strictly generalizes that
of (Payet and Mesnard 2004) and it has been fully implemented for CLP(Qlin ).
Acknowledgments
The authors thank the anonymous reviewers for helpful comments on the previous
versions of this paper.

References
Bol, R. N., Apt, K. R., and Klop, J. W. 1991. An analysis of loop checking mechanisms
for logic programs. Theoretical Computer Science 86, 35–79.
Codish, M. and Taboch, C. 1999. A semantics basis for termination analysis of logic
programs. Journal of Logic Programming 41, 1, 103–123.
De Schreye, D., Bruynooghe, M., and Verschaetse, K. 1989. On the existence of
nonterminating queries for a restricted class of Prolog-clauses. Artificial Intelligence 41,
237–248.
De Schreye, D. and Decorte, S. 1994. Termination of logic programs: the never-ending
story. Journal of Logic Programming 19-20, 199–260.
Gabbrielli, M. and Giacobazzi, R. 1994. Goal independency and call patterns in the
analysis of logic programs. In Proc. of the ACM Symposium on Applied Computing
(SAC’94). ACM Press, 394–399.
Giesl, J., Thiemann, R., and Schneider-Kamp, P. 2005. Proving and disproving termination of higher-order functions. In Proc. of the 5th International Workshop on Frontiers of Combining Systems (FroCoS’05), B. Gramlich, Ed. Lecture Notes in Artificial
Intelligence, vol. 3717. Springer-Verlag, 216–231.
Godefroid, P., Klarlund, N., and Sen, K. 2005. DART: Directed Automated Random
Testing. In Proc. of the ACM SIGPLAN 2005 Conference on Programming Language
Design and Implementation (PLDI’05), V. Sarkar and M. W. Hall, Eds. ACM, 213–223.
Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., and Xu, R.-G. 2008.
Proving non-termination. In Proc. of the 35th ACM SIGPLAN-SIGACT Symposium
on Principles of Programming Languages (POPL’08), G. Necula and P. Wadler, Eds.
ACM, 147–158.
Jaffar, J., Maher, M. J., Marriott, K., and Stuckey, P. J. 1998. The semantics of
constraint logic programs. Journal of Logic Programming 37, 1-3, 1–46.
Maher, M. 1988. Complete axiomatizations of the algebras of finite, rational and infinite
trees. In Proc. of the 3rd Annual Symposium on Logic in Computer Science (LICS’88).
IEEE Computer Society, 348–357.
Mesnard, F. and Ruggieri, S. 2003. On proving left termination of constraint logic
programs. ACM Transactions on Computational Logic 4, 2, 207–259.
Payet, E. 2008. Loop detection in term rewriting using the eliminating unfoldings. Theoretical Computer Science 403, 307–327.
Payet, E. and Mesnard, F. 2004. Non-termination inference for constraint logic programs. In Proc. of the 11th International Symposium on Static Analysis (SAS’04),
R. Giacobazzi, Ed. Lecture Notes in Computer Science, vol. 3148. Springer-Verlag,
377–392.

20

É. Payet and F. Mesnard

Payet, E. and Mesnard, F. March 2006. Non-termination inference of logic programs.
ACM Transactions on Programming Languages and Systems 28, Issue 2, 256–289.
Refalo, P. and Hentenryck, P. V. 1996. CLP(Rlin ) revised. In Proc. of the Joint
International Conf. and Symposium on Logic Programming, M. Maher, Ed. The MIT
Press, 22–36.
Sen, K., Marinov, D., and Agha, G. 2005. CUTE: a Concolic Unit Testing Engine
for C. In Proc. of the 10th European Software Engineering Conference held jointly with
13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, M. Wermelinger and H. Gall, Eds. ACM, 263–272.
Shen, Y.-D., Yuan, L.-Y., and You, J.-H. 2001. Loops checks for logic programs with
functions. Theoretical Computer Science 266, 1-2, 441–461.
Speirs, C., Somogyi, Z., and Søndergaard, H. 1997. Termination analysis for Mercury.
In Proc. of the 1997 Intl. Symp. on Static Analysis, P. van Hentenrick, Ed. Lecture Notes
in Computer Science, vol. 1302. Springer-Verlag.
Waldmann, J. 2004. Matchbox: A tool for match-bounded string rewriting. In Proc. of
the 15th International Conference on Rewriting Techniques and Applications (RTA’04),
V. van Oostrom, Ed. Lecture Notes in Computer Science, vol. 3091. Springer-Verlag,
85–94.
Waldmann, J. 2007. Compressed loops (draft).
Available at http://dfa.imn.htwk-leipzig.de/matchbox/methods/.
Wielemaker, J. 2003. An overview of the SWI-Prolog programming environment. In
Proceedings of the 13th International Workshop on Logic Programming Environments
(WLPE’03), F. Mesnard and A. Serebenik, Eds. Vol. CW371. Katholieke Universiteit
Leuven, Department of Computer Science, Celestijnenlaan 200A, B-3001 Heverlee (Belgium), 1–16.
Zankl, H. and Middeldorp, A. 2007. Nontermination of string rewriting using SAT.
In Proc. of the 9th International Workshop on Termination (WST’07). 52–55.
Zantema, H. 2005. Termination of string rewriting proved automatically. Journal of
Automated Reasoning 34, 2, 105–139.

Appendix A – Proof of the results in Section 3
A.1 – Lemma 3.3
If Set (Q) = ∅ then Set(Q) ⊆ Set (Q′ ). Otherwise, let hp(t̃) | di := Q and let
hp(t˜′ ) | d′ i := Q′ . As Q′ is a variant of Q, there exists a renaming γ such that
t˜′ = γ(t̃) and d′ = γ(d). Let p(ã) ∈ Set(Q). Then, there exists a valuation v such
that ã = [t̃]v and D |=v d. Let v1 be the valuation defined as: for all variable V ,
v1 (V ) = v(γ −1 (V )). Then, we have [t˜′ ]v1 = [γ(t̃)]v1 = [γ −1 (γ(t̃))]v = [t̃]v = ã.
Moreover, [d′ ]v1 = [γ(d)]v1 = [γ −1 (γ(d))]v = [d]v = 1. Consequently, D |=v1 d′ .
Therefore, p(ã) ∈ Set(Q′ ).
So, we always have Set(Q) ⊆ Set (Q′ ). The proof of Set(Q′ ) ⊆ Set(Q) follows by
symmetry.

A.2 – Lemma 3.4
Let hp(ũ) | di := Q.

21

Non-Termination of CLP

⇒) Suppose that there exists a derivation step of the form Q =⇒ Q1 . Then, H
r

has the form p(s̃). Let r′ := p(s̃′ ) ← c′ ⋄ B ′ be the input clause of this step.
We have D |= ∃(ũ = s̃′ ∧ c′ ∧ d). So, there exists a valuation v such that
D |=v (ũ = s̃′ ∧ c′ ∧ d). Notice that:
p([ũ]v ) ∈ Set(Q) and p([s̃′ ]v ) ∈ Set(hp(s̃′ ) | c′ i) and [ũ]v = [s̃′ ]v .
Hence, Set(Q) ∩ Set (hp(s̃′ ) | c′ i) 6= ∅. As hp(s̃′ ) | c′ i is a variant of hp(s̃) | ci, by
Lemma 3.3 we have Set(Q)∩Set (hp(s̃) | ci) 6= ∅ i.e. Set(Q)∩Set (hH | ci) 6= ∅.
⇐) Suppose that Set(Q) ∩ Set(hH | ci) 6= ∅. Then, H has the form p(s̃) and we
have Set(Q) ∩ Set(hp(s̃) | ci) 6= ∅. Let r′ := p(s̃′ ) ← c′ ⋄ B ′ be a variant of r
variable disjoint with Q. By Lemma 3.3, Set(hp(s̃′ ) | c′ i) = Set (hp(s̃) | ci), so
we have Set (Q) ∩ Set(hp(s̃′ ) | c′ i) 6= ∅. Let p(ã) ∈ Set(Q) ∩ Set (hp(s̃′ ) | c′ i).
Then, there exists:
— a valuation v1 such that ã = [ũ]v1 and D |=v1 d,
— a valuation v2 such that ã = [s̃′ ]v2 and D |=v2 c′ .
As r′ and Q are variable disjoint, there exists a valuation v such that:
— for all variable V ∈ Var (Q), v(V ) = v1 (V ) and
— for all variable V ∈ Var (r′ ), v(V ) = v2 (V ).
Then, we have [ũ]v = [ũ]v1 = ã, [s̃′ ]v = [s̃′ ]v2 = ã, [d]v = [d]v1 = 1 and
[c′ ]v = [c′ ]v2 = 1. Consequently, D |=v (ũ = s̃′ ∧ c′ ∧ d). Hence, solv (ũ =
s̃′ ∧ c′ ∧ d) = true, so we have Q =⇒hB ′ | ũ = s̃′ ∧ c′ ∧ di.
r

A.3 – Theorem 3.7
We have already proved that there exists a query Q′1 such that Q′ =⇒ Q′1 (see
r

beginning of Section 3.2). Let hp(ũ) | di := Q and hp(ũ′ ) | d′ i := Q′ . Let r1 :=
p(s̃1 ) ← c1 ⋄ q(t̃1 ) be the input clause in Q =⇒ Q1 and r1′ := p(s̃′1 ) ← c′1 ⋄ q(t̃′1 ) be
the input clause in Q′ =⇒ Q′1 . Then,

r

r

Q1 = hq(t̃1 ) | ũ = s̃1 ∧ c1 ∧ di

and Q′1 = hq(t̃′1 ) | ũ′ = s̃′1 ∧ c′1 ∧ d′ i .

Let us prove that Q′1 is more general than Q1 i.e. that Set(Q1 ) ⊆ Set (Q′1 ). If
Set(Q1 ) is empty, then the result trivially holds. Suppose that Set(Q1 ) is not empty.
Let q(ã) ∈ Set (Q1 ). Then, there exists a valuation v such that
ã = [t̃1 ]v

and D |=v (ũ = s̃1 ∧ c1 ∧ d) .

(A1)

Hence, D |=v d, so p([ũ]v ) ∈ Set(Q). As Q′ is more general than Q, then p([ũ]v ) ∈
Set(Q′ ). Consequently, there exists a valuation v1′ such that
[ũ]v = [ũ′ ]v1′

and D |=v1′ d′ .

(A2)

Notice that r1 and r1′ are variants, so r1 = γ(r1′ ) for a renaming γ. As Q′ and r1′
are variable disjoint (because r1′ is the input clause in Q′ =⇒ Q′1 ), there exists a
valuation v ′ such that:

r

22

É. Payet and F. Mesnard
• for all variable V ∈ Var (r1′ ), v ′ (V ) = v(γ(V )) and
• for all variable V ∈ Var (Q′ ), v ′ (V ) = v1′ (V ).

Then, we have [s̃′1 ]v′ = [γ(s̃′1 )]v = [s̃1 ]v with [s̃1 ]v = [ũ]v by (A1) and [ũ′ ]v′ = [ũ′ ]v1′
with [ũ′ ]v1′ = [ũ]v by (A2). So, [s̃′1 ]v′ = [ũ′ ]v′ . Moreover, [c′1 ]v′ = [γ(c′1 )]v = [c1 ]v
with [c1 ]v = 1 by (A1) and [d′ ]v′ = [d′ ]v1′ with [d′ ]v1′ = 1 by (A2). So, we have
D |=v′ (ũ′ = s̃′1 ∧ c′1 ∧ d′ ). As [t̃′1 ]v′ = [γ(t̃′1 )]v = [t̃1 ]v with [t̃1 ]v = ã by (A1), we
conclude that q(ã) ∈ Set(Q′1 ).
A.4 – Corollary 3.8 and Corollary 3.9
First, we need a lemma.
Lemma 1
Let r := H ← c ⋄ B be a clause. Then, there exists a derivation step hH | ci =⇒ Q
r

where Set(Q) = Set(hB | ci).
Proof
As D |= ∃c (by definition of a clause), we have Set(hH | ci) 6= ∅. Hence, Set(hH | ci)∩
Set(hH | ci) 6= ∅. Consequently, by Lemma 3.4, there exists a derivation step of the
form hH | ci =⇒ Q. Let us prove that Set(Q) = Set (hB | ci). Let p(s̃) := H and
r

q(t̃) := B. Let r′ := p(s̃′ ) ← c′ ⋄ q(t̃′ ) be the input clause in hH | ci =⇒ Q. Then,
r

Q = hq(t̃′ ) | s̃′ = s̃ ∧ c′ ∧ ci. Let γ be a renaming such that r = γ(r′ ).
• Let us prove that Set(hB | ci) ⊆ Set(Q). If Set(hB | ci) is empty, then the result
holds. Suppose that Set(hB | ci) is not empty. Let q(ã) ∈ Set(hB | ci). Then, there
exists a valuation v such that ã = [t̃]v and D |=v c. Let v1 be the valuation defined
as:
— for all variable V ∈ Var (r′ ), v1 (V ) = v(γ(V )) and
— for all variable V 6∈ Var (r′ ), v1 (V ) = v(V ).
Then, we have [t̃′ ]v1 = [γ(t̃′ )]v = [t̃]v = ã and [s̃′ ]v1 = [γ(s̃′ )]v = [s̃]v with [s̃]v =
[s̃]v1 because, as r′ is the input clause in hH | ci =⇒ Q, r′ is variable disjoint with
r

hH | ci = hp(s̃) | ci. Moreover, [c′ ]v1 = [γ(c′ )]v = [c]v = 1 and [c]v1 = [c]v (because
r′ is variable disjoint with hp(s̃) | ci) i.e. [c]v1 = 1. Consequently, [t̃′ ]v1 = ã and
D |=v1 (s̃ = s̃′ ∧ c′ ∧ c). Hence, q(ã) ∈ Set (Q).
• Let us prove that Set(Q) ⊆ Set (hB | ci). If Set(Q) is empty, then the result holds.
Suppose that Set(Q) is not empty. Let q(ã) ∈ Set(Q). Then, there exists a valuation
v such that ã = [t̃′ ]v and D |=v (s̃′ = s̃ ∧ c′ ∧ c). Let v1 be a valuation such that:
for all variable V ∈ Var(r), v1 (V ) = v(γ −1 (V )). Then, we have [t̃]v1 = [γ −1 (t̃)]v =
[t̃′ ]v = ã and [c]v1 = [γ −1 (c)]v = [c′ ]v = 1. Consequently, [t̃]v1 = ã and D |=v1 c.
Hence, q(ã) ∈ Set (hB | ci).

23

Non-Termination of CLP

Corollary 3.8
By Lemma 1, there exists a derivation step of the form hH | ci =⇒ Q with Set (Q) =
r

Set(hB | ci). Then, Set(hH | ci) ⊆ Set(Q) (because Set(hH | ci) ⊆ Set(hB | ci)) so,
by repeatedly using the Lifting Theorem 3.7, one can build an infinite derivation
of {r} ∪ {hH | ci}. Consequently, hH | ci loops w.r.t. {r}.
Corollary 3.9
By Lemma 1, we have hH | ci =⇒ Q where Q is more general than hB | ci. As there
r

exists an infinite derivation ξ of P ∪ {hB | ci}, by successively applying the Lifting
Theorem 3.7 to each step of ξ one can construct an infinite derivation of P ∪ {Q}.
Consequently, hH | ci loops w.r.t. P .

24

É. Payet and F. Mesnard
Appendix B – Proof of the results in Section 4
B.1 – Lemma 4.9 and Lemma 4.10

Lemma 4.9
If Set(Q) = ∅ then Set(Qτ ) = ∅, so the result holds. Otherwise, as Set(Q) ⊆
Set(Q′ ), then rel (Q) = rel(Q′ ) i.e. Q has the form hp(t̃) | di and Q′ has the form
hp(t˜′ ) | d′ i. Notice that
Qτ = hpτ (t̃τ (p) ) | di and Q′τ = hpτ (t̃′τ (p) ) | d′ i .
If Set(Qτ ) is empty, then the result holds. Suppose that Set (Qτ ) is not empty.
Let pτ (ã) ∈ Set(Qτ ). Then, there exists a valuation v such that ã = [t̃τ (p) ]v and
D |=v d. Let b̃ be the sequence of arity(p) elements of D defined as:
• b̃τ (p) = ã, i.e. b̃τ (p) = [t̃τ (p) ]v , and
• b̃τ (p) = [t̃τ (p) ]v .
Then, we have b̃ = [t̃]v with D |=v d. Therefore, p(b̃) ∈ Set(Q). As Set(Q) ⊆
Set(Q′ ), then p(b̃) ∈ Set(Q′ ). Consequently, there exists a valuation v ′ such that
b̃ = [t˜′ ]v′ and D |=v′ d′ . Hence, we have ã = b̃τ (p) = [t̃′τ (p) ]v′ and D |=v′ d′ . So,
pτ (ã) ∈ Set(Q′τ ).
Lemma 4.10
If Set(Q)∩Set (Q′ ) 6= ∅ then there exists p(ã) ∈ Set(Q)∩Set (Q′ ) i.e. p(ã) ∈ Set(Q)
and p(ã) ∈ Set (Q′ ). This implies that pτ (ãτ (p) ) ∈ Set (Qτ ) and pτ (ãτ (p) ) ∈ Set (Q′τ ).
So, pτ (ãτ (p) ) ∈ Set(Qτ ) ∩ Set(Q′τ ). Therefore, Set (Qτ ) ∩ Set (Q′τ ) 6= ∅.
B.2 – Lemma 4.16
Let ∆ := (τ, δ) be a filter. Let Q, Q′ and Q′′ be some queries such that Q′′ is ∆more general than Q′ and Q′ is ∆-more general than Q. As Q′′ is ∆-more general
′′
than Q′ , then Qτ is more general than Q′τ and Q′′ satisfies ∆. As Q′ is ∆-more
′′
general than Q, then Q′τ is more general than Qτ . Consequently, Qτ is more general
than Qτ (because the “more general than” relation is transitive) and Q′′ satisfies
∆. Therefore, Q′′ is ∆-more general than Q.
B.3 – Theorem 4.19
By Lemma 1, we have hH | ci =⇒ Q where Set (Q) = Set(hB | ci). So by Lemma 4.9,
r

Qτ is more general than hB | ciτ
and Set(Qτ ) ⊆ Set (hB | ciτ ). As hB | ci satisfies ∆ (because hB | ci is ∆-more general
than hH | ci), we have Set (hB | ciτ ) ⊆ Set(δ(q)) where we let q := rel (B). Hence,
Set(Qτ ) ⊆ Set (δ(q)) i.e.
Q satisfies ∆.

Non-Termination of CLP

25

Therefore, Q is ∆-more general than hB | ci. So, as hB | ci is ∆-more general than
hH | ci and the “∆-more general than” relation is transitive (by Lemma 4.16), we
have that Q is ∆-more general than hH | ci. As ∆ is DN for r, by repeatedly using
Definition 4.18, one can build an infinite derivation of {r} ∪{hH | ci}. Consequently,
hH | ci loops w.r.t. {r}.
B.4 – Lemma 4.23
Let hp(s̃) | di := Q. Let Q′ := hp(s̃′ ) | d′ i be a variant of Q variable disjoint with ũ.
⇒) Suppose that p([ũ]v ) ∈ Set(Q). Then, as by Lemma 3.3 Set(Q) = Set(Q′ ), we
have p([ũ]v ) ∈ Set (Q′ ). Hence, there exists a valuation w such that [ũ]v = [s̃′ ]w
and D |=w d′ . Let v1 be a valuation such that:
— for all variable V ∈ Var (Q′ ), v1 (V ) = w(V ) and
— for all variable V 6∈ Var (Q′ ), v1 (V ) = v(V ).
Then, as Q′ and ũ are variable disjoint, [ũ]v1 = [ũ]v . Moreover, [s̃′ ]v1 =
[s̃′ ]w = [ũ]v and [d′ ]v1 = [d′ ]w = 1. Hence, D |=v1 (ũ = s̃′ ∧ d′ ). Therefore,
D |=v ∃Var (Q′ ) (ũ = s̃′ ∧ d′ ) i.e. D |=v sat (ũ, Q).
⇐) Suppose that D |=v sat (ũ, Q) i.e. D |=v ∃Var (Q′ ) (ũ = s̃′ ∧ d′ ). Then, there
exists a valuation v1 such that
— D |=v1 (ũ = s̃′ ∧ d′ ) and
— for all variable V 6∈ Var (Q′ ), v1 (V ) = v(V ).
As Q′ and ũ are variable disjoint, we have [ũ]v = [ũ]v1 . Moreover, [ũ]v1 = [s̃′ ]v1
and D |=v1 d′ . Consequently, p([ũ]v ) ∈ Set(Q′ ). As, by Lemma 3.3, Set (Q) =
Set(Q′ ), we have p([ũ]v ) ∈ Set (Q).
B.5 – Theorem 4.27
First, we need a technical lemma:
Lemma 2
Let Q := hp(ũ) | di and Q′ := hp(ũ′ ) | d′ i be two variable disjoint queries. If Set(Q) ∩
Set(Q′ ) 6= ∅ then there exists a valuation v such that D |=v (ũ = ũ′ ∧ d ∧ d′ ).
Proof
Suppose that Set(Q)∩Set (Q′ ) 6= ∅. Then, there exists p(ã) such that p(ã) ∈ Set(Q)
and p(ã) ∈ Set(Q′ ). Hence, there exists:
• a valuation v1 such that ã = [ũ]v1 and D |=v1 d and
• a valuation v2 such that ã = [ũ′ ]v2 and D |=v2 d′ .
As Q and Q′ are variable disjoint, there exists a valuation v such that:
• for all variable V ∈ Var (Q), v(V ) = v1 (V ) and
• for all variable V ∈ Var (Q′ ), v(V ) = v2 (V ).

26

É. Payet and F. Mesnard

Then, [d]v = [d]v1 = 1, [d′ ]v = [d′ ]v2 = 1 and [ũ]v = [ũ]v1 = ã = [ũ′ ]v2 = [ũ′ ]v .
Consequently, D |=v (ũ = ũ′ ∧ d ∧ d′ ).
Given a clause r and a filter ∆ that is DNlog for r, we have to prove that ∆ is
DN for r. By Definition 4.18, given a derivation step Q =⇒ T , we have to establish
r
the following facts:
Fact 1. The query T satisfies ∆.
Fact 2. For each query Q′ that is ∆-more general than Q, there exists a derivation
step Q′ =⇒ T ′ where T ′ is ∆-more general than T .
r

Fact 1 is established by Proposition 3 below. We prove Fact 2 in two steps; given a
query Q′ that is ∆-more general than Q, we prove that:
Fact 2a. there exists a derivation step Q′ =⇒ T ′ where T ′ satisfies ∆ (see Proposition 4
r

below).
Fact 2b. the query T ′ in Q′ =⇒ T ′ is such that Tτ′ is more general than Tτ (see Propor

sition 5 below).
Then by Definition 4.14, the query T ′ is ∆-more general than T .
Proposition 3
Let ∆ be a filter that is DNlog for a clause r and Q =⇒ T be a derivation step.
r
Then, T satisfies ∆.
Proof
Let (τ, δ) := ∆ and hp(ũ) | di := Q. Let r1 := p(X̃) ← c ⋄ q(Ỹ ) be the input clause
in Q =⇒ T . Then, T = hq(Ỹ ) | X̃ = ũ ∧ c ∧ di. Let us prove that T satisfies ∆ i.e.
r

that Set (Tτ ) ⊆ Set (δ(q)). Let qτ (ã) ∈ Set (Tτ ). Then, there exists a valuation v
such that
ã = [Ỹτ (q) ]v

and D |=v X̃ = ũ ∧ c ∧ d .

(B1)

As ∆ is DNlog for r, it is also DNlog for r1 . Consequently, we have D |=v c →
sat(Ỹτ (q) , δ(q)). As D |=v c (by (B1)), then we have D |=v sat(Ỹτ (q) , δ(q)). Therefore, by Lemma 4.23, qτ ([Ỹτ (q) ]v ) ∈ Set(δ(q)) i.e. qτ (ã) ∈ Set(δ(q)).
Proposition 4
Let ∆ be a filter that is DNlog for a clause r, Q =⇒ T be a derivation step and
r

Q′ be a query that is ∆-more general than Q. Then, there exists a derivation step
Q′ =⇒ T ′ where T ′ satisfies ∆.
r

Proof
Let (τ, δ) := ∆ and H ← c ⋄ B := r. As Q′ is ∆-more general than Q, Set(Qτ ) ⊆
Set(Q′τ ). Moreover, as Q =⇒ T , by Lemma 3.4 we have Set (Q) ∩ Set(hH | ci) 6= ∅.
r

So, by Lemma 4.10, Set(Qτ ) ∩ Set (hH | ciτ ) 6= ∅. Hence,
Set(Q′τ ) ∩ Set (hH | ciτ ) 6= ∅ .

(B2)

Non-Termination of CLP

27

Let hp(ũ′ ) | d′ i := Q′ and r′ := p(X̃ ′ ) ← c′ ⋄ q(Ỹ ′ ) be a variant of r variable
disjoint with Q′ . By Lemma 3.3, we have Set(hH | ci) = Set(hp(X̃ ′ ) | c′ i) which
implies, by Lemma 4.9, that Set(hH | ciτ ) ⊆ Set (hp(X̃ ′ ) | c′ iτ ) i.e., by (B2), that
Set(Qτ′ ) ∩ Set (hp(X̃ ′ ) | c′ iτ ) 6= ∅. Therefore, by Lemma 2, there exists a valuation
v such that
D |=v (X̃τ′ (p) = ũ′τ (p) ∧ c′ ∧ d′ ) .

(B3)

As ∆ is DNlog for r, it is also DNlog for r′ . Hence, if we let Y := Ỹτ′(q) ∪local vars(r′ ),


we have D |=v c′ → ∀X̃ ′
sat(X̃τ′ (p) , δ(p)) → ∃Y c′ . As by (B3) D |=v c′ , then
τ (p)


D |=v ∀X̃ ′
sat(X̃τ′ (p) , δ(p)) → ∃Y c′ .
(B4)
τ (p)

Let v1 be the valuation defined as:
• for all variable V 6∈ X̃τ′ (p) , v1 (V ) = v(V ) and
• v1 (X̃τ′ (p) ) = [ũ′τ (p) ]v .
Then by (B4) we have:
D |=v1 sat (X̃τ′ (p) , δ(p)) → ∃Y c′ .

(B5)

Notice that pτ ([ũ′τ (p) ]v ) ∈ Set (Q′τ ) because, by (B3), D |=v d′ . Moreover, as Q′
satisfies ∆, Set (Q′τ ) ⊆ Set(δ(p)). Hence, pτ ([ũ′τ (p) ]v ) ∈ Set(δ(p)). As, by definition
of v1 , [ũ′τ (p) ]v = v1 (X̃τ′ (p) ) with v1 (X̃τ′ (p) ) = [X̃τ′ (p) ]v1 (by definition of [·]v1 ), we
have pτ ([X̃τ′ (p) ]v1 ) ∈ Set(δ(p)). So, by Lemma 4.23, D |=v1 sat (X̃τ′ (p) , δ(p)). Hence,
by (B5), D |=v1 ∃Y c′ . Therefore, there exists a valuation v2 such that:
• for all variable V 6∈ Y, v2 (V ) = v1 (V ) and
• D |=v2 c′ .
Notice that as Var(Q′ ) ∩ Var(r′ ) = X̃τ′ (p) ∩ (X̃τ′ (p) ∪ Y) = ∅, by definition of v2 and
v1 we have [d′ ]v2 = [d′ ]v1 = [d′ ]v , [ũ′ ]v2 = [ũ′ ]v1 = [ũ′ ]v and [X̃τ′ (p) ]v2 = [X̃τ′ (p) ]v1 =
[X̃τ′ (p) ]v . So, by (B3), we have
D |=v2 (X̃τ′ (p) = ũ′τ (p) ∧ c′ ∧ d′ ) .

(B6)

As X̃τ′ (p) and Y are variable disjoint, [X̃τ′ (p) ]v2 = [X̃τ′ (p) ]v1 with [X̃τ′ (p) ]v1 = [ũ′τ (p) ]v
by definition of v1 and [ũ′τ (p) ]v = [ũ′τ (p) ]v2 . So, D |=v2 (X̃τ′ (p) = ũ′τ (p) ). Hence
by (B6) D |=v2 (X̃ ′ = ũ′ ∧ c′ ∧ d′ ) i.e. solv (X̃ ′ = ũ′ ∧ c′ ∧ d′ ) = true. Consequently,
we have
Q′ =⇒ T ′
r

where

T ′ = hq(Ỹ ′ ) | X̃ ′ = ũ′ ∧ c′ ∧ d′ i .

Let us prove that T ′ satisfies ∆ i.e. that Set(Tτ′ ) ⊆ Set (δ(q)). Let qτ (ã) ∈ Set (Tτ′ ).
Then, there exists a valuation w such that
ã = [Ỹτ′(q) ]w

and D |=w X̃ ′ = ũ′ ∧ c′ ∧ d′ .

(B7)

As ∆ is DNlog for r′ , we have D |=w c′ → sat (Ỹτ′(q) , δ(q)). As D |=w c′ (by (B7)),
then we have D |=w sat (Ỹτ′(q) , δ(q)). So, by Lemma 4.23, qτ ([Ỹτ′(q) ]w ) ∈ Set(δ(q)).
As ã = [Ỹτ′(q) ]w (by (B7)), we have qτ (ã) ∈ Set(δ(q)).

28

É. Payet and F. Mesnard

Proposition 5
Let ∆ := (τ, δ) be a filter that is DNlog for a clause r. Let Q =⇒ T and Q′ =⇒ T ′
r

r

be some derivation steps such that Q′ is ∆-more general than Q. Then, Tτ′ is more
general than Tτ .
Proof
Let hp(ũ) | di := Q and hp(ũ′ ) | d′ i := Q′ . Let r1 := p(X̃) ← c ⋄ q(Ỹ ) be the input
clause in Q =⇒ T and r1′ := p(X̃ ′ ) ← c′ ⋄ q(Ỹ ′ ) that in Q′ =⇒ T ′ . Then, we have
r

r

′

′

′

T = hq(Ỹ ) | X̃ = ũ ∧ c ∧ di and T = hq(Ỹ ) | X̃ = ũ′ ∧ c′ ∧ d′ i .
Let us prove that Set(Tτ ) ⊆ Set(Tτ′ ). Let qτ (ã) ∈ Set(Tτ ). Then, there exists a
valuation v such that
ã = [Ỹτ (q) ]v

and D |=v X̃ = ũ ∧ c ∧ d .

(B8)

So, D |=v d, hence pτ ([ũτ (p) ]v ) ∈ Set(Qτ ). As Set(Qτ ) ⊆ Set (Qτ′ ) (because Q′ is ∆more general than Q), we have pτ ([ũτ (p) ]v ) ∈ Set (Q′τ ). So, there exists a valuation
v1′ such that
and D |=v1′ d′ .

[ũτ (p) ]v = [ũ′τ (p) ]v1′

(B9)

Notice that r1 and r1′ are variants, so r1 = γ(r1′ ) for a renaming γ. As Q′ and r1′
are variable disjoint (because r1′ is the input clause in Q′ =⇒ T ′ ), there exists a
r

valuation v ′ such that:
• for all variable V ∈ Var (r1′ ), v ′ (V ) = v(γ(V )) and
• for all variable V ∈ Var (Q′ ), v ′ (V ) = v1′ (V ).
Then, we have

• [X̃τ′ (p) ]v′ = ′ [γ(X̃τ′ (p) )]v = [X̃τ (p) ]v = [ũτ (p) ]v = [ũ′τ (p) ]v1′ = ′ [ũ′τ (p) ]v′
def v
def γ
def v
(B8)
(B9)
• [c′ ]v′ = ′ [γ(c′ )]v = [c]v = 1 and [d′ ]v′ = ′ [d′ ]v1′ = 1
def v
def v
def γ
(B9)
(B8)
′
′
• [Ỹτ (q) ]v′ = ′ [γ(Ỹτ (q) )]v = [Ỹτ (q) ]v = ã.
def v
def γ
(B8)
Hence,
D |=v′ X̃τ′ (p) = ũ′τ (p) ∧ c′ ∧ d′
As ∆ is DNlog for r, then it is DNlog for

r1′ .

local vars(r1′ ), we have D |=v′



and [Ỹτ′(q) ]v′ = ã .

(B10)

Consequently, if we let Y := Ỹτ′(q) ∪

sat (X̃τ′ (p) , δ(p)) → ∃Y c′ . As, by (B10),
c′ → ∀X̃ ′
τ (p)


sat (X̃τ′ (p) , δ(p)) → ∃Y c′ . Let w′ be the valuation

D |=v′ c′ , we have D |=v′ ∀X̃ ′
τ (p)
defined as:

• for all variable V 6∈ X̃τ′ (p) , w′ (V ) = v ′ (V ) and
• w′ (X̃τ′ (p) ) = [ũ′τ (p) ]v′ .
Then,
D |=w′ sat (X̃τ′ (p) , δ(p)) → ∃Y c′ .

(B11)

29

Non-Termination of CLP

Notice that pτ ([ũ′τ (p) ]v′ ) ∈ Set(Q′τ ) because D |=v′ d′ by (B10). As [ũ′τ (p) ]v′ =
[X̃τ′ (p) ]w′ (by definition of w′ ), then pτ ([X̃τ′ (p) ]w′ ) ∈ Set(Q′τ ). As Q′ is ∆-more
general than Q, we have Set(Q′τ ) ⊆ Set (δ(p)). Hence, pτ ([X̃τ′ (p) ]w′ ) ∈ Set (δ(p)). So,
by Lemma 4.23, D |=w′ sat (X̃τ′ (p) , δ(p)). Therefore, we have D |=w′ ∃Y c′ by (B11).
Hence, there exists a valuation w1′ such that:
• for all variable V 6∈ Y, w1′ (V ) = w′ (V ) and
• D |=w1′ c′ .
Then, as X̃τ′ (p) ∩ Y = X̃τ′ (p) ∩ (Y ∪ X̃τ′ (p) ) = Var (Q′ ) ∩ Var (r1′ ) = ∅, we have
• [X̃τ′ (p) ]w1′
•
•

= [X̃τ′ (p) ]w′ = ′ [ũ′τ (p) ]v′

=
[ũ′τ (p) ]w1′ ,
def w ′ +def w1′
[X̃τ′ (p) ]w1′ = ′ [X̃τ′ (p) ]w′ = ′ [X̃τ′ (p) ]v′ = [ũ′τ (p) ]v′
=
[ũτ′ (p) ]w1′ .
def w
def w ′ +def w1′
def w1
(B10)
[d′ ]w1′
=
[d′ ]v′ = 1.
def w1′ +def w ′
(B10)
def w1′

def w

So, D |=w1′ X̃ ′ = ũ′ ∧ c′ ∧ d′ . Moreover, [Ỹτ′(q) ]w1′ = [Ỹτ′(q) ]w′ = [Ỹτ′(q) ]v′ with
[Ỹτ′(q) ]v′ = ã by (B10). Consequently, qτ (ã) ∈ Set(Tτ′ ).
B.6 – Theorem 4.29
Suppose that for all atoms A whose arguments are elements of D, there exists a
query Q such that Set(Q) = {A}. Given a clause r := p(X̃) ← c ⋄ q(Ỹ ) and a
filter ∆ := (τ, δ) that is DN for r, we have to prove that ∆ is DNlog for r. By
Definition 4.24, we have to establish that


• DNlog1(∆, r) := c → ∀X̃τ (p) sat (X̃τ (p) , δ(p)) → ∃Y c and

• DNlog2(∆, r) := c → sat (Ỹτ (q) , δ(q))
hold. Proposition 6 below establishes that DNlog1(∆, r) is true and Proposition 6
below establishes that DNlog2(∆, r) is true.
Proposition 6
Assume that the following holds: for each atom A whose arguments are elements
of D, there exists a query Q such that Set(Q) = {A}. Let ∆ be a filter that is DN
for a clause r. Then, D |= DNlog1(∆, r).
Proof
We let ∆ := (τ, δ) and r := p(X̃) ← c ⋄ q(Ỹ ).
Let v be a valuation. Suppose that
D |=v c .
′

(B12)
′

Let v be a valuation such that for all variable V 6∈ X̃τ (p) , v (V ) = v(V ). Suppose
that
D |=v′ sat (X̃τ (p) , δ(p)) .

(B13)

Notice that for all variable V , [V ]v ∈ D and [V ]v′ ∈ D. So, there exists a query Q
such that Set(Q) = {p([X̃]v )} and a query Q′ such that Set (Q′τ ) = {pτ ([X̃τ (p) ]v′ )}
and Set(Q′τ ) = {pτ ([X̃τ (p) ]v )}. Let us prove that D |=v′ ∃Y c. We have:

30

É. Payet and F. Mesnard

• Set(Qτ ) = {pτ ([X̃τ (p) ]v )} = Set(Qτ′ ) and
• pτ ([X̃τ (p) ]v′ ) ∈ Set(δ(p)) because D |=v′ sat (X̃τ (p) , δ(p)) and by Lemma 4.23. So,
as Set(Q′τ ) = {pτ ([X̃τ (p) ]v′ )}, we have Set(Q′τ ) ⊆ Set(δ(p)).
Consequently, Q′ is ∆-more general than Q. Moreover, as D |=v c, we have p([X̃]v ) ∈
Set(hp(X̃) | ci). As Set(Q) = {p([X̃]v )}, this implies that Set(Q) ∩ Set (hp(X̃) | ci) 6=
∅. Hence, by Lemma 3.4, there exists a derivation step of the form Q =⇒ T . Let
r

r1 := p(Ũ ) ← c1 ⋄ q(Ṽ ) be the input clause in this derivation step. Then, if we let
Q := hp(t̃) | di, we have
T = hq(Ṽ ) | Ũ = t̃ ∧ c1 ∧ di .
As Q′ is ∆-more general than Q and ∆ is DN for r, there exists a query T ′ such
that Q′ =⇒ T ′ and T ′ is ∆-more general than T . Let r1′ := p(Ũ ′ ) ← c′1 ⋄ q(Ṽ ′ ) be
r

the input clause in Q′ =⇒ T ′ . Then, if we let Q′ := hp(t̃′ ) | d′ i, we have
r

T ′ = hq(Ṽ ′ ) | Ũ ′ = t̃′ ∧ c′1 ∧ d′ i .
As r1 is a variant of r, there exists a renaming γ such that r = γ(r1 ). Let v1 be the
valuation defined as:
• for all variable V ∈ Var (r1 ), v1 (V ) = v(γ(V )) and
• for all variable V 6∈ Var (r1 ), v1 (V ) = v(V ).
As Set (Q) = {p([X̃]v )}, there exists a valuation vQ such that
[t̃]vQ = [X̃]v

and D |=vQ d .

(B14)

Let v2 be the valuation defined as:
• for all variable V ∈ Var (Q), v2 (V ) = vQ (V ) and
• for all variable V 6∈ Var (Q), v2 (V ) = v1 (V ).
As Var (Q) ∩ Var (r1 ) = ∅ (because r1 is the input clause in Q =⇒ T ), we have
r

[c1 ]v2 = [c1 ]v1 = [γ(c1 )]v = [c]v
def v2

def v1

def γ

[Ũ ]v2 = [Ũ ]v1 = [γ(Ũ )]v = [X̃]v
def v2

Moreover, [d]v2 = [d]vQ
def v2

def v1

def γ

= 1

(B12)

and

= [t̃]vQ = [t̃]v2 .

(B14)

def v2

= 1. Consequently,

(B14)

D |=v2 Ũ = t̃ ∧ c1 ∧ d .
So, qτ ([Ṽτ (q) ]v2 ) ∈ Set (Tτ ). As [Ṽτ (q) ]v2 = [Ṽτ (q) ]v1 = [γ(Ṽτ (q) )]v = [Ỹτ (q) ]v we
def v2

def v1

def γ

have qτ ([Ỹτ (q) ]v ) ∈ Set(Tτ ). Moreover, as Set(Tτ ) ⊆ Set(Tτ′ ) (because T ′ is ∆-more
general than T ), qτ ([Ỹτ (q) ]v ) ∈ Set(Tτ′ ). Consequently, there exists a valuation v1′
such that
[Ṽτ′(q) ]v1′ = [Ỹτ (q) ]v
As

r1′

and D |=v1′ Ũ ′ = t̃′ ∧ c′1 ∧ d′ .
′

is a variant of r, there exists a renaming γ such that

r1′

(B15)
′

= γ (r). Let w

31

Non-Termination of CLP

be a valuation such that for all variable V ∈ Var (r), w(V ) = v1′ (γ ′ (V )). Then,
[c]w = [γ ′ (c)]v1′ = [c′1 ]v1′ = 1, so
(B15)
D |=w c .

(B16)

Notice that:
• [X̃τ (p) ]w = [γ ′ (X̃τ (p) )]v1′ = ′ [Ũτ′ (p) ]v1′

= [t̃′τ (p) ]v1′ = [X̃τ (p) ]v′ because, as D |=v1′
(B15)
d′ by (B15), we have pτ ([t̃′τ (p) ]v1′ ) ∈ Set(Q′τ ) = {pτ ([X̃τ (p) ]v′ )};
[X̃τ (p) ]w = [γ ′ (X̃τ (p) )]v1′ = ′ [Ũτ′ (p) ]v1′ = [t̃′τ (p) ]v1′ = [X̃τ (p) ]v because, as D |=v1′
def w
def γ
(B15)
′
′
′
d by (B15), we have pτ ([t̃τ (p) ]v1 ) ∈ Set(Qτ′ ) = {pτ ([X̃τ (p) ]v )}; moreover, by definition of v ′ , [X̃τ (p) ]v = [X̃τ (p) ]v′ because X̃τ (p) ∩ X̃τ (p) = ∅;
[Ỹτ (q) ]w = [γ ′ (Ỹτ (q) )]v1′ = ′ [Ṽτ′(q) ]v1′ = [Ỹτ (q) ]v = ′ [Ỹτ (q) ]v′ because we have that
def w
def v
def γ
(B15)
def w

•

•

def γ

Ỹτ (q) ∩ X̃τ (p) = ∅.
Consequently, as Var (c) \ Y ⊆ X̃τ (p) ∪ X̃τ (p) ∪ Ỹτ (q) , we have:
for all V ∈ Var(c) \ Y, w(V ) = v ′ (V ) .

(B17)

Let w1 be the valuation defined as:
• for all variable V ∈
6 Y, w1 (V ) = v ′ (V ) and
• for all variable V ∈ Y, w1 (V ) = w(V ).
Then, for all variable V ∈ Var (c), if V ∈ Y then w1 (V ) = w(V ) and if V 6∈ Y
def w1

then w1 (V ) = v ′ (V ) = w(V ). Consequently, [c]w1 = [c]w = 1. So, D |=w1 c
def w1
(B16)
(B17)
which implies, by definition of w1 , that D |=v′ ∃Y c.
Hence, as we supposed (B13), we have D |=v′ sat (X̃τ (p) , δ(p)) → ∃Y c. Therefore,
as v ′ denotes any valuation such that v ′ (V
 ) = v(V ) for all variable V 6∈ X̃τ (p) , we
get D |=v ∀X̃τ (p) sat (X̃τ (p) , δ(p)) → ∃Y c . As we supposed (B12), we deduce that


D |=v c → ∀X̃τ (p) sat (X̃τ (p) , δ(p)) → ∃Y c where v denotes any valuation. Hence
the result.
Proposition 7
Let ∆ be a filter that is DN for a clause r. Then, D |= DNlog2(∆, r).
Proof
We let ∆ := (τ, δ) and r := p(X̃) ← c ⋄ q(Ỹ ).
By Lemma 1, there exists a derivation step
hp(X̃) | ci =⇒ Q
r

where

Set(Q) = Set(hq(Ỹ ) | ci) .

Then, as ∆ is DN for r, Q satisfies ∆ i.e. Set(Qτ ) ⊆ Set(δ(q)). Moreover, as
Set(hq(Ỹ ) | ci) ⊆ Set(Q), by Lemma 4.9 Set (hq(Ỹ ) | ciτ ) ⊆ Set(Qτ ). So,
Set(hq(Ỹ ) | ciτ ) ⊆ Set(δ(q)) .

(B18)

32

É. Payet and F. Mesnard

Let v be a valuation. Suppose that
D |=v c .

(B19)

Notice that qτ ([Ỹτ (q) ]v ) ∈ Set(hq(Ỹ ) | ciτ ). So, by (B18), qτ ([Ỹτ (q) ]v ) ∈ Set(δ(q)).
Therefore, by Lemma 4.23, we have D |=v sat(Ỹτ (q) , δ(q)). As we supposed (B19),
then we have D |=v c → sat (Ỹτ (q) , δ(q)) where v denotes any valuation. Hence the
result.

