arXiv:cs/0201011v1 [] 16 Jan 2002

Under consideration for publication in Theory and Practice of Logic Programming

1

A Backward Analysis for
Constraint Logic Programs
ANDY KING
University of Kent at Canterbury, Canterbury, CT2 7NF, UK.
email: amk@ukc.ac.uk

LUNJIN LU
Oakland University, Rochester, MI 48309, USA.
email: l2lu@oakland.edu

Abstract
One recurring problem in program development is that of understanding how to re-use
code developed by a third party. In the context of (constraint) logic programming, part of
this problem reduces to ﬁguring out how to query a program. If the logic program does not
come with any documentation, then the programmer is forced to either experiment with
queries in an ad hoc fashion or trace the control-ﬂow of the program (backward) to infer
the modes in which a predicate must be called so as to avoid an instantiation error. This
paper presents an abstract interpretation scheme that automates the latter technique.
The analysis presented in this paper can infer moding properties which if satisﬁed by the
initial query, come with the guarantee that the program and query can never generate any
moding or instantiation errors. Other applications of the analysis are discussed. The paper
explains how abstract domains with certain computational properties (they condense) can
be used to trace control-ﬂow backward (right-to-left) to infer useful properties of initial
queries. A correctness argument is presented and an implementation is reported.

1 Introduction
The myth of the lonely logic programmer writing a program in isolation is just
that: a myth. Applications (and application components) are usually implemented
and maintained by a team. One consequence of this is a signiﬁcant proportion of
the program development eﬀort is devoted to understanding code developed by
another. One advantage of (constraint) logic programs for software development is
that their declarative nature makes them less opaque than, say, C++ programs. One
disadvantage of logic programs over C++ programs, however, is that the signature
(argument types) of a predicate do not completely specify how the predicate should
be invoked. In particular, a call to a predicate from an unexpected context may
generate an error if an argument of the call is insuﬃciently instantiated (even if
the program and query are well-typed). This is because logic programs contain
builtins and calls to these builtins often impose moding requirements on the query.
If the program is developed by another programmer, it may not be clear how to

2

Andy King and Lunjin Lu

query a predicate so as to avoid an instantiation error. In these circumstances, the
programmer will often resort to a trial and error tactic in their search for an initial
call mode. This can be both frustrating and tedious and, of course, cannot guarantee
coverage of all the program execution paths. This paper presents an analysis for
inferring moding properties which, if satisﬁed by the initial query, ensure that the
program does not generate instantiation errors. Of course, it does not mean that
the inferred call has the form exactly intended by the original programmer – no
analysis can do that – the analysis just recovers mode information. Nevertheless,
this is a useful ﬁrst step in understanding the code developed by another.
The problem of inferring initial queries which do not lead to instantiation errors
is an instance of the more general problem of deducing how to call a program
so that it conforms to some desired property, for example, calls to builtins do not
error, the program terminates, or calls to builtins behave predictably. The backward
analysis presented in this paper is designed to infer conditions on the query which,
if satisﬁed, guarantee that resulting derivations satisfy a property such as one of
those above. Speciﬁcally, the analysis framework can be instantiated to solve the
following analysis problems:
• Builtins and library functions can behave unpredictably when called with
inﬁnite rational trees. For example, the query ?- X = X + X, Y is X will
not terminate in SICStus Prolog because the arithmetic operator expects its
input to be a ﬁnite tree rather than an inﬁnite rational tree. Moreover, the
standard term ordering of Prolog does not lift to rational trees, so the builtin
sort can behave unpredictably when sorting rational trees. These problems
(and related problems with builtins) motivate the use of dependency analysis
for tracking which terms are deﬁnitely ﬁnite (Bagnara et al., 2001). The basic
idea is to describe the constraint x = f (x1 , . . . , xn ) by the Boolean function
x ⇔ ∧ni=1 xi which encodes that x is bound to a ﬁnite tree iﬀ each xi is
bound to a ﬁnite tree. Although not proposed in the context of backward
analysis (Bagnara et al., 2001), the framework proposed in this paper can be
instantiated with a ﬁnite tree dependency domain to infer ﬁniteness properties
on the query which, if satisﬁed, guarantee that builtins are not called with
problematic arguments.
• Termination inference is the problem of inferring initial modes for a query
that, if satisﬁed, ensure that a logic program terminates. This problem generalises termination checking which veriﬁes program termination for a class of
queries speciﬁed by a given mode. Termination inference dates back to (Mesnard, 1996) but it has been recently observed (Genaim & Codish, 2001) that
the missing link between termination checking and termination inference is
backward analysis. A termination inference analyser is reported in (Genaim
& Codish, 2001) composed from two components: a standard termination
checker (Codish & Taboch, 1999) and the backward analysis described in this
paper. The resulting analyser is similar to the cTI analyser of (Mesnard &
Neumerkel, 2001) – the main diﬀerence is its design as two existing black-

A Backward Analysis for Constraint Logic Programs

3

box components which, according to (Genaim & Codish, 2001), simpliﬁes the
formal justiﬁcation and implementation.
• Mode analysis is useful for implementing ccp programs. In particular (Debray
et al., 1992) explains how various low-level optimisations, such as returning
output values in registers, can be applied if goals can be scheduled left-toright without suspension. If the guards of the predicates are re-interpreted as
moding requirements, then the backward mode analysis can infer suﬃcient
conditions for avoiding deadlock under left-to-right scheduling. The analysis
presented in this paper thus has applications outside program development.
To summarise, the analysis presented in this paper can deduce properties of the call
which, if satisﬁed, guarantee that resulting derivations fulﬁll some desired property.
The analysis is unusual in that it applies lower approximation (see 2.4.1) as well
as upper approximation (see 2.3.1); it is formulated in terms of a greatest ﬁxpoint
calculation (see 2.4) as well as least ﬁxpoint calculation (see 2.3); the analysis also
imposes some unusual restrictions on the abstract domain (see 2.4.6).
1.1 Backward analysis
Backward analysis has been applied extensively in functional programming in,
among other things, projection analysis (Wadler & Hughes, 1987), stream strictness analysis (Hall & Wise, 1989), inverse image analysis (Dyber, 1991), etc. By
reasoning about the context of a function application, these analyses can identify
opportunities for eager evaluation that are missed by (forward) strictness analysis
as proposed by (Mycroft, 1981). Furthermore, backward reasoning on imperative
programs dates back to the early days of static analysis (Cousot & Cousot, 1982).
By way of contrast, backward analysis has been rarely applied in logic programming. One notable exception is the demand analysis of (Debray, 1993). This analysis
infers the degree of instantiation necessary for the guards of a concurrent constraint
program (ccp) to reduce. It is a local analysis that does not consider the possible
suspension of body calls. This analysis detects those (uni-modal) predicates which
can be implemented with specialised suspension machinery. A more elaborate backward analysis for ccp is presented by (Falaschi et al., 2000). This demand analysis
infers how much input is necessary for a procedure to generate a certain amount of
output. This information is useful for adding synchronisation (ask) constraints to a
procedure to delay execution and thereby increase grain size, and yet not introduce
deadlock. (Section 7 provides more extensive and reﬂective review of the related
work.)
1.2 Contributions
Our work is quite diﬀerent. As far as we are aware, it is unique in that it focuses on
the backward analysis of (constraint) logic programs with left-to-right scheduling.
Speciﬁcally, our work makes the following practical and theoretical contributions:
• it shows how to compute an initial mode of a predicate which is safe in that

4

Andy King and Lunjin Lu
if a query is at least as instantiated as the inferred mode, the execution is
guaranteed to be free from instantiation errors. The modes inferred are often
disjunctive, sometimes surprising and, for the small predicates that we veriﬁed
by hand, appear to be optimal.
• it speciﬁes a practical algorithm for calculating initial modes that is straightforward to implement in that it reduces to two bottom-up ﬁxpoint calculations. Furthermore, this backward analysis problem cannot be solved with
any existing abstract interpretation machinery.
• to the best our knowledge, it is the ﬁrst time domains that are closed under Heyting completion (Giacobazzi & Scozzari, 1998), or equivalently are
condensing (Marriott & Søndergaard, 1993), have been applied to backward
analysis. Put another way, our work adds credence to the belief that condensation is an important property in the analysis of logic programs.

The ﬁnal point requires some unpacking. Condensation was originally proposed in
(Langen, 1991), though arguably the simplest statement of this property (Marriott
& Søndergaard, 1993) is for downward closed domains such as P os (Armstrong
et al., 1998) and the P os-like type dependency domains (Codish & Lagoon, 2000).
Suppose that f : X → X is an abstract operation on a downward closed domain
X equipped with an operation ∧ that mimics uniﬁcation or constraint solving. X
is condensing iﬀ x ∧ f (y) = f (x ∧ y) for all x, y ∈ X. Hence, if X is condensing, x ∧ f (true) = f (x) where true represents the weakest abstract constraint.
More exactly, if f (true) represents the result of the goal-independent analysis, and
f (x) the result of the goal-dependent one with an initial constraint x, then the
equivalence f (x) = x ∧ f (true) enables goal-dependent analysis to be performed
in a goal-independent way without loss of precision. This, in turn, can simplify
the implementation of an analyser (Armstrong et al., 1998). Because of this, domain reﬁnement machinery has been devised to enrich a domain with new elements
to obtain the desired condensing property (Giacobazzi & Scozzari, 1998). It turns
out that it is always possible to systematically design a condensing domain for a
given downward closed property (Giacobazzi & Scozzari, 1998)[Theorem 8.2] by
applying Heyting completion. Conversely, under some reasonable hypotheses, all
condensing domains can be reconstructed by Heyting completion (Giacobazzi &
Scozzari, 1998)[Theorem 8.3]. One consequence of this is that condensing domains
come equipped with a (pseudo-complement) operator and this turns out to be an
operation that is important in backward analysis. To summarise, machinery has
been developed to synthesise condensing domains and condensing domains provide
operations suitable for backward analysis.
1.3 Organisation of the paper
The rest of the paper is structured as follows. Section 2 introduces the key ideas
of the paper in an informal way through a worked example. Section 3 introduces
the necessary preliminaries for the formal sections that follow. Section 4 presents
an operational semantics for constraint logic programs with assertions in which the
set of program states is augmented by a special error state. Section 5 develops a

A Backward Analysis for Constraint Logic Programs

5

semantics which computes those initial states that cannot lead to the error state.
The semantics deﬁnes a framework for backward analysis and formally argues correctness. Section 6 describes an instantiation of the framework for mode analysis.
Section 7 reviews the related work and section 8 concludes. Much of the formal
machinery is borrowed directly from (Giacobazzi et al., 1995; Giacobazzi & Scozzari, 1998) and in particular the reader is referred to (Giacobazzi et al., 1995) for
proofs of the semantic results stated in section 3 (albeit presented in a slightly different form). To aid continuity in the paper, the remaining proofs are relegated to
appendix A.

2 Worked example
2.1 Basic components
This section informally presents an abstract interpretation scheme which infers how
to query a given predicate so as to avoid run-time moding errors. In other words,
the analysis deduces moding properties of the call that, if satisﬁed, guarantee that
resulting derivations cannot encounter an instantiation error. To illustrate, consider
the Quicksort program listed in the left column of ﬁgure 1. This is the ﬁrst ingredient
of the analysis: the input program. The second ingredient is an abstract domain
which, in this case, is P os. P os is the domain of positive Boolean functions, that is,
the set of functions f : {0, 1}n → {0, 1} such that f (1, . . . , 1) = 1. Hence x∨y ∈ P os
since 1 ∨ 1 = 1 but ¬x 6∈ P os since ¬1 = 0. P os is augmented with the bottom
element 0 with 1 being the top element. The domain is ordered by entailment |=
and, in this example, will be used to represent grounding dependencies.
P os comes equipped with the logical operations: conjunction ∧, disjunction ∨,
implication ⇒ (and thus bi-implication ⇔). Conjunction is used to conjoin the
information from diﬀerent body atoms, while disjunction is used to combine the
information from diﬀerent clauses. Conjunction and disjunction, in turn, enable two
projection operators to be deﬁned: ∃x (f ) = f [x 7→ 0] ∨ f [x 7→ 1] and ∀x (f ) = f ′ if
f ′ ∈ P os otherwise ∀x (f ) = 0 where f ′ = f [x 7→ 0] ∧ f [x 7→ 1]. Note that although
f [x 7→ 0] ∨ f [x 7→ 1] ∈ P os for all f ∈ P os it does not follow that f [x 7→ 0] ∧ f [x 7→
1] ∈ P os for all f ∈ P os. Indeed, (x ⇐ y)[x 7→ 0] ∧ (x ⇐ y)[x 7→ 1] = ¬y. Both
operators are used to project out the body variables that are not in the head of
a clause. Speciﬁcally, these operators eliminate the variable x from the formula f .
They are dual in the sense that ∀x (f ) |= f |= ∃x (f ). These are the basic components
of the analysis.
2.2 Normalisation and abstraction
The analysis components are assembled in two steps. The ﬁrst is a bottom-up analysis for success patterns, that is, a bottom-up analysis which infers the groundness
dependencies which are known to be created by each predicate regardless of the
calling pattern. This step is a least ﬁxpoint (lfp) calculation. The second step is a
bottom-up analysis for input modes (the objective of the analysis). This step is a

6

Andy King and Lunjin Lu

qs([], s, s).
qs([m|xs], s, t) :pt(xs, m, l, h),
qs(l, s, [m|r]),
qs(h, r, t).
pt([], , [], []).
pt([x|xs], m, [x|l], h) :m =< x,
pt(xs, m, l, h).
pt([x|xs], m, l, [x|h]) :m > x,
pt(xs, m, l, h).

qs(t1 , s, t2 ) :t1 = [], t2 = s.
qs(t1 , s, t) :t1 = [m|xs],
t3 = [m|r],
pt(xs, m, l, h),
qs(l, s, t3 ),
qs(h, r, t).
pt(t1 , , t2 , t3 ) :t1 = [],
t2 = [], t3 = [].
pt(t1 , m, t2 , h) :t1 = [x|xs],
t2 = [x|l],
m =< x
pt(xs, m, l, h).
pt(t1 , m, l, t2 ) :t1 = [x|xs],
t2 = [x|h],
m > x,
pt(xs, m, l, h).

qs(t1 , s, t2 ) :1 ⋄ g1 .
qs(t1 , s, t) :1 ⋄ g2 ,
pt(xs, m, l, h),
qs(l, s, t3 ),
qs(h, r, t).
pt(t1 , , t2 , t3 ) :1 ⋄ g3 .
pt(t1 , m, t2 , h) :1 ⋄ g4 ,
=<’(m, x),
pt(xs, m, l, h).
pt(t1 , m, l, t2 ) :1 ⋄ g5 ,
>’(m, x),
pt(xs, m, l, h).
=<’(m, x) :- g6 ⋄ g6 .
>’(m, x) :- g6 ⋄ g6 .

Fig. 1. Quicksort: raw, normalised and abstracted

greatest ﬁxpoint (gfp) computation. To simplify both steps, the program is put into
a form in which the arguments of head and body atoms are distinct variables. This
gives the normalised program listed in the centre column of ﬁgure 1. This program
is then abstracted by replacing each Herbrand constraint x = f (x1 , . . . , xn ) with
a formula x ⇔ ∧ni=1 xi that describes its grounding dependency. This gives the abstract program listed in the right column of ﬁgure 1. The formula 1 in the assertion
represents true whereas the formulae gi that appear in the abstract program are
as follows:
g1 = t1 ∧ (t2 ⇔ s)
g2 = t1 ⇔ (m ∧ xs) ∧ t3 ⇔ (m ∧ r)
g 3 = t1 ∧ t2 ∧ t3

g4 = t1 ⇔ (x ∧ xs) ∧ t2 ⇔ (x ∧ l)
g5 = t1 ⇔ (x ∧ xs) ∧ t2 ⇔ (x ∧ h)
g6 = m ∧ x

Builtins that occur in the source, such as the tests =< and >, are handled by
augmenting the abstract program with fresh predicates, =<′ and >′ , which express
the grounding behaviour of the builtins. The ⋄ symbol separates an assertion (the
required mode) from another P os formula describing the grounding behaviour of a
successful call to the builtin (the success mode). For example, the formula g6 left
of ⋄ in the =<′ clause asserts that the =< test will error if its ﬁrst two arguments
are not ground, whereas the g6 right of ⋄ describes the state that holds if the
test succeeds. These formulae do not coincide for all builtins (see Table 1). For
quicksort, the only non-trivial assertions arise from builtins. This would change if
the programmer introduced assertions for veriﬁcation (Puebla et al., 2000a).

A Backward Analysis for Constraint Logic Programs

7

2.3 Least fixpoint calculation
An iterative algorithm is used to compute the lfp and thereby characterise the
success patterns of the program. A success pattern is a pair consisting of an atom
with distinct variables for arguments paired with a P os formula over those variables.
Renaming and equality of formulae induce an equivalence between success patterns
which is needed to detect the ﬁxpoint. The patterns hp(u, w, v), u ∧ (w ⇔ v)i and
hp(x1 , x2 , x3 ), (x3 ⇔ x2 ) ∧ x1 i, for example, are considered to be identical: both
express the same inter-argument groundness dependencies. Each iteration produces
a set of success patterns: at most one pair for each predicate in the program.
2.3.1 Upper approximation of success patterns
A success pattern records an inter-argument groundness dependency that describes
the binding eﬀects of executing a predicate. If hp(~x), f i correctly describes the
predicate p, and g holds whenever f holds, then hp(~x), gi also correctly describes
p. Success patterns can thus be approximated from above without compromising
correctness.
Iteration is performed in a bottom-up fashion and commences with F0 = ∅. Fj+1
is computed from Fj by considering each clause p(~x) ← d ⋄ f, p1 (~x1 ), . . . , pn (~xn ) in
turn. Initially Fj+1 = ∅. The success pattern formulae fi for the n body atoms
are conjoined with f to obtain g = f ∧ ∧ni=1 fi . Variables not present in p(~x), Y
say, are then eliminated from g by computing g ′ = ∃Y (g) (weakening g) where
∃{y1 ...yn } (g) = ∃y1 (. . . ∃yn (g)). Weakening g does not compromise correctness because success patterns can be safety approximated from above.
2.3.2 Weakening upper approximations
If Fj+1 already contains a pattern of the form hp(~x), g ′′ i, then this pattern is replaced with hp(~x), g ′ ∨ g ′′ i, otherwise Fj+1 is revised to include hp(~x), g ′ i. Thus the
success patterns become progressively weaker on each iteration. Again, correctness
is preserved because success patterns can be safety approximated from above.
2.3.3 Least fixpoint calculation for Quicksort
For brevity, let ~u = hx1 , x2 i, ~v = hx1 , x2 , x3 i and w
~ = hx1 , x2 , x3 , x4 i. Then the lfp
for the abstracted Quicksort program is obtained (and checked) in the following 3
iterations:




hqs(~v ), x1 ∧ (x2 ⇔ x3 )i
hqs(~v ), x2 ⇔ (x1 ∧ x3 )i










hpt(w),
~ x1 ∧ x3 ∧ x4 i
hpt(w),
~ x1 ∧ x3 ∧ x4 i
F1 =
F
=
2




h=<′ (~u), x1 ∧ x2 i
h=<′ (~u), x1 ∧ x2 i








′
h> (~u), x1 ∧ x2 i
h>′ (~u), x1 ∧ x2 i

Finally, F3 = F2 . The space of success patterns forms a complete lattice which
ensures that a lfp (a most precision solution) exists. The iterative process will
always terminate since the space is ﬁnite and hence the number of times each

8

Andy King and Lunjin Lu

success pattern can be updated is also ﬁnite. Moreover, it will converge onto the
lfp since iteration commences with the bottom element F0 = ∅.
Observe that F2 , the lfp, faithfully describes the grounding behaviour of quicksort: a qs goal will ground its second argument if it is called with its ﬁrst and third
arguments already ground and vice versa. Note that assertions are not considered
in the lfp calculation.
2.4 Greatest fixpoint calculation
A bottom-up strategy is used to compute a gfp and thereby characterise the safe
call patterns of the program. A safe call pattern describes queries that do not violate
the assertions. A call pattern has the same form as a success pattern (so there is one
call pattern per predicate rather than one per clause). One starts with assuming no
call causes an error and then checks this assumption by reasoning backwards over
all clauses. If an assertion is violated, the set of safe call patterns for the involved
predicate is strengthened (made smaller), and the whole process is repeated until
the assumptions turn out to be valid (the gfp is reached).
2.4.1 Lower approximation of safe call patterns
Iteration commences with D0 = {hp(~x), 1i | p ∈ Π} where Π is the set of predicate
symbols occurring in the program. An iterative algorithm incrementally strengthens
the call pattern formulae until they only describe queries which lead to computations that satisfy the assertions. Note that call patterns describe a subset (rather
than a superset) of those queries which are safe. Call patterns are thus lower approximations in contrast to success patterns which are upper approximations. Put
another way, if hp(~x), gi correctly describes some safe call patterns of p, and g holds
whenever f holds, then hp(~x), f i also correctly describes some safe call patterns
of p. Call patterns can thus be approximated from below without compromising
correctness (but not from above).
Dk+1 is computed from Dk by considering each p(~x) ← d ⋄ f, p1 (~x1 ), . . . , pn (~xn )
in turn and calculating a formula that characterises its safe calling modes. Initially
set Dk+1 = Dk . A safe calling mode is calculated by propagating moding requirements right-to-left by repeated application of the logical operator ⇒. More exactly,
let fi denote the success pattern formula for pi (~xi ) in the previously computed lfp
and let di denote the call pattern formula for pi (~xi ) in Dk . Set en+1 = 1 and then
compute ei = di ∧ (fi ⇒ ei+1 ) for 1 ≤ i ≤ n. Each ei describes a safe calling mode
for the compound goal pi (~xi ), . . . , pn (~xn ).
2.4.2 Intuition and explanation
The intuition behind the symbolism is that di represents the demand that is already
known for pi (~xi ) not to error whereas ei is di possibly strengthened with extra
demand so as to ensure that the sub-goal pi+1 (~xi+1 ), . . . , pn (~xn ) also does not error
when executed immediately after pi (~xi ). Put another way, anything larger than di

A Backward Analysis for Constraint Logic Programs

9

may possibly cause an error when executing pi (~xi ) and anything larger than ei may
possibly cause an error when executing pi (~xi ), . . . , pn (~xn ).
The basic inductive step in the analysis is to compute an ei which ensures that
pi (~xi ), . . . , pn (~xn ) does not error, given di and ei+1 which respectively ensure that
pi (~xi ) and pi+1 (~xi+1 ), . . . , pn (~xn ) do not error. This step translates a demand after
the call to pi (~xi ) into a demand before the call to pi (~xi ). The tactic is to set en+1 = 1
and then compute ei = di ∧ (fi ⇒ ei+1 ) for i ≤ n. This tactic is best explained
by unfolding the deﬁnitions of en , then en−1 , then en−2 , and so on. This reverse
ordering reﬂects the order in which the ei are computed; the ei are computed whilst
walking backward across the clause. Any calling mode is safe for the empty goal
and hence en+1 = 1. Note that en = dn ∧ (fn ⇒ en+1 ) = dn ∧ (¬fn ∨ 1) = dn . Hence
en represents a safe calling mode for the goal pn (~xn ).
Observe that ei should not be larger than di , otherwise an error may occur
while executing pi (~xi ). Observe too that if pi (~xi ), . . . , pn (~xn ) is called with a mode
described by di , then pi+1 (~xi+1 ), . . . , pn (~xn ) is called with a mode described by
(di ∧ fi ) since fi describes the success patterns of pi (~xi ). The mode (di ∧ fi ) may
satisfy the ei+1 demand. If it does not, then the minimal extra demand is added
to (di ∧ fi ) so as to satisfy ei+1 . This minimal extra demand is ((di ∧ fi ) ⇒ ei+1 ) –
the weakest mode that, in conjunction with (di ∧ fi ), ensures that ei+1 holds. Put
another way, ((di ∧ fi ) ⇒ ei+1 ) = ∨{f ∈ P os | (di ∧ fi ) ∧ f |= ei+1 }.
Combining the requirements to satisfy pi (~xi ) and then pi+1 (~xi+1 ), . . . , pn (~xn ),
gives ei = di ∧ ((di ∧ fi ) ⇒ ei+1 ) which reduces to ei = di ∧ (fi ⇒ ei+1 ) and
corresponds to the tactic used in the basic inductive step.
2.4.3 Pseudo-complement
This step of calculating the weakest mode that when conjoined with di ∧ fi implies ei+1 , is the very heart of the analysis. Setting ei = 0 would trivially achieve
safety, but ei should be as weak as possible to maximise the class of safe queries
inferred. For P os, computing the weakest ei reduces to applying the ⇒ operator,
but more generally, this step amounts to applying the pseudo-complement operator.
The pseudo-complement operator (if it exists for a given abstract domain) takes,
as input, two abstractions and returns, as output, the weakest abstraction whose
conjunction with the ﬁrst input abstraction is at least as strong as the second input
abstraction. If the domain did not possess a pseudo-complement, then there is not
always a unique weakest abstraction (whose conjunction with one given abstraction
is at least as strong as another given abstraction).
To see this, consider the domain Def (Armstrong et al., 1998) which does not
possess a pseudo-complement. Def is the sub-class of P os that is deﬁnite (Armstrong et al., 1998). This means that Def has the special property that each of its
Boolean functions can be expressed as a (possibly empty) conjunction of propositional Horn clauses. As with P os, Def is assumed to be augmented with the
bottom element 0. Def can thus represent the grounding dependencies x ∧ y, x,
x ⇔ y, y, x ⇐ y, x ⇒ y, 0 and 1 but not x ∨ y. Suppose that di ∧ fi = (x ⇔ y)
and ei+1 = (x ∧ y). Then conjoining x with di ∧ fi would be at least as strong

10

Andy King and Lunjin Lu

as ei+1 and symmetrically conjoining y with di ∧ fi would be at least as strong
as ei+1 . However, Def does not contain a Boolean function strictly weaker than
both x and y, namely x ∨ y, whose conjunction with di ∧ fi is at least as strong
as ei+1 . Thus setting ei = x or ei = y would be safe but setting ei = (x ∨ y) is
prohibited because x ∨ y falls outside Def . Moreover, setting ei = 0 would loose
an unacceptable degree of precision. A choice would thus have to be made between
setting ei = x and ei = y in some arbitrary fashion, so there would be no clear
tactic for maximising precision.
Returning to the compound goal pi (~xi ), . . . , pn (~xn ), a call described by the mode
di ∧ ((di ∧ fi ) ⇒ ei+1 ) is thus suﬃcient to ensure that neither pi (~xi ) nor the subgoal pi+1 (~xi+1 ), . . . , pn (~xn ) error. Since di ∧ ((di ∧ fi ) ⇒ ei+1 ) = di ∧ (fi ⇒ ei+1 )
= ei it follows that pi (~xi ), . . . , pn (~xn ) will not error if its call is described by ei . In
particular, it follows that e1 describes a safe calling mode for the body atoms of
the clause p(~x) ← d ⋄ f, p1 (~x1 ), . . . , pn (~xn ).
The next step is to calculate g = d ∧ (f ⇒ e1 ). The abstraction f describes
the grounding behaviour of the Herbrand constraint added to the store prior to
executing the body atoms. Thus (f ⇒ e1 ) describes the weakest mode that, in
conjunction with f , ensures that e1 holds, and hence the body atoms are called
safely. Hence d ∧ (f ⇒ e1 ) represents the weakest demand that both satisﬁes the
body atoms and the assertion d. One subtlety which relates to the abstraction
process, is that d is required to be a lower-approximation of the assertion whereas
f is required to be an upper-approximation of the constraint. Put another way,
if the mode d describes the binding on the store, then the (concrete) assertion is
satisﬁed, whereas if the (concrete) constraint is added to the store, then the store
is described by the mode f . Table 1 details how to abstract various builtins for
groundness for a declarative subset of ISO Prolog.
2.4.4 Strengthening lower approximations
Variables not present in p(~x), Y say, are then eliminated by g ′ = ∀Y (g) (strengthening g) where ∀{y1 ...yn } (g) = ∀y1 (. . . ∀yn (g)). A safe calling mode for this particular clause is then given by g ′ . Eliminating variables from g by strengthening g is
unusual and initially appears strange. Recall, however, that call patterns can be
approximated from below without compromising correctness (but not from above).
In particular the standard projection tactic of computing ∃{y1 ...yn } (g) would result
in an upper approximation of g that possibly describes a larger set of concrete call
patterns which would be incorrect. The direction of approximation thus dictates
that eliminating the variables Y from g must strengthen g. Indeed, g holds whenever
∀yi (g) holds and therefore g holds whenever ∀{y1 ...yn } (g) holds as required.
Dk+1 will contain a call pattern hp(~x), g ′′ i and, assuming g ′ ∧ g ′′ 6= g ′′ , this is
updated with hp(~x), g ′ ∧ g ′′ i. Thus the call patterns become progressively stronger
on each iteration. Correctness is preserved because call patterns can be safely approximated from below. The space of call patterns forms a complete lattice which
ensures that a gfp exists. In fact, because call patterns are approximated from below, the gfp is the most precise solution, and therefore the desired solution. (This

A Backward Analysis for Constraint Logic Programs

11

contrasts to the norm in logic program analysis where approximation is from above
and the lfp is the most precise solution). Moreover, since the space of call patterns
is ﬁnite, termination is assured. In fact, the scheme will converge onto the gfp since
iteration commences with the top element D0 = {hp(~x), 1i | p ∈ Π}.

2.4.5 Greatest fixpoint calculation for Quicksort
Under this procedure Quicksort generates the following Dk sequence:




hqs(~v ), 1i
hqs(~v ), 1i











hpt(w),
~ 1i
hpt(w),
~ 1i
D0 =
D1 =
′
′


h=< (~u), 1i
h=< (~u), x1 ∧ x2 i








′
h> (~u), 1i
h>′ (~u), x1 ∧ x2 i




hqs(~v ), 1i
hqs(~v ), x1 i












hpt(w),
~ x2 ∧ (x1 ∨ (x3 ∧ x4 ))i
hpt(w),
~ x2 ∧ (x1 ∨ (x3 ∧ x4 ))i
D2 =
D3 =
′
′




h=< (~u), x1 ∧ x2 i
h=< (~u), x1 ∧ x2 i








′
′
h> (~u), x1 ∧ x2 i
h> (~u), x1 ∧ x2 i

These calculations are non-trivial so consider how D2 is obtained from D1 by applying the clause pt(t1 , m, t2 , h) : −1 ⋄ g4 , =<′ (m, x), pt(xs, m, l, h). The following
ei and g formulae are generated:
e3 =
1
e2 = 1 ∧ ((xs ∧ l ∧ h) ⇒ 1) =
1
e1 = (m ∧ x) ∧ ((m ∧ x) ⇒ 1) =
m∧x
g = 1 ∧ (((t1 ⇔ x ∧ xs) ∧ (t2 ⇔ x ∧ l)) ⇒ (m ∧ x))
To characterise those pt(t1 , m, t2 , h) calls which are safe, it is necessary to compute
a function g ′ on the variables t1 , m, t2 , h which, if satisﬁed by the mode of a call,
ensures that g is satisﬁed by the mode of the call. Put another way, it is necessary to
eliminate the variables x, xs and l from g (those variables which do not occur in the
head pt(t1 , m, t2 , h)) to strengthen g obtain a function g ′ such that g holds whenever
g ′ holds. This is accomplished by calculating g ′ = ∀l ∀xs ∀x (g). First consider the
computation of ∀x (g):
g[x 7→ 0] = (((t1 ⇔ x ∧ xs) ∧ (t2 ⇔ x ∧ l)) ⇒ (m ∧ x))[x 7→ 0]
= ((t1 ⇔ 0 ∧ xs) ∧ (t2 ⇔ 0 ∧ l)) ⇒ (m ∧ 0)
= (¬t1 ∧ ¬t2 ) ⇒ 0
= t1 ∨ t2
g[x 7→ 1] = (((t1 ⇔ x ∧ xs) ∧ (t2 ⇔ x ∧ l)) ⇒ (m ∧ x))[x 7→ 1]
= ((t1 ⇔ xs) ∧ (t2 ⇔ l)) ⇒ m
Since g[x 7→ 0] ∧ g[x 7→ 1] ∈ P os it follows that:
∀x (g) = (((t1 ⇔ xs) ∧ (t2 ⇔ l)) ⇒ m) ∧ (t1 ∨ t2 )

12

Andy King and Lunjin Lu

(otherwise ∀x (g) would be set to 0). Eliminating the other variables in a similar
way we obtain:
∀xs ∀x (g) = ((t2 ⇔ l) ⇒ m) ∧ (t1 ∨ t2 )
g = ∀l ∀xs ∀x (g) = m ∧ (t1 ∨ t2 )
′

Observe that if ∀l ∀xs ∀x (g) holds then g holds. Thus if the mode of a call satisﬁes g ′
then the mode also satisﬁes g as required. This clause thus yields the call pattern
hpt(w),
~ x2 ∧ (x1 ∨ x3 )i. Similarly the ﬁrst and third clauses contribute the patterns
hpt(w),
~ 1i and hpt(w)
~ ← x2 ∧ (x1 ∨ x4 )i. Observe also that
1 ∧ (x2 ∧ (x1 ∨ x3 )) ∧ (x2 ∧ (x1 ∨ x4 )) = x2 ∧ (x1 ∨ (x3 ∧ x4 ))
which gives the ﬁnal call pattern formula for pt(w)
~ in D2 . The gfp is reached at
D3 since D4 = D3 . The gfp often expresses elaborate calling modes, for example,
it states that pt(w)
~ cannot generate an instantiation error (nor any predicate that
it calls) if it is called with its second, third and fourth argument ground. This is a
surprising result which suggests that the analysis can infer information that might
be normally missed by a programmer.
2.4.6 Restrictions posed by the framework
The chief computational requirement of the analysis is that the input domain is
equipped with a pseudo-complement operation. As already mentioned, it is always
possible to systematically design a domain with this operator (Giacobazzi & Scozzari, 1998) and any domain that is known to be condensing (see section 1.2) comes
equipped with this operator. Currently, however, there are only a few domains with
a pseudo-complement. Indeed, the domain described in (Codish & Lagoon, 2000)
appears to be unique in that it is the only type domain that is condensing. This is
the main limitation of the backward analysis described in this paper.
P os is downward-closed in the sense that if a function f describes a substitutions,
then f also describes all substitutions less general than the substitution. The type
domain of (Codish & Lagoon, 2000) is also downward-closed. It does not follow,
however, that a domain equipped with a pseudo-complement operation is necessarily downward-closed. Heyting completion, the domain reﬁnement technique used
to construct pseudo-complement, can be moved to linear implication (Giacobazzi
et al., 1998), though the machinery is more complicated. However, it is likely, that
in the short term tractable condensing domains will continue to be downwardclosed. In fact, constructing tractable downward-closed condensing domains is a
topic within itself.

3 Preliminaries
3.1 Basic Concepts
Sets and sequences Let N denote the set of non-negative integers. The powerset
of S is denoted ℘(S). The empty sequence is denoted ǫ and S ⋆ denotes the set of

A Backward Analysis for Constraint Logic Programs

13

(possibly empty) sequences whose elements are drawn from S. Sequence concatenation is denoted · and the length of a sequence s is |s|. Furthermore, let s0 = ǫ and
sn = s · sn−1 where n ∈ N. If n ∈ N and s ∈ N⋆ then max(n · s) = max(n, max(s))
where max(ǫ) = 0.
Orderings A pre-order on a set S is a binary relation ⊑ that is reﬂexive and transitive. A partial order on a set S is a pre-order that is anti-symmetric. A poset hS, ⊑i
is a partial order on a set S. If hS, ⊑i is a poset, then C ⊆ S is a chain iﬀ a ⊑ b or
b ⊑ a for all a, b ∈ C. A meet semi-lattice hL, ⊑, ⊓i is a poset hL, ⊑i such that the
meet (greatest lower bound) ⊓{x, y} exists for all x, y ∈ L. A complete lattice is
a poset hL, ⊑i such that the meet ⊓X and the join ⊔X (least upper bound) exist
for all X ⊆ L. Top and bottom are respectively deﬁned by ⊤ = ⊓∅ and ⊥ = ⊔∅. A
complete lattice is denoted hL, ⊑, ⊓, ⊔, ⊤, ⊥i. Let hS, ⊑i be a pre-order. If X ⊆ S
then ↓(X) = {y ∈ S | ∃x ∈ X.y ⊑ x}. If x ∈ S then ↓(x) = ↓({x}). The set of orderideals of S, denoted ℘↓(S), is deﬁned by ℘↓(S) = {X ⊆ S | X = ↓(X)}. Observe
that h℘↓(S), ⊆, ∪, ∩, S, ∅i is a complete lattice.
An algebraic structure is a pair hS, Qi where S is a non-empty set and Q is
collection of n-ary operations f : S n → S where n ∈ N. Let hS, ⊑i and hS ′ , ⊑′ i be
posets and hS, Qi and hS ′ , Q′ i algebraic structures such that Q = {fi | i ∈ I} and
Q′ = {fi′ | i ∈ I} for an index set I. Then α : S → S ′ is a semi-morphism between
hS, Qi and hS ′ , Q′ i iﬀ α(fi (s1 , . . . , sn )) ⊑ fi′ (α(s1 ), . . . , α(sn )) for all hs1 , . . . , sn i ∈
S n and i ∈ I.
Functions and fixpoints Let f : A → B. Then dom(f ) denotes the domain of f
and if C ⊆ A then f (C) = {f (c) | c ∈ C}. Furthermore, cod(f ) = f (dom(f )).
Let hL, ⊑, ⊔, ⊓i and hL′ , ⊑′ , ⊔′ , ⊓′ i be complete lattices. The map f : L → L′ is
additive iﬀ f (⊔X) = ⊔′ f (X) for all X ⊆ L; f is continuous iﬀ f (⊔C) = ⊔′ f (C)
for all chains C ⊆ L; f is co-continuous iﬀ f (⊓C) = ⊓′ f (C) for all chains C ⊆ L
and f is monotonic iﬀ f (x) ⊑′ f (y) for all x ⊑ y. Let x ⊑ y. If f is continuous
then f (y) = f (x ⊔ y) = ⊔′ {f (x), f (y)} and thus f (x) ⊑′ f (y). If f is co-continuous
then f (x) = f (x ⊓ y) = ⊓′ {f (x), f (y)} and thus f (x) ⊑′ f (y). Both continuity
and co-continuity thus imply monotonicity. If f : L → L, then f is idempotent
iﬀ f (x) = f 2 (x) for all x ∈ L and f is extensive iﬀ x ⊑ f (x) for all x ∈ L.
The Knaster-Tarski theorem states that any monotone operator f : L → L on a
complete lattice hL, ⊑, ⊔, ⊓, ⊤, ⊥i admit both greatest and least ﬁxpoints that are
characterised by gfp(f ) = ⊔{x ∈ L | x ⊑ f (x)} and lfp(f ) = ⊓{x ∈ L | f (x) ⊑ x}.
If f is co-continuous then gfp(f ) = ⊓n∈N f n (⊤) and dually if f is continuous then
lfp(f ) = ⊔n∈N f n (⊥). {f n (⊤) | n ∈ N} and {f n (⊥) | n ∈ N} are, respectively, the
lower and upper Kleene iteration sequences of f .
Galois insertions and closure operators If hS, ⊑i and hS ′ , ⊑′ i are posets and
α : S → S ′ and γ : S ′ → S are monotonic maps such that ∀x ∈ S.x ⊑ γ(α(x))
and ∀x′ ∈ S ′ .α(γ(x′ )) ⊑′ x′ , then the quadruple hS, γ, S ′ , αi is a Galois connection
between S and S ′ . In other words, α is the lower (or left) adjoint of γ and γ is the upper (or right) adjoint of α. If, in addition, ∀x′ ∈ S ′ .x′ ⊑′ α(γ(x′ )), then hS, γ, S ′ , αi

14

Andy King and Lunjin Lu

is a Galois insertion between S and S ′ . The operator ρ : L → L on a complete lattice hL, ⊑i is a closure operator iﬀ ρ is monotonic, idempotent and extensive. The
set of closure operators on L is denoted uco(L). The image set ρ(L) of a closure
operator ρ is a complete lattice with respect to ⊑. A Galois insertion hL, γ, L′ , αi
between the complete lattices L and L′ deﬁnes the closure operator ρ = γ ◦ α.
Conversely, a closure operator ρ : L → L on the complete lattice hL, ⊑, ⊔i deﬁnes
the Galois insertion hL, id, ρ(L), ρi where id denotes identity. Galois insertions and
closure operators are thus isomorphic, though closure operators are typically more
succinct and hence used in this paper.
Substitutions Let Sub denote the set of (idempotent) substitutions and let Ren
denote the set of (bijective) renaming substitutions.
3.2 Cylindric constraint systems
Let V denote a (denumerable) universe of variables and let C denote a constraint
system over V . An algebra hC, ✂, ⊗, 1, {∃x}x∈V , {dx,y }x,y∈V i is a semi-cylindric constraint system iﬀ hC, ✂, ⊗i is a meet semi-lattice with a top 1; ∃x is a family of
(unary) cylindriﬁcation operations such that: c ✂ ∃x (c), ∃x (c) ✂ ∃x (c′ ) if c ✂ c′ ,
∃x (c ⊗ ∃x (c′ )) = ∃x (c) ⊗ ∃x (c′ ); and dx,y is a family of (constant) diagonalisation
operations such that: dx,x = 1, dx,y = ∃z (dx,z ⊗ dz,y ) and dx,y ⊗ ∃x (c ⊗ dx,y ) ✂ c
if x 6= y. Cylindriﬁcation captures the concept of projecting out a variable (and is
useful in modeling variables that go out of scope) whereas diagonalisation captures
the notion of an alias between two variables (and is useful in modeling parameter
passing). (The reader is referred to (Giacobazzi et al., 1995) for further details on
cylindric constraint systems and their application in abstract interpretation.)
Example 3.1
An equation e is a pair (s = t) where s and t are terms. A ﬁnite conjunction of
equations is denoted E and Eqn denotes the set of ﬁnite conjunctions of equations. Let eqn(θ) = {x = t | x 7→ t ∈ θ} and unif y(E) = {θ ∈ Sub | ∀(s =
t) ∈ E.θ(s) = θ(t)}. Eqn is pre-ordered by entailment E1 ✂ E2 iﬀ unif y(E1 ) ⊆
unif y(E2 ) and quotiented by E1 ≈ E2 iﬀ E1 ✂ E2 and E2 ✂ E1 . This gives
the meet semi-lattice hEqn/ ≈, ✂, ⊗i with a top 1 where conjunction is deﬁned
[E1 ]≈ ⊗ [E2 ]≈ = [E1 ∪ E2 ]≈ and 1 = [∅]≈ . Let mgu(E) = {θ ∈ unif y(E) | ∀κ ∈
unif y(E) . eqn(κ)✂eqn(θ)}. Finally, let dx,y = [{x = y}]≈ and deﬁne project out by
∃x ([E]≈ ) = [eqn({y 7→ t ∈ θ | x 6= y})]≈ if θ ∈ mgu(E). Otherwise, if mgu(E) = ∅,
deﬁne ∃x ([E]≈ ) = [{a = b}]≈ where a and b are distinct constant symbols. Then
hEqn/≈, ✂, ⊗, 1, {∃x}x∈V , {dx,y }x,y∈V i is a semi-cylindric constraint system.
An algebra hC, ✂, ⊕, ⊗, 1, 0, {∃x}x∈V , {dx,y }x,y∈V i that extends a semi-cylindric
constraint system to a complete lattice hC, ✂, ⊕, ⊗, 1, 0i is a cylindric constraint system. A semi-cylindric constraint system can be lifted to a cylindric constraint system via a power-domain construction. In particular h℘↓(C), ⊆, ∪, ∩, C, ∅, {∃′x }x∈V ,
{d′x,y }x,y∈V i is a cylindric constraint system where ∃′x (C) = ↓({∃x (c) | c ∈ C}) and
d′x,y = ↓(dx,y ).

A Backward Analysis for Constraint Logic Programs

15

Example 3.2
The semi-cylindric system of example 3.1 can be lifted to the cylindric system
h℘↓ (Eqn), ⊆, ∪, ∩, Eqn, ∅, ∃′ , d′ i where ∃′x (C) = ↓({∃x (c)|c ∈ C}) and d′x,y = ↓(dx,y ).
In the sequel, unless otherwise stated, all constraint systems considered are
over the same V and thus a cylindric constraint system will be simply denoted
hC, ✂, ⊕, ⊗, 1, 0, ∃, di. Let var(o) denote the set of the variables in the syntactic
object o and let F V (c) denote the set of free variables in a constraint c ∈ C,
that is, F V (c) = {x ∈ var(c) | ∃y ∈ V . c 6= ∃x (c ⊗ dx,y )}. Abbreviate project
out by ∃{x1 ,...,xn } (c) = ∃x1 (. . . (∃xn (c))) and project onto by ∃X (c) = ∃F V (c)\X (c).
Let d~x,~y = ⊗ni=1 dxi ,yi where ~x = hx1 . . . xn i and ~y = hy1 . . . yn i. If c ∈ C then
let ∂~xy~ (c) denote the constraint obtained by replacing ~x with ~y , that is, ∂~xy~ (c) =
∃~z (∃~x (c ⊗ d~x,~z ) ⊗ d~z,~y ) where var(~z) ∩ (F V (c) ∪ var(~x) ∪ var(~y )) = ∅. Finally, if
C ⊆ C then ∂~xy~ (C) = {∂~xy~ (c) | c ∈ C}.
Example 3.3
Let X be a ﬁnite subset of V . The groundness domain hEP osX , |=, g, ∧, 1, 0i
(Heaton et al., 2000) is a ﬁnite lattice where EP osX = {0} ∪ {∧F | F ⊆ X ∪ EX },
EX = {x ⇔ y | x, y ∈ X} and f1 g f2 = ∧{f ∈ EP osX | f1 |= f ∧ f2 |= f }. EP osX
is a cylindric constraint system with dx,y = (x ⇔ y) and ∃x (f ) = f ′ ∧ f ′′ where
f ′ = ∧{y ∈ Y | f |= y}, f ′′ = ∧{e ∈ EY | f |= e} and Y = X \ {x}.
Example 3.4
Let BoolX denote the Boolean functions over X. The dependency domain P osX
(Armstrong et al., 1998) is deﬁned by P osX = {0} ∪ {f ∈ BoolX | ∧X |= f }.
Henceforth Y abbreviates ∧Y . The lattice hP osX , |=, ∨, ∧, 1, 0i is ﬁnite and is a
cylindric constraint system with dx,y = (x ⇔ y) and Schröder elimination deﬁning
∃x (f ) = f [x 7→ 1] ∨ f [x 7→ 0].
3.3 Complete Heyting algebras
Let hL, ⊑, ⊓i be a lattice with x, y ∈ L. The pseudo-complement of x relatively to
y, if it exists, is a unique element z ∈ L such that x ⊓ w ⊑ y iﬀ w ⊑ z. L is relatively
pseudo-completed iﬀ the pseudo-complement of x relative to y, denoted x → y,
exists for all x, y ∈ L. If L is also complete then it is a complete Heyting algebra
(cHa). If x, y ∈ L then x ⊓ (x → y) = x ⊓ y. Furthermore, if hL, ⊑, ⊔, ⊓i is a cHa
then x → y = ⊔{w ∈ L | x ⊓ w ⊑ y}. The intuition behind the pseudo-complement
of x relative to y is that it is the weakest element whose combination (meet) with
x implies y. Interestingly pseudo-complement can be interpreted as the adjoint
of conjunction. (The reader is referred to (van Dalen, 1997) for further details
on complete Heyting algebras.) The following result (Birkhoﬀ, 1967)[Chapter IX,
Theorem 15] explains how a cHa depends on the additivity of meet.
Theorem 3.1
A complete lattice L is relatively pseudo-complemented iﬀ x ⊓ (⊔Y ) = ⊔{x ⊓ y |
y ∈ Y } for all x ∈ L and Y ⊆ L.

16

Andy King and Lunjin Lu

Example 3.5
Let {x, y} ⊆ X and f = (x ⇔ y). Then returning to EP osX of example 3.3,
f ∧ (g{x, y}) = f ∧ (1) = f 6= (x ∧ y) = g{x ∧ y, x ∧ y} = g{f ∧ x, f ∧ y}. Hence,
by theorem 3.1, EP osX is not a cHa. Now consider P osX of example 3.4, and
speciﬁcally let f ∈ P osX and G ⊆ P osX . Since ∧ distributes over ∨, it follows that
f ⊓ (⊔G) = ⊔{f ⊓ g | g ∈ G}, thus by theorem 3.1, P osX is a cHa. Similarly, ∩
distributes over ∪, and thus it follows by theorem 3.1 that ℘↓ (C) is also a cHa.
3.4 Constraint logic programs
Let Π denote a (ﬁnite) set of predicate symbols, let Atom denote the set of (ﬂat)
atoms over Π with distinct arguments drawn from V , and let hC, ✂, ⊕, ⊗, 1, 0, ∃, di
be a semi-cylindric constraint system. The set of constrained atoms is deﬁned by
BaseC = {p(~x) :- c | p(~x) ∈ Atom ∧ c ∈ C}. Let F V (p(~x) :- c) = var(~x) ∪ F V (c).
Entailment ✂ lifts to BaseC by w1 ✂ w2 iﬀ ∃~x (d~x,~x1 ⊗ c1 ) ✂ ∃~x (d~x,~x2 ⊗ c2 ) where
wi = p(~xi ) :- ci and var(~x) ∩ (F V (w1 ) ∪ F V (w2 )) = ∅. This pre-order deﬁnes the
equivalence relation w1 ≈ w2 iﬀ w1 ✂ w2 and w2 ✂ w1 to give a set of interpretations
deﬁned by IntC = ℘(BaseC /≈). IntC is ordered by I1 ⊑ I2 iﬀ for all [w1 ]≈ ∈ I1
there exists [w2 ]≈ ∈ I2 such that w1 ✂ w2 . Let ≡ denote the induced equivalence
relation I1 ≡ I2 iﬀ I1 ⊑ I2 and I2 ⊑ I1 . hIntC / ≡, ⊑, ⊔, ⊓, ⊤, ⊥i is a complete
lattice where [I1 ]≡ ⊔ [I2 ]≡ = [I1 ∪ I2 ]≡ , [I1 ]≡ ⊓ [I2 ]≡ = [∪{I | I ⊑ I1 ∧ I ⊑ I2 }]≈ ,
⊤ = [{[p(~x) :- 1]≈ | p(~x) ∈ Atom}]≡ and ⊥ = [∅]≡ .
A constraint logic program P over C is a ﬁnite set of clauses w of the form
w = h :- c, g where h ∈ Atom, c ∈ C, g ∈ Goal and Goal = Atom⋆ . The ﬁxpoint
semantics of P is deﬁned in terms of an immediate consequences operator FPC .
Definition 3.1
Given a constraint logic program P over a semi-cylindric constraint system C, the
operator FPC : IntC → IntC is deﬁned by:


∃ p(~x) :- c, p1 (~x1 ), . . . , pn (~xn ) ∈ P . 

FPC (I) = [p(~x) :- c′ ]≈ ∃
.
{[pi (~xi ) :- ci ]≈ }ni=1 ⊆ I


c′ = c ⊗ ⊗ni=1 ∃x~i (ci )

The operator FPC lifts to IntC /≡ by FPC ([I]≡ ) = [FPC (I)]≡ . The lifting is monotonic
and hence the ﬁxpoint semantics for a program P over C exists and is denoted
F C (P ) = lfp(FPC ). (The reader is referred to (Bossi et al., 1994; Jaﬀar & Maher,
1994) for further details on semantics and constraint logic programming.)
The operational semantics of P is deﬁned in terms of a transition system →P
between states of the form State = Goal × C. To deﬁne the transition system,
let F V (hg; ci) = var(g) ∪ F V (c) and F V (h :- c, g) = var(h) ∪ F V (c) ∪ var(g). To
rename clauses with ϕ ∈ Ren it is necessary to rename constraints with ϕ. Thus
ϕ(~
x)
deﬁne ϕ(h :- c, g) = ϕ(h) :- ∂~x (c), ϕ(g). To rename apart from a syntactic object o,
let w ≪o P indicate that there exists w′ ∈ P and ϕ ∈ Ren such that var(cod(ϕ)) ∩
F V (w′ ) = ∅, ϕ(w′ ) = w and F V (o) ∩ F V (w) = ∅.
Definition 3.2

A Backward Analysis for Constraint Logic Programs

17

Given a constraint logic program P over a semi-cylindric constraint system C,
→P ⊆ State2 is the least relation such that:
s = hp(~x), g; ci →P hg ′ , g; c ⊗ d~x,~x′ ⊗ c′ i
where p(~x′ ) :- c′ , g ′ ≪s P .
The operational semantics is speciﬁed by the transitive closure of the transition
relation on (atomic) goals, that is, OC (P ) = [{[p(~x) :- c]≈ | hp(~x); 1i →⋆P hǫ; ci}]≡ .
The relationship between the operational and ﬁxpoint semantics is stated below.
Theorem 3.2
OC (P ) = F C (P ).
3.5 Abstract semantics for constraint logic programs
To apply abstraction techniques and ﬁnitely characterise F C (P ), and thereby OC (P ),
the semi-cylindric domain C is replaced by the cHa ℘↓(C) which is particularly
amenable to approximation and backward reasoning.
If P is a constraint logic program over C, then ↓(P ) = {h :- ↓(c), g | h :- c, g ∈ P }.
Furthermore, if I ∈ IntC , then let ↓([I]≡ ) = [{[p(~x) :- ↓(c)]≈ | [p(~x) :- c]≈ ∈ I}]≡ .
Note the overloading on ≈ and hence ≡. The ≈ of [p(~x) :- c]≈ is induced by hC, ✂i
whereas the ≈ of [p(~x) :- ↓(c)]≈ is induced by h℘↓(C), ⊆i. The following proposition
↓
details the relationship between F C and F ℘ (C) .
Proposition 3.1
↓
↓(F C (P )) ⊑ F ℘ (C) (↓(P )).
Let hC, ✂, ⊕, ⊗, 1, 0, ∃, di denote a cylindric constraint system. If ρ ∈ uco(C) then
hρ(C), ✂, ⊗i is a complete lattice. If ρ is additive, then hρ(C), ✂, ⊕, ⊗i is a sub-lattice
of hC, ✂, ⊕, ⊗i. More generally, the join is denoted ⊕′ . Observe that ρ(C) has 1 and
ρ(0) for top and bottom and c1 ⊕ c2 ✂ ρ(c1 ⊕ c2 ) = c1 ⊕′ c2 for all c1 , c2 ∈ ρ(C).
A cylindric constraint system is obtained by augmenting ρ(C) with cylindriﬁcation ∃′x and diagonalisation d′x,y operators. To abstract hC, ✂, ⊕, ⊗, 1, 0, ∃, di safely
with hρ(C), ✂, ⊕′ , ⊗, 1, ρ(0), ∃′ , d′ i, ρ is required to be a semi-morphism (Giacobazzi
et al., 1995) which additionally requires that ρ(∃x (c)) ✂ ∃′x (ρ(c)) for all c ∈ C and
ρ(dx,y ) ✂ d′x,y for all x, y ∈ V . In fact, these requirements turn out to be relatively
weak conditions: most abstract domains come equipped with (abstract) operators
to model projection and parameter passing.
Example 3.6
Consider the cylindric system h℘↓ (Eqn), ⊆, ∪, ∩, Eqn, ∅, ∃, di derived from the semicylindric system introduced in example 3.1. Let Bool = BoolV and P os = P osV .
Deﬁne αP os : ℘↓ (Eqn) → P os by αP os (C) = ∨{α(θ) | θ ∈ mgu(E) ∧ E ∈ C}
and α(θ) = ∧{x ⇔ var(t) | x 7→ t ∈ θ}. Also deﬁne γP os : P os → ℘↓ (Eqn) by
γP os (f ) = ∪{C ∈ ℘↓ (Eqn) | αP os (C) |= f } and observe ρP os ∈ uco(℘↓ (Eqn)) where
ρP os = γP os ◦ αP os . To construct a semi-morphism, put d′x,y = γP os (x ⇔ y) and
∃′x (C) = γP os (f [x 7→ 1]∨f [x 7→ 0]) where f = αP os (C). Then ρP os (dx,y ) ⊆ d′x,y and

18

Andy King and Lunjin Lu

ρP os (∃x (C)) ⊆ ∃′x (ρP os (C)) for all C ∈ ℘↓(Eqn). Note that C1 ∩ C2 = γP os (f1 ∧ f2 )
and C1 ⊕′ C2 = γP os (f1 ∨ f2 ) where Ci = γP os (fi ). Surprisingly C1 ⊕′ C2 6= C1 ∪ C2
(Filé & Ranzato, 1994), as witnessed by C1 = γP os (x) and C2 = γP os (x ⇔ y) since
{y = f (x, z)} 6∈ C1 ∪ C2 whereas αP os ({y = f (x, z)}) = y ⇔ (x ∧ z) |= x ∨ (x ⇔ y)
so that {y = f (x, z)} ∈ C1 ⊕′ C2 = γP os (x ∨ (x ⇔ y)). Nevertheless, ρP os is
a semi-morphism between h℘↓ (Eqn), ⊆, ∪, ∩, Eqn, ∅, ∃, di and hρP os (℘↓(Eqn)), ⊆
, ⊕′ , ∩, Eqn, ρP os (∅), ∃′ , d′ i.
The operator ρ lifts to the complete lattice IntC / ≡ by ρ([I]≡ ) = [ρ(I)]≡ where
ρ(I) = {[p(~x) :- ρ(c)]≈ | [p(~x) :- c]≈ ∈ I}. Thus ρ ∈ uco(IntC /≡). It is also useful to
lift ρ to programs by ρ(P ) = {h :- ρ(c), g | h :- c, g ∈ P }. The following result relates
the ﬁxpoint semantics of P to that of its abstraction ρ(P ).
Theorem 3.3
Let C be a cylindric constraint system. If ρ ∈ uco(C) is a semi-morphism, then
ρ(F C (P )) ⊑ F cod(ρ) (ρ(P )).
Corollary 3.1
Let C be a semi-cylindric constraint system. If ρ ∈ uco(℘↓(C)) is a semi-morphism,
then ρ(↓(F C (P ))) ⊑ F cod(ρ) (ρ(↓(P ))).
4 Constraint logic programs with assertions
We consider programs annotated with assertions (Drabent & Maluszyński, 1988).
When considering the operational semantics of a constraint logic program, it is
natural to associate assertions with syntactic elements of the program such as predicates or the program points between body atoms. Without loss of generality, we
decorate the neck of each clause with a set of constraints C that is interpreted as
an assertion. When C is encountered, the store c is examined to determine whether
c ∈ C (modulo renaming). If c ∈ C execution proceeds normally, otherwise an error
state, denoted ♦, is entered and execution halts.
To formalise this idea, let C be a semi-cylindric constraint system and
ρ ∈ uco(℘↓(C)). The assertion language (in whatever syntactic form it takes) is
described by ρ. A clause of a constraint logic program over C with assertions over
cod(ρ) then takes the form h :- C ⋄c, g where h ∈ Atom, C ∈ cod(ρ), c ∈ C, g ∈ Goal
and ⋄ separates the assertion from the body of the clause. Notice that C is an orderideal and thus downward closed. (C can thus represent disjunctions of constraints,
but the semantics presented in this section should not be confused with a collecting
semantics.) Note also that program transformation (Puebla et al., 2000a) can be
used to express program point assertions in terms of our assertion language. To
specify the behaviour of programs with assertions, let State♦ = State ∪ {♦}, and
let CLP(P ) = {h :- c, g | h :- C ⋄ c, g ∈ P }. The following deﬁnition details how the
operational semantics for the assertion language is realised in terms of projection,
renaming and a test for inclusion.
Definition 4.1

A Backward Analysis for Constraint Logic Programs

19

Given a constraint logic program P over a semi-cylindric constraint system C with
assertions over ρ(℘↓(C)), ⇒P ⊆ State × State♦ is the least relation such that:

if p(~x′ ) :- C ′ ⋄ c′ , g ′ ∈ P
 ♦
′
s = hp(~x), g; ci ⇒P
∧ ∂~x~x (∃x~ (c)) 6∈ C ′
 ′
hg , g; c ⊗ d~x,~x′ ⊗ c′ i else if p(~x′ ) :- c′ , g ′ ≪s CLP(P )

Recall that p(~x′ ) :- c′ , g ′ ≪s CLP(P ) ensures that the clause p(~x′ ) :- c′ , g ′ does not
share any variables with s. The operational semantics of P is then deﬁned in terms
of ⇒⋆P as Aρ,C (P ) = [{[p(~x) :- c]≈ | hp(~x); 1i ⇒⋆P hǫ; ci}]≡ . The relationship between
two operational semantics is stated in the following (trivial) result.
Proposition 4.1
Aρ,C (P ) ⊑ OC (CLP(P ))
Assertions are often used as interface between behaviour that is amenable to formalisation, for example as an operational semantics, and behaviour that is less
tractable, for example, the semantics of a builtin (Puebla et al., 2000b). More to
the point, it is not always possible to infer the behaviour of a builtin from its definition, partly because builtins are often complicated and partly because builtins
are often expressed in a language such as C. Our work requires assertions for each
builtin in order to specify: its calling convention (for example, which arguments are
required to be ground) and its success behaviour (for example, which arguments
are grounded).
5 Backward fixpoint semantics for constraint logic programs with
assertions
Let P be a constraint logic program over the semi-cylindric constraint system C
with assertions over ρ(℘↓(C)). One natural and interesting question is whether the
error state ♦ is reachable (or conversely not reachable) in P from an initial state
hp(~x); ci. For a given constraint logic program P with assertions, the backward
ﬁxpoint semantics presented in this section infers a (possibly empty) set of c ∈ C
for which hp(~x); ci 6⇒⋆P ♦. The semantics formalises the informal backward analysis
sketched in section 2.
For generality, the semantics is parameterised by C and ρ. The correctness argument requires ρ to be a semi-morphism between h℘↓ (C), ⊆, ∪, ∩, C, ∅, ∃, di and
hρ(℘↓(C)), ⊆, ⊕′ , ∩, C, ρ(∅), ∃′ , d′ i. Additionally, ρ(℘↓(C)) must be a cHa, that is, it
must possess a pseudo-complement →′ . To explain, how pseudo-complement aids
backward analysis consider the problem of inferring c ∈ C for which hg; ci 6⇒⋆P ♦
where g = p1 (~x1 ), . . . , pn (~xn ). Suppose fi ∈ ρ(℘↓(C)) describes the success pattern for pi (~xi ), that is, if hpi (~xi ); 1i →⋆P hǫ; ci then c ∈ fi . Moreover, suppose
di ∈ ρ(℘↓(C)) approximates the initial call pattern for pi (~xi ), that is, if c ∈ di
then hpi (~xi ); ci 6⇒⋆P ♦. Observe that hpn−1 (~xn−1 ), pn (~xn ); ci 6⇒⋆P ♦ if c ∈ dn−1 ∩ e
and e ∩ (dn−1 ∩ fn−1 ) ⊆ dn . This follows since hpn−1 (~xn−1 ); ci 6⇒⋆P ♦ because
c ∈ dn−1 ∩ e ⊆ dn−1 . Moreover, if hpn−1 (~xn−1 ), pn (~xn ); ci ⇒⋆P hpn (~xn ); c′ i then
c′ ∈ (dn−1 ∩ e) ∩ fn−1 ⊆ dn and thus hpn (~xn ); c′ i 6⇒⋆P ♦. Putting e = ρ(∅) ensures

20

Andy King and Lunjin Lu

e ∩ (dn−1 ∩ fn−1 ) ⊆ dn and thereby achieves correctness. However, for precision,
dn−1 ∩ e should be maximised. Since ρ(℘↓(C)) is a cHa, this reduces to assigning
e = ⊕′ {e′ ∈ ρ(℘↓(C)) | e′ ∩ (dn−1 ∩ fn−1 ) ⊆ dn } = (dn−1 ∩ fn−1 ) →′ dn . In general,
without pseudo-complement, there is no unique best e that maximises precision (see
example 5.1). The construction is generalised for g = p1 (~x1 ), . . . , pn (~xn ), by putting
en = C and ei = di ∩ ((di ∩ fi ) →′ ei+1 ) = di ∩ (fi →′ ei+1 ) for 1 ≤ i < n. Then
hg; ci 6⇒⋆P ♦ if c ∈ e1 as required. This iterated application of →′ to propagate
requirements right-to-left is the very essence of the backward analysis.
Example 5.1
Returning to examples 3.2–3.5, let αEP os (C) = g{α(θ) | θ ∈ mgu(E) ∧ E ∈ C},
γEP os (f ) = ∪{C ∈ ℘↓ (Eqn) | αEP os (C) |= f } and ρEP os = γEP os ◦ αEP os .
Note that C1 ∩ C2 = γEP os (f1 ∧ f2 ) and C1 ⊕′ C2 = γEP os (f1 g f2 ) where
Ci = γEP os (fi ). By deﬁning ∃′ and d′ in an analogous way to example 3.5, a
semi-morphism ρEP os is constructed between h℘↓ (Eqn), ⊆, ∪, ∩, Eqn, ∅, ∃, di and
hρEP os (℘↓(Eqn)), ⊆, ⊕′ , ∩, Eqn, ρEP os (∅), ∃′ , d′ i. Recall that ρEP os (℘↓(Eqn)) is not
a cHa. Now consider the problem of inferring an initial c for hpn−1 (~xn−1 ), pn (~xn ); ci
within ρEP os (℘↓(Eqn)). In particular let dn−1 = γEP os (1), fn−1 = γEP os (x ⇔ y)
and dn = γEP os (x ∧ y). Then ej ∩ (dn−1 ∩ fn−1 ) ⊆ dn for e1 = γEP os (x) and
e2 = γEP os (y) but (e1 ⊕′ e2 ) ∩ (dn−1 ∩ fn−1 ) = γEP os ((x g y) ∧ 1 ∧ (x ⇔ y)) =
γEP os (x ⇔ y) 6⊆ γEP os (x∧y) = dn . Thus there is no unique e maximising precision.
Example 5.2
Identity ρid = λx.x is the trivial semi-morphism between h℘↓ (C), ⊆, ∪, ∩, C, ∅, ∃, di
and h℘↓ (C), ⊆, ∪, ∩, C, ∅, ∃, di where the pseudo-complement is given by C1 →′ C2 =
{c ∈ C | ∀c′ ✂ c . c′ ∈ C1 ⇒ c′ ∈ C2 } (Birkhoﬀ, 1967).
Example 5.3
Recall that ρP os is a semi-morphism between h℘↓ (Eqn), ⊆, ∪, ∩, Eqn, ∅, ∃, di and
hρP os (℘↓(Eqn)), ⊆, ⊕′ , ∩, Eqn, ρP os (∅), ∃′ , d′ i. Although ⊕′ 6= ∪, ρP os (℘↓(Eqn)) is
a sub-cHa of ℘↓ (Eqn) with respect to ∩ and →′ (Scozzari, to appear). Moreover,
pseudo-complement (intuitionistic implication) →′ coincides with classic implication ⇒ in the sense that C1 →′ C2 = γP os (f1 ⇒ f2 ) where Ci = γP os (fi ).
This follows since V |= f2 |= (¬f1 ) ∨ f2 and thus f1 ⇒ f2 ∈ P os. Moreover,
f1 ∧ f |= f2 iﬀ |= (f1 ∧ f ) ⇒ f2 iﬀ |= f ⇒ (¬f1 ) ∨ f2 iﬀ f |= (¬f1 ) ∨ f2 . Hence
C1 →′ C2 = ⊕′ {C ∈ ρP os (℘↓(Eqn)) | C1 ∩ C ⊆ C2 } = γP os (f1 ⇒ f2 ). Thus →′ is
ﬁnitely computable for ρP os . Finally note that ¬ and ∨ are deﬁned on Bool rather
than P os since ¬f 6∈ P os iﬀ f ∈ P os.
Example 5.4
Now consider the problem of inferring an initial c for hpn−1 (~xn−1 ), pn (~xn ); ci within
ρP os (℘↓(Eqn)). Analogous to example 5.1, let dn−1 = γP os (1), fn−1 = γP os (x ⇔ y)
and dn = γP os (x ∧ y). Then ej ∩ (dn−1 ∩ fn−1 ) ⊆ dn for e1 = γP os (x) and e2 =
γP os (y) and (e1 ⊕′ e2 )∩(dn−1 ∩fn−1 ) = γP os ((x∨y)∧1∧(x ⇔ y)) = γP os (x∧y) = dn .
Thus there is a unique e maximising precision.

A Backward Analysis for Constraint Logic Programs

21

Since hρ(℘↓(C)), ⊆, ⊕′ , ∩, C, ρ(∅), ∃′ , d′ i is a cylindric constraint system, it follows
that e ⊆ ∃′x (e) for all e ∈ ρ(℘↓(C)). A consequence of e ⊆ ∃′x (e) is that projection
approximates from above. Approximation from above, however, is not entirely appropriate for backward analysis. In particular, observe that if hg; ci 6⇒⋆P ♦ for all
c ∈ e, then it does not necessarily follow that hg; ci 6⇒⋆P ♦ for all c ∈ ∃′x (e). What
is required is a dual notion of projection, say denoted ∀′ , that approximates from
below. Then hg; ci 6⇒⋆P ♦ for all c ∈ ∀′x (e). Although ∀′ is an abstract operator, the
concept is deﬁned for an arbitrary cylindric constraint system for generality.
Definition 5.1
If hC, ✂, ⊕, ⊗, 1, 0, ∃, di is a cylindric constraint system and x ∈ V then ∀x : C → C
is a monotonic operator such that: ∃x (∀x (c)) ✂ c and c ✂ ∀x (∃x (c)) for all c ∈ C.
Recall that ∃x is monotonic and thus α is the lower adjoint of γ and γ is the upper
adjoint of α. More exactly, it follows that ∀x can be automatically constructed from
∃x by ∀x (c) = ⊕{c′ ∈ C | ∃x (c′ ) ✂ c}. Observe that this ensures that ∀x is the most
precise projection operator from below. For succinctness, deﬁne ∀{x1 ,...,xn } (c) =
∀x1 (. . . (∀xn (c))) and ∀X (c) = ∀F V (c)\X (c).
Example 5.5
For ρid , let ∀′x (C) = ↓({c ∈ C | ∃x (c) = c}).
Example 5.6
For ρP os , let ∀′x (C) = γP os (f ′ ) if f ′ ∈ P os otherwise ∀′x (C) = γP os (0) where C =
γP os (f ) and f ′ = f [x 7→ 0] ∧ f [x 7→ 1]. Observe that ∃x (f )[x 7→ 0] ∧ ∃x (f )[x 7→ 1] =
∃x (f ) and hence C ⊆ ∃′x (C) = ∀′x (∃′x (C)) as required. Moreover, if ∀′x (C) = γP os (0)
then ∃′x (∀′x (C)) = γP os (0) ⊆ C. Otherwise ∃x (f [x 7→ 0] ∧ f [x 7→ 1]) = f [x 7→
0] ∧ f [x 7→ 1] |= f . Thus ∃′x (∀′x (C)) ⊆ C as required. Finally, note that ∀′x is ﬁnitely
computable for ρP os . For example if Ci = γP os (fi ), f1 = (x ⇐ y), f2 = (x ∧ y) and
f3 = (x ∨ y), then ∀′x (Ci ) = γP os (fi′ ) where f1′ = 0, f2′ = 0 and f3′ = y.
Backward analysis can now be formalised as follows.
Definition 5.2
Given a constraint logic program P over a semi-cylindric constraint system C with
assertions over ρ(℘↓(C)), the operator DPρ,C : Intcod(ρ) → Intcod(ρ) is deﬁned by:


∀
[p(~x) :- e]≈ ∈ E
.








∀
p(~x) :- C ⋄ c, p1 (~x1 ), . . . , pn (~xn ) ∈ P
.





n
[
∃
{[pi (~xi ) :- fi ]≈ }i=1 ⊆ F
.
ρ,C
E
DP (D) =
∃
{[pi (~xi ) :- di ]≈ }ni=1 ⊆ D
.





′




e
=
C
∧
e
=
d
∩
(f
→
e
)
∧
n+1
i
i
i
i+1




′


′
e ⊆ ∀~x (e0 ) ∧ e0 = C ∩ (ρ(↓(c)) → e1 )
where [F ]≡ = F cod(ρ) (ρ(↓(CLP(P )))).

Since D is parameterised by ρ and C it can interpreted as a backward analysis framework. D requires F , the success patterns of the program obtained by discarding the
assertions, to be pre-computed. D considers each clause in the program in turn and

22

Andy King and Lunjin Lu

calculates those states which ensure that the clause (and those it calls) will not violate an assertion. An abstraction which characterises these states is calculated by
propagating requirements, represented as abstractions, right-to-left by repeated application of pseudo-complement. Projection from below then computes those states
which, when restricted to the head variables, still ensure that no error arises in the
clause (and those it calls). Repeated application of D yields a decreasing sequence
of interpretations.
The operator DPρ,C lifts to Intcod(ρ) / ≡ by DPρ,C ([D]≡ ) = [DPρ,C (D)]≡ . Since
hcod(ρ), ⊑, ⊔, ⊓i is a complete lattice, DPρ,C will possess a gfp if DPρ,C is monotonic.
The existence of gfp(DPρ,C ) is guaranteed by the following result since co-continuity
implies monotonicity.
Proposition 5.1
DPρ,C : Intcod(ρ) /≡ → Intcod(ρ) /≡ is co-continuous.
Since gfp(DPρ,C ) exists, a backward ﬁxpoint semantics can be deﬁned
Dρ,C (P ) = gfp(DPρ,C ) and computed by lower Kleene iteration. To establish a connection between Dρ,C (P ) and the operational semantics of P , it is useful to annotate the goals of a state with their depth in the computation tree. To formalise this idea ⇒P is lifted to the annotated states Conf♦ = Conf ∪ {♦} where
Conf = Goal × C × N⋆ to obtain the transition system ⇛P .
Definition 5.3
Given a constraint logic program with assertions P over a semi-cylindric constraint
system C, ⇛P ⊆ Conf × Conf♦ is the least relation such that:

♦
if hp(~x), g; ci ⇒P ♦
hp(~x), g; c; n · hi ⇛P
′
hg ′ , g; c′ ; (n + 1)|g | · hi if hp(~x), g; ci ⇒P hg ′ , g; c′ i
′

The sequence (n + 1)|g | denotes |g ′ | concatenations of n + 1. The following result
relates the depth of the goals of the annotated states to the iterates obtained by
lower Kleene iteration. Informally, it says that if a constrained atom p(~x) :- e occurs
in the interpretation obtained by applying D k times, and e characterises an initial
state (in a certain sense), and the depth of the goals in a derivation starting at the
initial state does not exceed k, then the derivation will not violate an assertion.
The main safety theorem ﬂows out of this result.
Lemma 5.1
Let hp(~y ); c′′ ; 1i = s1 ⇛⋆P sn ⇛P ♦, si = hgi ; ci ; hi i and (DPρ,C )k (⊤) = [Dk ]≡ .
If max({max(hi ) | 1 ≤ i ≤ n}) ≤ k and [p(~y ) :- e]≈ ∈ Dk then ∃y~ (c′′ ) 6∈ ∃y~ (e).
Theorem 5.1
If Dρ,C (P ) = [D]≡ , [p(~y ) :- e]≈ ∈ D and c ∈ ∃y~ (e) then hp(~y ); ci 6⇒⋆P ♦.
6 Experimental evaluation
In order to evaluate the usefulness of the analysis framework presented in section 5,
a backward P os analyser has been constructed for inferring calling modes. The

A Backward Analysis for Constraint Logic Programs

23

ﬁxpoint component of the analyser is coded in SICStus Prolog 3.8.3. The domain
operations are coded in C and are essentially the binary decision diagram (BDD)
routines written by Armstrong and Schachte (Armstrong et al., 1998). The analyser
takes, as input, a program written in a declarative subset of ISO Prolog. It outputs
a mode for each program predicate. The safety result of theorem 5.1 ensures that
if a call to a predicate is at least as instantiated as the inferred mode, then the call
will not violate an instantiation requirement. Modes are expressed as grounding
dependencies (Armstrong et al., 1998).
The implementation follows the framework deﬁned in section 5 very closely. The
analyser was straightforward to implement as it is essentially two bottom-up ﬁxpoint computations: one for F and the other for D. The only subtlety is in handling
the builtins. For each builtin, it is necessary to select a grounding dependency that
is suﬃcient for avoiding an instantiation error. This is an lower approximation (the
required mode of table 1). It is also necessary to specify behaviour on success. This
is an upper-approximation (the success mode of table 1). The lower approximations
are the assertions that are added to Prolog program to obtain a constraint logic
program with assertions.
Interestingly, the success mode does not always entail the required mode. Univ
(=..) illustrates this. A suﬃcient but not necessary condition for univ not to error is
that either the ﬁrst or second argument is ground. This cannot be weakened in P os
(but could be weakened in a type dependency domain (Codish & Lagoon, 2000)
that expressed rigid lists). The success mode is that the ﬁrst argument is ground
iﬀ the second argument is ground (which does not entail the required mode). Note
too that keysort and sort error if their ﬁrst argument is free. A suﬃcient mode
for expressing this requirement is that the ﬁrst argument is ground. Again, this
requirement cannot be weakened in P os.
The analyser has been applied to some standard Prolog benchmarks which can
be found at http://www.oakland.edu/∼l2lu/benchmarks-BG.zip. The results of the
analysis, that is, the calling modes for the predicates in the smaller benchmarks, are
given in table 2. The results, though surprising in some cases (see sort of permSort
and insert of treesort for example) have been veriﬁed by hand and appear to be
optimal for P os. The analysis, of course, can be applied to larger programs (though
it becomes very diﬃcult to verify the results by hand) and table 3 demonstrates
that the analysis scales smoothly to medium-scale programs at least. The table lists
the larger benchmarks (which possibly include some unreachable code) in terms of
increasing size measured by the total number of atoms in the source. The abs
column records the time in milliseconds required to read, parse and normalise the
source into the ground program representation used by the analyser; lfp is the time
needed to compute the ﬁxpoint characterising the success modes; gfp is the time
needed to compute the calling modes; and ﬁnally sum is the total analysis time.
This includes the (usually negligible) overhead of annotating the source with the
modes required by builtins. Timings were performed on a Dell GX200 1GHz PC
with 128 MB memory running Windows 2000. The timings suggest that the analysis
is practical at least for medium-scale programs (though the running time for BDDs
can be sensitive to the particular dependencies that arise). Moreover, with a state-

24

Andy King and Lunjin Lu
builtin
t1 == t2 , t1 \== t2 , t1 @< t2 , t1 @> t2 ,
t1 @=< t2 ,
t1 @>= t2 ,
t1 \= t2 ,
!,
compound(t1 ), display(t1 ), listing, listing(t1 ),
nl, nonvar(t1 ), print(t1 ), portray clause(t1 ),
read(t1 ), repeat, true, var(t1 ), write(t1 ),
writeq(t1 )
atom(t1 ), atomic(t1 ), compare(t1 , t2 , t3 ),
ﬂoat(t1 ), ground(t1 ), integer(t1 ), number(t1 )
length(t1 , t2 )
statistics(t1 , t2 )
abort, fail, false
keysort(t1 , t2 ), sort(t1 , t2 )
tab(t1 ), put(t1 )
t1 is t2
t1 =:= t2 , t1 =\= t2 , t1 < t2 , t1 > t2 ,
t1 =< t2 , t1 >= t2
arg(t1 , t2 , t3 )
name(t1 , t2 )
t1 =.. t2
functor(t1 , t2 , t3 )

required mode
true

success mode
true

true

f1

true
true
true
f1
f1
f2
g1

f2
g1
f alse
g2
f1
g1
g1

g1
g4
g4
g5

g3
g1
g2
g6

Table 1. Abstracting builtins where fi = ∧var(ti ), g1 = f1 ∧ f2 , g2 = f1 ⇔ f2 ,
g3 = f1 ∧ (f2 ⇒ f3 ), g4 = f1 ∨ f2 , g5 = f1 ∨ (f2 ∧ f3 ) and g6 = f2 ∧ f3 .
of-the-art GER factorised BDD package (Bagnara & Schachte, 1999) the analysis
would be faster. Interestingly, the time to compute the lfp often dominates the
whole analysis. BDD widening will be required to analyse very large applications
but this is a study within itself (Heaton et al., 2000).
7 Related work
Our work was motivated by the recent revival of interest in logic programming
with assertions (Boye et al., 1997; Puebla et al., 2000a). For example, (Puebla
et al., 2000b) argues that it is useful to trap an unexpected call to a predicate with
an assertion otherwise a program may error at a point that is far from the source of
the problem. Moreover, (Puebla et al., 2000a) observe that predicates are normally
written with an expectation on the initial calling pattern, and hence provide an
entry assertion to make the, moding say, of the top-level queries explicit. Our
work shows how entry assertions can be automatically synthesised which ensure
that instantiation errors do not occur while executing the program.
The most closely related work concerns the demand analysis of ccp (Debray, 1993;
Falaschi et al., 2000). A demand analysis for the ccp language Janus (Saraswat et al.,
1990) is proposed in (Debray, 1993) which determines whether or not a predicate is
uni-modal. A predicate is uni-modal iﬀ the argument tuple for each clause share the
same minimal pattern of instantiation necessary for reduction. The demand analysis
of a predicate simply traverses the head and guard of each clause to determine
the extent to which arguments have to be instantiated. Body atoms need not be
considered so the analysis does not involve a ﬁxpoint computation. A related paper

A Backward Analysis for Constraint Logic Programs
benchmark
bubblesort

dnf

heapify

predicate
sort(x1 , x2 )
ordered(x1 )
append(x1 , x2 , x3 )
go
dnf(x1 , x2 )
norm(x1 , x2 )
literal(x1 )
greater(x1 , x2 )
adjust(x1 , x2 , x3 , x4 )

permSort

queens

quicksort

treeorder

treesort

heapify(x1 , x2 )
select(x1 , x2 , x3 )
ordered(x1 )
permutation(x1 , x2 )
sort(x1 , x2 )
noattack(x1 , x2 , x3 )
safe(x1 )
delete(x1 , x2 , x3 )
perm(x1 , x2 )
queens(x1 , x2 )
append(x1 , x2 , x3 )
qsort(x1 , x2 )
partition(x1 , x2 , x3 , x4 )
member(x1 , x2 )
select(x1 , x2 , x3 )
split(x1 , x2 , x3 , x4 )
split(x1 , . . . , x7 )
visits2tree(x1 , x2 , x3 )
v2t(x1 , x2 , x3 )
tree to list aux(x1 , x2 , x3 )
tree to list(x1 , x2 )
list to tree(x1 , x2 )
insert list(x1 , x2 , x3 )
insert(x1 , x2 , x3 )
treesort(x1 , x2 )

25

mode
x1
x1
true
true
true
true
true
x
1 ∧ x2


(x1 ∧ x4 )
∨
 (x1 ∧ x2 ∧ x3 ) ∨ 
(¬x2 ∧ ¬x3 ∧ x4 )
x1
true
x1
true
x1 ∨ x2
x1 ∧ x2 ∧ x3
x1
true
true
x1 ∨ x2
true
x1
x2 ∧ (x1 ∨ (x3 ∧ x4 ))
true
true
true
true
true
true
true
true
x1
x1 ∧ x2
x1 ∧ (x2 ∨ x3 )
x1

Table 2. Precision of the Mode Analysis (small benchmarks)
(Debray et al., 1992) presents a goal-dependent (forward) analysis that detects those
ccp predicates which can be scheduled left-to-right without deadlock. If assertions
are used to approximate synchronisation, then the analysis described in this paper
can be re-interpreted as a backward suspension analysis of ccp under left-to-right
scheduling.
When reasoning about module interaction it can be advantageous to reverse
the traditional deductive approach to abstract interpretation that is based on the
abstract unfolding of abstract goals. In particular (Giacobazzi, 1998) shows how
abduction and abstraction can be combined to compute those properties that one
module must satisfy to ensure that its composition with another fulﬁls certain
requirements. Abductive analysis can, for example, determine how an optimisation

26
file
astar
ﬀt
knight
browse wamcc
cal wamcc
life
crypt wamcc
cry mult
browse
bid
disj r
consultant
ncDP
tsp
elex scanner
robot
sorts
cs2
scc
bp0-6
bnet
jons
mathlib
intervals
barnes hut

Andy King and Lunjin Lu
size
100
104
105
106
108
110
113
118
125
128
148
151
156
162
165
165
172
175
175
201
205
222
226
230
240

abs lfp gfp sum
file
10 10 0 20
tictactoe
20
0 10 30
jons2
10
0 0 10
kalah
10
0 0 10
draw
10 10 0 20
cs r
10 10 10 30
reducer
10
0 0 10
sdda
10 10 10 30
bryant
10 10 0 20
ga
10 10 0 20
neural
30
0 10 40
press
20
0 10 30
peep
10 10 0 20
nbody
30 20 10 60
eliza
20 10 0 30
read
10 10 0 20 simple analyzer
0 10 10 20
ann
30 10 10 50
diﬀsimpsv
10 141 0 151
arch1
20 10 0 30
asm
20 20 0 40
poker
40
0 10 50
pentomino
10 10 0 20
chat
20 10 10 40
sim v5-2
40 30 40 110
semigroup

size
258
261
269
289
311
320
336
349
363
378
381
414
421
432
434
512
547
681
692
800
962
981
1037
1308
2328

abs
lfp gfp sum
20
10
10
40
20
10
0
30
30
10
20
60
70
91
40 201
40
20
10
70
40
30
0
70
20
21
0
41
30 120
21 171
50
30
20 100
30
10
0
40
30
20
0
50
50
20
10
80
40
20
20
80
50
20
0
70
40
20
10
70
90 701
20 811
50
30
10
90
61 100
0 161
50
40
10 100
60
40
30 130
81
70
10 161
50
40
80 170
411 1422 1082 2915
80
70
0 150
180
90
60 350

Table 3. Speed of the Mode Analysis (medium-scale benchmarks)

in one module depends on a predicate deﬁned in another module. Abductive analysis
is related to the backward analysis presented in this paper since abduction is the
inverse image of a forward semantics whereas pseudo-complement is the inverse
image of conjunction – the basic computational step in forward (and backward)
semantics.
The termination inference engine of (Genaim & Codish, 2001) decomposes the
cTI analyser of (Mesnard, 1996) into two components: a termination checker (Codish
& Taboch, 1999) and the backward analysis described in this paper. First, the termination inference engine computes a set of binary clauses which describe possible
loops in the program with size relations. Second, a Boolean function is inferred
for each predicate that describes moding conditions suﬃcient for each loop to only
be executed a ﬁnite number of times. Third, the backward analysis described in
this paper is applied to infer initial modes by calculating a greatest ﬁxpoint which
guarantee that the moding conditions hold and thereby assure termination. Interestingly, the cTI analyser involves a µ-calculus solver to compute the greatest
ﬁxpoint of an equivalent (though more complex) system of equations. This seems
to suggest that greatest ﬁxpoints are important in backward analysis.
Cousot and Cousot (Cousot & Cousot, 1992) explain how a backward collecting semantics can be deployed to precisely characterise states that arise in ﬁnite
SLD-derivations. First, they present a forward collecting semantics that records the

A Backward Analysis for Constraint Logic Programs

27

descendant states that arise from a set of initial states. Second, they present a dual
(backward) collecting semantics that records those states which occur as ascendant
states of the ﬁnal states. By combining both semantics, they characterise the set
of descendant states of the initial states which are also ascendant states of the ﬁnal states of the transition system. This use of backward analysis is primarily as
a device to improve the precision of a classic goal-dependent analysis. Our work is
more radical in the sense that it shows how a bottom-up analysis performed in a
backward fashion, can be used to characterise initial queries. Moreover it is used
for lower approximation rather than upper approximation.
Mazur, Janssens and Bruynooghe (Mazur et al., 2000) present a kind of ad hoc
backward analysis to derive reuse conditions from a goal-independent reuse analysis
for Mercury (Somogyi et al., 1996). The analysis propagates reuse information from
a point where a structure is decomposed in a clause to the point where the clause
is invoked in its parent clause. This is similar in spirit to how demand is passed
from a callee to a caller in the backward analysis described in this paper. However,
the reuse analysis does not propagate information right-to-left across a clause using
pseudo-complement, and so one interesting topic for future work will to be relate
these two analyses. Another matter for future work, will be to investigate the extent
to which our backward mode analysis can be reconstructed by inverting abstract
functions (Hughes & Launchbury, 1994).

8 Conclusion
We have shown how abstract interpretation, and speciﬁcally a backward analysis,
can infer moding properties which if satisﬁed by the initial query, come with the
guarantee that the program and query cannot generate instantiation errors. Backward analysis has other applications in termination inference and also in inferring
queries for which the builtins called from within the program behave predictably in
the presence of rational trees. The analysis is composed of two bottom-up ﬁxpoint
calculations, a lfp and a gfp, both of which are straightforward to implement. The
lfp characterises success patterns. The gfp, uses these success patterns to infer safe
initial calling patterns. It propagates moding requirements right-to-left, against the
control-ﬂow, using the pseudo-complement operator. This operator ﬁts with backward analysis since it enables moding requirements to be minimised (maximally
weakened) in right-to-left propagation. This operator, however, requires that the
computational domain be closed under Heyting completion (or equivalently condense). This requirement seems reasonable because disjunctive dependencies occur
frequently in right-to-left propagation and therefore signiﬁcant precision would be
lost if the requirement were relaxed. Experimental evaluation has demonstrated that
the analysis is practical in the sense that it can infer calling modes for mediumscaled programs. Finally, our work adds weight to the belief that condensing is an
important property in the analysis of logic programs.

28

Andy King and Lunjin Lu
Acknowledgements

We thank Maurice Bruynooghe, Mike Codish, Samir Genaim, Roberto Giacobazzi,
Jacob Howe, Fred Mesnard, Germán Puebla and Francesca Scozzari for helpful discussions. We would also like to thank the anonymous referees for their comments
and Peter Schachte for his BDD analyser. We also thank Roberto Bagnara for the
use of some of the China benchmarks. This work was supported, in part, by EPSRC
grant GR/MO8769.

References
Armstrong, T., Marriott, K., Schachte, P., & Søndergaard, H. (1998). Two Classes of
Boolean Functions for Dependency Analysis. Science of Computer Programming, 31(1),
3–45.
Bagnara, R., & Schachte, P. (1999). Factorizing Equivalent Variable Pairs in ROBDDBased Implementations of Pos. Pages 471–485 of: International Conference on Algebraic
Methodology and Software Technology. Lecture Notes in Computer Science, vol. 1548.
Springer-Verlag.
Bagnara, R., Zaﬀanella, E., Gori, R., & Hill, P. M. (2001). Boolean Functions for FiniteTree Dependencies. Pages 575–589 of: International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Lecture Notes in Artiﬁcial Intelligence, vol.
2250. Springer-Verlag.
Birkhoﬀ, G. (1967). Lattice Theory. AMS Press.
Bossi, A., Gabbrielli, M., Levi, G., & Martelli, M. (1994). The s-Semantics Approach:
Theory and Applications. The Journal of Logic Programming, 19/20, 149–197.
Boye, J., Drabent, W., & Maluszyński, J. (1997). Declarative Diagnosis of Constraint
Programs: an Assertion-based Approach. Pages 123–141 of: Proceedings of the Third
International Workshop on Automated Debugging. University of Linköping Press.
Codish, M., & Lagoon, V. (2000). Type Dependencies for Logic Programs using ACIuniﬁcation. Theoretical Computer Science, 238, 131–159.
Codish, M., & Taboch, C. (1999). A Semantic Basis for the Termination Analysis of Logic
Programs. The Journal of Logic Programming, 41(1), 103–123.
Cousot, P., & Cousot, R. (1982). Inductive Principles for Proving Invariance Properties of
Programs. Pages 75–119 of: Tools and Notions for Program Construction. Cambridge
University Press.
Cousot, P., & Cousot, R. (1992). Abstract Interpretation and Application to Logic Programs. The Journal of Logic Programming, 13(2–3), 103–179.
Debray, S. (1993). QD-Janus: a Sequential Implementation of Janus in Prolog. Software
Practice and Experience, 23(12), 1337–1360.
Debray, S., Gudeman, D., & Bigot, P. (1992). Detection and Optimization of Suspensionfree Logic Programs. The Journal of Logic Programming, 29(1–3), 171–194.
Drabent, W., & Maluszyński, J. (1988). Inductive Assertion Method for Logic Programs.
Theoretical Computer Science, 59(1), 133–155.
Dyber, P. (1991). Inverse Image Analysis Generalises Strictness Analysis. Information
and Computation, 90(2), 194–216.
Falaschi, M., Hicks, P., & Winsborough, W. (2000). Demand Transformation Analysis for
Concurrent Constraint Programs. The Journal of Logic Programming, 41(3), 185–215.
Filé, G., & Ranzato, F. (1994). Improving Abstract Interpretations by Systematic Lifting

A Backward Analysis for Constraint Logic Programs

29

to the Powerset. Pages 655–669 of: International Logic Programming Symposium. MIT
Press.
Genaim, S., & Codish, M. (2001). Inferring Termination Conditions for Logic Programs
using Backwards Analysis. Pages 681–690 of: International Conference on Logic for
Programming, Artificial Intelligence and Reasoning. Lecture Notes in Artiﬁcial Intelligence, vol. 2250. Springer-Verlag.
Giacobazzi, R. (1998). Abductive Analysis of Modular Logic Programs. Journal of Logic
and Computation, 8(4), 457–484.
Giacobazzi, R., & Scozzari, F. (1998). A Logical Model for Relational Abstract Domains.
ACM Transactions on Programming Languages and Systems, 20(5), 1067–1109.
Giacobazzi, R., Debray, S., & Levi, G. (1995). Generalized Semantics and Abstract Interpretation for Constraint Logic Programs. The Journal of Logic Programming, 25(3),
191–248.
Giacobazzi, R., Ranzato, F., & Scozzari, F. (1998). Building Complete Abstract Interpretations in a Linear Logic-based Setting. Pages 215–229 of: Static Analysis Symposium.
Lecture Notes in Computer Science, vol. 1503. Springer-Verlag.
Hall, C., & Wise, D. (1989). Generating Function Versions with Rational Strictness
Patterns. Science of Computer Programming, 12, 39–74.
Heaton, A., Abo-Zaed, M., Codish, M., & King, A. (2000). A Simple Polynomial Groundness Analysis for Logic Programs. The Journal of Logic Programming, 45(1–3), 143–156.
Hughes, R. J. M., & Launchbury, J. (1994). Reversing Abstract Interpretations. Science
of Computer Programming, 22, 307–326.
Jaﬀar, J., & Maher, M. J. (1994). Constraint Logic Programming: A Survey. The Journal
of Logic Programming, 19/20, 503–581.
Langen, A. (1991). Advanced Techniques for Approximating Variable Aliasing in Logic
Programs. Ph.D. thesis, Computer Science Department, Los Angeles, California 900890782.
Marriott, K., & Søndergaard, H. (1993). Precise and Eﬃcient Groundness Analysis for
Logic Programs. ACM Letters on Programming Languages and Systems, 2(4), 181–196.
Mazur, N., Janssens, G., & Bruynooghe, M. (2000). A Module Based Analysis for Memory
Reuse in Mercury. Pages 1255–1269 of: Computational Logic. Lecture Notes in Artiﬁcial
Intelligence, vol. 1861.
Mesnard, F. (1996). Inferring Left-terminating Classes of Queries for Constraint Logic
Programs. Pages 7–21 of: Joint International Conference and Symposium on Logic
Programming. MIT Press.
Mesnard, F., & Neumerkel, U. (2001). Applying Static Analysis Techniques for Inferring
Termination Conditions of Logic Programs. Pages 93–110 of: Static Analysis Symposium. Lecture Notes in Computer Science, vol. 2126. Springer-Verlag.
Mycroft, A. (1981). Abstract Interpretation and Optimising Transformations for Applicative Programs. Ph.D. thesis, University of Edinburgh.
Puebla, G., Bueno, F., & Hermenegildo, M. (2000a). An Assertion Language for Constraint
Logic Programs. Pages 23–61 of: Analysis and Visualization Tools for Constraint Programming. Lecture Notes in Computer Science, vol. 1870. Springer-Verlag.
Puebla, G., Bueno, F., & Hermenegildo, M. (2000b). A Generic Preprocessor for Program
Validation and Debugging. Pages 63–107 of: Analysis and Visualization Tools for Constraint Programming. Lecture Notes in Computer Science, vol. 1870. Springer-Verlag.
Saraswat, V., Kahn, K., & Levy, J. (1990). Janus: a Step Towards Distributed Constraint
Programming. Pages 431–446 of: North American Conference on Logic Programming.
MIT Press.

30

Andy King and Lunjin Lu

Scozzari, F. (to appear). Logical Optimality of Groundness Analysis. Theoretical Computer
Science.
Somogyi, Z., Henderson, F., & Conway, T. (1996). The execution algorithm of Mercury,
an eﬃcient purely declarative logic programming language. The Journal of Logic Programming, 29(1–3), 17–64.
van Dalen, D. (1997). Logic and Structure. Springer.
Wadler, P., & Hughes, R. J. M. (1987). Projections for Strictness Analysis. Pages 385–407
of: Functional Programming and Computer Architecture. Lecture Notes in Computer
Science, vol. 274. Springer-Verlag.

A Backward Analysis for Constraint Logic Programs

31

A Proof appendix
Proof for proposition 3.1
℘↓(C)
′
Proof by induction. Let I0 = ∅, I0′ = ∅, Ik+1 = FPC (Ik ) and Ik+1
= F↓(P ) (Ik′ ). To
show ↓(Ik ) ⊑ Ik′ since then it follows that ↓(lfp(FPC )) = ↓(⊔k∈N Ik ) ⊑ ⊔k∈N ↓(Ik ) ⊑
℘↓(C)

⊔k∈N Ik′ = lfp(F↓(P ) ). The base case is trivial so suppose ↓(Ik ) ⊑ Ik′ .
Let [p(~x) :- c′ ]≈ ∈ Ik+1 . Then there exists p(~x) :- c, p1 (~x1 ), . . . , pn (~xn ) ∈ P and
{[pi (~xi ) :- ci ]≈ }ni=1 ⊆ Ik such that c′ = c ⊗ ⊗ni=1 ∃x~i (ci ). Observe that ↓(c′ ) ⊆
↓(c) ∩ ∩ni=1 ↓(∃x~i (ci )) ⊆ ↓(c) ∩ ∩ni=1 ∃x~i (↓(ci )). But by the inductive hypothesis, there
′
exist {[pi (~xi ) :- c′i ]≈ }ni=1 ⊆ Ik′ such that ↓(ci ) ⊆ c′i . Hence [p(~x) :- c′′ ]≈ ∈ Ik+1
such
′
′′
′
that ↓(c ) ⊆ c so that Ik+1 ⊑ Ik+1 and the result follows.
Proof for theorem 3.3
The proof tactic is analogous to that used for proposition 3.1.
Proof for corollary 3.1
Let C be a semi-cylindric constraint system and ρ ∈ uco(℘↓(C)) be a semi-morphism.
↓
By proposition 3.1 it follows that ↓(F C (P )) ⊑ F ℘ (C) (↓(P )) and hence ρ(↓(F C (P ))) ⊑
↓
↓
ρ(F ℘ (C) (↓(P ))) and by theorem 3.3 ρ(F ℘ (C) (↓(P ))) ⊑ F cod(ρ) (ρ(↓(P ))) and so the
result follows.
Proof for proposition 5.1
Let Dn+1 ⊑ Dn for all n ∈ N. Put En = ∪{Dl | l ≥ n} and E = ∩{En |
n ∈ N}. Since Dn+1 ⊑ Dn observe that En ≡ Dn for all n ∈ N and hence
DPρ,C (⊓{[Dn ]≡ | n ∈ N}) = DPρ,C (⊓{[En ]≡ | n ∈ N}) = DPρ,C ([E]≡ ) = [DPρ,C (E)]≡ =
[∩{DPρ,C (En ) | n ∈ N}]≡ = ⊓{[DPρ,C (En )]≡ | n ∈ N} = ⊓{DPρ,C ([En ]≡ ) | n ∈ N} =
⊓{DPρ,C ([Dn ]≡ ) | n ∈ N}.
Proof for lemma 5.1
Proof by (double) induction. Let hp(~y ); c′′ ; 1i = s1 ⇛⋆P sn ⇛P ♦, si = hgi ; ci ; hi i
and suppose (DPρ,C )k (⊤) = [Dk ]≡ . The outer induction is on k.
base case: Suppose max({max(hi ) | 1 ≤ i ≤ n}) ≤ 1 and [p(~y ) :- e]≈ ∈ D1 . Thus
s1 ⇛P ♦ so that s1 ⇒P ♦ and hence there exists p(~x′ ) :- C ′ ⋄ c′ , g ′ ∈ P such that
′
∂y~~x (∃y~ (c′′ )) 6∈ C ′ . Then [p(~x′ ) :- e′ ]≈ ∈ D1 where ∃~z (d~z,~y ⊗ e) = ∃~z (d~z,~x′ ⊗ e′ ) and
var(~z) ∩ (var(~y ) ∪ F V (e) ∪ var(~x′ ) ∪ F V (e′ )) = ∅. Observe that e′ ⊆ ∀~x′ (C ′ ) and
′
′
thus ∂y~~x (∃y~ (e)) = ∃~x′ (e′ ) ⊆ ∃~x′ (∀~x′ (C ′ )) = ∀x~ ′ (C ′ ) ⊆ C ′ . Hence ∂y~~x (∃y~ (c′′ )) 6∈
′
∂y~~x (∃y~ (e)) so that ∃y~ (c′′ ) 6∈ ∃y~ (e) as required.
inductive case: Suppose k = max({max(hi ) | 1 ≤ i ≤ n}) > 1 and [p(~y ) :- e]≈ ∈ Dk .
Suppose, for the sake of a contradiction, that ∃y~ (c′′ ) ∈ ∃y~ (e). Since k > 1 there
exists w = p(~x) :- C ⋄ c, p1 (~x1 ), . . . , pl (~xl ) ∈ P , ϕ ∈ Ren such that ϕ(CLP(w)) =
p(~x′ ) :- c′ , p1 (~x′1 ), . . . , pl (~x′l ) ≪s1 CLP(P ) and s2 = hp1 (~x′1 ), . . . , pl (~x′l ); c′1 ; 2l i and
c′1 = c′′ ⊗ dy~,~x′ ⊗ c′ . Suppose hp1 (~x′1 ); c′1 i ⇒⋆P hǫ; c′2 i, . . . , hpm (~x′m ); c′m i ⇒⋆P ♦.
Without loss of generality assume F V (CLP(w))∩F V (c′i ) = ∅ for all i ∈ [1, m]. Let
~v = ~x·~x1 · · · ~xl and ~v ′ = ~x′ ·~x′1 · · · ~x′l . Let gi′ ∈ C such that hpi (~x′i ); 1i →⋆P hǫ; gi′ i and
c′i+1 = c′i ⊗gi′ for all i ∈ [1, m). For all i ∈ [1, m), put gi = ∂~x~x′i (gi′ ). Put c1 = ∂~v~v′ (c′1 )
i

and for all i ∈ [2, m], put ci = ∂~x~x′i (c′i ). Then ci+1 = ci ⊗ gi for all i ∈ [1, m).
i

32

Andy King and Lunjin Lu

Let OC (P ) = [F ]≡ . By proposition 4.1, [pi (~xi ) :- gi ]≈ = [pi (~x′i ) :- gi′ ]≈ ∈ F for all
i ∈ [1, m). By theorem 3.2, OC (P ) = F C (P ) and by corollary 3.1, ρ(↓(F C (P ))) ⊑
F cod(ρ) (ρ(↓(P ))). Thus for i ∈ [1, m) there exists [pi (~xi ) :- fi ]≈ ∈ F such that
ρ(↓(gi )) ⊆ fi . Put fi = 0 for all i ∈ [m, l] to ensure [pi (~xi ) :- fi ]≈ ∈ F for
all i ∈ [m, l]. Let [pi (~xi ) :- di ]≈ ∈ Dk for all i ∈ [1, l]. Finally put en+1 = C,
ei = di ∩ (fi →′ ei+1 ) for all i ∈ [1, l] and e0 = C ∩ (ρ(↓(c)) →′ e1 ). The inner
induction is on i and is used to show ρ(↓(ci )) ⊆ ei for all i ∈ [1, m].
base case: Now c1 = ∂~v~v′ (c′1 ) ✂ ∂y~~x (∃y~ (c′′ )) ∈ C. Thus ρ(↓(c1 )) ⊆ C. Furthermore,
c1 = ∂~v~v′ (c′1 ) ✂ ∂~v~v′ (c′ ) = c. Thus ρ(↓(c1 )) ⊆ ρ(↓(c)). Moreover, c1 ✂ ∂y~~x (∃y~ (c′′ )) ∈
∂y~~x (∃y~ (e)) ⊆ ∀~x (e0 ) ⊆ e0 . Thus ρ(↓(c1 )) ⊆ e0 . However, e0 = C∩(ρ(↓(c)) →′ e1 ).
Thus ρ(↓(c1 )) ⊆ C ∩(ρ(↓(c)) →′ e1 ) and ρ(↓(c1 )) ⊆ ρ(↓(c1 ))∩C ∩(ρ(↓(c)) →′ e1 )
= ρ(↓(c1 )) ∩ (ρ(↓(c)) →′ e1 ) = ρ(↓(c1 )) ∩ ρ(↓(c)) ∩ (ρ(↓(c)) →′ e1 ) = ρ(↓(c1 )) ∩
ρ(↓(c)) ∩ e1 = ρ(↓(c1 )) ∩ e1 . Therefore ρ(↓(c1 )) ⊆ e1 as required.
inductive case: Suppose ρ(↓(ci )) ⊆ ϕ(ei ). Now ρ(↓(ci+1 )) = ρ(↓(ci ⊗ gi ))
⊆ ρ(↓(ci )) ∩ ρ(↓(gi )) ⊆ ei ∩ ρ(↓(gi )) ⊆ ei ∩ ρ(↓(gi )) ⊆ ei ∩ fi ⊆ (fi →′ ei+1 ) ∩ fi
= ei+1 . Therefore ρ(↓(ci+1 )) ⊆ ei+1 as required.
~
x′

m
(∃~xm (dm )) and
Thus ρ(↓(cm )) ⊆ em ⊆ dm so that cm ∈ dm . Let d′m = ∂~xm

~
x′

m
(∃~xm (cm ))
observe that [pm (~x′m ) :- d′m ]≈ = [pm (~xm ) :- dm ]≈ ∈ Dk . Put c′′m = ∂~xm
′
′′
′
′
′
⋆
so that cm ✂ cm ∈ dm . By the inductive hypothesis hpm (~xm ); cm i 6⇒P ♦ which is
a contradiction and hence ∃y~ (c′′ ) 6∈ ∃y~ (e) as required.

The result follows.
Proof for theorem 5.1
Let Dρ,C (P ) = [D]≡ , [p(~y ) :- e]≈ ∈ D and c′′ ∈ ∃y~ (e). Thus ∃y~ (c′′ ) ∈ ∃y~ (∃y~ (e)) =
∃y~ (e). Suppose, for the sake of a contradiction, that hp(~y ); c′′ ; 1i = s1 ⇛⋆P sn ⇛P ♦
where si = hgi ; ci ; hi i. Let k = max({max(hi ) | 1 ≤ i ≤ n}). Suppose (DPρ,C )k (⊤) =
[Dk ]≡ . Since D ⊑ Dk and by lemma 5.1 there exists [p(~y ) :- e′ ]≈ ∈ Dk such that
∃y~ (c′′ ) 6∈ ∃y~ (e′ ). Since ∃y~ (e) ⊆ ∃y~ (e′ ) it follows that ∃y~ (c′′ ) 6∈ ∃y~ (e) which is a
contradiction. The result follows.

