A hierarchy of Constraint Systems for Data-Flow Analysis of Constraint Logic-Based Languages

Roberto Bagnara

Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125 Pisa, Italy

Many interesting analyses for constraint logic-based languages are aimed at the detection of monotonic properties, that is to say, properties which are preserved as the computation progresses. Our basic claim is that most, if not all, of these analyses can be described within a unified notion of constraint domains. We present a class of constraint systems which allows for a smooth integration within an appropriate framework for the definition of non-standard semantics of constraint logic-based languages. Such a framework is also presented and motivated. We then show how such domains can be built, as well as construction techniques which induce a hierarchy of domains with interesting properties. In particular, we propose a general methodology for domain combination with asynchronous interaction (i.e. the interaction is not necessarily synchronized with the domains’ operations). Following this methodology, interesting combinations of domains can be expressed with all the the semantic elegance of concurrent constraint programming languages.

Key words: Constraint Systems, Constraint-based Languages, Data-flow Analysis, Abstract Interpretation.

1 Introduction

Many interesting and useful data-flow analyses for constraint logic-based languages are aimed at the detection of monotonic properties, that is to say, properties which are preserved as the computation progresses. They usually consist in determining the shape of the set of solutions of the constraint store at some program points. Analyses which fall in this category include definiteness (or groundness), symbolic patterns, types, numerical bounds and relations, symbolic size-relations and so on. The typical examples of non-monotonic properties are freeness and aliasing. A key observation is that monotonic properties can be conveniently expressed by constraints, which are then accumulated in the analysis process much in the same way as it happens during the “concrete”

Preprint submitted to Science of Computer Programming 8 July 1996

executions. Thus, frameworks of constraint-based languages are, in principle, general enough to encompass several of their own data-flow analyses. Intuitively, this is done by replacing the standard constraint domain with one suitable for expressing the desired information. This fundamental aspect was brought to light, for the case of CLP, in [9] and elaborated in [21]. In [21] it is presented a generalized algebraic semantics for constraint logic programs, which is parameterized with respect to an underlying constraint domain. The main advantages of this approach are that: (1) different instances of CLP can be used to define non-standard semantics for constraint logic programs; and (2) several abstract interpretations of CLP programs can be thus formalized inside the CLP paradigm. In this setting, data-flow analysis is then performed (or at least justified) through abstract interpretation [13,14], i.e. “mimicking” the program run-time behavior by “executing” it, in a finite way, on an approximated (abstract) constraint domain. Following a generalized semantic approach, the concrete and abstract semantics are more easily related, being instances (over two different constraint systems) of the same generalized semantics, which is entirely parametric on a constraint domain. Thus, to ensure correctness, it will be sufficient to exhibit an “abstraction function” α which is a semi-morphism between the constraint domains [7,15].

We move our steps from [21] by providing a more general notion of constraint domain which allows one to adequately describe both the “logical part” of concrete computations (i.e. answer constraints) and all the monotonic abstract interpretations we know of. In particular our notion of constraint system is able to accommodate approximate inference techniques whose importance relies on very practical considerations, such as representing good compromises between precision and computational efficiency. Some of these techniques will be sketched in the examples. The new notion of constraint domain requires the introduction of a new generalized semantics framework which is more liberal than the one of [21].

Moreover, and here comes the main point, we show that our constraint domains admit interesting constructions. The most important one consists in upgrading a domain so that it will be able to represent and manipulate dependencies among constraints. This is done by regarding a restricted class of cc agents as constraints. This construction, among other things, opens up the possibility of combining domains in a novel and interesting way. Following this methodology, the asynchronous interaction between domains can be expressed with all the elegance which derives from the cc framework.

For space reasons we have omitted many details. The interested reader is referred to [4], a much longer version of this paper including all the proofs and more examples. The plan of the paper is as follows: Section 2 introduces some basic notions and notations used throughout the paper. Section 3 explains our generalized semantics for CLP languages, as well as the abstract interpretation framework we employ. Section 4 introduces simple constraint systems: some important building blocks of the hierarchy. Section 5 builds on the previous one presenting standard ways of representing and composing finite constraints: determinate constraint systems. In Section 6 it is shown how a constraint system is upgraded to incorporate a weak form of disjunction (suitable to monotonic properties) by means of powerset constraint systems. Section 7 presents a different kind of upgrade: the one needed in order to have the notion of dependency built into the constraint system. This is done considering ask-and-tell constraint systems. Section 8 deals with the interesting problem of combining domains. A technique is shown which consists in applying the ask-and-tell construction to product constraint systems. We feel that, indeed, this is one of the more important contributions of this work. Finally, Section 9 draws some conclusions and presents some directions for further study.

2 Preliminaries

Throughout the paper we will assume familiarity with the basic notions of lattice theory, semantics of logic programming languages, and abstract interpretation.

Let U be a set. The set of all subsets of U will be denoted by ℘(U). The set of all finite subsets of U will be denoted by ℘_{f}(U). The notation S ⊆_{f} T stands for S ∈ ℘_{f}(T). For S ⊆ U we will denote the complement U \ S by \overline{S}, when U is clear from the context. For S, T ⊆ U the notation S ⊎ T denotes disjoint union, emphasizing the fact that S ∩ T = ∅. By U^{⋆} we will denote the set of all finite sequences of elements drawn from U. The empty sequence is denoted by ε. For x ∈ U^{⋆}, the length of x will be denoted by # x, and, for i such that 1 ≤ i ≤ # x, the notation x[i] stands for the i-th element of x. Let S_{1}, …, S_{n} be sets. We will denote elements of S_{1} × ⋯ × S_{n} by ⟨e_{1}, …, e_{n}⟩. The projection mappings π_{i}: S_{1} × ⋯ × S_{n} → S_{i} are defined, for i = 1, …, n,

by π_{i}(⟨e_{1}, …, e_{n}⟩) =^{def} e_{i}. The liftings π_{i}: ℘(S_{1} × ⋯ × S_{n}) → ℘(S_{i}) given by

π_{i}(T) =^{def} { π_{i}(t) | t ∈ T } will also be used.

A partial order ⪯ over a set P is a binary relation which is reflexive, transitive, and antisymmetric. ⪯ is a total order if, in addition, for each x, y ∈ P, either x ⪯ y or y ⪯ x. A set P equipped with a partial (resp. total) order ⪯ is said to be partially ordered (resp. totally ordered), and sometimes written ⟨P, ⪯⟩. Partially ordered sets are also called posets. A subset S of a poset ⟨P, ⪯⟩ is said to be a chain if it is totally ordered wrt ⪯. Given x ∈ P, the downward closure of x in ⟨P, ⪯⟩ is given by { y ∈ P | y ⪯ x } and denoted by ↓ x. Given a poset ⟨P, ⪯⟩ and S ⊆ P, y ∈ P is an upper bound for S iff x ⪯ y for each x ∈ S. An upper bound y for S is the least upper bound (or lub) of S iff for every upper bound y′ for S it is y ⪯ y′. The lub, when it exists, is unique.

In this case we write y = lub S. Lower bounds and greatest lower bounds are defined dually. ⟨P, ⪯⟩ is said bounded if it has a minimum and a maximum element. A monotone and idempotent self-map ρ: P → P over a poset ⟨P, ⪯⟩ is a kernel operator (or lower closure operator) if it is reductive, that is to say ∀x ∈ P : ρ(x) ⪯ x.

A poset ⟨L, ⪯⟩ such that, for each x, y ∈ L, both lub{x, y} and glb{x, y} exist, is called a lattice. In this case, lub and glb are also called, respectively, the join and the meet operations of the lattice. A poset where only the glb operation is well-defined is called a meet-semilattice. A complete lattice is a lattice ⟨L, ⪯⟩ such that every subset of L has both a least upper bound and a greatest lower bound.

An algebra ⟨L, ∧, ∨⟩ is also called a lattice if ∧ and ∨ are two binary operations over L which are commutative, associative, idempotent, and satisfy the following absorption laws, for each x, y ∈ L: x ∧ (x ∨ y) = x and x ∨ (x ∧ y) = x. The two definitions of lattices are equivalent. This can be seen by setting up the isomorphism given by: x ⪯ y ⟺^{def} x ∧ y = x ⟺^{def} x ∨ y = y, glb{x, y} =^{def} x ∧ y, and lub{x, y} =^{def} x ∨ y.

The notions of meet-semilattice and of bounded lattice are imported into the algebraic definition in the natural way. For instance, a bounded lattice is an algebra ⟨L, ∧, ∨, ⊥, ⊤⟩ such that ⟨L, ∧, ∨⟩ is a lattice and the following two annihilation laws are satisfied for each x ∈ L: x ∧ ⊥ = ⊥ and x ∨ ⊤ = ⊤. A lattice is said distributive if it satisfies, for each x, y, z ∈ L, the distributive laws x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z) and x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z). It is well known that, for lattices, the distributive laws are equivalent.

An algebra ⟨M, ·, 1⟩ is a monoid iff ‘·’ is an associative binary operator over M, and 1 ∈ M satisfies the identity law: for each x ∈ M, x · 1 = 1 · x = x. The monoid ⟨M, ·, 1⟩ is said commutative or idempotent if ‘·’ is so.

The sets of all natural, real, and ordinal numbers will be denoted, respectively, by ℕ, ℝ, and 𝕆. The first limit ordinal equipotent with the set of natural numbers is denoted by ω.

3 A case study: CLP

The constraint domains which are the subject of this work are not bound to a particular class of constraint logic-based languages. However, for the sake of clarity and to help the intuition, we will focus on the class of CLP languages [26,28], which is more and more influential and captures several existing, implemented languages. We will present a generalized approach to the semantics of CLP programs of which abstract interpretation is an important instance. This is necessary for a full understanding of how the domains of later sections are employed in data-flow analysis of CLP languages.

3.1 CLP: the syntax

Here we give a precise definition of what we will call a CLP(C) program. Notice that here we are concerned with syntax only. In general, C (the language of atomic constraints) is a subset of a first order language L (the language of constraints). Let us start by defining L itself.

Definition 1 (Language of constraints.) Let V and Λ be two disjoint denumerable sets of variable symbols. Let us also fix two particular isomorphisms between Λ and ℕ, and between V and ℕ. Let Vars =^{def} V ⊎ Λ. Let Ω and Π_{C} be two finite sets of operation and predicate symbols, respectively, each symbol being characterized with its arity. Let also Vars, Ω and Π_{C} be mutually disjoint. L = L(Vars, Ω, Π_{C}, …) is a language of constraints iff it is any first order language with equality built (by means of standard constructions, possibly with connectives and quantifiers) over the given sets of symbols.

(The extra-set of variables Λ allows us to simplify the following treatment. We will stipulate that the heads of clauses can only contain variable’s symbols drawn from Λ.) Now, a CLP language can impose restrictions on the form of constraints that may actually appear in programs. However these restrictions must not destroy too much of the language’s expressivity.

Definition 2 (Atomic constraint.) Given a language of constraints L, any subset C of L is a language of atomic constraints if

(i) it is closed under variable renaming; and (ii) it contains all the formulas of the form X = t, where X ∈ Vars and t is

a term built over Ω and Vars.

Before introducing the full syntax of CLP programs a few remarks about notation are in order. We will denote program variables by means of capital letters. Tuples of distinct variable will be denoted by X̄, Ȳ, and so forth. Tuples are always assumed to be of the right cardinality, e.g., if p is a predicate symbol of arity n and we write p(X̄), then X̄ is an n-tuple. Special tuples denoted by Λ⃗, denoting initial finite segments of Λ, will also be used (notice that we have fixed a total ordering on Λ). In the above hypotheses, by writing p(Λ⃗) we understand that Λ⃗ denotes the n-tuple consisting of the first n variable’s symbols in Λ. We will also abuse the notation by confusing a tuple with the set of its components. We can now introduce the notion of CLP(C) program.

Definition 3 (CLP program.) Let C be a language of atomic constraints with distinguished variable symbols in Λ. Let Π_{P} be a finite set of predicate symbols, disjoint from the symbols used in C. We will denote by A_{P} the set of atoms over Π_{P}, that is

A_{P} =^{def} { q(X̄) | q ∈ Π_{P} , X̄ ∈ Vars^{⋆} }.

A CLP(C) program P over Π_{P} is a finite sequence of clauses of the form

p(Λ⃗) :− ⟨b_{1}, …, b_{k}⟩, with p ∈ Π_{P} and k ≥ 0,

where, for 1 ≤ i ≤ k, b_{i} ∈ C ∪ A_{P} and vars(b_{i}) ∩ Λ ⊆ Λ⃗. p(Λ⃗) is called the head of the rule, whereas ⟨b_{1}, …, b_{k}⟩ is the body.

The syntax of any CLP language can be defined in such a way, by augmenting the first order language on which it is based with the set of distinguished variable symbols Λ and transforming each program along the lines of Definition 3 by means of standard techniques. This transformation is always possible by virtue of Definition 2. This normalization of programs has the property that predicate’s symbols are always applied to tuples of distinct variables. Further, all the heads of the rules defining a program predicate p/n have the same variables in the same positions. Observe that the body B of a clause p(Λ⃗) :− B is a sequence, that is an element of (C ∪ A_{P})^{⋆}. As programs themselves are sequences, the semantic constructions will be free to take into account the selection and search rules used in real languages. So far for the syntax, we now examine the (possibly non-standard) semantics of CLP languages.

3.2 Non-standard semantics for CLP

Here we start from very basic facts. We recognize the existence of four different activities in the execution, and thus in the analysis, of constraint logic programs:

(i) different execution paths are explored; (ii) along any path, constraints are accumulated in the so called constraint

store; (iii) the constraint store is recursively subdivided into parts. The activity of

imposing restrictions in the way different parts can interact is usually called hiding.

(iv) Pieces of information (parameters) are passed between program rules.

In a generalized semantics setting [21] these activities are captured by algebraic structures of the form

⟨D, ⊴, ⊗, ⊕, 0, 1, {¯∃ ; ¯∃Λ⃗}_{Λ⃗∈Λ^{⋆}}, {dX̄Ȳ }_{X̄,Ȳ ∈Vars^{⋆}}⟩,

The ⊕ operator models the merging of information coming from different execution paths. The 0 elements represent the information content of an empty (or failed) execution path. The ⊗ operator models the constraint accumulation process. The element 1 stands, intuitively, for the empty constraint store, i.e. the one containing no information at all. The ¯∃ ; ¯∃Λ⃗ operators represent the hiding process: any variable X ∉ Λ⃗ appearing in the scope of ¯∃ ; ¯∃Λ⃗ is isolated (hidden) from other occurrences of X outside the scope. The “complement sign” which appears on top of ¯∃ ; ¯∃Λ⃗ signifies that we formalize hiding in a dual way with respect to traditional approaches [35,21]. The so-called diagonal elements dX̄Ȳ represent, roughly speaking, the fact that the tuples of variables X̄ and Ȳ are tightly correlated with respect to the properties of interest. The relation ⊴ specifies the relative precision of program properties. D_{1} ⊴ D_{2} means that “D_{1} is more precise than D_{2}”. In other words, every set of computations which enjoys property D_{1} also enjoys property D_{2}. In the framework of abstract interpretation, ⊴ is referred to as the approximation ordering of the domain [15].

The way we define domains of interpretation for CLP languages is clearly highly dependent on the application we have in mind. For our current purposes we restrict ourselves to a specific class of domains which is obtained by imposing restrictions on the general scheme (see [4]). For a full understanding of the hypotheses which are behind our approach, we now spell out the above mentioned restrictions. This makes clear what is the class of properties which are captured by the hierarchy of domains that will be presented later.

– We are interested properties of programs which are valid for all terminating and successful computations;

– we are neither interested in the order in which computations are taken, nor in their multiplicities;

– we focus on monotonic properties, that is, those which are preserved as computation progresses;

– further, we restrict out interest to logical properties. This means, roughly speaking, that ⊗ is interpreted as logical conjunction.

Now the question is: how do we represent the properties of interest? A simple, but far reaching answer was first given in [9]: we can represent properties by means of constraints. This opens up the possibility of computing non-standard semantics of CLP, and, in particular, abstract interpretations, within the CLP framework. In this setting the result of the abstract interpretation of a CLP program P is obtained by “executing” (in a finite way) another CLP program P′, strongly related to P, over a non-standard domain. Intuitively, this is done by replacing the standard constraint domain with one suitable for expressing the desired information. This possibility led to the idea of a generalized semantics for CLP programs, proposed in [21]. A generalized semantics is parameterized over the (possibly non-standard) constraint system which constitute the domain of the computation. The main advantages of this approach are that:

(i) different instances of CLP can be used to define non-standard semantics for constraint logic programs;

(ii) the semantics of these instances are all captured within a unified algebraic

framework; and, in particular, (iii) many relevant abstract interpretations of CLP programs can be formal-

ized inside the CLP paradigm.

The next section is devoted to the class of domains outlined above.

3.3 Constraint systems

Since we aim at a pervasive treatment, we would like to avoid talking too much about what a constraint is. However, we cannot overlook some basic facts on the relationship between constraints and program variables. The purpose of constraints is, roughly speaking, to restrict the range of values variables can take. For our present objectives the following definition suffices.

Definition 4 (Constraint.) The class of constraints is defined by:

(i) a well-formed formula of any first-order language L with variables’ symbols in Vars is a constraint;

(ii) any set of constraints is a constraint; (iii) any (meta-level) predicate p/n applied to n constraints is a constraint; (iv) nothing is a constraint if not by virtue of (i), (ii), and (iii).

Now, on the relationship between constraints and variables, we can reason inductively as follows.

Definition 5 (Variables, free variables, and renaming.) With reference to Definition 4, if c is a constraint by virtue of (i) then the notions of variables of c and of free variables of c are assumed as primitive. These sets of variables are denoted, respectively, by vars(c) and FV (c). An invertible and idempotent mapping from and to variable’s symbols which is the identity almost everywhere is called renaming. We will use the notation [Ȳ /X̄] for renamings, where Ȳ and X̄ are disjoint tuples of distinct variables. The renaming [Y/X] has no effect on c if X ∉ FV (C), whereas variables’ capture is avoided by consistent renaming of bound variables. Besides that, the constraint c[Ȳ /X̄] is assumed as defined.

If C is a constraint because of (ii) then vars(C) =^{def} ⋃_{c∈C} vars(c) and^{1}

FV (C) =^{def} { X ∈ Vars | ∃c ∈ C . ∃Y ∈ Vars . c[Y/X] ∉ C }.  (1)

With these definitions the notion of renaming for C is extended as expected. The application of a renaming to C is defined element-wise.

If μ(C_{1}, …, C_{n}) is a constraint by virtue of (iii) then the above notions are extended as they would be in any first-order language.

In the sequel we will apply renamings carefully so that, when we write C[Ȳ /X̄], it is ensured that FV (C) ∩ Ȳ = ∅. We will emphasize this fact by saying that [Ȳ /X̄] is a renaming for C.

All the members of our hierarchy of domains will turn out to be constraint systems in the precise sense stated by the following definition.

Definition 6 (Constraint system.) Any algebra D̄ of the form

⟨D, ⊗, ⊕, 0, 1, {¯∃ ; ¯∃Λ⃗}_{Λ⃗∈Λ^{⋆}}, {dX̄Ȳ }_{X̄,Ȳ ∈Vars^{⋆}}⟩

is a constraint system if and only if it satisfies the following conditions:

G_{0}. D is a set of constraints; G_{1}. ⟨D, ⊗, 1⟩ is a commutative and idempotent monoid; G_{2}. ⟨D, ⊕, 0⟩ is a commutative and idempotent monoid; G_{3}. 0 is an annihilator for ⊗, i.e., for each C ∈ D, C ⊗ 0 = 0; G_{4}. for each C_{1}, C_{2} ∈ D, C_{1} ⊗ (C_{1} ⊕ C_{2}) = C_{1}; G_{5}. for each Λ⃗ ∈ Λ^{⋆} and C ∈ D, it is FV (¯∃ ; ¯∃Λ⃗ C) ⊆ Λ⃗.

A c.s. induces the relation ⊢ ⊆ D × D given, for each C_{1}, C_{2} ∈ D, by

C_{1} ⊢ C_{2} ⟺^{def} C_{1} ⊗ C_{2} = C_{1}.  (2)

The relation ‘ ⊢’ is referred to as the approximation ordering of the constraint system. The notation C_{1} ⊩ C_{2} stands for C_{1} ⊢ C_{2} ∧ C_{1} ≠ C_{2}.

In the sequel we will feel free to drop the quantifiers from the notation of the families of projection operators and diagonal elements. Condition G_{4} can be restated as

C_{1} ⊢ C_{1} ⊕ C_{2} and C_{2} ⊢ C_{1} ⊕ C_{2}.

1 This definition of FV is an adaptation of the one of dependent variables given in [33, Definition 2.3].

In this form it clearly stands for the correctness of the merge operation, characterizing it as a (not necessarily least) upper bound operator with respect to the approximation ordering.

Hypothesis 7 Indeed, constraint systems must satisfy some other (very technical) conditions related to how they deal with variables. For instance, they do not invent new free variables: FV (C_{1} ⊗ C_{2}) ⊆ FV (C_{1}) ∪ FV (C_{2}), and similarly for the merge operator. The operators are also generic in that they are insensible to variable names. This implies that, if [Ȳ /X̄] is a renaming for both C_{1} and C_{2}, then

(C_{1} ⊗ C_{2})[Ȳ /X̄] = C_{1}[Ȳ /X̄] ⊗ C_{2}[Ȳ /X̄].

In particular, if we have also C_{1} ⊢ C_{2}, then C_{1}[Ȳ /X̄] ⊢ C_{2}[Ȳ /X̄]. In the sequel we will take all these overwhelmingly reasonable requirements for granted.

Constraint systems enjoy several properties.

Proposition 8 (Properties of c.s.) Any constraint system satisfies the following properties, for each C, C_{1}, C_{2} ∈ D:

(i) ⟨D, ⊢, ⊗, 0, 1⟩ is a bounded meet-semilattice; (ii) C ⊕ 1 = 1; (iii) C_{1} ⊢ C_{1} ⊕ (C_{1} ⊗ C_{2}); (iv) C_{1} ⊕ C_{2} = C_{2} ⟹ C_{1} ⊢ C_{2}.

Observe that ⟨D, ⊗, ⊕, 0, 1⟩, in general, is not a lattice. Both ‘⊗’ and ‘⊕’ are associative, commutative, and idempotent, but, as stated above, while one of the absorption laws holds (axiom G_{4} of Definition 6), only one direction of the dual law is generally valid (property (iii) of Proposition 8). In particular, ‘⊕’ might be not component-wise monotone with respect to ‘ ⊢’, and ‘⊕’ does not distribute, in general, over ‘⊗’ (this would imply the equivalence of the two absorption laws).

So far for generic constraint systems, we consider now some strengthenings of Definition 6.

Definition 9 (Stronger c.s.’s) Consider the following conditions:

G_{c}. for each family {C_{i} ∈ D}_{i∈ℕ}, ⨁_{i∈ℕ} C_{i} =^{def} C_{1}⊕C_{2}⊕⋯ exists and is unique in D; moreover, associativity, commutativity, and idempotence of ‘⊕’ apply to denumerable as well as to finite families of operands;

G_{d}. ⟨D, ⊗, ⊕, 0, 1⟩ is a distributive lattice; G_{D}. for each C ∈ D and each family {C_{i} ∈ D}_{i∈ℕ} such that ⨁_{i∈ℕ} C_{i} exists,

we have C ⊗ (⨁_{i∈ℕ} C_{i}) = ⨁_{i∈ℕ}(C ⊗ C_{i}); G_{N}. in D every strictly ascending chain, C_{0} ⊩ C_{1} ⊩ C_{2} ⊩ ⋯, is finite.

A constraint system is said closed if it satisfies condition G_{c}. It is said distributive if it satisfies G_{d}. If it satisfies the stronger condition G_{D} then it is said completely distributive. Finally, a constraint system is said Noetherian if it satisfies the ascending chain condition G_{N}.

So, the operation of merging together the information coming from all the computation paths always makes sense in a closed constraint system. Notice however that property G_{c} is only necessary when the semantic construction requires it. This will never happen when considering “abstract semantic constructions” formalizing data-flow analyses (which are finite in nature). In these cases the idea of merging infinitely many pieces of information is a nonsense in itself. Closedness will instead be a must for the constraint systems intended to capture “concrete” program semantics. Distributivity is useful for proving the equivalence of different abstract semantics constructions used for dataflow analysis. Complete distributivity is required for proving that a concrete semantics corresponds to the operational model of the language [21]. Observe that closed and completely distributive constraint systems are instances of the closed semi-rings used in [21].

For the abstract semantics constructions we will make use of another class of operators over constraints. These operators were introduced in [12].

Definition 10 (Widening.) [12] Given a constraint system D̄, a binary operator ∇: D → D is called a widening for D̄ if

W_{1}. for each C_{1}, C_{2} ∈ D we have C_{1} ⊢ C_{1} ∇ C_{2} and C_{2} ⊢ C_{1} ∇ C_{2}; W_{2}. for each increasing chain C_{0} ⊢ C_{1} ⊢ C_{2} ⊢ ⋯, the sequence given by

C′_{0} =^{def} C_{0} and, for n ≥ 1, C′_{n} =^{def} C′_{n−1} ∇ C_{n}, is stationary after some k ∈ ℕ.

Widenings allow to define convergence acceleration methods which ensure termination of the “abstract interpreter”. However, even when termination is granted anyway (e.g., when the constraint system is Noetherian), these methods are often crucial for achieving rapid termination, that is, for obtaining usable data-flow analyzers. More sophisticated methods for convergence acceleration exist which employ also narrowing operators, and more complex widenings than the ones defined above (see [16,15]).

3.4 Generalized semantics

In a generalized semantics setting, the first thing to do is to provide atomic constraints with an interpretation on the chosen constraint system. Suppose that we are interested in deriving information about just two kind of program points: clause’s entries and clause’s successful exits. In a data-flow analysis setting (where this is often the case) that is to say that we want to derive call-patterns and success-patterns. In other words, for each clause we want to derive properties of the constraint store which are valid

– whenever the clause is invoked (call-patterns);

– whenever a computation starting with the invocation of the clause terminates with success (success-patterns).

Observe that call-patterns depend on the ordering of atoms in the body of clauses and on the selection rule employed. By means of program transformations similar to the magic one [8,19] we can obtain the call-patterns of the original program (with respect to the selection rule employed) as success-patterns of the transformed one. These transformations, in fact, besides modifying the clauses of the original program, introduce new clauses that characterize the conditions under which the original clauses are invoked. In the transformed program the ordering of atoms in the clause’s bodies is no longer important. Notice that the technique proposed in [19], while restricted to logic programs^{2} , is more sophisticated than usual transformation approaches, and allows not to loose the connection between call and success patterns. For these reasons we will consider only one kind of program points: clause’s exits. Furthermore, in our domains the operation capturing constraint composition is associative, commutative, and idempotent. This means that we can assume without prejudice that all the clauses are of the form

p(Λ⃗) :− {c_{1}, …, c_{n}} □ {b_{1}, …, b_{k}},

where {c_{1}, …, c_{n}} is a set of atomic constraints, and {b_{1}, …, b_{k}} is a set of atoms. All the other restrictions imposed by Definition 3 must continue to hold. We now must associate a meaning to the finite sets of atomic constraints which occurs in clauses.

Definition 11 (Constraint interpretation.) Given a language C of atomic constraints and a constraint system D̄, a constraint interpretation of C in D̄ is a computable function [[·]]D̄ ; C : ℘_{f}(C) → D.

Then usually one considers, instead of the syntactic program P, its semantic version over the domain D̄, obtained by interpreting the atomic constraints of clauses through [[·]]D̄ ; C. For r = 1, …, # P, we denote the r-th clause of P by P [r].

Definition 12 (Generalized program.) When D̄ is a constraint system, a CLP(D̄) program is a sequence of Horn-like formulas of the form

p(Λ⃗) :− C □ {b_{1}, …, b_{k}},

2 Actually, we have developed a technique, still based on program transformation, which is general enough to accommodate the entire CLP framework [37].

where C ∈ D̄ is finitely representable. Given a CLP(C) program P and a constraint interpretation [[·]]D̄ ; C, the CLP(D̄) program [[P ]]D̄ ; C is given, for each r = 1, …, # P, by

[[P ]]D̄ ; C[r] ≡ p(Λ⃗) :− [[C]]D̄ ; C □ B ⟺^{def} P [r] ≡ p(Λ⃗) :− C □ B.  (3)

An interpretation for a program P over a constraint system D̄ is a function from its program points (one for each clause) to D.

Definition 13 (Interpretation.) Let D̄ be a constraint system, and P a CLP(D̄) program. An interpretation for P over D̄ is any element of

I D̄ ; P =^{def} {1, …, # P } → D.

All the operations and relations over D̄ are extended point-wise to I D̄ ; P. In particular I D̄ ; P is partially ordered by the lifting of ⊢, i.e., for each I_{1}, I_{2} ∈ I D̄ ; P,

I_{1} ⊢ I_{2} ⟺^{def} ∀r ∈ {1, …, # P } : I_{1}(r) ⊢ I_{2}(r).

We will represent interpretations by means of function graphs. It is straightforward to show that all the interesting properties of constraint systems lift smoothly to interpretations.

We are left with the choice of the semantics construction, that is, of the “interpretation transformer”. For the purpose of this work we choose a bottom-up construction expressed by a flavor of the usual immediate consequence operator T_{P}, taking an interpretation and returning a new interpretation.

Our set of program variables is Vars = Λ ⊎ V, where Λ and V are totally ordered. For Λ⃗ ∈ Λ^{⋆} and W ⊆_{f} Vars, we denote by Ȳ ≪Λ⃗ W the fact that, with respect to the ordering of V, Ȳ is a tuple of distinct consecutive variables in V such that # Ȳ = # Λ⃗ and the first element of Ȳ immediately follows the greatest variable in W.

Definition 14 (Interpretation transformer.) Let P be a CLP(D̄) program, where D̄ is a constraint system. The operator induced by P over I D̄ ; P,

T D̄ ; P: I D̄ ; P → I D̄ ; P, is

T D̄ ; P(I) =^{def} { (r, T D̄ ; P(r, I)) | 1 ≤ r ≤ # P },  (4)

where T D̄ ; P: {1, …, # P } × I D̄ ; P → D is given by

T D̄ ; P(r, I) =^{def} ⨁ \{ ¯∃ ; ¯∃Λ⃗ C̃ | \begin{matrix}P [r] ≡ p(Λ⃗) :− C □ \{p_{1}(X̄_{1}), …, p_{n}(X̄_{n})\} \\ and, for each i = 1, …, n: \\ P [r_{i}] ≡ p_{i}(Λ⃗_{i}) :− C_{i} □ B_{r_{i}} \\ Ȳ_{i} ≪Λ⃗_{i} FV (P [r]) ∪ Ȳ_{1} ∪ ⋯ ∪ Ȳ_{i−1} \\ C̃_{i} = I(r_{i})[Ȳ_{i}/Λ⃗_{i}] \\ C′_{i} = dX̄_{i}Ȳ_{i} ⊗ C̃_{i} \\ C̃ = C ⊗ C′_{1} ⊗ ⋯ ⊗ C′_{n} \end{matrix} \} . (5)

Notice that, in this construction, the merge operator is applied only to finite sets of operands. In summary, once we have fixed the constraint domain D̄ and the interpretation of atomic constraints [[·]]D̄ ; C, the meaning of a CLP(C) program P over D̄ is encoded into the T D̄ ; P operator. Before rushing to require that T D̄ ; P must be continuous on the complete lattice D̄ we better have a closer look to our real needs.

3.5 Defining, computing and correlating non-standard semantics

Given our current focus on data-flow analysis of CLP programs, we only consider, for simplicity, the typical case in this field. On one hand we have a “concrete” constraint system D̄^{♮}: it must capture the properties of interest, it must ensure the existence of the least fixpoint of T D̄^{♮} ; P^{♮}, that is, of the meaning of each program P. And, of course, this meaning must correspond to the one obtained by means of the top-down construction representing the operational model of the language (namely, some kind of extended SLD-resolution). This last requirement implies, as shown in [21], that D̄^{♮} must be closed and completely distributive, hence a complete lattice.

One the other hand, in data-flow analysis, we have an “abstract” constraint system D̄^{♯}. Here we are much less demanding: we simply want to compute in a finite way an approximation of a post-fixpoint of T D̄^{♯} ; P^{♯} (the least fixpoint might not even exist, or it might be too expensive to compute). And, of course, we need a guarantee that what we compute is a correct approximation of the concrete meaning. Finite computability can be ensured, in general, by using a widening operator. Thus, in this setting, the concrete and abstract iteration sequences defining, respectively, the concrete meaning and approximations of the abstract meaning of programs are quite different.

Definition 15 (Concrete and abstract iteration sequences.) Consider a closed and completely distributive constraint system D̄^{♮}, and a CLP(D̄^{♮}) program P^{♮}. The concrete iteration sequence for P^{♮} is inductively defined as follows, for all ordinals κ ∈ 𝕆:

\{ \begin{matrix}T D̄^{♮} ; P^{♮} ↑ 0 & =^{def} & 0^{♮}, \\ T D̄^{♮} ; P^{♮} ↑ (κ + 1) & =^{def} & T D̄^{♮} ; P^{♮}(T D̄^{♮} ; P^{♮} ↑ κ), \\ T D̄^{♮} ; P^{♮} ↑ κ & =^{def} & ⨁_{β<κ}^{♮}(T D̄^{♮} ; P^{♮} ↑ β), when κ > 0 is a limit ordinal. \end{matrix} (6)

Let D̄^{♯} be any constraint system, and let ∇^{♯} be a widening operator over D̄^{♯}. For a CLP(D̄^{♯}) program P^{♯}, the abstract iteration sequence for P^{♯} with widening ∇^{♯} is inductively defined by

\{ \begin{matrix}T D̄^{♯} ; P^{♯} ⇑ 0 & =^{def} & 0^{♯}, \\ T D̄^{♯} ; P^{♯} ⇑ (k + 1) & =^{def} & (T D̄^{♯} ; P^{♯} ⇑ k) ∇^{♯} T D̄^{♯} ; P^{♯}(T D̄^{♯} ; P^{♯} ⇑ k), for k ∈ ℕ. \end{matrix}  (7)

Observe that, when D̄^{♯} is Noetherian or when termination can be ensured in other ways, π_{2} (the second projection) can be substituted for ∇^{♯} in (7). In these cases, indeed, the restriction of π_{2} to the iterates’ values is a widening operator. The following fact is easily proved using standard techniques [21].

Theorem 16 If D̄^{♮} is a closed and completely distributive constraint system then, for each CLP(D̄^{♮}) program P^{♮} the least fixpoint of T D̄^{♮} ; P^{♮} exists and is given

by lfp(T D̄^{♮} ; P^{♮}) = T D̄^{♮} ; P^{♮} ↑ ω.

We now come at the problem of ensuring the correctness of the analysis. We use an abstraction correspondence between the concrete and the abstract constraint systems, which induces an abstraction correspondence between the respective semantics [7,15].

Definition 17 (Abstraction function.) Let D̄^{♮} and D̄^{♯} be two constraint systems as in Definition 15. A function α: D^{♮} → D^{♯} is an abstraction function of D̄^{♮} into D̄^{♯} if and only if

A_{1}. α is a semi-morphism, namely, for each C^{♮}, C_{1}^{♮}, C_{2}^{♮}, d_{X̄Ȳ}^{♮} ∈ D^{♮} and Λ⃗ ∈ Λ^{⋆}:

α(C_{1}^{♮} ⊗^{♮} C_{2}^{♮}) ⊢^{♯} α(C_{1}^{♮}) ⊗^{♯} α(C_{2}^{♮}),  α(0^{♮}) ⊢^{♯} 0^{♯},
α(C_{1}^{♮} ⊕^{♮} C_{2}^{♮}) ⊢^{♯} α(C_{1}^{♮}) ⊕^{♯} α(C_{2}^{♮}),  α(d_{X̄Ȳ}^{♮} ) ⊢^{♯} d_{X̄Ȳ}^{♯} ,
α(¯∃ ; ¯∃♮ ; Λ⃗ C^{♮}) ⊢^{♯} ¯∃ ; ¯∃♯ ; Λ⃗ α(C^{♮}).

A_{2}. for each increasing chain {C_{j}^{♮} ∈ D^{♮}}_{j∈ℕ},

∃C^{♯} ∈ D^{♯} . ∀j ∈ ℕ : α(C_{j}^{♮}) ⊢^{♯} C^{♯} ⟹ α( \begin{matrix}⨁ & ♮ \\ j∈ℕ \end{matrix} C_{j}^{♮}) ⊢^{♯} C^{♯};

A_{3}. for each C^{♮} ∈ D^{♮} and each renaming [Ȳ /X̄] for C^{♮}, it happens that

α(C^{♮})[Ȳ /X̄] = α(C^{♮}[Ȳ /X̄]).

Any abstraction function α: D^{♮} → D^{♯} is naturally extended to α: I D̄^{♮} ; P^{♮} → I D̄^{♯} ; P^{♯}, when # P^{♮} = # P^{♯}, in the obvious way.

As anticipated above, one of the beautiful things of the generalized approach is that the abstract meaning of CLP programs can be encoded into other CLP programs. We have thus an abstract compilation approach, where the soundness of the compilation function [[·]]D̄^{♯} ; C is expressed, for CLP(C) programs, by the requirement α∘[[·]]D̄^{♮} ; C ⊢^{♯} [[·]]D̄^{♯} ; C. The following result is an application of a theorem in [15, Proposition 6.20].

Theorem 18 Given a CLP(C) program P, two constraint systems D̄^{♮} and D̄^{♯}, the constraint interpretations [[·]]D̄^{♮} ; C and [[·]]D̄^{♯} ; C, and the abstraction function

α: D^{♮} → D^{♯} such that α ∘ [[·]]D̄^{♮} ; C ⊢^{♯} [[·]]D̄^{♯} ; C, P^{♮} = [[P ]]D̄^{♮} ; C and P^{♯} = [[P ]]D̄^{♯} ; C, we have

that the abstract iteration with widening (7) is eventually stable after ℓ ∈ ℕ steps and

α(lfp(T D̄^{♮} ; P^{♮})) = α(T D̄^{♮} ; P^{♮} ↑ ω) ⊢^{♯} (T D̄^{♯} ; P^{♯} ⇑ ℓ).

We now describe a hierarchy of constraint systems which capture most of the analysis domains used for deriving monotonic properties of programs, as well as the “concrete” collecting semantics they abstract. The basis is constituted by any constraint system which satisfies the conditions of Definition 6. In Section 5 we will show a way (which, of course, is not the only one) of defining such a structure. This requires introducing simple constraint systems, which is the purpose of the following section.

4 Simple constraint systems

A constraint system can be built starting from a set of finite constraints (or tokens), each expressing some partial information. We now define a notion of simple constraint systems (or s.c.s.), very similar to the one introduced in [35].

Definition 19 (Simple constraint system.) A simple constraint system is a structure ⟨C, ⊢, ⊥, ⊤⟩, where C is a set of constraints, ⊥ ∈ C, ⊤ ∈ C, and ⊢ ⊆ ℘_{f}(C) × C is an entailment relation such that, for each C, C′ ∈ ℘_{f}(C), each c, c′ ∈ C, and X, Y ∈ Vars:

E_{1}. c ∈ C ⟹ C ⊢ c; E_{2}. C ⊢ ⊤; E_{3}. (C ⊢ c) ∧ (∀c′ ∈ C : C′ ⊢ c′) ⟹ C′ ⊢ c; E_{4}. {⊥} ⊢ c; E_{5}. C ⊢ c ⟹ C[Y/X] ⊢ c[Y/X].

The ‘ ⊢’ symbol is overloaded to denote also the extension ⊢ ⊆ ℘(C) × ℘(C) such that, for each C, C′ ∈ ℘(C),

C ⊢ C′ ⟺^{def} ∀c′ ∈ C′ : ∃C′′ ⊆_{f} C . C′′ ⊢ c′.

It is clear that condition E_{1} implies reflexivity of ‘ ⊢’, while condition E_{3} amounts to transitivity. E_{2} qualifies ‘⊤’ as the least informative token: it will be needed just as a “marker” when the product of simple constraint systems will be considered (see Section 8 and [36]). E_{4} ensures that C is a finitely generable element (see Definition 21). Condition E_{5}, referred to as genericity, states that the entailment is insensible to variables’ names^{3} .

By axioms E_{1} and E_{3} of Definition 19 the entailment relation of a simple constraint system is a preorder. Now, instead of considering the quotient poset with respect to the induced equivalence relation, a particular choice of the equivalence classes’ representatives is made: closed sets with respect to entailment. This representation is a very convenient domain-independent strong normal form for constraints.

Definition 20 (Elements.) [35] The elements of an s.c.s. ⟨C, ⊢, ⊥, ⊤⟩ are the entailment-closed subsets of C, namely those C ⊆ C such that, whenever ∃C′ ⊆_{f} C . C′ ⊢ c, then c ∈ C. The set of elements of ⟨C, ⊢, ⊥, ⊤⟩ is denoted by |C|.

The poset of elements is thus given by ⟨|C|, ⊇⟩. Notice that we deviate from [35] in that we order our constraint systems in the dual way.

Definition 21 (Inference map, finite elements.) Given a simple constraint system ⟨C, ⊢, ⊥, ⊤⟩, the inference map of ⟨C, ⊢, ⊥, ⊤⟩ is ρ: ℘(C) → ℘(C) given, for each C ⊆ C, by

ρ(C) =^{def} { c | ∃C′ ⊆_{f} C . C′ ⊢ c }.

3 In [33] a stronger notion of genericity is used, namely C[t/X] ⊢ c[t/X] whenever C ⊢ c, for any term t. This is too strong for our purposes: e.g. it would force us to treat non-linear numeric constraints in the same way as linear ones in CLP(R).

It is well known that ρ is a kernel operator, over the complete lattice ⟨℘(C), ⊇⟩, whose image is |C|. The image of the restriction of ρ onto ℘_{f}(C) is denoted by |C|_{0}. Elements of |C|_{0} are called finitely generated constraints or simply finite constraints.

From here on we will only work with finitely generated constraints, since we are not concerned with infinite behavior of (CLP) programs.

In general, describing the “standard” semantics of a CLP(X) language is done as follows. Let T be the theory which corresponds to the domain X [26]. Let D be an appropriate set of formulas in the vocabulary of T closed under conjunction and existential quantification. Define Γ ⊢ c iff Γ entails c in the logic, with non-logical axioms T. Then (D, ⊢) is the required simple constraint system. For CLP(H) (i.e. pure Prolog) one takes the Clark’s theory of equality in some disguise. For CLP(ℝ)^{4} the theory RCF of real closed fields would do the job. We see now some examples of simple constraint systems.

4.1 The atomic simple constraint system

This is probably the simplest useful example of s.c.s. The tokens include variable names. A variable name, when present in a constraint, expresses the fact that the variable has some (unspecified) property. For instance, being definitely bound to a ground value. In this case, X is just a shorthand for ground(X). This s.c.s. is thus given by C =^{def} Vars ∪ {⊥, ⊤} and by the smallest relation ⊢ ⊆ ℘_{f}(C) × C satisfying conditions E_{1}–E_{5} of Definition 19. In the sequel we will refer to this structure as to the atomic s.c.s.

A useful extension is to include tokens involving two variable names. These tokens state that the two variables involved share the property of interest: one enjoys it iff the other one does. More formally, we have

C′ =^{def} C ∪ { X ⇋ Y | X, Y ∈ Vars },

and the entailment relation is suitably extended to C′ requiring, for each X, Y, Z ∈ Vars:

{X ⇋ Y } ⊢ Y ⇋ X; {X ⇋ Y, Y ⇋ Z} ⊢ X ⇋ Z; {X, X ⇋ Y } ⊢ Y.

4 Beware not to confuse CLP(ℝ), the idealized language over the reals [28], with CLP(R), the (far from ideal) implemented language and system [27].

4.2 Bounds and relations analysis for numeric domains

The analysis described in [5,6,3] is based on constraint inference, a variant of constraint propagation [18]. This technique, developed in the field of artificial intelligence, has been applied to temporal and spatial reasoning [1,38].

Let us focus our attention to arithmetic domains, where the constraints are binary relations over expressions. Let E be the set of arithmetic expressions of interest. Let F ⊂ ℝ a computable set of numbers, e.g. some family of rational numbers. The set of boundaries is given by B =^{def} F∪{+∞, −∞}, and is ordered by the natural extension of the ‘≤’ relation. The set I of intervals is

I =^{def} { (b_{1}, b_{2}) | b_{1} ∈ B, b_{2} ∈ B } ∪ { [ b_{1}, b_{2}) | b_{1} ∈ F, b_{2} ∈ B }
∪ { (b_{1}, b_{2} ] | b_{1} ∈ B, b_{2} ∈ F } ∪ { [ b_{1}, b_{2} ] | b_{1} ∈ F, b_{2} ∈ F }.

Since any I ∈ I is a finite representations of a subset of ℝ we will confuse intervals with their denotation. Thus we can state that intervals are closed under intersection, i.e., for each I_{1}, I_{2} ∈ I, I_{1} ∩ I_{2} ∈ I. The set of arithmetic relations is R =^{def} {=, ≠, ≤ <, ≥, >} and our constraints are given by

C =^{def} { e_{1} ▷◁ e_{2} | e_{1}, e_{2} ∈ E, ▷◁ ∈ R } ∪ { e ◁ I | e ∈ E, I ∈ I } ∪ {⊥, ⊤}.

The meaning of the constraint e ◁ I is the obvious one: any real value the expression e can take is contained in I. Thus C provides a mixture of qualitative (relationships between expressions) and quantitative (bounds on the values of the expressions) knowledge.

The approximate inference techniques we are interested in can be encoded into an entailment relation ‘ ⊢’ over C. First we need to specify how we deal with intervals: we can intersect them, weaken them, and we detect failure by recognizing the empty ones:

{e ◁ I_{1}, e ◁ I_{2}} ⊢ e ◁ I_{1} ∩ I_{2},
{e ◁ I} ⊢ e ◁ I′,  if I ⊆ I′,
{e ◁ I} ⊢ ⊥,  if I = ∅.

Two techniques for exploiting pure qualitative information are symmetric and transitive closure:

\begin{aligned}\{e_{1} ▷◁ e_{2}\} & ⊢ & e_{2} ▷◁^{−1} e_{1}, \\ \{e_{1} ▷◁ e_{2}, e_{2} ▷◁′ e_{3}\} & ⊢ & e_{1} ▷◁′′ e_{3}, & if ▷◁′′ = tc(▷◁, ▷◁′), \end{aligned}

where ▷◁^{−1} is the inverse of ▷◁ (e.g. < is the inverse of >, ≥ of ≤ and so on), and tc : R × R ↣ R is the partial function individuated by the following table:

tc  <  ≤  >  ≥  =  ≠
<  <  <  <
≤  <  ≤  ≤
>  >  >  >
≥  >  ≥  ≥
=  <  ≤  >  ≥  =  ≠
≠  ≠

This technique allows the inference of A < C from A ≤ B and B < C. Of course, qualitative information can be combined and can led to the detection of inconsistencies:

\begin{aligned}\{e_{1} ▷◁ e_{2}, e_{1} ▷◁′ e_{2}\} & ⊢ & e_{1} ▷◁′′ e_{2}, & if ∀x, y ∈ ℝ : (x ▷◁ y ∧ x ▷◁′ y) ⇒ x ▷◁′′ y, \\ \{e_{1} ▷◁ e_{2}, e_{1} ▷◁′ e_{2}\} & ⊢ & ⊥, & if ∀x, y ∈ ℝ : ¬(x ▷◁ y ∧ x ▷◁′ y). \end{aligned}

A classical quantitative technique is interval arithmetic which allows to infer the variation interval of an expression from the intervals of its sub-expressions. Let f(e_{1}, …, e_{k}) be any arithmetic expression having e_{1}, …, e_{k} as subexpressions. Then

{f(e_{1}, …, e_{k}) ◁ I, e_{1} ◁ I_{1}, …, e_{k} ◁ I_{k}} ⊢ f(e_{1}, …, e_{k}) ◁ f̈(I_{1}, …, I_{k}),

where f̈: I^{k} → I is such that for each x_{1} ∈ I_{1}, …, x_{k} ∈ I_{k}, it happens that f(x_{1}, …, x_{k}) ∈ f̈(I_{1}, …, I_{k}). For example, A ◁ [ 3, 6) ∧ B ◁ [ −1, 5 ] ⊢ A + B ◁ [ 2, 11). Another technique is numeric constraint propagation, which consists in determining the relationship between two expressions when their associated intervals do not overlap, except possibly at their endpoints. The associated family of axioms is

{e_{1} ◁ I_{1}, e_{2} ◁ I_{2}} ⊢ e_{1} ▷◁ e_{2}, if ∀x_{1} ∈ I_{1}, x_{2} ∈ I_{2} : x_{1} ▷◁ x_{2}.

For example, if A ∈ (−∞, 2 ], B ∈ [ 2, +∞), and C ∈ [ 5, 10 ], we can infer that A ≤ B and A < C. It is also possible to go the other way around, i.e. knowing that U < V may allow to refine the intervals associated to U and V so that they do not overlap. We call this weak interval refinement:

{e_{1} ▷◁ e_{2}, e_{1} ◁ I_{1}, e_{2} ◁ I_{2}} ⊢ e_{1} ◁ I′_{1}

where I′_{1} =^{def} { x_{1} ∈ I_{1} | ∃x_{2} ∈ I_{2} . x_{1} ▷◁ x_{2} }. This is an example of localconsistency technique [32,30]. In summary, by considering the transitive closure of ⊢ and with some minor technical additions we end up with a simple constraint system which characterizes precisely the combination of the above techniques. Other techniques, such as interval refinement, can be easily incorporated. What we have just presented is a watered-down version of the numerical component (presented as a simple constraint system) employed in the China analyzer [3].

5 Determinate constraint systems

Determinate constraint systems are at the bottom of the hierarchy. Such a construction is uniquely determined by a simple constraint system together with appropriate merge operator and diagonal elements. Notice that, for simplicity, we only present the finite fragment of the constraint system, that is, the sub-structure consisting of the finite elements only.

Definition 22 (Determinate constraint system.) Let S =^{def} ⟨C, ⊢, ⊥, ⊤⟩ be a simple constraint system. Let 0, 1 ∈ |C|_{0} and ⊗: |C|_{0} × |C|_{0} → |C|_{0} be given, for each C_{1}, C_{2} ∈ |C|_{0}, by

0 =^{def} C,  1 =^{def} ρ(∅),  C_{1} ⊗ C_{2} =^{def} ρ(C_{1} ∪ C_{2}).

Let ⊕: |C|_{0} × |C|_{0} → |C|_{0} be an operator satisfying conditions G_{2} and G_{4} of Definition 6. The projection operators ¯∃ ; ¯∃Λ⃗ : |C|_{0} → |C|_{0} are given, for each Λ⃗ ∈ Λ^{⋆} and each C ∈ |C|_{0}, by

¯∃ ; ¯∃Λ⃗ C =^{def} ρ({ c ∈ C | FV (c) ⊆ Λ⃗ }).

Finally, let {dX̄Ȳ }_{X̄,Ȳ ∈Vars^{⋆}} a family of elements of |C|_{0}. We will call the structure ⟨|C|_{0}, ⊗, ⊕, 0, 1, {¯∃ ; ¯∃Λ⃗}, {dX̄Ȳ }⟩ a determinate constraint system over S and ‘ ⊕’.

Theorem 23 Each determinate constraint system is indeed a constraint system. Also, for each C_{1}, C_{2} ∈ |C|_{0}, we have C_{1} ⊢ C_{2} ⟺ C_{1} ⊇ C_{2}.

The choice of a suitable merge operator, required in addition to an s.c.s. to obtain a determinate constraint system, can be done with relative freedom. This freedom can often be conveniently exploited in order to get a reasonable complexity/precision tradeoff. The same will apply to the ask-and-tell constraint systems of Section 7.

Observe that, given C_{1}, C_{2} ∈ |C|_{0}, there is no a priori guarantee that C = C_{1} ∩ C_{2} ∈ |C|_{0}. In fact, there are simple constraint systems where this is false. Defining the merge operator as set intersection, however, works in many cases.

A trivial example of merge operator is the following, whose definition is independent from the simple constraint system at hand:

C_{1} ⊕ C_{2} =^{def} \{ \begin{matrix}C_{1}, & if C_{1} = C_{2} or C_{2} = 0; \\ C_{2}, & if C_{1} = 0; \\ 1, & otherwise. \end{matrix}  (8)

For a less trivial example, suppose we are approximating subsets of ℝ^{n} by means of (closed) convex polyhedra. Of course they will be represented by sets of linear disequations over x_{1}, …, x_{n}, but, for the purpose of the present example, we will consider the polyhedra themselves. For any convex polyhedra X, Y ⊆ ℝ^{n}, define X ⊢ Y iff X ⊆ Y and

X ⊕ Y =^{def} \{ \begin{matrix}X, & if X = Y or Y = ∅; \\ Y, & if X = ∅; \\ bb(X ∪ Y), & otherwise, \end{matrix}  (9)

where bb(Z) is the smallest “bounding box” containing Z ⊆ ℝ^{n}, namely

bb(Z) =^{def} { (x_{1}, …, x_{n}) | ∀i = 1, …, n : inf π_{i}(Z) ≤ x_{i} ≤ sup π_{i}(Z) }.

The most precise merge operator is, of course, given by the convex hull, i.e.

X ⊕ Y =^{def} min{ W ⊆ ℝ^{n} | W ⊇ X ∪ Y and W is a c.p. }.  (10)

Notice that (10) satisfies both the absorption laws (thus giving rise to a lattice),

(8) and (9) do not. None of them results in a distributive constraint system. Furthermore, (8) and (9) are closed, while (10) is not.

5.1 Definiteness analysis: Con

Consider the extension of the atomic simple constraint system, C′, introduced in Section 4.1, and apply to it the determinate constraint system construction with C_{1} ⊕ C_{2} =^{def} C_{1} ∩ C_{2} for each C_{1}, C_{2} ∈ |C′|. Let also the diagonal elements be given, for each X̄, Ȳ ∈ Vars^{⋆} of the same cardinality, by

dX̄Ȳ =^{def} ρ({ π_{i}(X̄) ⇋ π_{i}(Ȳ) | 1 ≤ i ≤ # X̄ }).

The resulting domain (a closed and Noetherian d.c.s.) is the simplest one for definiteness analysis, and it was used in early groundness analyzers [31,29]. The name Con comes from the fact that elements of the form {X_{1}, …, X_{n}} are usually regarded as the conjunction X_{1}∧⋯∧X_{n}, meaning that X_{1}, …, X_{n} are definitely bound to a unique value. In this view ‘⊗’ corresponds to logical conjunction. Con is a very weak domain for definiteness analysis. It cannot capture neither “aliasing” (apart from the special kind of aliasing arising from parameter passing) nor more complex dependencies between variables such as those implied by “concrete” constraints like A = f(B, C) and A + B + C = 0. Moreover it cannot represent or exploit disjunctive information.

6 Powerset constraint systems

For the purpose of program analysis of monotonic properties it is not necessary to represent the “real disjunction” of constraints collected through different computation paths, since we are interested in the common information only. To this end, a weaker notion of disjunction suffices. We define powerset constraint systems, which are instances of a well known construction, i.e. disjunctive completion [15]. For doing that we need some notions from the theory of posets.

Given a poset ⟨L, ⊥, ≤⟩, the relation ⪯ ⊆ ℘(L) × ℘(L) induced by ≤ is given, for each S_{1}, S_{2} ∈ ℘(L) by

(S_{1} ⪯ S_{2}) ⟺ (∀x_{1} ∈ S_{1} : ∃x_{2} ∈ S_{2} . x_{1} ≤ x_{2}).

A subset S ∈ ℘(L) is said non-redundant iff ⊥ ∉ S and

∀x_{1}, x_{2} ∈ S : x_{1} ≤ x_{2} ⟹ x_{1} = x_{2}.

The set of non-redundant subsets of L wrt ≤ is denoted by ℘_{n}(L, ≤). The function Ω_{L}^{≤}: ℘(L) → ℘_{n}(L, ≤) mapping each set into its non-redundant counterpart is given, for each S ∈ ℘(L), by

Ω_{L}^{≤}(S) = S \ { x ∈ S | x = ⊥ ∨ ∃x′ ∈ S . x < x′ }.

Thus, for S ∈ ℘(L), Ω_{L}^{≤}(S) is the set of maximal elements of S. However, there is no guarantee, in general, that such maximal elements exist: L could be an infinite chain without an upper bound in L, and thus would be mapped to ∅ by Ω_{L}^{≤}. We will denote by ℘_{c}(L) the set of all those S ∈ ℘(L) such that, if S contains an infinite chain C, then it also contains an upper bound for C. Observe that ℘_{f}(L) ⊆ ℘_{c}(L) and that, if L satisfies the ascending chain condition, then ℘(L) = ℘_{c}(L).

The powerset construction upgrades a domain by considering sets of elements of the base-level domain which are non-redundant with respect to the approximation ordering.

Definition 24 (Powerset constraint systems.) Given a Noetherian constraint system D̄ = ⟨D, ⊗, ⊕, 0, 1, {¯∃ ; ¯∃Λ⃗}, {dX̄Ȳ }⟩, the powerset constraint system over D̄ is given by

⟨℘_{n}(D, ⊢), ⊗_{P}, ⊕_{P}, 0_{P}, 1_{P}{¯∃ ; ¯∃Λ⃗^{P}}, {dX̄Ȳ^{P} }⟩,

where

S_{1} ⊗_{P} S_{2} =^{def} Ω_{D}^{⊢}({ C_{1} ⊗ C_{2} | C_{1} ∈ S_{1}, C_{2} ∈ S_{2} }),
S_{1} ⊕_{P} S_{2} =^{def} Ω_{D}^{⊢}(S_{1} ∪ S_{2}),
0_{P} =^{def} ∅,
1_{P} =^{def} {1},
¯∃ ; ¯∃Λ⃗^{P} S =^{def} Ω_{D}^{⊢}({ ¯∃ ; ¯∃Λ⃗ C | C ∈ S }),
dX̄Ȳ^{P} =^{def} {dX̄Ȳ }.

If D̄ is any constraint system, the finite powerset constraint system over D̄ is

⟨℘_{n}(D, ⊢) ∩ ℘_{f}(D), ⊗_{P}, ⊕_{P}, 0_{P}, 1_{P}{¯∃ ; ¯∃Λ⃗^{P}}, {dX̄Ȳ^{P} }⟩,

where all the operators are as above.

This double definition reflects the two possible uses of powerset constraint systems. One is to define concrete domains in those cases where the base-level constraint system is Noetherian. The other is when designing abstract domains and, clearly, only the finite elements are of interest. In both cases, when we deal with monotonic properties, we loose nothing if we restrict ourselves to nonredundant sets in order to capture the non-determinism of CLP languages. This is a consequence of the fact that, when ⟨L, ⊥, ≤⟩ is a poset, we have both Ω_{L}^{≤}(S) ⪯ S and S ⪯ Ω_{L}^{≤}(S), for each S ∈ ℘_{c}(L). Of course, when the base-level c.s. is not Noetherian, one has to consider all the subsets in the design of a concrete domain.

Theorem 25 Any powerset constraint system built over a Noetherian c.s. D̄,

⟨℘_{n}(D, ⊢), ⊗_{P}, ⊕_{P}, 0_{P}, 1_{P}{¯∃ ; ¯∃Λ⃗^{P}}, {dX̄Ȳ^{P} }⟩,

is a closed and completely distributive constraint system, where the ordering is given, for each S_{1}, S_{2} ∈ ℘_{n}(D, ⊢), by

S_{1} ⊢_{P} S_{2} ⟺ ∀C_{1} ∈ S_{1} : ∃C_{2} ∈ S_{2} . C_{1} ⊢ C_{2}.  (11)

For any c.s. D̄, the finite powerset c.s. built over D̄ is a distributive constraint system, where the ordering is given by (11), for S_{1}, S_{2} ∈ ℘_{n}(D, ⊢) ∩ ℘_{f}(D).

7 Ask-and-tell constraint systems

We now consider constraint systems having additional structure. This additional structure allows to express, at the constraint system level, that the imposition of certain constraints must be delayed until some other constraints are imposed. In [34] similar constructions are called ask-and-tell constraint systems. In our construction, ask-and-tell constraint systems are built from constraint systems by regarding some kernel operators as constraints. We follow [34] in considering cc as the language framework for expressing and computing with kernel operators. For this reason we will present kernel operators as cc agents. For our current purposes we only need a very simple fragment of the determinate cc language: the one of finite cc agents. This fragment is described in [35] by means of a declarative semantics. Here we give also an operational characterization which is better suited to our needs.

Definition 26 (Finite cc agents: syntax.) A finite cc agent over a constraint system D̄ = ⟨D, ⊗, ⊕, 0, 1, {¯∃ ; ¯∃Λ⃗}, {dX̄Ȳ }⟩ is any string generated by the following grammar:

A ::= tell(C) | ask(C) → A | A ∥ A

where C ∈ D. We will denote by A(D̄) the language of such strings. The following explicit definition is also given:

ask(C_{1}; …; C_{n}) → A ≡ ( ask(C_{1}) → A) ∥ ⋯ ∥( ask(C_{n}) → A).

When this will not cause confusion we will freely drop the syntactic sugar, writing C and C → A where tell(C) and ask(C) → A are intended. One of the beautiful properties of kernel operators is that they can be uniquely represented by their range, i.e. the set of their fixed points [23]. The denotational semantics of finite cc agents over D̄ is thus conveniently expressed by a function [[·]]: A(D̄) → ℘(D) defined following [35].

Definition 27 (Semantics of finite cc agents.) The semantics of finite cc agents is given by the following equations:

[[C]] =^{def} ↓ C,  [[C → A]] =^{def} \overline{↓ C} ∪ ↓ A,  [[A ∥ B]] =^{def} [[A]] ∩ [[B]].

Observe that the actual kernel operator A^{K} corresponding to a finite agent A ∈ A(D̄) can be recovered from [[A]] as A^{K} =^{def} λC . sup((↓ C) ∩ [[A]]). The introduction of a syntactic normal form for finite cc agents allows to simplify the subsequent semantic treatment.

Definition 28 (Finite cc agents: syntactic normal form.) The transformation η over A(D̄) is defined, for C^{a}, C_{1}^{a}, C_{2}^{a}, C^{t} ∈ D and A, A_{1}, A_{2} ∈ A(D̄), as follows:

η(C^{a} → C^{t}) =^{def} \{ \begin{matrix}1 → 1, & if C^{a} ⊢ C^{t}; \\ C^{a} → (C^{a} ⊗ C^{t}), & otherwise; \end{matrix}
η(C^{t}) =^{def} 1 → C^{t};
η(C_{1}^{a} → (C_{2}^{a} → A)) =^{def} η((C_{1}^{a} ⊗ C_{2}^{a}) → A);
η(C^{a} → (A_{1} ∥ A_{2})) =^{def} η((C^{a} → A_{1}) ∥ (C^{a} → A_{2}));
η(A_{1} ∥ A_{2}) =^{def} η(A_{1}) ∥ η(A_{2}).

The following fact is easily proved.

Proposition 29 The transformation η of Definition 28 is well defined. Furthermore, if A ∈ A(D̄) then [[η(A)]] = [[A]] and η(A) is of the form

(C_{1}^{a} → C_{1}^{t}) ∥ ⋯ ∥ (C_{n}^{a} → C_{n}^{t}), where C_{i}^{t} ⊩ C_{i}^{a} for each i = 1, …, n.

Thus, by considering only agents of the form ∥_{i=1}^{n} C_{i}^{a} → C_{i}^{t} we do not loose any generality. We will call elementary agents of the kind C^{a} → C^{t} ask-tell pairs. Now we express the operational semantics of finite cc agents by means of rewrite rules. An agent in syntactic normal form is rewritten by applying the logical rules of the calculus modulo a structural congruence. This congruence states, intuitively, that we can regard an agent as a set of (concurrent) ask-tell pairs. The semantics given in Definition 27 clearly allows that. From now on we will treat the ‘∥’ operator as a (polymorphic) constructor for flat sets.

Definition 30 (A calculus of finite cc agents.) Let 1_{A} =^{def} 1 → 1. The structural congruence of the calculus is the smallest congruence relation ≡_{s} such that ⟨A(D̄), ∥, 1_{A}⟩_{/≡_{s}} is a commutative and idempotent monoid. The reduction rules of the calculus are given in Figure 1. We also define the relation ρ_{A} ⊆ A(D̄) × A(D̄) given, for each A, A′ ∈ A(D̄), by

A ρ_{A} A′ ⟺^{def} ∃n ∈ ℕ . A = A_{1} ∧ A_{n} = A′ ∧ A_{1} ↦ A_{2} ↦ ⋯ ↦ A_{n} ↛

In the following we will systematically abuse the notation denoting A(D̄)_{/≡_{s}} simply by A(D̄). Consequently, every assertion concerning A(D̄) is to be intended modulo structural congruence. We introduce now, following [35], a normal form for finite cc agents.

Structure

{A_{1} ≡_{s} A′_{1} A′_{1} ⟼ A′_{2} A′_{2} ≡_{s} A_{2} \atop A_{1} ⟼ A_{2}}  {A_{1} ⟼ A′_{1} \atop A_{1} ∥ A_{2} ⟼ A′_{1} ∥ A_{2}}

Reduction r(1, 2)

{C_{1}^{a} ⊢ C_{2}^{a} C_{1}^{a} ⊗ C_{2}^{t} ⊢ C_{1}^{t} \atop (C_{1}^{a} → C_{1}^{t}) ∥ (C_{2}^{a} → C_{2}^{t}) ⟼ (C_{2}^{a} → C_{2}^{t})}

Deduction d(1, 2)

C_{1}^{t} ⊢ C_{2}^{a} C_{1}^{t} ⊬ C_{2}^{t} ; (C_{1}^{a} → C_{1}^{t}) ∥ (C_{2}^{a} → C_{2}^{t}) ⟼ (C_{1}^{a} → (C_{1}^{t} ⊗ C_{2}^{t})) ∥ (C_{2}^{a} → C_{2}^{t})

Absorption a(1, 2)

C_{1}^{a} ⊩ C_{2}^{a}  C_{1}^{a} ⊬ C_{2}^{t}  C_{1}^{t} ⊩ C_{1}^{a} ⊗ C_{2}^{t} ; (C_{1}^{a} → C_{1}^{t}) ∥ (C_{2}^{a} → C_{2}^{t}) ⟼ ((C_{1}^{a} ⊗ C_{2}^{t}) → C_{1}^{t}) ∥ (C_{2}^{a} → C_{2}^{t})

Fig. 1. Reduction rules for finite cc agents.

Definition 31 (Semantic normal form.) [35] An agent A ∈ A(D̄) is in semantic normal form if and only if A = 1_{A} or A = ∥_{i=1}^{n} C_{i}^{a} → C_{i}^{t} and, for each i, j ∈ {1, …, n}:

N_{1}. C_{i}^{t} ⊩ C_{i}^{a}; N_{2}. i ≠ j ⟹ C_{i}^{a} ≠ C_{j}^{a}; N_{3}. C_{i}^{a} ⊩ C_{j}^{a} ⟹ C_{i}^{a} ⊩ C_{j}^{t}; N_{4}. C_{i}^{t} ⊢ C_{j}^{a} ⟹ C_{i}^{t} ⊢ C_{j}^{t}.

It turns out that this normal form is indeed very strong, whence its name.

Theorem 32 [35] Two agents A_{1}, A_{2} ∈ A(D̄) have the same semantic normal form if and only if [[A_{1}]] = [[A2]].

The purpose of our rewriting system is to put finite cc agents into semantic normal form, preserving their original semantics.

Theorem 33 For each agent A ∈ A(D̄) in syntactic normal form, if A ρ_{A} A′ then [[A]] = [[A′]] and A′ is in semantic normal form. The term-rewriting system depicted in Figure 1 is strongly normalizing. Thus the relation ρ_{A} is indeed a function ρ_{A} : A(D̄) → A(D̄). Finally, for A_{1}, A_{2} ∈ A(D̄) we have ρ_{A}(A_{1}) = ρ_{A}(A_{2}) if and only if [[A_{1}]] = [[A2]].

The situation here is almost identical to the one of Definition 21, in that we have a domain-independent strong normal form also for the present class of constraints (i.e. agents) incorporating the notion of dependency.

Definition 34 (Elements.) The elements of A(D̄) are the fixed points of the inference map ρ_{A}. The set of elements of A(D̄) will be denoted by |A(D̄)|.

We are now in position to introduce a new class in our hierarchy of constraint systems.

Definition 35 (Ask-and-tell constraint system.) Given a constraint sys-

tem D̄ = ⟨D, ⊗, ⊕, 0, 1, {¯∃ ; ¯∃Λ⃗}, {dX̄Ȳ }⟩, let A = |A(D̄)|. Then let 0_{A}, 1_{A} ∈ A,

and ⊗_{A} : A × A → A be given, for each A_{1}, A_{2} ∈ A, by

0_{A} =^{def} 1 → 0,
1_{A} =^{def} 1 → 1,

A_{1} ⊗_{A} A_{2} =^{def} ρ_{A}(A_{1} ∥ A_{2}).

The projection operators ¯∃ ; ¯∃Λ⃗^{A} : A → A are given, for each Λ⃗ ⊆_{f} Vars and A ∈ A, by

¯∃ ; ¯∃Λ⃗^{A} A =^{def} ρ_{A} (\{ (¯∃ ; ¯∃Λ⃗ C^{a} → ¯∃ ; ¯∃Λ⃗ C^{t}) | \begin{matrix}(C^{t} → C^{a}) ∈ A and \\ ((1 → ¯∃ ; ¯∃Λ⃗ C^{a}) ⊗_{A} A) ⊢_{A} (1 → C^{a}) \end{matrix} \}) .

Finally, let ⊕_{A} : A × A → A be an operator satisfying the conditions G_{2} and G_{4} of Definition 6. For any indexed family {dX̄Ȳ^{A} }_{X̄,Ȳ ∈Vars^{⋆}} of elements of A, we will call ⟨A(D̄), ⊗_{A}, ⊕_{A}, 0_{A}, 1_{A}, {¯∃ ; ¯∃Λ⃗^{A}}, {dX̄Ȳ^{A} }⟩ an ask-and-tell constraint system over D̄ and ‘ ⊕_{A}’.

Notice that, as far as the diagonal elements are concerned, we have left complete freedom. This is because, in an ask-and-tell construction, the induced diagonals dX̄Ȳ^{A} = 1 → dX̄Ȳ are not necessarily a good choice (see Section 7.3 for a simple example).

Theorem 36 If D̄ is a c.s., then ⟨|A(D̄)|, ⊗_{A}, ⊕_{A}, 0_{A}, 1_{A}, {¯∃ ; ¯∃Λ⃗^{A}}, dX̄Ȳ^{A} ⟩ is so.

The projection operators are indeed quite complicated. The problem is originated from requirement N_{3} of the normal form of Definition 31. This requirement enforces the need of the absorption rule in the calculus. The rule, by strengthening the ask-constraint of pairs, introduces “false dependencies”. Consider, for instance, a constraint system where elements include the finite subsets of { p(X), q(X), r(X) | X ∈ Vars } and the operators ⊗ and ⊕ are set union and intersection, respectively. The non-normalized cc agent over this constraint system

A = 1 → {q(Y)} ∥ {p(X)} → {r(X), q(Y)}

is normalized, by means of the absorption rule, to

A′ = 1 → {q(Y)} ∥ {p(X), q(Y)} → {r(X), q(Y)}.

The absorption rule has thus introduced the dependency of r(X) from q(Y), which is indeed false in the context of A′ (as it was in the context of A). A definition of the projection operators not taking into account this phenomenon would cause the inaccurate result ¯∃ ; ¯∃X^{A} A′ = 1_{A}. The projection operators given in Definition 35, instead, recognize the false dependency by noting that {p(X)} = ¯∃ ; ¯∃_{X}{p(X), q(Y)} is, in the context of A′, equivalent to {p(X), q(Y)}, that is

1 → {p(X)} ∥ A′ ⊢_{A} 1 → {p(X), q(Y)}.

We can thus obtain the expected result ¯∃ ; ¯∃X^{A} A′ = {p(X)} → {r(X)}. We will see in a moment other problems provoked by the absorption rule and, in turn, by the normal form we employ for agents.

7.1 Merge operators

Even though the ask-and-tell construction is parameterized with respect to a merge operator, it is possible to induce such an operator from the one of the base-level constraint system. Since this is a problematic point we proceed with care.

Suppose that the base-level constraint system D̄ is a lattice. Thus kernel operators over D̄ form again a lattice, where the lub is given, for k_{1} and k_{2} kernel operators and for each C ∈ D, by

(k_{1} ⊔ k_{2})(C) =^{def} k_{1}(C) ⊕ k_{2}(C), for C ∈ D,  (12)

whose fixed points are

(k_{1} ⊔ k_{2})(D) = { C_{1} ⊕ C_{2} | C_{1}, C_{2} ∈ k_{1}(D) ∪ k_{2}(D) }.

In terms of kernel operators, as pointed out in [34], this can be thought of as a kind of determinate disjunction: k_{1} ⊔ k_{2} gives, on any input C, the strongest common information between k_{1} and k_{2}. The computational significance of this concept has been first recognized in [39], where determinate disjunction allows for significant improvements in some constraint propagation algorithms.

The problem is that, even when k_{1} and k_{2} are represented by finite cc agents A_{1} and A_{2}, namely k_{1} = A_{1}^{K} and k_{2} = A_{2}^{K}, we have no guarantees whatsoever that k_{1} ⊔ k_{2} is representable by a finite cc agent. In other words, (syntactic) finite cc agents are not, in general, closed under the (semantic) lub operation.

As a consequence, we must content ourselves with upper bounds (unless we are willing to enrich our representation language with a construct like A_{1} + A_{2} expressing determinate disjunction, and we are not). Observe that the very precise effect of (12) can be obtained (at a consequently high cost) applying a powerset construction (Section 6) to the ask-and-tell constraint system considered. This way, when merging two (non-redundant) agents we will keep both of them, thus realizing, in practice, the ‘+’ construct mentioned above. If we do that, obviously, there is no need at all to define a merge operator at the ask-and-tell level.

In our general situation, the base-level constraint system D̄ might not be a lattice, and (12) might not define a kernel operator. In these cases, an upper bound on the poset of kernel operators over D̄ can be given as

(k_{1} ˜⊔ k_{2})(C) =^{def} C ⊗ (k_{1}(C) ⊕ k_{2}(C)), for C ∈ D,  (13)

which, still, is not guaranteed to correspond to any finite cc agent over D̄. We stress again that our non-commitment to lattices in the general definition of constraint systems (Section 3.3) is not merely dictated by the desire of freely managing the complexity/precision tradeoff. In cases like the one at hand we have no other sensible choice due to representation problems.

Our study of computable merge operators starts with a simple operation merging two (not necessarily normalized) agents into one. This is done, roughly speaking, by taking the meet of the ask constraints, and the merge of the tell constraints.

Definition 37 (Merge operator over agents.) Consider a constraint system D̄ = ⟨D, ⊗, ⊕, 0, 1, {¯∃ ; ¯∃Λ⃗}, {dX̄Ȳ }⟩, and any two finite cc agents over D̄ in syntactic normal form: A_{1} = ∥_{i=1}^{n} C_{i}^{a} → C_{i}^{t} and A_{2} = ∥_{j=1}^{m} D_{j}^{a} → D_{j}^{t}. Then

A_{1} ˜⊕_{A} A_{2} =^{def} ∥_{i=1}^{n} ∥_{j=1}^{m}(C_{i}^{a} → C_{i}^{t}) ˜⊕_{A} (D_{j}^{a} → D_{j}^{t}),  (14)

where, if we define C_{ij}^{a} =^{def} C_{i}^{a} ⊗ D_{j}^{a} and C_{ij}^{t} =^{def} C_{i}^{t} ⊕ D_{j}^{t}, we have

(C_{i}^{a} → C_{i}^{t}) ˜⊕_{A} (D_{j}^{a} → D_{j}^{t}) =^{def} \{ \begin{matrix}1_{A}, & if C_{ij}^{a} ⊢ C_{ij}^{t}; \\ C_{ij}^{a} → (C_{ij}^{a} ⊗ C_{ij}^{t}), & otherwise. \end{matrix}  (15)

It is easy to see that this syntactic operation corresponds, at the semantic level, to an upper bound.

Proposition 38 If A_{1} and A_{2} are as stated in Definition 37, then A_{1} ˜⊕_{A} A_{2} is in syntactic normal form. Further, we have both [[A_{1}]] ⊆ [[A_{1} ˜⊕_{A} A_{2}]] and [[A_{2}]] ⊆ [[A_{1} ˜⊕_{A} A_{2}]], that is, A_{1} ⊢_{A} A_{1} ˜⊕_{A} A_{2} and A_{2} ⊢_{A} A_{1} ˜⊕_{A} A_{2}.

We now have an obvious merge operator which is completely determined by the underlying, base-level constraint system.

Definition 39 (Canonical ask-tell merge operator.) Let A =^{def} |A(D̄)|. The operator ˆ⊕_{A} : A × A → A given, for each A_{1}, A_{2} ∈ A, by

A_{1} ˆ⊕_{A} A_{2} =^{def} ρ_{A}(A_{1} ˜⊕_{A} A_{2})

is called the canonical merge operator over A induced by D̄.

Unfortunately, the canonical merge operator turns out to be inaccurate, due to the normal form employed for agents. Consider the ask-and-tell construction applied to the Con domain of Section 5.1, and the agents in normal form^{5}

A_{1} =^{def} 1 → Z ∥ XZ → XY Z and A_{2} =^{def} X → XY.

It easy to see that the canonical merge operator gives

A_{1} ˆ⊕_{A} A_{2} =^{def} ρ_{A}(A_{1} ˜⊕_{A} A_{2}) = XZ → XY Z.

If we consider the non-normalized agent A′_{1} = 1 → Z ∥ X → XY Z, we have [[A′_{1}]] = [[A_{1}]] but ρ_{A}(A′_{1} ˜⊕_{A} A_{2}) = X → XY, which is strictly stronger than A_{1} ˆ⊕_{A} A_{2}. The problem can be tracked down, as in the case of the projection operators, to the introduction, by means of the absorption rule, of “unnecessary dependencies” needed to satisfy condition N_{3} of the semantic normal form. However, while for projection operators we had a standard solution, here the situation is more difficult. As the example suggests, in order to define a precise merge operator we need mechanisms for

(i) weakening constraints (now we only strengthen them), and (ii) splitting ask-tell pairs (now we only combine them).

We now give a general way of defining merge and widening operators for the ask-and-tell construction which are more precise than the canonical merge operator. First of all, let us deal with the problem of constraints’ weakening.

Definition 40 (Weakening.) An operation ⊚: D → D over a constraint system D̄ = ⟨D, ⊗, ⊕, 0, 1, {¯∃ ; ¯∃Λ⃗}, {dX̄Ȳ }⟩ is said a weakening operator for D̄ if it satisfies, for each C, C_{1}, C_{2} ∈ D:

Q_{1}. (C_{1} ⊚ C_{2}) ⊗ C_{1} = C_{1}, Q_{2}. (C_{1} ⊚ C_{2}) ⊗ C_{2} = C_{1} ⊗ C_{2}, Q_{3}. (C_{1} ⊚ C_{2}) ⊚ C_{2} = C_{1} ⊚ C_{2}.

5 For simplicity we use juxtaposition instead of the usual set notation.

The intuitive explanation of this axiomatization is as follows. Condition Q_{1}, which can be restated as C_{1} ⊢ C_{1} ⊚ C_{2}, means that the weakening operation is correct (it does not add anything). Condition Q_{2} states that weakenings are not too aggressive: a weakened constraint can be restored by adding what was taken out. Q_{3} says that taking out twice the same thing is pointless. Observe that these conditions are very weak, while being sufficient for what follows.

Example 41 (Weakening over intervals.) Consider a domain for numerical bounds analysis based on intervals. For instance, take the simple constraint system of Section 4.2, restricted to the intervals component, and apply to it the determinate c.s. construction. A weakening operator can be defined along the following lines, considering, for simplicity, only closed intervals:

[ l_{1}, u_{1} ] ⊚ [ l_{2}, u_{2} ] =^{def} [ l, u],

where

l =^{def} \{ \begin{matrix}−∞, & if l_{1} ≤ l_{2}; \\ l_{1}, & otherwise; \end{matrix}  and  u =^{def} \{ \begin{matrix}+∞, & if u_{1} ≥ u_{2}; \\ u_{1}, & otherwise. \end{matrix}

Such an operator is easily verified being a weakening.

We are now in position to define a class of procedures for weakening the ask constraints of finite cc agents while preserving the semantics. As this operation is somewhat opposite to the absorption rewrite rule of our rewriting system, we call it de-absorption. This involves the splitting of ask-tell pairs.

Definition 42 (De-absorption step.) Let A = ∥_{i=1}^{n} C_{i}^{a} → C_{i}^{t} an agent in syntactic normal form over a c.s. D̄, and let ⊚ be a weakening over D̄. Then A′ is obtained from A by means of a de-absorption step based on ⊚ if and only if h, k ∈ {1, …, n} are such that C_{h}^{a} ⊢ C_{k}^{a}, the condition C_{h}^{a} ≠ (C_{h}^{a} ⊚C_{k}^{t})⊗C_{k}^{a} holds, and

A′ = ((C_{h}^{a} ⊚ C_{k}^{t}) ⊗ C_{k}^{a} → C_{h}^{t}) ∥ A.

Observe that any de-absorption step results in the strict weakening of an ask constraint. In fact, we have C_{h}^{a} ⊢ (C_{h}^{a} ⊚C_{k}^{t}) by Q_{1}, and C_{h}^{a} ⊢ C_{k}^{a} by hypothesis, thus C_{h}^{a} ⊩ (C_{h}^{a} ⊚ C_{k}^{t}) ⊗ C_{k}^{a}.

Definition 43 (De-absorption procedure.) A de-absorption procedure is any algorithm transforming a finite cc agents in syntactic normal form which can be characterized as follows:

phase 1. transform the input agent A into A′ by performing any number of de-absorption steps; phase 2. transform A′ into the output agent A′′ by applying the rewriting

system of Figure 1 restricted to the structural and reduction rules.

A de-absorption procedure will be called maximal if it applies all the possible de-absorption steps.

It is now possible to prove the following result.

Theorem 44 Any de-absorption procedure is semantics-preserving.

In all those cases where we have a de-absorption procedure which is a function over |A(D̄)| we have an obvious way to define a merge operator: by applying the syntactic merge operator of Definition 39 to de-absorbed agents.

Definition 45 (Merge operator with de-absorption.) Let D̄ be a constraint system, and let δ_{⊚}: |A(D̄)| → A(D̄) be a de-absorption procedure. The merge operator based on δ_{⊚} is given, for each A_{1}, A_{2} ∈ |A(D̄)|, by

A_{1} ˙⊕_{A} A_{2} =^{def} ρ_{A}(δ_{⊚}(A_{1}) ˜⊕_{A} δ_{⊚}(A_{2})).

Any such operator, by virtue of Theorem 44 and Proposition 38, is clearly a merge operator in the sense of Definition 6. De-absorption procedures which are not functions are still useful for designing widening operators.

We now quickly show some examples of ask-and-tell constraint systems. For the more interesting things we have to wait until the next section, where combination of constraint domains are introduced.

7.2 More bounds and relations analysis for numeric domains

Ask-and-tell constraint systems are suitable for modeling approximate inference techniques which are very useful in a practical setting. Following Section 4.2, there is another technique which is used for the analysis described in [5,6,3]: relational arithmetic [38]. This technique allows to infer constraints on the qualitative relationship of an expression to its arguments. Consider the simple constraint system of Section 4.2, and apply to it the determinate construction of Section 5. Now apply the ask-and-tell construction to the result. Relational arithmetic can be described by a number of (concurrent) agents. Here are some of them, where x and y are arithmetic expressions, and ▷◁ ranges in R =^{def} {=, ≠, ≤ <, ≥, >}:

ask(x ▷◁ 0) → tell((x + y) ▷◁ y)
ask(x > 0 ∧ y > 0 ∧ x ▷◁ 1) → tell((x ∗ y) ▷◁ y)
ask(x > 0 ∧ y < 0 ∧ x ▷◁ 1) → tell(y ▷◁ (x ∗ y))
ask(x ▷◁ y) → tell(e^{x} ▷◁ e^{y})

An example of inference is deducing X + 1 ≤ Y + 2X + 1 from X ≥ 0 ∧ Y ≥ 0. Notice that there is no restriction to linear constraints.

7.3 Definiteness analysis: Def, Pos, and more

The prototypical example of data-flow analysis taking advantage of dependency information is definiteness analysis. In our setting a domain for definiteness can be obtained as follows. Take the atomic s.c.s. of Section 4.1. Apply to it the determinate construction as outlined in Section 5.1. Now apply the ask-and-tell construction to the result, with the merge operator obtained along the lines of Definition 45 choosing:

(i) diagonal elements like dXY^{A} =^{def} {X} → {X, Y } ∥ {Y } → {X, Y }; (ii) set-theoretic difference as weakening operator; (iii) the maximal de-absorption procedure (i.e. the one which applies all the

possible de-absorption steps).

It can be shown that the domain so obtained is Def [17,2]. Its elements can keep track of non-trivial dependencies like the ones induced by symbolic and numeric constraints. For example, the dependencies of A = f(B, C) are captured by the agent {A} → {B, C} ∥ {B, C} → {A}. This example gives us the possibility of pointing out that the entire business of weakenings and de-absorption procedures is not something we can easily avoid. When using definite sentences to represent dependencies, as in our case and in the representations for Def studied in [2], obtaining a maximal weakening of the antecedents is crucial for obtaining precise merge operators, let alone for computing the join when it exists. Our present requirement of employing maximal de-absorption corresponds to the requirement, in the representations studied in [2], of the sentences being in orthogonal form (which has its costs, since orthogonality must be obtained and preserved by all the domain’s operations). In [2] it is also presented a merge operator, for the representation RCNF_{Def}, intended to trade precision for efficiency. It does that by not insisting on orthogonality, which in our setting corresponds to the use of a partial de-absorption procedure.

Pos is (like Def ) a domain of boolean functions [10,2]. It consists precisely of those functions assuming the true value under the everything-is-true assignment. In [2] it is shown that Pos is strictly more precise than Def for groundness analysis. If we apply the powerset construction of Section 6 to the ask-and-tell c.s. of the previous section we obtain a very precise (and complex) domain for simple dependencies. In [22] it is referred to as ℧(Def) (where ℧ denotes disjunctive completion) and is shown to be equivalent to ℧(Pos). On the other hand, in [20] it has been shown that ℧(Pos) is strictly more precise than Pos, even though this extra-precision is not needed for definiteness analysis.

8 Combination of domains

It is well known that different data-flow analyses can be combined together. In the framework of abstract interpretation this can be achieved by means of standard constructions such as reduced product and down-set completion [13,14]. The key point is that the combined analysis can be more precise than each of the component ones for they can mutually improve each other. However, the degree of cross-fertilization is highly dependent on the degree and quality of interaction taking place among the component domains.

We now propose a general methodology for domain combination with asynchronous interaction. The interaction among domains is asynchronous in that it can occur at any time, or, in other words, it is not synchronized with the domain’s operations. This is achieved by considering ask-and-tell constraint systems built over product constraint systems. These constraint systems allow to express communication among domains in a very simple way. They also inherit all the semantic elegance of concurrent constraint programming languages, which provide the basis for their construction. Recently, a methodology for the combination of abstract domains has been proposed in [11], which is directly based onto low-level actions such as tests and queries. While the approach in [11] is immediately applicable to a wider range of analyses (including the ones dealing with non-monotonic properties) the approach we follow here for our restricted set of analyses has the merit of being much more elegant. We start with a finite set of constraint systems each expressing some properties of interest, and we wish to combine them so to: (1) perform all the analyses at the same time; and (2) have the domains cooperate to the intent of mutually improving each other. The first goal is achieved by considering the product of the given constraint systems.

A product constraint system can easily be obtained: given the constraint systems D̄_{1}, …, D̄_{n} just consider their algebraic direct product (where all the operations and relations are defined point-wise). An alternative way of obtaining a product constraint system is to start from a collection of simple constraint systems and then applying the determinate construction.

Definition 46 (Product of simple constraint systems.) Given a finite family of simple constraint systems S_{i} = ⟨C_{i}, ⊢_{i}, ⊥_{i}, ⊤_{i}⟩ for i = 1, …, n, the product of the family is the structure given by

∏_{i=1}^{n} S_{i} =^{def} ⟨C_{×}, ⊢_{×}, ⊥_{×}, ⊤_{×}⟩,

where the product tokens are

C_{×} =^{def} { (c_{1}, ⊤_{2}, …, ⊤_{n}) | c_{1} ∈ C_{1} }
∪ { (⊤_{1}, c_{2}, ⊤_{3}, …, ⊤_{n}) | c_{2} ∈ C_{2} }
⋮
∪ { (⊤_{1}, …, ⊤_{n−1}, c_{n}) | c_{n} ∈ C_{n} }
∪ {⊥_{×}},

⊥_{×} =^{def} (⊥_{1}, …, ⊥_{n}), ⊤_{×} =^{def} (⊤_{1}, …, ⊤_{n}), and the product entailment is defined as the least relation satisfying conditions E_{1}–E_{5} of Definition 19 and the following ones, for each C ∈ ℘_{f}(C_{×}):

π_{1}(C) ⊢_{1} c_{1} ⟹ C ⊢_{×} (c_{1}, ⊤_{2}, …, ⊤_{n})
⋮  ⋮  ⋮
π_{n}(C) ⊢_{n} c_{n} ⟹ C ⊢_{×} (⊤_{1}, …, ⊤_{n−1}, c_{n}).

Taking the product of constraint systems, we have realized the simplest form of domain combination. It corresponds to the direct product construction of [13], allowing for different analyses to be carried out at the same time. Notice that there is no communication at all among the domains.

However, as soon as we consider the ask-and-tell constraint system built over the product, we can express asynchronous communication among the domains in complete freedom. At the very least we would like to have the smash product among the component domains. This is realized by the agent ∥_{i=1}^{n} 0_{i} → 0_{×}. To say it operationally, the smash agent globalizes the (local) failure on any of the component domains. This is the only domain-independent agent we have. Things become much more interesting when instantiated over particular constraint domains. In the CLP(R) system [27] non-linear constraints (like X = Y ∗ Z) are delayed (i.e. not treated by the constraint solver) until they become linear (e.g. until either Y or Z are constrained to take a single value). In standard semantic treatments this is modeled in the operational semantics by carrying over, besides the sequence of goals yet to be solved, a set of delayed constraints. Constraints are taken out from this set (and incorporated into the constraint store) as soon as they become linear. We believe that this can be viewed in an alternative way which is more elegant, as it easily allows for taking into account the delay mechanism also in the bottom-up semantics, and makes sense from an implementation point of view. The basic claim is the following: CLP(R) has three computation domains: Herbrand, ℝ (well, an approximation of it), and definiteness. In other words, it also manipulates, besides the usual ones, constraints of the kind ground^{♮}(X) which is interpreted as the variable X being definitively bound to a unique value. We can express the semantics of CLP(R) (at a certain level of abstraction) with delay of non-linear constraints by considering the ask-and-tell constraint system over the product of the above three domains. In this view, a constraint of the form X = Y ∗ Z in a program actually corresponds to the agent

ask(ground^{♮}(Y); ground^{♮}(Z)) → tell(X = Y ∗ Z).

In fact, any CLP(R) user must know that X = Y ∗ Z is just a shorthand for that agent! (A similar treatment can be done for logic programs with delay declarations.) Obviously, this cannot be forgotten in abstract constraint systems intended to formalize correct data-flow analyses of CLP(R). Referring back to sections 4.2 and 7.2, when the abstract constraint system extracts information from non-linear constraints, for example with the agent

A = ask(Y > 0 ∧ Z > 0 ∧ Y ▷◁ 1) → tell((Y ∗ Z) ▷◁ Z)

of relational arithmetic, you cannot simply let X = Y ∗ Z stand by itself. By doing this you would incur the risk of overshooting the concrete constraint system (thus loosing soundness), which is unable to deduce anything from nonlinear constraints. The right thing to do is to combine the numeric abstract constraint system with one for definiteness (by the product and the ask-and-tell constructions) and using, instead of A, the agent

A′ = ask(ground^{♯}(Y); ground^{♯}(Z)) → A.

Beware not to confuse ground^{♮}(X) with ground^{♯}(X). The first is the concrete one: X is definite if and only if ground^{♮}(X) is entailed in the current concrete store. In contrast, having ground^{♯}(X) entailed in the abstract constraint store at some program point, and assuming a correct definiteness analysis, means that X is certainly bound to a unique value in the concrete computation at that program point. The vice-versa, of course, does not necessarily hold.

Let us see another example. The analysis described in [24] aims at the compiletime detection of those non-linear constraints that will become linear at runtime. This analysis is important for remedying the limitation of CLP(R) to linear constraints by incorporating powerful (and computationally complex) methods from computer algebra as the ones employed in RISC-CLP(Real) [25]. With the results of the above analysis this extension can be done in a smooth way: non-linear constraints which are guaranteed to become linear will be simply delayed, while only the other non-linear constraints will be treated with the special solving techniques. Thus, programs not requiring the extra power of these techniques will be hopefully recognized as such, and will not pay any penalties. The analysis of [24] is a kind of definiteness. One of its difficulties shows up when considering the simplest non-linear constraint: X = Y ∗ Z. Clearly X is definite if Y and Z are such. But we cannot conclude that the definiteness of Y follows from the one of X and Z, as we need also the condition Z ≠ 0. Similarly, we would like to conclude that X is definite if Y or Z have a zero value. Thus we need approximations of the concrete values of variables (i.e. bounds analysis), something which is not captured by common definiteness analyses while being crucial when dealing with nonlinear constraints. If we take the ask-and-tell construction over the product of a constraint system for definiteness with a numerical one we can solve the problem. X = Y ∗ Z would be abstractly compiled into the agent

ask(ground^{♯}(Y) ∧ ground^{♯}(Z)) → tell(ground^{♯}(X))
∥ ask(Y = 0; Z = 0) → tell(ground^{♯}(X))
∥ ask(ground^{♯}(X) ∧ ground^{♯}(Z) ∧ Z ≠ 0) → tell(ground^{♯}(Y))
∥ ask(ground^{♯}(X) ∧ ground^{♯}(Y) ∧ Y ≠ 0) → tell(ground^{♯}(Z)).

Of course, this is much more precise than the Def formula X ← Y ∧ Z. Observe that, when analyzing CLP(R) programs, there is a bidirectional flow of information: definiteness information is required for a correct handling of delayed constraints and thus for deriving more precise numerical patterns which, in turn, are used to provide more precise definiteness information. There is another obvious way in which numerical bounds and relations improve definiteness (and any other analysis, indeed): by excluding computation paths which are doomed to fail (this is modeled in a domain-independent way by the smash agent seen above). We are thus requiring a quite complicated interaction between domains. It is even more complicated if you consider that the numerical component we have sketched is the combination (in the sense of the present section) of a domain for intervals with one for arithmetic relationships (even though, for simplicity, it was not presented in that way).

The techniques we propose are suitable for approximating the behavior of several common built-ins. Consider, for instance, the functor/3 built-in. Consider a product constraint system with four components: one for simple types (where tokens like compound(X) or atom(X) indicate that the variable X is bound to take Herbrand compounds or constants, respectively) one for definiteness, one incorporating numerical information (including at least signs, e.g. tokens of the kind X ≥ 0, X > 0 and X = 0), and one involving symbolic, structural information. Then, the (success) semantics of functor(T, F, N) can be approximated easily and quite precisely by means of the following finite agent over the product:

tell(term(T), atom(F), ground(F), integer(N), N ≥ 0, ground(N))∥

ask(atom(T); N = 0; T = F ) →
tell(atom(T), ground(T), N = 0, T = F ) ∥
ask(compound(T); N > 0; T ≠ F ) →
tell(compound(T), N > 0, T ≠ F ).

9 Conclusion and future work

We have shown a notion of constraint system which is general enough to encompass both the concrete domains of computation of actual constraint logicbased languages, and several of their abstract interpretations useful for dataflow analysis. We have also shown how these constraint systems are integrated within an appropriate framework for the definition of non-standard semantics of constraint logic-based languages. Some significant members of the introduced class of constraint systems have been presented, together with construction techniques which induce a hierarchy of domains. These domains have several nice features from a theoretical point of view. In particular, we have proposed a general methodology for domain combination with asynchronous interaction. In this kind of combinations the communication among domains can be expressed in a very simple way. The methodology also inherits all the semantic elegance of concurrent constraint programming languages, which provide the basis on which it is built. Future work includes studying in depth the problem of the semantic normal form for finite cc agents, both in general and in particular cases. The aim is to find more satisfactory solutions to the problem of merging finite cc agents. We also would like to answer the following question: are there variations of these ideas which are applicable also to analysis oriented towards “non-logical” properties?

Acknowledgement

I wish to thank Maurizio Gabbrielli, Roberto Giacobazzi, Giorgio Levi, Catuscia Palamidessi, Francesca Rossi, Vijay Saraswat, and Enea Zaffanella for the discussions we had on the subject and for reading draft versions of this paper. Enea was especially kind in helping me with some technical issues. Special thanks to Giorgio for his extensive support.

References

[1] J. F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832–843, 1983.

[2] T. Armstrong, K. Marriott, P. Schachte, and H. Sondergaard. Two classes of boolean functions for dependency analysis. Technical Report 94/211, Dept. Computer Science, Monash University, Melbourne, 1994.

[3] R. Bagnara. On the detection of implicit and redundant numeric constraints in CLP programs. In M. Alpuente, R. Barbuti, and I. Ramos, editors, Proceedings of the “1994 Joint Conference on Declarative Programming (GULP-PRODE ’94)”, pages 312–326, Peñíscola, Spain, September 1994.

[4] R. Bagnara. A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. Technical Report TR-96-10, Dipartimento di Informatica, Università di Pisa, 1996.

[5] R. Bagnara, R. Giacobazzi, and G. Levi. Static analysis of CLP programs over numeric domains. In M. Billaud, P. Castéran, MM. Corsini, K. Musumbu, and A. Rauzy, editors, Actes “Workshop on Static Analysis ’92”, volume 81–82 of Bigre, pages 43–50, Bordeaux, September 1992. Extended abstract.

[6] R. Bagnara, R. Giacobazzi, and G. Levi. An application of constraint propagation to data-flow analysis. In Proceedings of “The Ninth Conference on Artificial Intelligence for Applications”, pages 270–276, Orlando, Florida, March 1993. IEEE Computer Society Press, Los Alamitos, CA.

[7] R. Barbuti and A. Martelli. A structured approach to semantics correctness. Science of Computer Programming, 3:279–311, 1983.

[8] M. Codish and B. Demoen. Analysing logic programs using “Prop”-ositional logic programs and a magic wand. In Dale Miller, editor, Logic Programming - Proceedings of the 1993 International Symposium, pages 114–129, Vancouver, Canada, 1993. The MIT Press.

[9] P. Codognet and G. Filè. Computations, abstractions and constraints. In Proc. Fourth IEEE Int’l Conference on Computer Languages. IEEE Press, 1992.

[10] A. Cortesi, G. Filè, and W. Winsborough. Prop revisited: Propositional formula as abstract domain for groundness analysis. In Proc. Sixth IEEE Symp. on Logic In Computer Science, pages 322–327. IEEE Computer Society Press, 1991.

[11] A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming. In Conference Record of POPL ’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 227–239, Portland, Oregon, January 1994.

[12] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. Fourth ACM Symp. Principles of Programming Languages, pages 238– 252, 1977.

[13] P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. Sixth ACM Symp. Principles of Programming Languages, pages 269–282, 1979.

[14] P. Cousot and R. Cousot. Abstract interpretation and applications to logic programs. Journal of Logic Programming, 13(2 & 3):103–179, 1992.

[15] P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–549, 1992.

[16] P. Cousot and R. Cousot. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. In M. Bruynooghe and M. Wirsing, editors, Proc. of PLILP’92, volume 631 of Lecture Notes in Computer Science, pages 269–295. Springer-Verlag, Berlin, 1992.

[17] P. Dart. On derived dependencies and connected databases. Journal of Logic Programming, 11(2):163–188, 1991.

[18] E. Davis. Constraint propagation with interval labels. Artificial Intelligence, 32:281–331, 1987.

[19] S. K. Debray and R. Ramakrishnan. Abstract interpretation of logic programs using magic transformations. The Journal of Logic Programming, 18(2):149– 176, February 1994.

[20] G. Filé and F. Ranzato. Improving abstract interpretations by systematic lifting to the powerset. In M. Bruynooghe, editor, Proceedings of the 1994 International Logic Programming Symposium (ILPS ’94), pages 655–669. The MIT Press, 1994.

[21] R. Giacobazzi, S. K. Debray, and G. Levi. Generalized semantics and abstract interpretation for constraint logic programs. Journal of Logic Programming, 25(3):191–247, 1995.

[22] R. Giacobazzi and F. Ranzato. Compositional optimization of disjunctive abstract interpretations. In H.R. Nielson, editor, Proc. of the 1996 European Symposium on Programming, volume 1058 of Lecture Notes in Computer Science, pages 141–155. Springer-Verlag, Berlin, 1996.

[23] G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, 1980.

[24] M. Hanus. Analysis of nonlinear constraints in CLP(R). In David S. Warren, editor, Proceedings of the Tenth International Conference on Logic Progra mming, pages 83–99, Budapest, Hungary, 1993. The MIT Press.

[25] H. Hong. RISC-CLP(Real): Logic programming with non-linear constraints over the reals. In F. Benhamou and A. Colmerauer, editors, Constraint Logic Programming: Selected Research. The MIT Press, Cambridge, Mass., 1993.

[26] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. Fourteenth Annual ACM Symp. on Principles of Programming Languages, pages 111–119. ACM, 1987.

[27] J. Jaffar, S. Michaylov, P. Stuckey, and R. Yap. The CLP(R) language and system. ACM Transactions on Programming Languages and Systems, 14(3):339–395, 1992.

[28] J. Jaffar and M. J. Maher. Constraint logic programming: A survey. The Journal of Logic Programming, 19 & 20:503–582, May 1994.

[29] N. D. Jones and H. Søndergaard. A semantics-based framework for the abstract interpretation of Prolog. In S. Abramsky and C. Hankin, editors, Abstract Interpretation of Declarative Languages, pages 123–142. Ellis Horwood Ltd, 1987.

[30] A. K. Mackworth. Consistency in networks of relations. Artificial Intelligence, 8:99–118, 1977.

[31] C. Mellish. Some global optimizations for a Prolog compiler. Journal of Logic Programming, 2:43–66, 1985.

[32] U. Montanari. Networks of constraints: Fundamental properties and applications to picture processing. Inform. Sci., 7:95–132, 1974.

[33] V. A. Saraswat. The category of constraint systems is cartesian-closed. In Proc. 7th IEEE Symp. on Logic in Computer Science, Santa Cruz, 1992.

[34] V. A. Saraswat. Concurrent Constraint Programming. MIT Press Cambridge, Mass., 1993.

[35] V. A. Saraswat, M. Rinard, and P. Panangaden. Semantic foundation of concurrent constraint programming. In Proc. Eighteenth Annual ACM Symp. on Principles of Programming Languages, pages 333–353. ACM, 1991.

[36] D. Scott. Domains for denotational semantics. In M. Nielsen and E. M. Schmidt, editors, Proc. ninth Int. Coll. on Automata, Languages and Programming, volume 140 of Lecture Notes in Computer Science, pages 577–613. Springer-Verlag, Berlin, 1982.

[37] M. C. Scudellari. Analisi bottom-up di programmi logici con vincoli basata su trasformazioni magic-set. M.Sc. dissertation, R. Bagnara and G. Levi supervisors, University of Pisa, April 1996. In Italian, available on WWW

at URL http://www.di.unipi.it/~bagnara.

[38] R. Simmons. Commonsense arithmetic reasoning. In Proc. AAAI-86, pages 118–124, 1986.

[39] P. Van Hentenryck, V. A. Saraswat, and Y. Deville. Constraint logic programming over finite domains: the design, implementation, and applications of cc(fd). Technical report, Brown University, Providence, RI, 1992.