J. LOGIC PROGRAMMING 1995:25, 3:191–248

GENERALIZED SEMANTICS AND ABSTRACT INTERPRETATION FOR CONSTRAINT LOGIC PROGRAMS

ROBERTO GIACOBAZZI, SAUMYA K. DEBRAY, AND GIORGIO LEVI

▷ We present a simple and powerful generalized algebraic semantics for constraint logic programs that is parameterized with respect to the underlying constraint system. The idea is to abstract away from standard semantic objects by focusing on the general properties of any—possibly non-standard— semantic definition. In constraint logic programming, this corresponds to a suitable definition of the constraint system supporting the semantic definition. An algebraic structure is introduced to formalize the notion of a constraint system, thus making classical mathematical results applicable. Both top-down and bottom-up semantics are considered. Non-standard semantics for constraint logic programs can then be formally specified using the same techniques used to define standard semantics. Different nonstandard semantics for constraint logic languages can be specified in this framework. In particular abstract interpretation of constraint logic programs can be viewed as an instance of the constraint logic programming framework itself. ◁ 1. INTRODUCTION

Partly supported by the EEC Human Capital and Mobility individual grant: “Semantic Definitions, Abstract Interpretation and Constraint Reasoning”, N. ERB4001GT930817 and by the Esprit Basic Research Action 3012 - Compulog I.

Partly supported by the National Science Foundation under grants CCR-8901283 and CCR-9123520.

Partly supported by “Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo” of C.N.R.

under grants no. 9100880.PF69.

Address correspondence to Roberto Giacobazzi, Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125 Pisa, E-mail: giaco@di.unipi.it

Received October 1993; revised June 1994; accepted February 1995.

THE JOURNAL OF LOGIC PROGRAMMING \begin{matrix}c \\ ◯ \end{matrix} Elsevier Science Inc., 1994 0743-1066/95/$9.50 655 Avenue of the Americas, New York, NY 10010 SSDI 0743-1066(95)00038-L

Constraint logic programming is a generalization of the pure logic programming paradigm, having similar model-theoretic, declarative and operational semantics [45]. Since the fundamental linguistic aspects of constraint logic programming can be separated from the details specific to particular constraint systems, it seems natural to parameterize the semantics of constraint logic programming languages with respect to the underlying constraint systems. We refer to such a semantics as a generalized semantics. Such generalized semantics provide a powerful tool for dealing with a variety of applications relating to the semantics of CLP programs. For example, by considering a domain of “abstract constraints” instead of the “concrete constraints” that are actually manipulated during program execution, we obtain for free a formal treatment of abstract interpretation. In this paper we focus on algebraic properties that characterize (possibly non-standard) semantic constructions in constraint logic programming. In particular we will focus on computed answer constraint semantics and abstraction. Our framework is therefore suitable to analyze successful computations and call patterns (the latter case can be obtained with a magic-like transformation as in [15]) of constraint logic programs. The algebraic approach we take to constraint interpretation makes it easy to identify a suitable set of operators that can be instantiated in different ways to obtain both standard and non-standard interpretations, relying on some simple axioms to ensure that desirable semantic properties are satisfied.

This work has two main technical contributions. The first is the definition of a structure for constraint interpretation that is weak enough to have general applicability, thus dealing with a variety of non-standard interpretations, and at the same time strong enough to ensure that relevant properties of the standard semantic construction, such as the existence of the fixed-point semantics and the equivalence between the top-down and the bottom-up semantics, still hold. The second is to show how a wide class of analysis techniques developed for pure and constraintbased logic programs can themselves be viewed as instances of the constraint logic programming paradigm. Indeed, the approximation of the meaning of programs by means of relations among the variables involved in the computation is a well known technique for specifying a space of approximate assertions for program analysis. We argue that the ability of the constraint logic programming paradigm to handle relations on a variety of semantic domains (e.g., real arithmetics, boolean algebras, etc.) allows this paradigm to be used for program analysis, both as a tool for the formal specification of abstract domains, and for the rapid prototyping of static analysis systems. Of course, in order that abstract domains and operators form constraint systems, we require additional (and orthogonal) conditions than simple correctness for semantic operators. Correctness is obviously necessary to get sound approximations in abstract interpretation (most frameworks for static analysis of logic programs require only correctness [5, 11, 15]), so apparently our approach may result a simple restriction of the standard abstract interpretation theory (at the current “state of the art”, some analyses like freeness are not directly definable as constraint systems). However, lot of interesting semantic properties of analysis (e.g. the equivalence between forward and backward evaluations) are orthogonal to soundness. We prove that all the (abstract) domains and operators that satisfy the constraint system conditions, provide (abstract) interpretations that satisfy the standard results of constraint logic programming semantics as proposed by Jaffar and Lassez [45]. This approach has some interesting practical applications, such as the ability to compile the dataflow analysis directly to an abstract machine for constraint logic programs—a logical extension of the “abstract compilation” scheme discussed by Hermenegildo et al. [42]. This removes the overhead of program interpretation incurred by keeping separate abstract and concrete interpretations, and can lead to significant improvements in the speed of analysis (e.g., see [17, 42, 68]). Our approach also makes it possible to close the gap that often exists between the formalization of dataflow analyses in terms of abstract interpretation and the realization of efficient implementations by means of appropriate data-structures and efficient algorithms. Applications of our framework to systematically derive efficient algorithms for dataflow analysis (e.g., by means of constraint propagation techniques for constraint solving) have been recently studied in [4]. Moreover, while non-standard semantics such as those considered in various dataflow analyses, are typically more abstract than the standard semantics, it is also possible, in our framework, to define non-standard semantics that are much more concrete than the standard semantics, i.e., take into account details of a particular implementation. Such semantics, illustrated in Section 4.3, can be used, for example, for reasoning about the correctness of compilers, debuggers, and other low-level tools for program manipulation.

The paper is structured as follows: in Section 2 we introduce the basic mathematical notations used throughout the paper. Section 3 introduces an incremental step-by-step algebraic specification for constraint systems. Section 4 provides both a top-down and a bottom-up semantics for constraint logic programs, parameterized with respect to the constraint system. In Section 5 we consider generalized semantics for constraint logic programs as a framework for semantics-based analyses for constraint logic programs. An example, namely rigidity analysis, is considered associating Boolean constraints with standard equations on terms. Some results on approximating constraints by means of upper closure operators on constraint systems are also given. This approach points out how some well-known program analysis techniques can be obtained by evaluating an abstract program into a variation of some existing CLP systems, such as CLP (Bool) for rigidity analysis; and, as shown in Section 6, CLP (R), where a weaker notion of “constraint system” for program analysis purposes is introduced by illustrating how a compile-time analysis problem, linear relationships analysis, can be formulated in terms of constraint logic programming over an appropriate constraint system. Section 7 contains a survey of the most important related works, and a discussion on limitations of our approach. Section 8 concludes. For continuity and ease of readability, the proofs of most of the results, together with auxiliary lemmata, have been moved to the appendix. This paper is an extended version of [36] and [37].

2. PRELIMINARIES

Throughout the paper we will assume familiarity with the basic notions of lattice theory (Birkhoff’s text [8] provides the necessary background) and abstract interpretation (see [22, 24]). In the following we summarize some of the mathematical notation used in the paper.

The set of natural numbers and reals are denoted by N and ℜ respectively. The cardinality of a set A is denoted |A|. Given sets A and B, A \ B denotes the set A where the elements in B have been removed. The powerset of a set S is denoted by ℘(S). The class of finite (possibly empty) subsets of a set S is denoted ℘^{f}(S). Let Σ be a possibly infinite set of symbols. Sequences are typically denoted by ⟨a_{1}, ..., a_{n}⟩ or simply a_{1}, ..., a_{n}, where a_{i} ∈ Σ and n ≥ 0. The empty sequence is denoted by ε. The set (family) of objects a_{i} indexed on a set of symbols Σ is denoted {a_{i}}_{i∈Σ}. The set of n-tuples of symbols in Σ is denoted Σ^{n}. When the length of sequences is fixed, sequences and tuples will be often considered equivalent notions. We occasionally abuse notation and treat sequences as sets. The transitive closure of a binary relation R is denoted by R^{∗}. Syntactic identity is denoted ≡.

A partial ordering is a binary relation that is reflexive, transitive and antisymmetric. A set P equipped with a partial order ≤ is said to be partially ordered, and sometimes written ⟨P, ≤⟩. Let ⟨P, ≤⟩ be a partially ordered set (poset), S ⊆ P is convex iff for each c, c′′ ∈ S, c′ ∈ P such that c ≤ c′ ≤ c′′ then c′ ∈ S. A chain is a (possibly empty) subset X of a partially ordered set P such that for all x, x′ ∈ X: x ≤ x′ or x′ ≤ x. Given a partially ordered set ⟨P, ≤⟩ and X ⊆ P, y ∈ P is an upper bound for X iff x ≤ y for each x ∈ X. An upper bound y for X is the least upper bound iff for every upper bound y′: y ≤ y′; lower bounds and greatest lower bounds are defined dually. A complete lattice is a partially ordered set L such that every subset of L has a least upper bound and a greatest lower bound. A complete lattice L with partial ordering ≤, least upper bound ∨, greatest lower bound ∧, least element ⊥ = ∨∅ = ∧L, and greatest element ⊤ = ∧∅ = ∨L, is denoted (L, ≤, ⊥, ⊤, ∨, ∧). In the following we will often abuse notation by denoting lattices with their poset notation. We write f : A → B to mean that f is a total function of A into B. Function composition is denoted ∘ . Let f : A → B be a mapping, for each C ⊆ A we denote by f(C) the image of C by f: {f(x) | x ∈ C}. Functions from a set to the same set are usually called operators. The identity operator λx.x is often denoted id. Given partially ordered sets ⟨A, ≤_{A}⟩ and ⟨B, ≤_{B}⟩, a function f : A → B is monotonic if for all x, x′ ∈ A : x ≤_{A} x′ implies f(x) ≤_{B} f(x′). If A and B are complete lattices, f is continuous iff for each non-empty chain X ⊆ A: f(∨_{A}X) = ∨_{B}f(X). A function f is additive iff the previous condition is satisfied for each non-empty set X ⊆ A (f is also called complete join-morphism). An upper closure operator on a partially ordered set ⟨A, ≤⟩ is a function ρ : A → A that is idempotent, i.e., ρ(ρ(c)) = ρ(c); extensive, i.e., c ≤ ρ(c); and monotonic (more on closure operators can be found in [23]).

Let (L, ≤, ⊥, ⊤, ∨, ∧) be a non-empty complete lattice. Let f : L → L be a function. The ordinal powers of f are defined as follows for x ∈ L:

f ↑0(x) = x

f ↑α(x) = f(f ↑(α − 1)(x)) for every successor ordinal α; and f ↑α(x) = ∨_{δ<α} f ↑δ(x) for every limit ordinal α.

The first limit ordinal equipotent with the set of natural numbers is denoted by ω. The Knaster-Tarski fixed-point theorem states that the set of fixed-points fp(f) of a monotonic function f over a complete lattice is itself a complete lattice [69]; in particular, this implies that a monotonic function f over a complete lattice has a least fixed-point lfp(f). Moreover, if f is continuous then lfp(f) = f ↑ω(⊥).

An algebraic structure [41] is a pair (C, Q) where C is a non-empty set, called the universe of the structure and Q is a function ranging over an index set I such that for each i ∈ I, Q_{i} are finitary operations on and to elements of C. Algebraic structures are also denoted as (C, Q_{i})_{i∈I}. In addition to the operations Q_{i}, some special symbols (e.g., ⊗, ⊕, 0,...) will be used to denote algebraic operations, including constants. With an abuse of notation, we will often denote distinguished elements of C as constant operations Q_{i} on C. A structure is (Q_{i}) α-complete for some i ∈ I and an infinite cardinal number α, if Q_{i}(X) is defined for every set X ⊆ C such that |X| ≤ α. It is complete if it is α-complete for any α. Given algebraic structures (A, Q_{A}) and (B, Q_{B}) with universes A and B and provided with a common set of basic operators Q, (we denote Q_{A} and Q_{B} the operators in Q defined on A and B respectively) a (homo)morphism σ from (A, Q_{A}) to (B, Q_{B}), denoted by σ : (A, Q_{A}) ⟶^{m} (B, Q_{B}) is a function σ : A → B such that: σ(f_{A}) = f_{B} for each constant symbol in Q and σ(f_{A}(a_{1}, ..., a_{n})) = f_{B}(σ(a_{1}), ..., σ(a_{n})) for each n-ary operation f in Q and a_{1}...a_{n} ∈ A. Let (A, Q_{A}) and (B, Q_{B}) as above. Given partially ordered sets ⟨A, ≤_{A}⟩ and ⟨B, ≤_{B}⟩, a semimorphism is a function σ : A → B such that σ(f_{A}) ≤_{B} f_{B}, for each constant symbol f in Q, and σ(f_{A}(a_{1}, ..., a_{n})) ≤_{B} f_{B}(σ(a_{1}), ..., σ(a_{n})), for each n-ary operation symbol f in Q.

3. CONSTRAINT ALGEBRAS

As defined by Jaffar and Lassez [45], and Jaffar and Maher [46], the semantics of constraints are given in terms of an algebraic structure that interprets constraint formulae, while the semantics of a constraint logic program is given in terms of fixed-point, model-theoretic and operational characterizations. In this section we introduce an incremental algebraic specification for constraint systems: our interest is in the algebraic properties on which the semantic constructions are based. Constraints are then viewed as elements of an algebraic structure, providing a uniform treatment of semantic domains (collections of constraints) and domain-dependent operators. For this purpose we adapt a widely known algebraic definition of first order logic, namely, cylindric algebras [41].

We start from a general notion of term system that provides an algebraic treatment for the data objects of a program. Constraint systems are then defined as algebraic structures whose universe represents constraints and whose operations include term substitution, constraint composition and projection. The use of such structures in the definition of operational and fixpoint semantics for constraint logic programs is discussed in Section 4. Such a construction has several advantages. First, it provides a uniform algebraic treatment of data objects and domain dependent operators. This is particularly helpful in dataflow analysis by abstract interpretation, as it allows the derivation of the standard properties of (possibly abstract) semantics from few simple axioms (see Section 5). Second, it treats terms explicitly in the algebraic treatment of constraints. This provides a treatment of notions such as term substitution, which play a fundamental role in logic programming, that is general enough to be applicable to abstract data descriptions as well as concrete ones. This includes a formal treatment of variable renaming on abstract data objects, something that is glossed over in much of the literature on abstract interpretation of logic languages. Moreover, this corresponds precisely to the algebraic generalization of the original CLP framework of Jaffar and Lassez [45], where equality is applied on arbitrary terms to provide (for instance) parameter passing in procedure calls. Finally, it distinguishes between two typical processes in semantic abstraction: term abstraction and constraint abstraction. The first provides standard data-abstraction (e.g., type information, groundness etc.) while the second is actually oriented to interpret relations between abstract data objects as (abstract) constraints.

It is worth noting that cylindric algebras, as formulated by Henkin, Monk and Tarski [41], are actually oriented towards languages without function symbols, thus ignoring all terms but variables. There is a great deal of literature devoted to extending cylindric algebras to deal with terms (see [13] for some references). The idea is that the algebraic definition of a system deals not only with its formulae (the elements of the underlying structure) but also with terms. To motivate this choice, we follow Cirulis [13] and see what arises in logic. Given a first order language with equality (note that equality is always assumed in any constraint system [45]), denote by F and T the sets, respectively, of formulae and terms in the language and by V ⊆ T the set of variables. Let furthermore Θ be a theory in the language, i.e., a set of sentences closed with respect to logical consequence. A Boolean algebra can be obtained by considering F/ ≡_{Θ}, which can be extended by defining a unary operator ∃_{x} : F/ ≡_{Θ}⟶ F/ ≡_{Θ} for x ∈ V, specifying existential quantification as in [41]. To obtain a cylindric algebra, we have to specify diagonal elements, i.e., equations of the form x = y for arbitrary variables x and y. If we consider a more extensive set of possible equations including terms, such as s = t for s, t ∈ T, then it is easy to see that the structure (F/ ≡_{Θ}, ∃_{x}, (s = t))_{x∈V,s,t∈T} does not reflect the information Θ contains about equality of terms. In fact Θ gives rise also to an equivalence on T, denoted with abuse of notation ≡_{Θ}. Hence a more adequate structure is: (F/ ≡_{Θ}, ∃_{x}, (s = t))_{x∈V,s,t∈T/≡_{Θ}}. Therefore, to axiomatically characterize this extension, we have to take into account the structure of T/ ≡_{Θ} in the whole construction of the algebra. Cirulis solves this problem by specifying T/ ≡_{Θ} as a term system and by making cylindric algebras parametric on it [13]. We follow this construction in our definition of constraint systems.

3.1. Term Systems

In the following we introduce the notion of term system as an algebra of terms provided with a binary operator which realizes substitutions ([13]). We are interested in term systems where each term depends only on a finite number of variables (also called finitary term systems). They represent the first basic definition in the semantics construction.

Definition 3.1. [term systems [13]] A term system of dimension α is an algebraic structure (τ, S, V) (later abbreviated by τ) where τ is a set of objects called τterms (terms for short); V is a countable set of τ-variables (variables, for short) in τ; |V | = α; S is a countable set of binary operations on τ, indexed by V; and the following conditions are satisfied, for all x, y ∈ V and t, t′, t′′ ∈ τ:

T_{1}. s_{x}(t, x) = t, identity T_{2}. s_{x}(t, y) = y, where x ≠ y, annihilation T_{3}. s_{x}(t, s_{x}(y, t′)) = s_{x}(y, t′) where x ≠ y, renaming T_{4}. s_{x}(t′, s_{y}(t′′, t)) = s_{y}(s_{x}(t′, t′′), s_{x}(t′, t)) where x ≠ y and y ind t′

independent composition

where a τ-term t is independent on the τ-variable x, denoted by “x ind t”, if s_{x}(t′, t) = t for any t′ ∈ τ. If X ⊆ V then X ind t iff x ind t for all x ∈ X.

We say that a variable v occurs in a term t if ¬(x ind t). We denote the set of variables occurring in a term t as var(t). If τ = V, the term system is said to be trivial.

Observe that all trivial term systems with same dimension are isomorphic [13]. In the following we will often omit the specification of the dimension in term systems, when this is obvious from the context.

Intuitively, s_{x}(t, t′) denotes the operation “substitute t for every occurrence of the variable x in t′”. It is easy to see that axioms T_{1}–T_{4} are indeed satisfied by the standard notion of substitutions as finite mappings from variables to terms (e.g., [2]). In particular: renaming (T_{3}) specifies that renaming a variable x in a term t′ with y (x ≠ y) makes the resulting term invariant under further substitutions on x; while independent composition (T_{4}) specifies the independency on the order of substitution composition. Notice that in general, the substitution operators do not perform idempotent substitutions. For notational convenience, we often denote s_{x}(t, t′) as [t/x] t′. This notation can be extended to substitutions on multiple (but finitely many) variables, by writing s_{x_{1}}(t_{1}, s_{x_{2}}(t_{2}, ⋯ s_{x_{k}}(t_{k}, t) ⋯)) as [t_{1}/x_{1} … t_{k}/x_{k}] t, where i ≠ j implies x_{i} ≠ x_{j}. Notice that, from T_{4}, if also x ind t′′ then [t′/x] [t′′/y] t = [t′′/y] [t′/x] t. Moreover, by T_{2}, for each x, y ∈ V: x ind y iff x ≠ y. The condition that terms depend on a finite number of variables can be formalized by requiring that the set {x ∈ V | [t/x] t′ ≠ t′ for some t ∈ τ} is finite for every t′ ∈ τ. Our interest in finitary term systems is not related only to their common use in logic programming. Finitary term systems in fact can be induced (built) from any free algebra τ with generators V. This is important in the context of this work, where we need a generalized notion of terms. Define a term system (τ, s_{x}, V)_{x∈V} to be algebraic if there exists a relatively free algebra τ with generators V (i.e., where each element of τ is generated by a finite subset of V and any mapping f : V ⟶ τ can be extended to an endomorphism of τ) such that s_{x}(t, t′) = s_{x}^{t}t′ where s_{x}^{t} is the endomorphism of τ that takes x into t and agrees with the identity everywhere else. Then, a crucial result on term systems states that a term system is algebraic iff it is finitary [13]. Standard properties of term systems and substitutions, such as the properties of composition, can be found in [13].

Example 3.1. Let Σ be a finite collection of function symbols. T (Σ, V) denotes the family of first-order terms defined on Σ and V. The standard term system τ_{(Σ,V)} = (T (Σ, V), Sub, V) is a term system provided that substitutions in Sub perform standard substitutions.

Atoms are constructed in the standard way on an arbitrary term system, as specified by the following

Definition 3.2. Let Π be a finite collection of predicate symbols and τ be a term system. A (τ, Π)-atom has the form p(t_{1}, ..., t_{n}) where p ∈ Π and t_{i} ∈ τ, for each i = 1, ..., n. If t_{i} are distinct variables, we say that the atom is flat.

When clear from the context, we sometimes denote by ō both a tuple and a set of syntactic objects o (terms, atoms, etc.). In particular we denote by x̄ a tuple (set) of distinct variables.

The following example shows a non-standard instance of the term system algebraic structure. It provides an adequate term system for the ground dependency analysis discussed in Section 5.1.

Example 3.2. Let Σ be a finite set of symbols. Let τ_{Σ} = (℘^{f}(Σ), S, Σ), where S is the family of basic operators s_{x}, for x ∈ Σ, such that for each X_{1}, X_{2} ∈ ℘^{f}(Σ):

s_{x}(X_{1}, X_{2}) = \{ \begin{matrix}(X_{2} \ \{x\}) ∪ X_{1} & if x ∈ X_{2} \\ X_{2} & otherwise \end{matrix}

In this case, for each x ∈ Σ and finite set X ⊆ Σ: x ind X iff x ∉ X. Then, τ_{Σ} is a term system. It is straightforward to show that τ_{Σ} satisfies the axioms of identity (T_{1}), annihilation (T_{2}), and renaming (T_{3}). To show that it satisfies the axiom of independent composition (T_{4}), assume that X, X′, X′′ ⊆ Σ are finite sets, x, y ∈ Σ, x ≠ y and y ∉ X′. If any of X, X′ and X′′ is empty, the proof is trivial. If y ∉ X or x ∉ X ∪ X′′, the proof is straightforward. Assume y ∈ X and x ∈ X ∪ X′′:

s_{x}(X′, s_{y}(X′′, X)) = (((X \ {y}) ∪ X′′) \ {x}) ∪ X′

[ definition ]

= (((X \ {x}) ∪ X′) \ {y}) ∪ ((X′′ \ {x}) ∪ X′)

[ distributing {x} ∪ X′ and x ∉ X ]

= s_{y}(s_{x}(X′, X′′), s_{x}(X′, X))

[ definition ]

3.2. An Algebraic Framework for Constraint Systems

We give now a formal algebraic specification for the language of constraints on a given term system. The process of building constraints in any fixed-point evaluation of a given CLP program is mainly based on set union and conjunction. We want to give an algebraic characterization of this process in order to provide a framework for generalized interpretations of constraint logic programs.

Definition 3.3. [closed semirings [1, 30]] A closed semiring^{1}is an algebraic structure (C, ⊗, ⊕, 1, 0) satisfying the following:

• R_{1}. (C, ⊗, 1) and (C, ⊕, 0) are monoids.

• R_{2}. ⊕ is commutative and idempotent.

• R_{3}. 0 is an annihilator for ⊗ , i.e., for every c ∈ C, c ⊗ 0 = 0 ⊗ c = 0.

• R_{4}. for any possibly infinite family {a_{i}}_{i∈I} of elements in C: the sum a_{1} ⊕ a_{2} ⊕ ⋯, denoted ∑_{i∈I} a_{i} exists and is unique, i.e., it is a well defined

element in C. Moreover associativity, commutativity and idempotence of ⊕ apply to infinite as well as to finite applications of ⊕.

• R_{5}. ⊗ is left- and right-distributive over finite and infinite applications of ⊕, i.e., if C = {a_{i}}_{i∈I} is a possibly infinite family of elements in C and c ∈ C, then c⊗(∑ C) = ∑({c⊗a_{i} | i ∈ I}) and (∑ C)⊗c = ∑({a_{i}⊗c | i ∈ I}),

1They are known as (join) complete semirings in the literature (e.g., see [30]). Note that, with respect to [30], in our construction we assume ⊕ be idempotent on infinite applications of ⊕. We will use the slightly naive name of closed semirings adopted from [1] to distinguish them from the more general complete case.

where ∑ C =∑_{i∈I} a_{i}.

Closed semirings provide an algebraic characterization of multiplicity in automata [30]. This phenomenon is evident when multiple paths (or computations) are possible for a given automata. Ioannides and Wong have also shown that the class of relational operators form a closed semiring [43], thus providing a formalization of recursion in the database context. In logic programming, closed semirings summarize, in an algebraic framework, all aspects of dealing with composition of terms, such as unification and set union. The idea is that of finding the (possibly infinite) set of all paths in the semantic construction. From a semantic viewpoint, each path is a sequence of constraints between vertices in the call graph associated with the program. Each successful path constitutes a computation, and will be a sequence (conjunction) of constraints. The multiplicity of paths corresponds to multiple solutions for a query. Idempotence, associativity and commutativity are necessary to allow the operator ⊕ (join) to model, in a general way, the “merging” together of information via set union. The operator ⊗ (meet) corresponds to conjunction of constraints and plays the important role of collecting information during computation. Distributivity allows the representation of constraints as possibly infinite joins of finite meets (also called simple constraints). Distributivity plays a fundamental role in the equivalence between the bottom-up and the top-down semantics constructions. Closure on infinite sequences of elements in C is necessary to admit constraints that are infinite joins of constraints (this is important in the semantic development given in Section 4). Closed semirings are thus an appropriate algebraic generalization to model constraint construction as an observable property. Indeed, the asymmetry between joins (disjunctions) and meets (conjunctions) corresponds precisely to the traditional interpretation of observables: infinite disjunctions of observable properties are still observables—to see that ∨_{i∈I} a_{i} holds

of a process we only need to observe that any one of the a_{i} holds—while infinite conjunctions clearly cannot be observed on the basis of a finite amount of information (e.g., see [66]). A topology for closed (complete) semirings has been recently studied in [51].

Semirings can be naturally ordered by defining a binary relation ≤ such that for any a, b ∈ C: a ≤ b iff a ⊕ c = b for some c ∈ C ([30]). In our case, since ⊕ is idempotent, there exists a unique natural order for a semiring:

Definition 3.4. Given a closed semiring (C, ⊗, ⊕, 1, 0), the relation ≤ ⊆ C × C is defined as follows: for any c_{1}, c_{2} ∈ C, c_{1} ≤ c_{2} iff c_{1} ⊕ c_{2} = c_{2}.

Proposition 3.1. Closed semirings are continuous, namely for any infinite family {a_{i}}_{i∈I} of elements in C and c ∈ C:

if ∑_{i∈F} a_{i} ≤ c for all F ∈ ℘^{f}(I) then ∑_{i∈I} a_{i} ≤ c.

Karner gives a general treatment of continuous complete semirings [50]. Continuity here corresponds to requiring that ∑{a_{i} | i ∈ I} is the least upper bound of all ∑{a_{i} | i ∈ F } for any finite subset F of I, and is essential for proving the following proposition.

Proposition 3.2. C is partially ordered by ≤, and forms a complete lattice.

A semantic definition necessarily implies some notion of “observable behavior”: programs that have the same semantics must not be observationally different. Modelling the semantics of constraint logic programs in terms of answer constraints corresponds to considering answer constraints as the appropriate observable property (this approach to semantics has been considered in [33]), and requires the ability to restrict an answer constraint to the variables appearing in the query. Closed semirings are too weak to capture this restriction operation. We follow Saraswat et al. [64] in handling this using a family of “hiding” operators. Cylindric algebras, formed by enhancing Boolean algebras with a family of unary operations called cylindrifications, provide a suitable framework for this [41]. The intuition here is that given a constraint c, the cylindrification operation ∃_{S}(c) yields the constraint obtained by “projecting out” from c all information about the variables in S. Technically, cylindric algebras allow us to make projections on finite sets of variables. However, since our semantic formulation is in terms of infinite unfolding, as discussed later in the paper, it may also be necessary to allow projections on infinite sets. To this end, we allow possibly countably many cylindrifications. Diagonal elements [41], which represent equations on elements of the underlying term system, are considered as a way to provide parameter passing. However, cylindric algebras, which are oriented towards first-order languages without function symbols, are not adequate as an algebraic semantic framework for general constraint logic programs where parameter passing between procedures is defined by syntactic equality on terms (as in [45]). Therefore, we extend diagonal elements to deal with generic terms, following the approach of Cirulis [13]. This provides an algebraic generalization for syntactic equality on terms as parameter passing applied in [45].

Definition 3.5. [Constraint systems] Given a term system τ of dimension α with variables V, a τ-based constraint system A of dimension α is an algebraic structure (C, ⊗, ⊕, 1, 0, ∃_{X}, d_{t,t′})_{X⊆V;t,t′∈τ} where C is a set of A-constraints generated by a given set of atomic constraints over terms from τ, and is called the universe of A; 0, 1, d_{t,t′} are distinct (atomic) elements of C, for each t, t′ ∈ τ; {∃_{X}}_{X⊆V} is a family of unary operations on C; ⊗, ⊕ are binary operations on C; such that the following postulates are satisfied for any c, c′ ∈ C; {x}, X, Y ⊆ V and t, t′, t′′ ∈ τ:

• R . the structure (C, ⊗, ⊕, 1, 0) is a closed semiring;

• C_{1}. ∃_{X}0 = 0

• C_{2}. c ⊕ ∃_{X}c = ∃_{X}c;

• C_{3}. ∃_{X}(c ⊗ ∃_{X}c′) = ∃_{X}(∃_{X}c ⊗ c′) = ∃_{X}c ⊗ ∃_{X}c′;

• C_{4}. ∃_{X}∃_{Y} c = ∃_{(X∪Y)}c;

• C_{5}. ∃_{X} distributes over finite and infinite joins;

• D_{1}. d_{t,t} = 1;

• D_{2}. d_{t,t′} = d_{t′,t};

• D_{3}. ∃_{{x}}(d_{x,t} ⊗ d_{t′,t′′}) = d_{[t/x]t′,[t/x]t′′} for x ind t;

• D_{4}. ∃_{{x}}(d_{x,t} ⊗ (c ⊗ c′)) = ∃_{{x}}(d_{x,t} ⊗ c) ⊗ ∃_{{x}}(d_{x,t} ⊗ c′).

Where the underlying term system τ for a τ-based constraint system is unimportant or is obvious from the context, we will omit reference to it.

The meaning of cylindrification is given by the axioms from C_{1} to C_{5}, while diagonal elements are specified by the axioms from D_{1} to D_{4}. Notice that Axioms D_{3} and D_{4} relate the notion of substitution in the term system τ with diagonal elements of C (which intuitively correspond to the notion of equality constraints) in the expected way. We follow Henkin, Monk and Tarski [41] in considering a family of (derived) operations ∂_{x}^{t}, defined on C for x ∈ V and t ∈ τ such that x ind t:

∂_{x}^{t}c = ∃_{{x}}(d_{x,t} ⊗ c).

We call these operations substitutions, since intuitively they extend the notion of substitution from the underlying term system to the universe of constraints. With an abuse of notation, we denote ∂_{x}^{t}(c) as [t/x] c when the meaning is clear from the context.

In the following we distinguish between constraints and simple constraints. A constraint is any object in the universe of a constraint system, while a simple constraint is an atomic constraint, or the cylindrification of a simple constraint, or a finite conjunction (i.e., meet) of simple constraints. Therefore, simple constraints do not contain joins. The compact constraints of a constraint system A are the compact elements in C, namely the finite joins of simple constraints. As we will see later in the semantic construction, an answer of a query to a program will be a compact constraint, corresponding to a single finite computation for the query. The join operator is applied to model the non-deterministic clause choice in logic programs, which may provide possibly multiple answers for a query.

The function var and the notions of “independence” and “occurrence” of variables extend in the obvious way from terms in τ to constraints in C. Let c ∈ C and x ∈ V: x ind c iff ∂_{x}^{t}c = c for any t ∈ τ such that x ind t. A variable x is bound in c iff it is existentially quantified in c; x is free in c iff x ∈ var(c) and x is not bound in c. The set of free variables in a constraint c is denoted by F V (c). A renaming of c with respect to x is a constraint ∂_{x}^{y}c such that x ≠ y and y ind c.

Let τ be a term system with variables V and (C, ⊗, ⊕, 1, 0) be a closed semiring. (C, ⊗, ⊕, 1, 0) can be extended to a constraint system by letting d_{t,t′} = 1 for each t, t′ ∈ τ and ∃_{X}c = c for each c ∈ C and X ⊆ V (here ∂_{x}^{t}c = c for each x ∈ V and t ∈ τ). Following Henkin et al. [41], we refer to these as discrete constraint systems. Let X ⊆ V, in the following we will denote ∃_{var(c)\X}c, i.e., hiding all the variables in c except X, as ∃(c)_{X}. We will often omit parentheses in cylindrifications on sets of variables. We also denote by d_{⟨t_{1},...,t_{n}⟩,⟨t′_{1},...,t′_{n}⟩} the element d_{t_{1},t′_{1}} ⊗ ... ⊗ d_{t_{n},t′_{n}}, where t_{1}, ..., t_{n}, t′_{1}, ..., t′_{n} ∈ τ.

In the following we use A to denote an arbitrary constraint system.

Theorem 3.1 [Elementary properties of constraint systems]. Let A be an arbitrary constraint system. For any c, c′ ∈ C, x ∈ V, X ⊆ V and t, t′, t′′ ∈ τ such that x ind t, the following properties hold:

• P 1 : ∃_{X}∃_{X}c = ∃_{X}c;

• P 2 : c ≤ c′ ⇒ ∃_{X}c ≤ ∃_{X}c′;

• P 3 : ∀c, c′ ∈ C : c′ ≤ ∃_{X}c ⇔ ∃_{X}c′ ≤ ∃_{X}c;^{2}

• P 4 : ∀c, c′ ∈ C : c ≤ c′ ∧ c′ ≤ ∃_{X}c ⇒ ∃_{X}c = ∃_{X}c′;

• P 5 : ∃_{{x}}c = c iff ∃_{{x}}c̃ = c for some c̃ ∈ C;

• P 6 : ∃_{{x}}c = c if x ind c (in particular ∃_{{x}}d_{t′,t′′} = d_{t′,t′′} when x ind t′, t′′); • P 7 : d_{t,t′} = ∃_{{x}}(d_{t,x} ⊗ d_{x,t′}) where x ind t, t′,

2This property corresponds to Morgado’s characterization of closure operators by means of a single axiom [61].

• P 8 : c ≤ c′ ⇒ ∂_{x}^{t}c ≤ ∂_{x}^{t}c′;

• P 9 : ∂_{x}^{t}∃_{{x}}c = ∃_{{x}}c;

• P 10 : ∂_{x}^{t} c = c iff ∂_{x}^{t}c̃ = c for some c̃ ∈ C;

• P 11 : ∃_{X}1 = 1; ∃_{X}c = 0 iff c = 0;

• P 12 : ∃_{{x}}d_{x,t} = 1;

• P 13 : (d_{t,t′} ⊗ d_{t′,t′′}) ⊕ d_{t,t′′} = d_{t,t′′} (transitivity).

In particular, from properties P1, P2, and axioms C_{2} and C_{5}, ∃_{X} is an additive upper closure operator on C for each X ⊆ V. Moreover, by properties P8, P10, and from the distributivity of ∃ and ⊗ over ⊕, the substitution operator on constraints defines an additive retraction on C, where a retraction on a partially ordered set A is an idempotent and monotonic mapping over A. Notice that substitution is not, in general, extensive. Other elementary properties of constraint systems can be derived from similar properties of cylindric algebras in [41]. Notice that (by P9) ∂_{x}^{t}c ≤ ∃_{{x}}c and if x is bound in c then x ind c. Therefore, if c is a renaming apart of c′ with respect to x, then x ind c.

The following lemma describes the interaction of variable projection with (hidden) variables in constraints, thus extending the elementary property P6 to conjunctions of constraints.

Lemma 3.1 [independence]. For any constraint system A, if c and c′ are Aconstraints and X is a set of variables such that x ind c for every x ∈ X, then ∃_{X}(c ⊗ c′) = c ⊗ ∃_{X}(c′).

The following lemma shows an important relation between cylindrification (hiding variables) and renaming apart of constraints with “fresh” variables.

Lemma 3.2. For any constraints c and c′ in a constraint system A, c ⊗ ∃_{{x}}c′ = ∃_{{y}}(c ⊗ c̃′), where y ind c, c′; y ≠ x and c̃′ = ∂_{x}^{y}c′.

The following examples show some standard constraint systems.

Example 3.3. [CLP (H)] Let Σ be a finite collection of function symbols. Atomic constraints are equations on the term system τ_{(Σ,V)} (see Example 3.1). Let E_{H} be the set of possibly existentially quantified finite conjunctions of equations over τ_{(Σ,V)}, and let I_{H} represent the Herbrand interpretation structure, interpreting diagonal elements as syntactic equality [45]. In this case, a solution θ for a possibly quantified finite conjunction (set) of equations ∃_{X}E = ∃_{X}{s_{1} = t_{1}, ..., s_{n} = t_{n}} is a grounding substitution for the free variables in E such that there exists a grounding substitution σ for the bound variables X, and s_{1}σθ ≡ t_{1}σθ , …, s_{n}σθ ≡ t_{n}σθ. I_{H} ⊧ Eθ denotes that θ is a solution for E. We extend this definition to deal with possibly infinite joins: θ is a solution for ∪_{i∈I} E_{i} iff there exists i ∈ I such that θ is a solution for

E_{i}. ∃ is existential quantification, which is assumed to be distributive (as well as conjunction) over arbitrary joins: if X ⊆ V, θ is a solution for ∃_{X}( ∪_{i∈I} E_{i}) iff θ

is a solution for ∃_{X}E_{i} for some i ∈ I; true denotes any constraint having every grounding substitution as a solution while false denotes any constraint having an empty set of solutions. Note that ∂_{x}^{t}, for x not occurring in t, performs idempotent substitutions on constraints, by extending in the obvious way the term substitution notion to constraints. Moreover, for each c_{1} = ∪_{i∈I_{1}} E_{i} and c_{2} = ∪_{i∈I_{2}} E′_{i} denoting

possibly infinite joins of (finite) quantified sets of atomic constraints (equations) E_{i} and E′_{i}:

c_{1} ∼_{EQ} c_{2} iff ∪_{i∈I_{1}} { ϑ | I_{H} ⊧ E_{i}ϑ } = ∪_{i∈I_{2}} { ϑ | I_{H} ⊧ E′_{i}ϑ } .

Then, the Herbrand constraint system H is the quotient algebra

(℘(E_{H}), ∧, ∪, true, false, ∃_{X}, {t = t′})_{X⊆V;t,t′∈τ_{(Σ,V )}}/∼_{EQ},

Example 3.4. [CLP (LR_{n})] This example describes the case of CLP (R) [45] on linear constraints, where the number of variables is restricted a priori to some fixed value n, as an instance of our framework (the case with n = ω is of little interest in our construction since constraint logic programs can define only finitary predicates). This constraint system will be used for static analysis of CLP (H) programs in Section 6.1. In the following x⃗ = (x_{1}, …, x_{n}) is a point in ℜ^{n} and x_{i} is its i-th element. A hyperplane (atomic constraint) is the set of points x⃗ ∈ ℜ^{n} satisfying an equation of the form a_{1}x_{1} + ⋯ + a_{n}x_{n} = b, and defines two halfspaces in the obvious way. A convex polyhedron is the (possibly unbounded) set of points constituting the intersection of a finite number of halfspaces. For any finite n, the constraint system of n-dimension linear constraints (the non-linear case is a straightforward extension), denoted by LR_{n}, is: (P, ∩, ∪, ℜ^{n}, ∅, ˆ∃_{X}, [t_{1} = t_{2}])_{X⊆V_{n};t_{1},t_{2}∈τ_{Exp}}, where V_{n} = {x_{1}, ..., x_{n}} is a set of n variables, τ_{Exp} is a term system of linear expressions on V_{n} (an example of definition for τ_{Exp} is in Section 6.1) and P is the set of all space regions in ℜ^{n} defined as possibly infinite unions of convex polyhedra. Each constraint c ∈ P can be represented as a possibly infinite set of finite conjunctions of linear equations and disequations on V_{n}. The variable restriction operation ˆ∃ is performed by cylindrification parallel to an axis [41]: if c is a constraint in ℜ^{n} and i ≤ n, we define:

ˆ∃_{x_{i}}c = { y⃗ ∈ ℜ^{n} | y_{j} = x_{j} for x⃗ ∈ c and j ≠ i } .

ˆ∃_{x_{i}}c is the cylinder generated by moving the point set c parallel to the x_{i} axis. For any two linear expressions t, t′ ∈ τ_{Exp} and R ∈ {=, ≥, ≤, >, <} we denote by [t R t′] the corresponding space. It is not difficult to show that the resulting structure is a constraint system (see [34]).

4. GENERALIZED SEMANTICS

Constraint logic programming was defined by Jaffar and Lassez to specify relations on a constraint language by means of constraint-based Horn clauses. We follow this approach by defining Horn-like clauses on constraint systems. Constraint logic programs are defined in the usual way: let A be a constraint system on a term system τ and Π be a finite set of predicate symbols. An A-goal is a formula ‘c [] B_{1}, ..., B_{n},’ with n ≥ 0, where c is a compact A-constraint and B_{1}, …, B_{n} is a sequence of (τ, Π)-atoms. An A-clause is a formula of the form ‘H :− c [] B_{1}, ..., B_{n}’ where H (the head) is a (τ, Π)-atom and ‘c [] B_{1}, ..., B_{n}’ (the body) is an A-goal. If the body is empty, the clause is a unit clause. Given a set of clauses S, we use preds(S) to denote the set of predicate symbols in the heads of clauses in S. A (generalized) constraint logic program, also called A-program, is a finite set of clauses. If the constraint system under consideration is obvious from the context, we will sometimes not indicate it explicitly in the various semantic functions. The family of A-programs is denoted by CLP (A). Finally, the notion of renamings of variables in constraints and terms, as well as the function var and the notion of independence, extend their meaning in the obvious way to syntactic objects such as atoms, goals, clauses, and programs.

4.1. Top-Down Operational Semantics

Let A be a constraint system and P ∈ CLP (A). Define ⇝_{P} (an A-derivation step) to be the least relation on A-goals such that G ⇝_{P} G′ iff the following hold:

1. G = c_{0} [] p_{1}(t̄_{1}), ..., p_{n}(t̄_{n});

2. there is a renamed version of a clause in P: p_{1}(t̄′_{1}) :− c_{1} [] B̄_{1}, such that var(G) ∩ var(B̄_{1} ∪ t̄′_{1}) = ∅;

3. G′ = c_{0} ⊗ d_{t̄_{1},t̄′_{1}} ⊗ ∃(c_{1})_{var(B̄_{1}∪t̄′_{1})} [] B̄_{1}, p_{2}(t̄_{2}), ..., p_{n}(t̄_{n}).

An A-derivation from an A-goal G is a finite or infinite sequence of A-goals such that every goal is obtained from the previous one by means of a single A-derivation step. A successful derivation is a finite sequence whose last element has an empty body. The constraint obtained from a successful derivation is the answer constraint. Notice that, since projection of the local variables is performed after the whole computation, an accurate definition of the operational semantics requires a denumerable set of variables on which to perform renamings (a different solution can be obtained by extending the scope of cylindrification to clause bodies).

The goal-dependent success set semantics of a program P is defined in terms of a function J_{P} that yields the set of computed answer constraints for any Agoal, such that J_{P} (G) = {∃(c)_{var(G)} | G ⇝_{P}^{∗} c [] ε}. Since the operator ⊗ in a constraint system may not be commutative, the independence of the selection rule does not hold in general in these semantic characterizations, and for simplicity we have assumed a left-to-right selection rule. If ⊗ is commutative it is straightforward to prove the independence on the selection rule for the success set [54].

The following lemma specifies an important equivalence between syntactically different goals. This result will be useful later in proving the equivalence between top-down and bottom-up semantics. Here, a variable is said to be “used” in a derivation if it occurs in some goal in that derivation.

Lemma 4.1. 1 [] p(t̄) ⇝_{P}^{∗} c [] ε iff d_{x̄,t̄} [] p(x̄) ⇝_{P}^{∗} c′ [] ε and ∃_{{x̄}}c′ = c, where no variable in x̄ is used in the derivation 1 [] p(t̄) ⇝_{P}^{∗} c [] ε.

It is worth noting that a similar argument can be applied to prove that if P is a program and P′ is obtained from P by transforming each clause C = ‘p(t̄) :− c [] B̄’ ∈ P to ‘p(x̄) :− d_{x̄,t̄} ⊗ c [] B̄’ for x ind C, then for any goal G it is the case that J_{P} (G) = J_{P′}(G). Both this observation and Lemma 4.1 are consequences of the constraint system structure, extending diagonal elements (i.e., parameter passing) to terms. Because of this observation, in the following we will always write program clauses with flat heads.

Observation 4.1. The explicit treatment of terms in constraint systems also provides a characterization for a number of expected equivalences among syntactically different programs. All of these are consequences of the axioms and therefore are satisfied in any constraint system. For example, it is easy to prove from the axioms that the following two programs have the same goal dependent success set semantics for any goal.

\begin{aligned}\{ & p(t) :− q(x) \\ & q(t′) :− 1 & \} \end{aligned} \begin{aligned}\{ & p([t′/x] t) :− 1 \\ & q(t′) :− 1 & \} \end{aligned}

This is a typical consequence of the equivalence induced by the constraint system structure on formulae including terms, like those obtained from term substitution and parameter passing.

4.2. Success-Set and Bottom-up Fixed-point Semantics

In this section we define a bottom-up fixed-point semantics that is proved to be equivalent to the operational semantics of successful computations for any constraint system. We also study a condensing operator which will be useful in abstract interpretation of CLP programs by abstraction of constraints. The approach we take follows that of Falaschi et al. [31] and Gabbrielli and Levi [33], and derives a bottom-up fixed-point based semantics from the operational notion of computed answer constraint for atomic goal.

Definition 4.1. Let A be a constraint system. A constrained atom has the form ‘A :− c’ where A is an (τ, Π)-atom, c is an A-constraint, and F V (c) ⊆ var(A). We denote B^{A} the set of constrained atoms on a constraint system A.

The (operational) computed answer constraint semantics is defined in terms of the the set of successful computations specified by the transitive closure of the derivation relation ⇝ on atomic A-goals:

O(P) = { p(x̄) :− ∃(c)x̄ | 1 [] p(x̄) ⇝_{P}^{∗} c [] ε } .

This generalizes the computed answer constraint semantics of Gabbrielli and Levi [33] to arbitrary constraint systems. Intuitively, a constrained atom ‘p(x̄) :− c’ in O(P) represents the set of instances p(θ(x̄)), where θ is a solution to the answer constraint c. The following lemma proves the AND-compositionality for the operational semantics of constraint logic programs, providing a characterization of answer constraints for conjunctive goals in terms of the computed answer constraint semantics (an equivalent lemma is proved in [33] for the classical constraint structure of Jaffar and Lassez [45]).

Lemma 4.2. Let G = c_{0} [] p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) be an A-goal and P ∈ CLP (A). J_{P} (G) = c iff there exist p_{i}(x̄_{i}) :− c_{i} ∈ O(P), such that x̄_{i} ind G and x̄_{i}∩x̄_{j} = ∅ for 1 ≤ i, j ≤ n, i ≠ j; and c = ∃(c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ c_{1}... ⊗ d_{x̄_{n},t̄_{n}} ⊗ c_{n})_{var(G)}.

It can be shown that the unfolding of a clause (goal) with constrained atoms is independent from the variable names used in constrained atoms (see Lemma A.1 in Appendix). This can be expressed in the semantics by a relation ∼ that captures the notion of equivalence upto renaming on constrained atoms. Define the binary relation ∼ on B^{A} as follows: given A_{1} ≡ ‘p(x̄_{1}) :− c_{1}’ and A_{2} ≡ ‘p(x̄_{2}) :− c_{2}’ in B^{A}, A_{1} ∼ A_{2} if and only if there exist “renaming apart” variables x̄′ such that x̄′, x̄_{1}, and x̄_{2} are mutually disjoint; x̄′ ind c_{1}, c_{2}; and ∂x̄′ ; x̄_{1}c_{1} = ∂x̄′ ; x̄_{2}c_{2}. It is easy to show that ∼ is an equivalence relation.

Definition 4.2. The A-base of interpretations is B^{A}/∼.

In the remainder of the paper we will be concerned primarily with the quotient structure B^{A}/∼, and for notational simplicity, denote this by B^{A}. Given a syntactic object o, we denote by ‘p(x̄) :− c <<_{o} I’ a variant of a constrained atom ‘p(x̄) :− c’ in I that has been renamed apart from o, i.e., such that [p(x̄) :− c]_{∼} ∈ I and x̄ ind o. We extend this to specify tuples of syntactic objects that have been renamed apart, so that ⟨A_{1}, …, A_{n}⟩ <<_{o} I represents a tuple ⟨A′_{1}, …, A′_{n}⟩ where each of the A′_{i} is a variant of an element A_{i} in I that has been renamed apart from o, and where i ≠ j implies A_{i} and A_{j} are variable-disjoint.

The fixed-point semantics is defined in terms of an immediate consequence operator on the complete lattice ⟨℘(B^{A}), ⊆⟩, in the style of van Emden and Kowalski [71].

Definition 4.3. Let A be a constraint system and P ∈ CLP (A). The mapping T_{P} : ℘(B^{A}) → ℘(B^{A}), is defined as follows

T_{P} (I) = ⋃_{C∈P} \{ [p(x̄) :− ∃(c̃)x̄]_{∼} | \begin{matrix}C ≡ ‘p(t) :− c [] p_{1}(t̄_{1}), …, p_{n}(t̄_{n})’ \\ n ≥ 0, x̄ ind C and for each i = 1...n : \\ p_{i}(x̄_{i}) :− c_{i} <<_{C,x̄_{1},...,x̄_{i−1}} I \\ x̄_{i} ∩ x̄ = ∅, c′_{i} = d_{x̄_{i},t̄_{i}} ⊗ c_{i}, \\ c̃ = d_{x̄,t̄} ⊗ c ⊗ c′_{1} ⊗ ⋯ ⊗ c′_{n} \end{matrix} \}

Interestingly, it turns out that the fixed-point semantics of a program can always be computed into a finite dimension constraint system. This follows from the properties of cylindrification with respect to substitution (see Theorem 3.1). Intuitively, the hiding operator allows the definition of “local environments” that cannot be influenced by substitution, and allows hidden variables to be “recycled” outside the scope of the hiding operator, making it possible to get by with only a finite set of variables that are recycled over and over. This is useful for program analysis purposes, since it simplifies the construction of Noetherian abstract domains (e.g., see the affine relation analysis in Section 6.1).

By analogy with the operator ⊕, which expresses the notion of “merging together” the information present in two constraints, we define a condensing operator ♭ : ℘(B^{A}) ⟶ ℘(B^{A}) such that for any I ∈ B^{A}:

I^{♭} = {[p(x̄) :− ∑{∂x̄ ; ȳc′ | p(ȳ) :− c′ <<x̄ I}]_{∼} | p ∈ preds(I)}

The operator ^{♭} captures the notion of merging together the information present in a set of constrained atoms. The result of condensing is an interpretation containing at most one constrained atom for each predicate symbol p in the program. Such constrained atoms have the form ‘p(x̄) :− ∑ c_{j}’ and represent the join (intuitively corresponding to disjunction) of all the answer constraints c_{j} for the goal p(x̄). Since the number of such answer constraints can be infinite, infinite joins of constraints are allowed in constrained atoms. This is modeled by having the universe C of a constraint system be closed under infinite joins. Note that this closure property cannot be specified by any finitary first-order formula.

To specify the relation between interpretations and condensed interpretations, we consider a lower powerdomain preorder ⊑. Let a << I denote a variant of an object a ∈ I that has been renamed apart from all elements of I. The preorder ⊑ is defined as follows: I ⊑ I′ iff for each p(x̄) :− c << I there exists p(x̄) :− c′ << I′ such that c ≤ c′. Let ≈ denote the induced equivalence relation: I_{1} ≈ I_{2} iff I_{1} ⊑ I_{2} and I_{2} ⊑ I_{1}. In the discussion that follows, we will be concerned primarily with the partial order over ℘(B^{A})/ ≈ induced by ⊑. For simplicity of exposition, we abuse notation and use ⊑ to denote this partial order and ℘(B^{A}) to denote the set ℘(B^{A})/ ≈. It is easy to prove that ⟨℘(B^{A}), ⊑⟩ is a complete lattice, with join operator ⊔ defined as I ⊔ I′ = (I ∪ I′)^{♭}.

Proposition 4.1. ^{♭} is an upper closure operator on ⟨℘(B^{A}), ⊑⟩.

We denote by ℘^{♭}(B^{A}) the set of condensed interpretations (℘(B^{A}))^{♭}. It is easy to prove that for any I, I′ ∈ ℘^{♭}(B^{A}): I ⊑ I′ iff (I ∪ I′)^{♭} = I′, and that ⟨℘^{♭}(B^{A}), ⊑⟩ is a complete lattice.

An analogous operator T_{P}^{♭} : ℘^{♭}(B^{A}) ⟶ ℘^{♭}(B^{A}) on condensed interpretations can be defined as T_{P}^{♭} (I) = (T_{P} (I))^{♭}. The existence and uniqueness of the least fixpoints of these operators is, in both cases, a consequence of continuity of T_{P} and T_{P}^{♭}:

Lemma 4.3. Let A be a constraint system and P ∈ CLP (A). For any I ∈ ℘(B^{A}): (T_{P} (I^{♭}))^{♭} = (T_{P} (I))^{♭}.

Proposition 4.2. Let A be a constraint system and P ∈ CLP (A). T_{P} is a continuous function on the complete lattice ⟨℘(B^{A}), ⊆⟩ and T_{P}^{♭} is continuous on the complete lattice ⟨℘^{♭}(B^{A}), ⊑⟩.

Definition 4.4. [Fixed-point semantics] The fixed-point semantics of a program P over a constraint system A is given by F(P) = lfp(T_{P}) and F^{♭}(P) = lfp(T_{P}^{♭}) .

The following result states the equivalence between the operational and the (possibly condensed) fixed-point semantics, for any constraint system A.

Theorem 4.1. Let A be a constraint system with dimension ω, and P ∈ CLP (A), then F(P) = O(P)/∼ and F^{♭}(P) = (O(P)/∼)^{♭}.

It is worth noting that the condensing operator ^{♭} is actually an abstract interpretation. Indeed, with any condensed interpretation I^{♭}, there are many (possibly) different interpretations J such that J^{♭} = I^{♭}. While the non-condensed semantics associates with each predicate the collection of all possible constraints that one may obtain for it, the condensed one associates a single constraint with each predicate defined in the program. The latter case is particularly useful for specifying termination conditions in terms of ascending chains, ordered by entailment (≤), of constraints (see Section 5).

Observation 4.2. Note that from Theorem 4.1, the semantics F(P) corresponds precisely to the s-semantics, which is well known to be fully abstract with respect to computed answer substitutions in (pure) logic programming ([10, 31]). This because O characterizes precisely the set of computed answer constraints for arbitrary atomic goals. In this case, when an atomic goal p(x) has the two answer constraints x = a and true in the Herbrand constraint system, we obtain the denotation {[p(x) :− x = a]_{∼}, [p(x) :− true]_{∼}}. A similar approach to characterize computed answer constraints in constraint logic programming is also considered in [33]. The condensed semantics instead, corresponds to the so called Clark’s semantics [14] (c-semantics in [31]), which characterizes correct answer substitutions in logic programming. In this case, for the atomic goal p(x) above, we obtain the denotation {[p(x) :− true]_{∼}}. This semantics is proved to be optimal for ground dependency and covering analysis in [35]. The relation between collecting semantics for logic programs and abstract interpretation has been recently studied in [35] for a number of different observable properties.

The semantics given thus far in this section generalize the corresponding results for traditional logic programs to arbitrary constraint systems. We conclude this section with an example that shows that they can be used for other, very different, purposes as well.

4.3. Machine-level Traces

This example illustrates a non-standard semantics for constraint logic programs, that of machine-level traces, as an instance of the framework of this paper (Stoy discusses similar non-standard semantics in a denotational context [67]). Such a semantics is essential, for example, if we wish to reason formally about the correctness of a compiler (e.g., see [39]), low-level compiler optimizations, or about the behavior of debuggers or profilers. Instead of constrained atoms where each atom is associated with a constraint, this semantics will associate with each atom a set of instruction sequences that may be generated on an execution of that atom.

Suppose we are given some low-level WAM-like abstract machine for the execution of CLP programs. Let Instr denote the (possibly infinite) set of all possible machine instructions (by “instruction” we mean an instruction name—the opcode— together with the values of the operands). A computation is defined by a sequence of states obtained as instructions are executed. If each instruction is a function over states, and we assume that all programs start execution in some given (fixed) initial state, then the results of a computation can be specified simply by the sequence of instructions executed. We refer to such a sequence as a trace. The set of all traces is denoted by Trace = Instr^{∗}. The meaning of a program is given by the set of all of its possible executions, i.e., by a set of traces. In the case of a low-level trace semantics for constraint logic programs, therefore, the universe is given by C = ℘(Trace).

In general, certain minimal capabilities are necessary in any low-level instruction set in order to execute a constraint logic program. To this end, we assume the following:

1. Corresponding to each primitive constraint c of the language there is a sequence of machine instructions impl(c) that realizes c at the machine level.

2. There is an instruction hide(x) with the following behavior: for any variable x, hide(x) removes any constraint on the variable x in the data structures representing the computed constraint at that point.

The basic operations on sets of traces are defined as follows: given S, S_{1}, S_{2} ∈ C:

1. S_{1} ⊕ S_{2} = S_{1} ∪ S_{2}.

2. ⊗ is pointwise concatenation: let ‘::’ denote the concatenation operation on sequences, then S_{1} ⊗ S_{2} = {s_{1} :: s_{2} | s_{1} ∈ S_{1}, s_{2} ∈ S_{2}}.

3. 0 = ∅.

4. 1 = {ε}.

5. Let X = {x_{1}, …, x_{n}}, then ∃_{X}S = {s :: ⟨hide(x_{1}), hide(x_{2}), ⋯, hide(x_{n})⟩ | s ∈ S}.

6. d_{t,t′} = impl(t = t′).

In a low level machine, the constraints manipulated and accumulated during the execution of a program are necessarily represented in terms of machine-level entities, e.g., by means of data structures constructed in memory. It follows that references to constraints c in the derivation relation ⇝_{P} or the immediate consequence operator T_{P} will, in the low-level semantics, be replaced by references to impl(c). The corresponding high-level constraints can be reconstructed where necessary, e.g., for displaying a computed answer constraint to the user, or for debugging purposes. Given our assumption that there is a single initial state that every program begins execution in, given a trace s it is possible to reconstruct the constraint obtained in the state resulting from the execution of s: this is denoted by constraint(s). This extends in the obvious way to sets of traces: given any S ∈ C, constraint(S) = {constraint(s) | s ∈ S}. Define the relation ≃ ⊆ C × C as follows: for any S_{1}, S_{2} ∈ C: S_{1} ≃ S_{2} if and only if constraint(S_{1}) = constraint(S_{2}). ≃ is an equivalence relation.

It is easy to see that the structure (C, ⊗, ⊕, 1, 0) satisfies the axioms of a closed semiring, so Axiom R in the definition of constraint systems is satisfied. The remaining axioms, namely C_{1}−C_{5} and D_{1}−D_{4}, are satisfied modulo the equivalence relation ≃. Thus, the machine level semantics presented forms a constraint system modulo ≃.

As a simple example of an application of such a semantics, consider the following program over the Herbrand constraint domain:

      p(X) :- X = a, q(Z).
      q(Y) :- Y = a.
      q(Y) :- Y = b.

The only primitive constraint over this domain is ‘=’/2: suppose that the lowlevel instruction set under consideration contains an instruction unify such that impl(t_{1} = t_{2}) = unify(t_{1}, t_{2}). In addition, assume the instructions call, return, and fail for managing procedure calls. The (operational) semantics of the procedure q is then given by

      q(Y_{i}) :− {⟨unify(Y_{i}, a), return⟩, ⟨unify(Y_{i}, b), return⟩} | i ≥ 0}.

Here, the subscripts on the variables denote alphabetic variants of the program clauses that may be used at runtime: the idea is that there is a trace describing the execution of every possible variant of the clause appearing in the source program. Thus, the meaning of a predicate is an infinite set of traces representing instruction sequences that may be obtained at runtime, rather than finite sets of instruction sequences that may be generated by a compiler. The semantics for the procedure p can similarly be obtained as:

p(X_{i}) :− {⟨unify(X_{i}, a), unify(Z_{i}, Y_{i}), call q/1, unify(Y_{i}, a), return,
          hide(Z_{i}), return⟩,
         ⟨unify(X_{i}, a), unify(Z_{i}, Y_{i}), call q/1, unify(Y_{i}, b), fail, fail⟩ | i ≥ 0}

We have deliberately kept the instruction set under consideration here small, in order to simplify the presentation. It is not difficult to see how such an instruction set could be embellished to be more realistic. For example, argument passing through a fixed set of registers, as in the WAM, can be modelled by requiring that the arguments in the head of each clause of an n-ary predicate be distinct variables A_{1}, …, A_{n}; if a is a constant and a variable x occurs for the first time in a trace for a procedure in an instruction ‘unify(x, a)’, we could replace this instruction by a more specialized one of the form ‘get constant(x, a)’ (and similarly for function symbols of nonzero arity); and so on.

5. ABSTRACT CONSTRAINT SYSTEMS

The definition of an abstract constraint system, which specifies a non-standard semantics for a constraint programming language, is performed in two steps: term abstraction and constraint abstraction. In the first step new syntactic objects are introduced to represent concrete terms. In the second one, constraints on the abstracted term system are defined.

In general, a constraint system is an interpretation (in a closed semiring) for constraint formulae. To relate constraint systems, we follow the approach to “static semantic correctness” in [7]. Correctness of non-standard semantic specifications can be handled in an algebraic way through the notion of morphism (see [70]). The algebraic notion of morphism can be made less restrictive by assuming that the carriers of the algebras involved are partially ordered sets. We use this weaker notion of morphism between algebraic structures, capturing the approximation possibly induced by abstract interpretations or by any approximate semantics defined in the framework. This provides, at the same time, a characterization for domain correctness conditions (traditionally specified by Galois connections) and the correctness of abstract operations.

Definition 5.1. [Morphism, semimorphism] Let τ and τ′ be term systems over sets of variables V and V′, and with substitution operators s and s′ respectively. A morphism κ : τ ⟶^{m} τ′, is a function mapping terms of τ to terms of τ′ such that for any t_{1}, t_{2} ∈ τ and x ∈ V: κ(s_{x}(t_{1}, t_{2})) = s′_{κ(x)}(κ(t_{1}), κ(t_{2})). Consider constraint systems A and A′, where

A = (C, ⊗, ⊕, 1, 0, ∃_{X}, d_{t_{1},t_{2}})_{X⊆V;t_{1},t_{2}∈τ}

and

A′ = (C′, ⊗′, ⊕′, 1′, 0′, ∃′_{X}, d′_{t_{1},t_{2}})_{X⊆V′;t_{1},t_{2}∈τ′}.

A mapping α_{κ} : A ⟶^{s} A′ is a semimorphism iff there is a morphism of term systems κ : τ ⟶^{m} τ′ such that for each c, c_{1}, c_{2} ∈ C, C ⊆ C, X ⊆ V and t_{1}, t_{2} ∈ τ, the following hold:

1. α_{κ}(0) = 0′;

2. α_{κ}(1) ≤′ 1′;

3. α_{κ}(∑ C) ≤′ ∑′ α_{κ}(C);

4. α_{κ}(∃_{X}c) ≤′ ∃′_{κ(X)}α_{κ}(c);

5. α_{κ}(c_{1} ⊗ c_{2}) ≤′ α_{κ}(c_{1}) ⊗′ α_{κ}(c_{2});

6. α_{κ}(d_{t_{1},t_{2}}) ≤′ d′_{κ(t_{1}),κ(t_{2})}.

The intuition behind this definition may be understood as follows. Recall that the natural order ≤′ over C′ is defined as x≤′y iff x⊕′y = y, where ⊕′ intuitively denotes some kind of “merge” operation. For the purposes of abstract interpretation, the objects that are merged in this manner represent possible program behaviors, and the smaller the set of behaviors denoted by an object the more information it conveys. Thus, x ≤′ y denotes that x provides more information than y, i.e., is a more precise description of program behavior. The requirements for a semimorphism given above, therefore, state simply that for each of the operations in the (concrete) constraint system A, operating on objects in C and then applying the semimorphism (i.e., abstracting) is no worse than applying the semimorphism first and then applying the corresponding operation in the (abstract) constraint system A′. The following proposition states that semimorphisms correctly abstract the (derived) notion of substitution into constraints:

Proposition 5.1 [Substitution correctness]. Let A and A′ be constraint systems as above. Let also c ∈ C, x ∈ V and t ∈ τ such that x ind t. If α_{κ} : A ⟶^{s} A′ is a semimorphism then α_{κ}(∂_{x}^{t}c) ≤′ ∂_{κ(x)}^{′κ(t)}α_{κ}(c).

For notational simplicity in the discussion that follows, we will sometimes omit the subscript from a semimorphism when the morphism κ on the underlying term system need not be considered explicitly.

We are now able to provide a notion of correctness for constraint systems. It corresponds precisely to the Galois insertion-based notion of domain and operator correctness belonging to the classical framework of abstract interpretation [22], as specified by Proposition 5.3 below. Here, the unifying framework of constraint systems provides a uniform treatment for domain and operator correctness, both specified by the simple notion of semimorphism.

Definition 5.2. Let A and A′ be constraint systems as above. A′ is correct with respect to A iff there exists a semimorphism α_{κ} (i.e., κ : τ ⟶^{m} τ′ and α : A ⟶^{s} A′) that is a surjective and additive mapping of ⟨C, ≤⟩ into ⟨C′, ≤′⟩.

The following proposition provides the basis for designing abstract constraint systems by consecutive approximations.

Proposition 5.2. For any constraint system A, A′ and A′′: if A′′ is correct with respect to A′ and A′ is correct with respect to A, then A′′ is correct with respect to A.

Additivity and surjectivity allow the semimorphism to associate the “best” approximating constraint in A′ with any concrete constraint in A. This is captured by the notion of Galois insertion, where a pair of functions (α, γ)—denoting abstraction and concretization respectively—is a Galois insertion of ⟨C′, ≤′⟩ into ⟨C, ≤⟩ iff α and γ are monotonic, α(γ(c′)) = c′ and c ≤ γ(α(c)) for each c ∈ C and c′ ∈ C′ ([22, 24, 60]). The following proposition relates the notion of semimorphism with the notion of Galois insertion:

Proposition 5.3. Let A and A′ be constraint systems with universes C and C′ respectively. If A′ is correct with respect to A by means of a semimorphism α, there exists a mapping γ : C′ ⟶ C such that (α, γ) is a Galois insertion of ⟨C′, ≤′⟩ into ⟨C, ≤⟩.

Notice that, as observed in [24], by additivity and surjectivity, ∑{c | α(c) ≤′ c′} = ∑{c | α(c) = c′}.

In the framework of abstract interpretation, correctness of fixed-point approximations requires some additional conditions on correctness of the non-standard (abstract) semantic operators [22]. With the assumption of additivity, semimorphisms are adequate for specifying both Galois insertions, as seen in Proposition 5.3, and operator-correctness. Let A′ be a constraint system that is correct with respect to A, by means of a semimorphism α_{κ}. Let P = {C_{1}, ..., C_{m}} be a program in CLP (A). The corresponding program on A′, denoted T_{α_{κ}}(P) is a set of clauses {C′_{1}, ..., C′_{m}} such that for each i = 1, ..., m if C_{i} = ‘p(t̄) :− c [] p_{1}(t̄_{1}), …, p_{n}(t̄_{n})’ then C′_{i} = ‘p(κ(t̄)) :− α(c) [] p_{1}(κ(t̄_{1})), …, p_{n}(κ(t̄_{n}))’ where κ extends elementwise on tuples of terms. Therefore, if P specifies a set of relations on A, then T_{α_{κ}}(P) specifies a corresponding set of relations on A′. Correctness of A′ with respect to A provides the correctness of the relations defined in T_{α_{κ}}(P) (the semantics of T_{α_{κ}}(P)) with respect to those defined in P (the semantics of P). The following theorem relates the semantics of a program with that of a corresponding one defined on a correct constraint system.

Theorem 5.1. Let P ∈ CLP (A) and P′ ∈ CLP (A′) be the corresponding program on A′. If A′ is correct with respect to A, then β(F(P)) ⊑′ F(P′) and β(F^{♭}(P)) ⊑′ F^{♭}(P′), where β : ℘^{♭}(B^{A}) → ℘^{♭}(B^{A′}) is defined as

β(I) = { [p(κ(x̄)) :− α(c)]_{∼} | p(x̄) :− c << I } .

It is worth noting that the relation between the semantics of a program and that of the corresponding one on a correct constraint system corresponds precisely to the correctness condition in abstract interpretation. Therefore, dataflow analysis for a program can be obtained by transforming it (by T_{α}) into a corresponding program defined on an abstract (approximated) constraint system (see later Section 5.2 for a formal treatment of constraint approximation). The key point here is that both the concrete program P and the corresponding abstract one T_{α_{κ}}(P) are CLP programs (i.e, T_{α_{κ}} is a program transformation), and the corresponding semantic interpretations are instances, over two different constraint systems, of the same generalized semantics for CLP, as shown in Figure 1 (see [42] for a discussion of implemented systems that use this transformational approach for the analysis of Prolog programs).

[figure: T_{α}(P); F^{(♭)}(T_{α}(P)); P; F^{(♭)}(P); F^{(♭)}; F^{(♭)}; β; T_{α}]

FIGURE 1. Abstract interpretation by program transformation.

Given a (fixed-point) concrete semantics, dataflow analysis usually requires computing the limit of Kleene chains. Convergence to the least fixed-point in finitely many steps can be obtained either by requiring the abstract domain to satisfy the ascending chain condition, or by using widening operators to force convergence [22]. In the following we consider the conditions on the constraint system that ensure that the resulting abstract domain satisfies the ascending chain condition. We will focus primarily on abstract interpretation by condensing interpretations. This is because condensing provides a description of the multiplicity of answer constraints in terms of (possibly infinite) joins in the constraint system. This is essential in abstract interpretation by program transformation, where the termination of the analysis has to follow from the structure of the constraint system (this condition is satisfied by several well known constraint systems useful for analysis, e.g., see Section 6.1 below). We introduce the ascending chain condition on constraint systems and we show how this condition ensures finiteness in fixed-point computations. This approach is more closely related to the constraint system structure than the widening one, which is in turn more related with the (semantic) fixed-point computation. A set of constraints {c_{1}, ..., c_{n}, ..} is said to be free-variable bounded if there is a finite set of variables V such that F V (c_{i}) ⊆ V for each i ≥ 1. The following definition is important for abstract interpretation purposes:

Definition 5.3. A constraint system A is Noetherian iff its universe C does not contain any infinite ascending chain of free-variable bounded constraints.

The free-variable-boundedness condition here is important, for otherwise any constraint system with a denumerable set of variables is not Noetherian. To see this, consider the constraints c_{i} ≡ X_{1} ∨ ⋯ ∨ X_{i}: the set of constraints {c_{i} | i ≥ 1}, ordered by entailment, forms an infinite ascending chain even on a two-valued boolean interpretation. However, it is easy to see that this set is not free-variable-bounded.

Given a Noetherian constraint system A, it is easy to prove that the set of A-interpretations ℘^{♭}(B^{A}) is Noetherian. An abstract constraint system is then a Noetherian constraint system. Let A be a constraint system, then a correct abstract interpretation for constraints in A is a tuple (A, α_{κ}, A^{a}) where A^{a} is an abstract constraint system and α_{κ} is a semimorphism which specifies the correctness of the abstraction process.

Different semantic characterizations lead to different abstract evaluation strategies. Top-down abstract interpretation corresponds to the abstraction of the standard operational semantics discussed in Section 4.1. Our approach to top-down abstract interpretation encompasses various abstract interpretation frameworks defined in the literature. For example, Bruynooghe’s top-down abstract interpretation scheme for positive logic programs [11], based on an AND/OR-tree construction, encodes our interpretation structure in a corresponding tree-structure where ANDnodes interpret the ⊗ operator and OR-nodes implement the ⊕ operation on constraints. As usual, abstract unification is encoded by appropriately defining the ⊗ operator. The search strategy is the same as the one given in [11]. Bottom-up abstract interpretation, on the other hand, allows the computation of finite approximations to the fixed-point semantics associated with a given constraint logic program (this approach has been applied to static analysis of pure logic programs in [5]). Given an abstract constraint system, the corresponding abstract transformation map is defined as in the concrete case, by considering the corresponding abstract operators instead of the concrete ones. As in the pure logic programming case, the correctness of a suitable set of operators implies the correctness of the entire framework (both top-down and bottom-up). In the constraint logic programming case, the correctness of the analysis corresponds then to the correctness of the constraint system, as shown in Theorem 5.1. In the following we will concentrate on bottom-up (fixed-point-based) abstract interpretations only. For any Noetherian lattice ℘^{♭}(B^{A}), we have:

Proposition 5.4. Let A be an abstract constraint system. If P ∈ CLP (A), there is a finite k ≥ 0 such that F^{♭}(P) = T_{P}^{♭} ↑k(∅).

Proposition 5.4 does not hold in general for non-condensed interpretations, unless the constraint system is finite.

Observation 5.1. It is worth noting that our constraint system construction imposes some restrictions on the traditional lattice-based theory of abstract interpretation [24]. However, most of these restrictions come from the standard interpretation of the fundamental (domain-dependent) operators involved in logic programming. Indeed, from the domain viewpoint, the basic restriction is only the distributivity law of closed semirings. The impact of this law in the semantics of CLP programs and the application of a weaker structure in dataflow analysis is discussed later in Section 6. The remaining laws are associated with domain-dependent operators and formalize their expected behaviour. These operators are quite common in most of the frameworks for abstract interpretation of logic programs (e.g., see [5, 11]). Our approach has the advantage of axiomatically unifying all these operators into a single general structure: the constraint system. The definition of a common structure underlying the construction of abstract domains and operators has many important benefits, in particular: (1) it summarizes the general properties of domain dependent operators, which should be invariant with respect to abstraction, in order to preserve the standard properties of the semantics; and (2) it provides an immediate correspondence between well known structures of constraints and the intended dataflow analysis (e.g., see the constraint system of propositional formulae in the next section or the system of linear equalities in Section 6.1). Of course, abstract domains which are not complete lattices, and operators that do not satisfy the axioms, cannot be modeled as constraint systems in our framework. The rigid structure of constraint systems can be weakened to include more analyses, as discussed in Section 6.

5.1. An Example: Rigidity Analysis

A number of researchers have considered abstract interpretation techniques for the analysis of ground dependences for pure logic programs (see, for examples, [5, 21, 40, 58, 59]); this notion can be generalized to that of rigidity with respect to size measures, or “norms”, for terms. Intuitively, a norm is a function from the set of terms to the set of natural numbers such that the norm of a term depends only on the its principal functor and (some of) its subterms. In the following we consider the length and size norms on the Herbrand term system:

|t|_{length} = 0 if t is a variable or t = [], |t|_{length} = 1 + |tail|_{length} if t = [h|tail],

|t|_{size} = 1 if t is a variable or a constant,

|t|_{size} = 1 + |t_{1}|_{size}, ..., |t_{n}|_{size} if t = f(t_{1}, ..., t_{n}).

Given a norm | · |, a variable x is said to be relevant to a term t with respect to | · | if there is some term t′ such that | t | ≠ | s_{x}(t′, t) |.

Definition 5.4. [Rigidity [9]] Given a term system τ = (T, Sub, V), a term t ∈ τ is rigid with respect to a norm | · |_{S} on τ iff |σ(t)|_{S} = |t|_{S} for every substitution σ ∈ Sub.

Consider the term system τ_{(Σ,V)} being defined over a finite set of variables V. Let us consider the term system τ_{Σ} as defined in Example 3.2, where Σ = V: terms are finite sets of (relevant) variables with respect to a given norm. Rigid terms are denoted by the empty set of variables. Given a norm | · |_{S}, consider the mapping Vrel_{S} : τ → τ_{V}:

Vrel_{S}(t) = { v ∈ V | v is relevant to t with respect to | · |_{S} } .

It is easy to see that the traditional notion of groundness is a special case of rigidity under the selection of the norm size, since Vrel_{size}(t) = ∅ iff t is ground.

Proposition 5.5. Vrel_{S} is a morphism of term systems.

Marriott and Søndergaard have proposed an elegant domain, named Prop, to represent ground dependences among arguments in atoms ([21, 56, 58, 59]). This domain can be expressed as an instance of our framework using the algebra of propositional formulae with disjunction. Let P rop = (P rop_{V} , ∧, ∨, true, false, ∃_{X}, ∧(t) ↔ ∧(t′))_{X⊆V;t,t′∈τ_{V} ∪{∅}} be the algebra of possibly existentially quantified disjunctions of formulae, defined on the term system τ_{V}, by the connectives ∧ and ↔; where, for each finite set of variables {x_{1}, ..., x_{m}} ∈ τ_{V}: ∧({x_{1}, ..., x_{m}}) = x_{1} ∧ ... ∧ x_{m}, and ∧(∅) = true. Intuitively, the formula x ∧ y ∧ z ↔ w ∧ v represents an equation t = t′ where Vrel_{S}(t) = {x, y, z} and Vrel_{S}(t′) = {w, v}; x ∧ y represents a term whose rigidity depends upon variables x and y; while x ∨ y represents a set of terms whose rigidity depends upon variables x or y. Local variables are hidden by existential quantification, projecting away non-global variables in the computation.

Since x ↔ true is equivalent to x, a variable x that is guaranteed to be bound to a ground term is denoted x (i.e., the expression x denotes that x is rigid). It is easy to prove that, because of the finiteness of V, P rop/ ↔ is a finite constraint system.

In this section we outline the proof of correctness for the constraint system P rop/ ↔ with respect to H. Recall that an equation set is in solved form if it has the form {v_{1} = t_{1}, ..., v_{n} = t_{n}} where the v_{i}’s are distinct variables that do not occur in the right hand side of any equation [53]. Any simple equational constraint can be transformed into an equivalent constraint of the form ∃_{X}c where c is in solved form. In particular we say that a quantified set of equations is in solved form if it has the form ∃_{X}{v_{1} = t_{1}, ..., v_{n} = t_{n}} where {v_{1} = t_{1}, ..., v_{n} = t_{n}} is in solved form and X ⊆ ∪{var(t_{i}) | 1 ≤ i ≤ n}. Given a norm | · |_{S}, each set of equational constraints c = {x_{1} = t_{1}, ..., x_{n} = t_{n}} in H is associated with a boolean expression specifying rigidity relationships among (relevant) variables by means of a mapping α_{S} that is defined as follows:

α_{S}(c) = ⋀_{i=1}^{n} (x_{i} ↔ ∧(Vrel_{S}(t_{i}))).

Let E, E′ be two equivalent (finite) sets of equations and let sol(E) and sol(E′) denote the corresponding (quantifier-free) sets of equations in solved form. In this case, correctness follows from the observation that any two sets of equations in solved form are equivalent iff they are isomorphic, where a solved form equation set E is isomorphic to E′ iff there is a subset {x_{1} = y_{1}, ..., x_{k} = y_{k}} of E where y_{i}’s are distinct variables such that E′ = E [y_{1}/x_{1}, ..., y_{k}/x_{k}, x_{1}/y_{1}, ..., x_{k}/y_{k}] (see Theorem 3.13, page 81 in [53]). It is straightforward to prove that if E and E′ are equivalent sets of equations then α_{S}(sol(E)) ↔ α_{S}(sol(E′)). Since Prop_{V} is finite, we can extend α_{S} to be an additive semimorphism from the constraint system H to P rop: if c = ∪{∃_{X_{i}}c_{i} | i ∈ I} is an arbitrary H-constraint (where c_{i} are simple constraints), for a possibly infinite set of indices I, we define α(c) = ∨{∃_{X_{i}}α_{S}(sol(c_{i})) | i ∈ I}.

Theorem 5.2.

α is an additive semimorphism from the constraint system H to P rop.

Example 5.1. Notice that, because of the use of solved form equation sets, α behaves as a semimorphism. Consider the equation e = {[x|y] = [z|[w|h]]} with the norm “length” (l). While α(e) = α_{l}({x = z, y = [w|h]}) = {x ↔ z, y ↔ h}, the diagonal element is {Vrel_{l}([x|y]) ↔ Vrel_{l}([z|[w|h]])} = {y ↔ h}. It is easy to see that the diagonal element is weaker than the abstraction of the corresponding concrete constraint.

Example 5.2. Consider the norm “length” and the following constraint logic program on the Herbrand constraint system P specifying the append procedure:

   append([], L, L).
   append([H|Y], X2, [H|Z]) : −append(Y, X2, Z).

The abstract semantics for length-rigidity analysis is

T_{P}^{♭} ↑0(∅) = ∅
T_{P}^{♭} ↑1(∅) = append(x_{1}, x_{2}, x_{3}) :− x_{1} ∧ (x_{2} ↔ x_{3})
T_{P}^{♭} ↑2(∅) = append(x_{1}, x_{2}, x_{3}) :− (x_{1} ∧ x_{2} ↔ x_{3})∨
∃_{{x′_{1},x′_{2},x′_{3}}}(x_{1} ↔ x′_{1} ∧ x_{2} ↔ x′_{2} ↔ x′_{3} ↔ x_{3})
= append(x_{1}, x_{2}, x_{3}) :− x_{1} ∧ (x_{2} ↔ x_{3})  (fixed-point)

The abstract semantics obtained above generalizes the standard ground behavior to length-rigidity behavior: “the second argument list-length can change iff the third argument does”. In ground dependence analysis Vrel_{size}(t) = var(t) and the abstract meaning of append is described by the relation

append(x_{1}, x_{2}, x_{3}) :− x_{3} ↔ (x_{1} ∧ x_{2}).

This result can be obtained by size-rigidity analysis. It is worth noting that all the standard semantic properties are still valid in P rop, since P rop is a constraint system. Therefore, given the abstract goal G = append({H, X}, {Y }, {H, Z}) (which abstracts append([H|X], Y, [H|Z])), by Lemma 4.2 and Theorem 4.1 we obtain from the size-rigidity analysis: ∨J_{α(P)}(G) = {(X ∧ Y) ↔ Z}.

5.2. The Approximation Operator on Constraint Systems

A space of approximate constraints can be specified using upper closure operators on a domain of constraints [24]. This is justified by observing that (by extensivity) they map any constraint into a weaker one. In this section we discuss basic properties of upper closure operators on constraint systems such that the image of a constraint system under such an operator is also a constraint system. This provides a systematic way to construct the abstract operators of an abstract constraint system, given any such closure operator on the universe of the concrete constraint system. This class of closure operators includes those associated with any abstraction α that behaves as a morphism of constraint systems. As shown later in this section, this way of defining abstract constraint systems is applicable to many, but not all, abstractions. This limitation drives our interest in weaker constraint structures, discussed in Section 6.

We first observe that any upper closure approximation of a constraint system defines a partition of the universe of constraints into convex sets, i.e., if ρ is an upper closure on the universe of constraints C, the set {c′ ∈ C | ρ(c) = ρ(c′)} is convex. As a consequence, the image of a universe of constraints C under a given upper closure operator ρ is a set of “abstract” constraints each representing a convex space of “concrete” solutions. However, in general, the abstract constraints so obtained may not satisfy the axioms for constraint systems: additional conditions have to be applied to ensure that they still provide a constraint system structure.

Definition 5.5. Let A be a constraint system with universe C, term system τ and set of variables V. An upper closure operator ρ on ⟨C, ≤⟩ is ∃-consistent if for each c ∈ C and X ⊆ V: ρ(∃_{X}c) = ∃_{X}ρ(∃_{X}c). An upper closure operator ρ on ⟨C, ≤⟩ is ∂-consistent if for each c ∈ C, x ∈ V and t ∈ τ such that x ind t: ρ(∂_{x}^{t}c) = ∂_{x}^{t}ρ(∂_{x}^{t}c).

∃-consistency for a closure operator ensures that the approximation of a constraint where the variables in X are hidden, have the same set X hidden.From this condition we prove that ρ satisfies the similar condition of ∂-consistency, the ∃-quasi-morphism condition (see Lemma 5.2) and that ρ ∘ ∃_{X} is an upper closure operator.

Lemma 5.1. ρ ∘ ∃_{X} is an upper closure operator.

Notice that ∃_{X} ∘ ρ is not idempotent, unless ∃_{X} and ρ commute. This is in accordance with a classical result of the theory of closure operators saying that any composition of two upper closure operators is an upper closure operator iff they commute [62].

Lemma 5.2 [∂-consistency, ∃-quasi-morphism]. Let ρ be an ∃-consistent upper closure operator on the constraint system A with universe C, term system τ and set of variables V. Then:

1. for each c ∈ C, x ∈ V and t ∈ τ such that x ind t: ρ(∂_{x}^{t}c) = ∂_{x}^{t}ρ(∂_{x}^{t}c); and 2. for each c ∈ C, X ⊆ V: ρ(∃_{X}c) = ρ(∃_{X}ρ(c)).

In the remainder of this section we discuss some conditions to systematically specify abstract constraint systems. This characterizes the class of abstract constraint systems (analyses) which can be systematically obtained as images of closure operators. As we will see, this program is not applicable to a number of abstract interpretations. This problem is addressed in Section 6.

Definition 5.6. Let A be a constraint system with universe C. A ∃/⊗-consistent upper closure operator (consistent for short) ρ on A is an ∃-consistent upper closure operator on ⟨C, ≤⟩ that is a ⊗-quasi morphism, namely for each c, c′ ∈ C: ρ(c ⊗ c′) = ρ(ρ(c) ⊗ ρ(c′)).

In addition to ∃-consistency, ⊗-quasi morphism relates meets of abstract constraints with meets of concrete constraints (recall that an upper closure operator is also a quasi-complete join-morphism, namely for each C ⊆ C, ρ(∑ C) = ρ(∑ ρ(C)) [74]).

Lemma 5.3. Let ρ be a consistent upper closure operator on the constraint system A, with universe C, term system τ and set of variables V. Then for each c ∈ C, x ∈ V and t ∈ τ such that x ind t: ρ(∂_{x}^{t}c) = ρ(∂_{x}^{t}ρ(c)).

As observed in [24], any Galois insertion (α, γ) defines an upper closure operator ρ = γ ∘ α on the corresponding (concrete) complete lattice. The following propositions provide some sufficient conditions for consistency of upper closures induced by a Galois insertion.

Proposition 5.6. Let A and A^{♯} be constraint systems with universes C and C^{♯} respectively, such that A^{♯} is correct with respect to A by means of a surjective and additive semimorphism α. Let γ : C^{♯} ⟶ C be defined as γ(c^{♯}) = ∑{c | α(c) ≤^{♯} c^{♯}} and ρ = γ ∘ α. Then:

1. ρ(C) is isomorphic to C^{♯}; 2. if α(∃_{X}c) = ∃_{κ(X)}^{♯}α(∃_{X}c) for every X ⊆ V and c ∈ C, then γ ∘ α is ∃-

consistent.

For example note that condition (2) is satisfied by the additive semimorphism associated with the abstract constraint system P rop.

The consistency of γ ∘ α can be proved when α is actually a morphism of constraint systems.

Proposition 5.7. Let A and A^{♯} be constraint systems with universes C and C^{♯} respectively, such that A^{♯} is correct with respect to A by means of a surjective and additive semimorphism α. Let γ : C^{♯} ⟶ C be defined as γ(c^{♯}) = ∑{c | α(c) ≤^{♯} c^{♯}} and ρ = γ ∘ α. Let X ⊆ V and c, c_{1}, c_{2} ∈ C. If α_{κ} is a morphism on constraint systems then:

1. ∃_{X}ρ(c) = ρ(∃_{X}c); and

2. ρ(ρ(c_{1}) ⊗ ρ(c_{2})) = ρ(c_{1} ⊗ c_{2}).

This result gives also a sufficient condition on A^{♯} such that the composition of ∃ and ρ is a closure, i.e., that ∃ and ρ commute.

Let A = (C, ⊗, ⊕, 1, 0, ∃_{X}, d_{t_{1},t_{2}})_{X⊆V;t_{1},t_{2}∈τ} be a constraint system and ρ be an upper closure operator on A. We define:

ρ(A) = (ρ(C), ˜⊗, ˜⊕, 1, ρ(0), ρ ∘ ∃_{X}, ρ(d_{t_{1},t_{2}}))_{X⊆V;t_{1},t_{2}∈τ}

where ρ(C) = {c ∈ C | c = ρ(c)}; c_{1} ˜⊗c_{2} = ρ(c_{1} ⊗ c_{2}) for each c_{1}, c_{2} ∈ ρ(C); and and ˜⊕ is defined, for possibly infinite families C ⊆ C, as: ˜∑C = ρ(∑ C). In the following we denote by ˜∂ the induced substitution operator in ρ(A).

Observation 5.2. It is worth noting that ρ(A) corresponds (i.e., is isomorphic) to any structure of abstract constraints such that (α, γ) is a Galois insertion between the concrete and the abstract universe of constraints, ρ = γ ∘ α and where the abstract operators of meet, join and cylindrification are defined as the corresponding best correct approximations with respect to α and γ (see [24]), namely: λc_{1}, c_{2}.α(γ(c_{1}) ⊗ γ(c_{2})), λc_{1}, c_{2}.α(γ(c_{1}) ⊕ γ(c_{2})) and for any X ⊆ V λc.α(∃_{X}γ(c)), respectively. However, ˜∂ may not correspond to the best approximation for substitution (i.e., ρ ∘ ∂) unless ρ is consistent (see Lemma 5.4 below) or satisfies other properties (see Secion 6). However, for any closure ρ, c ∈ ρ(C), x ∈ V and t ∈ τ such that x ind t, it is easy to prove by extensivity that ρ(∂_{x}^{t}c) ≤ ˜∂_{x}^{t}c.

Lemma 5.4. Let ρ be a consistent upper closure operator on the constraint system A, with universe C, term system τ and set of variables V. Then for each c ∈ ρ(C), x ∈ V and t ∈ τ such that x ind t: ˜∂_{x}^{t}c = ρ(∂_{x}^{t}c).

Theorem 5.3. If ρ is a consistent upper closure operator on A, then ρ(A) is a constraint system.

By ⊗/⊕-quasi-morphism and Lemmata 5.2, 5.3 and 5.4: ρ(A) is correct with respect to A by means of the morphism ρ_{id}.

Example 5.3. Cylindrifications are monotonic operators, while idempotence and extensivity are specified by axioms C_{4} and C_{2} respectively. Moreover, cylindrifications commute, so if X and Y are sets of variables and c is a constraint:

∃_{X}∃_{Y} ∃_{X}c = ∃_{X}∃_{Y} c. However, for each set of variables X: ∃_{X} is not a consistent upper closure operator on the constraint system because it does not satisfy the ⊗-quasi morphism condition (see Axiom C_{3}).

Example 5.4. Another example of non-consistent closure is given by the well known interval approximation. Consider the concrete constraint system LR_{n} in Example 3.4. An extensive operator on LR_{n} can be obtained by approximating any convex polyhedron with a hypercube, which is a polyhedron whose facets are parallel to the axes (similar techniques have been used for static array bound checking by interval approximation in [22]). For any set of polyhedra c ∈ P, define box(c) as the least hypercube containing c. box is clearly an upper closure operator on the domain of convex polyhedras ordered by set inclusion. It is worth noting that box(∅) = ∅ and for each X ⊆ V_{n}: box(ˆ∃_{X}c) = ˆ∃_{X}box(c), but box is not a ⊗- quasi morphism. A similar behaviour is shared by the convex hull operator in [27] combining convex polyhedra for linear restraint analysis. Both the interval and the convex polyhedron abstractions can be used to statically detect future redundant constraints in CLP (R) computations (this problem has been studied in the context of compiler optimization in [48]). Intuitively, a constraint c in a clause is future redundant if, once c has been tested for satisfiability, it does not matter whether c is added to the constraint store, because the computation will inevitably add constraints stronger than c to the store. Here we sketch a formalization of this analysis as a non-standard CLP computation using a slightly different notion of redundancy. Consider the constraint system LR_{n} of Example 3.4. Let P ∈ CLP (LR_{n}) and ρ be any extensive operator on LR_{n}. Assume p be a predicate symbol defined in P and let C = ‘p(t̄) :− ĉ∩ c′ [] B’ ∈ P be a clause defining p. Let P′ = (P \ {C}) ∪ {p(t̄) :− c′ [] B}. If p(x̄) :− c_{p} is in F^{♭}(P′), i.e., c_{p} is the answer constraint for p in the modified program, c_{p} ∩ ĉ ≠ ∅ (i.e., c_{p} ∧ ĉ is solvable) and for each convex polyhedron c ∈ c_{p}: ρ(c) ⊆ ĉ (i.e., ĉ is weaker than ρ(c)), then ĉ is future redundant in C. To prove this claim we just note that by ρ-extensivity, for each constraint c: c ⊆ ρ(c).

It is worth noting that the hypothesis that α is a morphism of constraint systems in Proposition 5.7, is often too strong for reasonable analyses (e.g., it is easy to see that the abstraction in P rop is not a morphism). More generally, when the concrete semantics is defined on constraint systems where ⊗ is idempotent and 1 is the annihilator for ⊕, any consistent abstraction becomes a ⊗-morphism. For this family of constraint systems, any meet of closed constraints is still closed: i.e., ρ(c_{1}) ⊗ ρ(c_{2}) = ρ(ρ(c_{1}) ⊗ ρ(c_{2})). Therefore ˜⊗ is equivalent to ⊗ in ρ(A).

Theorem 5.4. Let ρ be a consistent upper closure operator for a constraint system A with universe of constraints C and let c_{1}, c_{2} ∈ C. Suppose that ρ(c_{1}) ⊗ ρ(c_{2}) ≤ ρ(c_{1} ⊗c_{2}). If A is ⊗-idempotent and 1 is the annihilator for ⊕, then ρ(c_{1} ⊗c_{2}) = ρ(c_{1}) ⊗ ρ(c_{2}).

The behavior of consistent closures is too restrictive for most of the abstract interpretations, where the intended meet approximation does not support the ⊗-quasi morphism condition. However weakening consistency may result in a structure of constraints ρ(A) that is not, in general, a constraint system. Therefore, more general abstractions require a weaker notion of constraint system. In the following section we consider ⊗-idempotent constraint systems where 1 is annihilator for ⊕, as these conditions are satisfied in most “concrete” constraint systems, e.g., CLP (H). These structures turn out to be distributive lattices [38].^{3}

6. NON-DISTRIBUTIVE CONSTRAINT SYSTEMS

In this section we discuss the impact of different closure operators (abstractions) on the general properties of constraint systems. Let A be a constraint system. By a quick inspection of Theorem 5.3 we can observe that, for any upper closure operator ρ, axioms R_{1}, R_{2}, R_{4} of Definition 3 and C_{2}, D_{1} and D_{2} of Definition 5 are satisfied in ρ(A). Therefore, we identify the remaining axioms: R_{3}, R_{5} (of Definition 3), C_{1}, C_{3}, C_{4}, C_{5}, D_{3} and D_{4} (of Definition 5) as those possibly affected by a generic abstraction (later we abuse terminology by referring to these as the distributivity laws). A non-distributive constraint system with universe C, term system τ and set of variables V is then a structure similar to a constraint system, as defined in Definition 5, except that the distributivity laws are replaced by the following respectively, where c, c′ ∈ C, C ⊆ C, t, t′, t′′ ∈ τ and {x}, X ⊆ V such that x ind t:

R_{3}. 0 ≤ 0 ⊗ c ; R_{5}. c ⊗ (∑ C) ≤ ∑{c ⊗ c′ | c′ ∈ C} ; C_{1}. 0 ≤ ∃_{X}0 ; C_{3}. ∃_{X}(c ⊗ ∃_{X}c′) ≤ ∃_{X}c ⊗ ∃_{X}c′  C_{4}. ∃_{X∪Y} c ≤ ∃_{X}∃_{Y} c ; C_{5}. ∑{∃_{X}c′ | c′ ∈ C} ≤ ∃_{X}(∑ C) ; D_{3}. d_{[t/x]t′,[t/x]t′′} ≤ ∂_{x}^{t}(d_{t′,t′′}); ; D_{4}. ∂_{x}^{t}(c ⊗ c′) ≤ ∂_{x}^{t}c ⊗ ∂_{x}^{t}c′.

In the following we identify a set of reasonable restrictions for a generic upper closure operator ρ on a constraint system A. They provide a characterization for the analyses that can be captured in some non-distributive constraint system. We list them below, each one provided with the set of non-distributive laws satisfied in ρ(A). In the following, t, t′ ∈ τ, x ∈ V and x ind t. The proofs of the following claims can be easily derived by inspection of the proof of Theorem 6.1 below.

• P_{1}. \underline{ρ(0) = 0}. The abstraction of inconsistent constraints is still inconsistent. This extends the consistency check from concrete to abstract computations. It is applied in common analysis such as: P rop, linear equalities (see Section 6.1 and [49]), inequalities (see [27]), ∃-approximation and interval approximations in Example 5.4, etc. The constraint system ρ(A) is R_{5}, C_{4}, C_{5}, D_{3} and D_{4} non-distributive, but C_{3} does not hold.

• P_{2}. \underline{ρ(d_{t,t′}) = d_{t,t′}}. Diagonal elements are invariant under abstraction. This is a typical assumption in static analysis by approximating numerical relations between variables of a program, such as: interval approximation, linear equalities and inequalities. The constraint system ρ(A) is R_{3}, R_{5}, C_{1}, C_{4}, C_{5} and D_{4} non-distributive, but C_{3} does not hold.

3Commutativity of ⊗ is not needed to show that ⟨C, ≤, 0, 1, ⊕, ⊗⟩ is a lattice, this being a consequence of R_{1}, R_{2}, R_{3}, R_{5}, ⊗-idempotence and annihilation for 1. In particular it is possible to prove from these hypotheses that a ⊗ b and b ⊗ a are both the greatest lower bounds of a and b, whence, by uniqueness, ⊗ is commutative [52]. This extends the result in [38] which requires commutativity of ⊗.

• P_{3}. \underline{ρ is additive}. The universe of abstract constraints is isomorphic to a sublattice of the concrete one. An additive closure can be obtained by lifting the abstraction on the powerset (see [26]). This provides a more precise interpretation for disjunction. The ∃-approximation in Example 5.4 is additive. The constraint system ρ(A) is R_{3}, C_{1}, C_{4}, D_{3} and D_{4} non-distributive, but C_{3} does not hold.

Axiom C_{3} can be satisfied, in its distributive or non-distributive form, provided that one of the following existential conditions is verified:

• E_{1}. \underline{ρ ∘ ∃ = ∃ ∘ ρ ∘ ∃}. This is the ∃-consistency condition in Definition 5. The constraint system ρ(A) is R_{3}, R_{5}, C_{3}, D_{3} and D_{4} non-distributive.

• E_{2}. \underline{∃ ∘ ρ = ρ ∘ ∃ ∘ ρ}. ∃ preserves the closure, i.e., existentially quantified closed constraints are still closed. In particular, ∃ ∘ ρ is a closure operator. This condition is satisfied in numerical abstract domains of constraints such as linear equalities and interval analysis. The constraint system ρ(A) is R_{3}, R_{5}, C_{1}, C_{5}, D_{3} and D_{4} non-distributive.

• E_{3}. \underline{∃ ∘ ρ = ρ ∘ ∃}. This condition is true iff both E_{1} and E_{2} are true. In this case, both ρ ∘ ∃ and ∃ ∘ ρ are closure operators [62]. This property is shared by most of the well known abstractions such as: P rop, linear equalities and inequalities, ∃ and interval abstractions, etc. The constraint system ρ(A) is R_{3}, R_{5}, D_{3} and D_{4} non-distributive.

Properties P_{1}–P_{3} can be combined with the existential conditions E_{1}–E_{3} in order to satisfy more distributivity laws. For example, we notice that for any upper closure operator ρ satisfying P_{2} and E_{1}, ρ(A) is only R_{3}, R_{5} and C_{3} non-distributive, while if it satisfies P_{2} and E_{3} then it is only R_{3} and R_{5} non-distributive. The following section shows an application of such closure operators to dataflow analysis of CLP programs.

Theorem 6.1. Let A be a constraint system with universe C, variables V and term system τ. If ρ is an upper closure operator satisfying any of the existential conditions E_{1}–E_{3} and a (possibly empty) combination of properties P_{1}–P_{3}, then ρ(A) is a non-distributive constraint system.

It is worth noting that, under the hypothesis of the previous theorem, ρ(A) is always distributive in C_{4}. The following example shows that we can prove the D_{3} distributivity, by combining P_{1} and E_{3} with a particular definition for diagonal elements (namely the best corresponding approximation).

Example 6.1. In this example we sketch the systematic derivation of abstract constraint systems from a given data-abstraction. This corresponds to generate the best approximating operator (see [24]) for each basic operator in the constraint system, including diagonal elements. As we will see, this abstraction reduces the loss of distributivity in the abstract constraint system. In the following we assume that A is a ⊗ idempotent (distributive) constraint system on the term system τ with dimension α: A = (C, ⊗, ⊕, 1, 0, ∃_{X}, d_{t_{1},t_{2}})_{X⊆V;t_{1},t_{2}∈τ} where 1 is an annihilator for ⊕.

Term systems. Let τ^{a} be a set of objects including a set V such that |V| = |V | = α. Let κ : τ ⟶ τ^{a} be a surjective function such that, by defining δ : τ^{a} ⟶ ℘(τ) as δ(a) = {t ∈ τ | κ(t) = a} for a ∈ τ^{a}, then: κ ∘ δ(a) = a and {t} ⊆ δ ∘ κ({t}) for a ∈ τ^{a} and t ∈ τ. Assume also that κ satisfies the following conditions on the structure of the constraint system τ: κ(V) = V (therefore V and V are isomorphic by κ), and for each t, t_{1}, t_{2}, t_{3} ∈ τ, x, y ∈ V: κ(s_{x}(t, t_{1})) = κ(s_{y}(t_{2}, t_{3})) when κ(x) = κ(y), κ(t) = κ(t_{2}) and κ(t_{1}) = κ(t_{3}), namely substitution is compatible with the equivalence relation induced by κ.

For any y ∈ V, a, b ∈ τ^{a}, define s_{y}^{a}(a, b) = κ(s_{x}(t, t_{1})) where κ(x) = y, t ∈ δ(a) and t_{1} ∈ δ(b). From the previous hypothesis it is easy to see that s^{a} is well defined on τ^{a}, and

Proposition 6.1. (τ^{a}, S^{a}, V) is a term system of dimension α, and κ is a morphism from τ into τ^{a}.

Constraint systems. Let ⟨X , ≤, ⊤, ⊥, ∨, ∧⟩ be a complete lattice containing a set of objects d_{a,b} for a, b ∈ τ^{a}. Assume (α, γ) be a Galois insertion of ⟨X , ≤⟩ into ⟨C, ≤⟩ such that γ(⊥) = 0. We also assume that: α(d_{t,t′}) = d_{κ(t),κ(t′)} and γ(d_{a,b}) = ⊕{d_{t,t′} | κ(t) = a and κ(t′) = b}. This corresponds to require that (α, γ) is also a Galois insertion between the corresponding sublattices generated by the diagonal elements. Finally, we assume E_{3} as existential condition for γ ∘ α.

It is straightforward, from the previous hypothesis, that γ ∘ α is an upper closure on C satisfying condition P_{1}. However, the abstract constraint system ρ(A) is only R_{5} and D_{4} non-distributive, namely we can prove D_{3} distributivity, which cannot be derived from P_{1} and E_{3} only.

Proposition 6.2. ρ(A) is a correct R_{5} and D_{4} non-distributive constraint system.

We conclude, from the previous proposition, that the behaviour of abstract diagonal elements with respect to substitution is preserved when they are derived systematically from the abstract term system. Here, the construction of abstract diagonal elements helps in proving an important distributive property.

6.1. Non-distributive Analysis: Linear Relationships

This section considers a quite common form of non-distributivity for constraint systems and applies it to the problem of inferring linear size relationships between the arguments of procedures. We consider a constraint system A with universe C, where only axiom R_{5} of Definition 3 is replaced by the weaker relation: c⊗(∑ C)≤ ∑{c ⊗ c′ | c′ ∈ C} for c ∈ C and C ⊆ C. We abuse terminology by referring to these systems as non-distributive. Axiom R_{5} is needed to prove the continuity of T_{P}^{♭}, with the eventual objective of showing the equivalence of the fixed-point and operational semantics. However the weaker property of monotonicity can be proved for any non-distributive constraint system. The following proposition follows from the monotonicity of ∃ and ⊗.

Proposition 6.3. T_{P}^{♭} is monotonic in any non-distributive constraint system A.

It follows that for Noetherian non-distributive constraint systems, T_{P}^{♭} is also continuous. Moreover, as far as equivalence of semantics is concerned, the operational semantics is, in some sense, an “all solutions” semantics where the join is taken at the end of all the possible computations; in the fixed-point case, by contrast, the join operator is applied at each partial computation step (an equivalent operational semantics can be easily defined: this would correspond to the bottom-up execution strategy of deductive databases rather than the standard operational interpretation of logic programs [54]). In this case, as the constraint system is not distributive any more, we can only have a further approximation level by applying bottom-up instead of top-down, i.e., (O(P))^{♭} ⊑ F^{♭}(P). This behavior was already observed by Jacobs and Langen [44] in the analysis of pure logic programs with condensing. In the following we study this class of constraint systems by means of an example: the linear relationship analysis.

The linear relationship analysis is useful for a variety of applications such as compile-time overflow detection, integer subrange checking, array bound checking, termination analysis, etc., has been considered by a number of researchers (e.g., [27, 49, 72, 73]). The approach of Verschaetse and De Schreye [73] for automatic inference of linear size relations among variables in logic programs can be specified as a constraint computation in our framework.

Let τ_{(Σ,V)} be defined as in Example 3.1, over a finite set of variables V. Let | · |_{S} be a norm on the term system τ_{(Σ,V)}. We define a term system τ_{Exp} of linear expressions where terms are first order terms in the language {+, 0, 1, V } (i.e., terms in τ_{({+,0,1},V)}). Since we are interested only in relations having finite arity, we can always represent any answer constraint as a constraint on the finite dimensional space of its free variables. Moreover, the use of a bottom-up semantics construction does not require any infinite set of variables for renamings. Therefore, the set of variables V can be assumed to be a finite set V_{n} = {x_{1}, ..., x_{n}}. Substitutions are performed as standard substitutions. In the following, if f(t_{1}, ..., t_{n}) is a term, then t_{1}, ..., t_{n} are its 1-subterms.

Proposition 6.4. τ_{Exp} is a term system.

The mapping Exp_{S} : τ_{(Σ,V)} → τ_{Exp} associates a linear expression with each term in τ_{(Σ,V)}, as follows: let t be a term and S_{t} be the set of selectors for the “relevant” subterms of t, i.e., s ∈ S_{t} iff s(t) is a 1-subterm of t and s(t) is not rigid.

Exp_{S}(t) = \{ \begin{matrix}t & if t is a variable \\ c_{0}+ ∑_{s∈S_{t}} Exp_{S}(s(t)) & otherwise \end{matrix}

It is straightforward to prove that Exp_{S} is a morphism.

Example 6.2. With length and size norms we have: Exp_{length}([X[a|Z]]) = 1 + 1 + Z and Exp_{size}([X[a|Z]]) = 1 + X + 1 + Z respectively.

Karr [49] shows that size relations among variables in a program can be obtained by manipulating affine relationships i.e., linear equalities of the form c_{0} = c_{1}X_{1} + ... + c_{n}X_{n}. In our framework, this corresponds to a constraint system as follows: let L be the set of affine subspaces corresponding to linear equalities on a fixed n-dimensional space (e.g., ℜ^{n}); the universe of constraints is ℘(L); the meet operation ⊗ is simply intersection of affine subspaces; the join operation is set union; cylindrification, which corresponds to the variable restriction of Verschaetse and De Schreye, corresponds to “projection” parallel to an axis, which maps a set of affine subspaces into a set of affine subspaces; let S be a set of affine subspaces and x ∈ V, t ∈ τ_{Exp}, then the substitution of x with t in S is the affine subspace ˆ∃_{{x}}([x = t] ∩ S). The elements 0 and 1 are defined as ∅ and the entire space ℜ^{n} respectively. Diagonal elements are (single) equations on the term system τ_{Exp}. As usual, for each equation t_{1} = t_{2}, we denote by [t_{1} = t_{2}] ⊆ ℜ^{n} the corresponding affine subspace.

Proposition 6.5. Rel = (℘(L), ∩, ∪, ℜ^{n}, ∅, ∃_{X}, [t = t′])_{X⊆V_{n};t,t′∈τ_{Exp}} is a constraint system.

Given a norm S, the abstraction function α_{S} can be defined by extending Exp_{S}, similarly to that of Section 5.1, therefore Rel is correct with respect to H. Note however that Rel is not Noetherian, therefore it is not directly applicable for static analysis of CLP (H) programs.

The approximation introduced in Karr [49] corresponds precisely to the abstraction of Rel given by an upper closure operator ρ_{aff} , mapping any set of points into the smallest affine subspace containing them. It is immediate to observe that: ρ_{aff} (∅) = ∅, ∃ ∘ ρ_{aff} = ρ_{aff} ∘ ∃ (in particular: cylindrification maps affine subspaces into affine subspaces) and ρ_{aff} ({c}) = c for c ∈ L (i.e., diagonal elements are not affected by abstraction). Therefore, ρ_{aff} satisfies P_{1}, P_{2} and E_{3}, and ρ_{aff} (Rel) is a R_{5} non-distributive constraint system, which is correct with respect to H. The join of two affine subspaces A_{1} and A_{2}, given by ρ_{aff} (A_{1} ∪A_{2}), is here the smallest affine subspace containing A_{1} and A_{2} (since the union of two affine subspaces is not, in general, an affine subspace). To prove that ρ_{aff} (Rel) is a non-distributive closed semiring we observe that (x_{1} = 0.5, x_{3} = 0.5 + x_{2}) ∩ ρ_{aff} ((x_{1} = 0, x_{2} = x_{3}) ∪ (x_{1} = 1, x_{3} = 1 + x_{2})) = (x_{1} = 0.5, x_{3} = 0.5 + x_{2}) while (x_{1} = 0.5, x_{3} = 0.5 + x_{2}) ∩ (x_{1} = 0, x_{2} = x_{3}) = ∅ and (x_{1} = 0.5, x_{3} = 0.5 + x_{2}) ∩ (x_{1} = 1, x_{3} = 1 + x_{2}) = ∅. As pointed out in [49], there are no infinitely ascending chains of free-variable bounded constraints in ρ_{aff} (Rel) (i.e., bounded dimension affine spaces), otherwise in any properly ascending chain of subspaces U_{1} ≤ U_{2} ≤ …, the subspaces U_{i} must have a dimension of at least one greater than U_{i−1}. ρ_{aff} (Rel) is therefore Noetherian.

Example 6.3. Consider the logic program defining the predicate append in Example 5.2, together with the norm length. The corresponding abstract program and semantics are:

\begin{matrix}append(x_{1}, x_{2}, x_{3}) :− x_{1} = 0, x_{2} = x_{3}. \\ append(x_{1}, x_{2}, x_{3}) :− x_{1} = 1 + y, x_{3} = 1 + z [] append(y, x_{2}, z). \end{matrix}

T_{P}^{♭} ↑0(∅) = ∅
T_{P}^{♭} ↑1(∅) = {append(x_{1}, x_{2}, x_{3}) :− x_{1} = 0, x_{2} = x_{3}}
T_{P}^{♭} ↑2(∅) = {append(x_{1}, x_{2}, x_{3}) :− ρ_{aff} ((x_{1} = 0, x_{2} = x_{3})∪
(x_{1} = 1, x_{3} = 1 + x_{2}))}
= {append(x_{1}, x_{2}, x_{3}) :− x_{1} + x_{2} = x_{3}}

The affine subspace x_{1} +x_{2} = x_{3} specifies the relationship among the lengths of the arguments of the predicate append in the expected way. For example, a solution for the length of the tail X in the goal append([H|X], [d|e|f], [a|b|c|d|e|f]) can be found by solving the corresponding abstract goal append(1 + X, 3, 6), resulting in X = 2. A possible implementation can be obtained by slightly modifying the CLP (R) interpreter in [47] to cope with affine relations. This corresponds to implement (at the meta level) the join operator for affine subspaces so as to combine the computed answer constraints generated by the interpreter. Thus, abstract interpretation for linear size relationships can be joined to a concrete interpretation on CLP (R) of a modified program.

7. DISCUSSION AND RELATED WORKS

Our definition of constraint systems was motivated by earlier work of Debray and Ramakrishnan [29], which gives an algebraic formulation for standard and nonstandard semantics of logic programs, but over a very different algebraic structure. In particular, we modify closed semirings (already used in [29]) to cope with constraint-like objects including cylindrification of constraints, and diagonal elements as atomic constraints. This provides a direct definition, at the constraint system level, for standard semantic notions like variable projection and unification.

Our definition of constraint logic programs is close to the original one of Jaffar and Lassez [45]. We generalize the notion of constraint system so as to apply it to possibly non-standard (e.g. abstract) interpretations. We follow [45] by defining parameter passing as generic term equations, and we generalize this notion to any possibly non-standard term system. This corresponds precisely to generalize CLP including non-standard objects (trace sequences, abstract constraints etc.) as constraints. With respect to [45], we also give an algebraic presentation for constraint systems, involving variable projection. This approach is more suitable to reason about abstract interpretation, in particular when studying closure operators on constraint systems (e.g. see Section 5.2 and Section 6).

Saraswat et al. define the semantics of concurrent constraint languages in terms of cylindric algebras [64], specifying constraint systems in the style of Scott’s information systems [65] via a set of “primitive” constraints C and an entailment relation ⊢ ⊆ ℘(C) × C. Composition of constraints is defined in terms of set union, hiding in terms of cylindrification, and parameter passing using diagonal elements. There is a fundamental difference between our work and that of Saraswat et al. in the underlying algebraic structure. Information systems are general structures where the primary role of entailment provides a very convenient mechanism for modelling blocking-ask synchronization in concurrent constraint programming languages [64]. By contrast, we are interested less with entailment as a primitive notion, than with identifying algebraic structures that make it easier to generalize the standard semantic results for constraint logic programming. In our case, the constraint system is based on closed semirings and is parametric with respect to a given term system (it is easy to associate an information system with a closed semiring^{4}(C, ⊗, ⊕, 1, 0) if ⊗ is commutative and idempotent, but of course this may not hold in general). This makes it possible to define non-standard constraint systems, e.g., for abstract interpretation, in a simpler and more structured way. In our opinion, it is easier to specify standard logical and arithmetic operators as an instance of a closed semiring than as an instance of an information system, making closed semirings a more natural basis for generalizing constraint systems to deal with standard and nonstandard semantics. This is because the lattice-structure of usual abstract domains provides a suitable abstract interpretation for ⊗, ⊕, etc. (see P rop or the affine relationship analysis). Moreover, the join operator can often be interpreted as a widening of constraints, and this can be easily characterized in a closed semiring structure. More recently, the framework of concurrent constraint programming has been extended to cope with function symbols (terms). Technically this is handled by a hyperdoctrinal account of existential and diagonal notions in [63]. However, the use of hyperdoctrines in the context of the present work does not add significant results, if compared with the classic, and somehow more standard, treatment of cylindric algebras by Cirulis [13].

4An interesting work on the relation between the Scott’s topology and a topology for closed semirings is in [51].

The idea of generalized semantics has been recently applied to the family of cc languages by Zaffanella et al. in [75]. The extension of our framework to cc is not straightforward, as we cannot (in general) provide a correct approximation of program’s behaviour by abstractly evaluating abstract versions of cc programs. This is a consequence of synchronization based on blocking ask. Intuitively a correct approximation of the program meaning generates weaker answers for any possible program behaviour. Therefore, in order to correctly characterize answers associated with suspended computations, we must guarantee that whenever a concrete computation suspends the corresponding abstract computation suspends too. This can only be obtained by replacing ask constraints with stronger constraints, which is usually not the case in abstract interpretation. Some solutions to this problem are addressed in [75].

Abstract interpretation of (sequential) constraint logic programs was considered firstly by Marriott and Søndergaard [57]. Their treatment is based on abstracting a denotational semantics for constraint logic programs. A meta-language based on the typed λ-calculus is used to specify the semantics of logic languages in a denotational style, and both the standard and non-standard semantics are viewed as instances of the meta-language specification. In our case, instead of defining a meta-language for dataflow analysis, we consider the constraint specification on which the CLP paradigm is defined. Non-standard semantics for a given constraint-based program can thus be obtained simply by appropriately modifying the underlying constraint system. This gives a formal account for abstract compilation, which is a quite standard technique in dataflow analysis implementation [68], as constraint-based computation.

A related approach is also considered by Codognet and Filè, who firstly give an algebraic definition of constraint systems and consider abstract interpretation of constraint logic programs as constraint abstraction [19]. However, the algebraic structure considered by these authors is very different: only ⊗-composition is considered, and while a notion of “computation system” is introduced, the underlying structure is not provided with a join operator. Because of this construction, mainly based on a generalization of the top-down SLD semantics, they cannot characterize, at the constraint level, the “condensing” of multiple solutions, which is very useful in abstract interpretation (e.g., see P rop and the linear relationships analysis). Thus, by applying a loop-checker consisting in a “tabled” interpreter, only finite abstract domains can be handled. In our framework, by contrast, extraneous devices such as loop checking and tabulation are not considered. Instead, finiteness is treated simply as a property of the constraint system, expressed in terms of ≤- chains. This allows non-standard computations to be specified as standard CLP computations over an appropriate (possibly Noetherian) constraint system (e.g., affine subspaces represent a suitable abstraction for linear relationships, providing an approximation that is inherently Noetherian but is not finite). Moreover, both the traditional top-down and bottom-up semantics can be specified in the standard way thus providing goal-independent static analysis of CLP programs.

Recently, constraint programming techniques have been applied to the abstract interpretation of Prolog programs. In [20] a new language: Toupie is introduced to compile the abstract semantics of Prolog into a constraint based language, where constraints over finite domains are implemented as decision diagrams. In [17], an efficient implementation of ground dependency analysis is obtained by implementing the constraint solver for propositional formulae as a Datalog program, as suggested earlier by Dart [28]. While the approach does not encode disjunction of propositional formulae, it provides a simple and powerful tool for static analysis of groundness in Prolog. Magic-like transformations are applied to get call patterns.

It should be noted here that while the framework described can describe a wide variety of program analyses, there are some kinds of analyses that it cannot express. Specifically, it cannot capture analyses where the join operator ⊕ is not commutative, since this would violate the axioms of closed semirings. Non-commutative join operators may be found in analyses that model the depth-first execution strategy of Prolog (e.g. see [6]). It is also interesting to observe that ⊕ idempotence is in contrast with the typical multiplicity of solutions for a Prolog-like system. Weaker structures can be studied for these cases.

At the constraint system level, we abstract a system of constraints which actually contains the standard (logical) interpretation of constraints: i.e., constraints as lower-closed sets of formulae, and where the approximation order is the same as entailment. This is of course a restriction, and weaker constraint systems and abstractions can be studied. In particular, by dropping axiom C_{2}, we can obtain a weaker structure which can be instantiated with (possibly non lower-closed) powerset constructions. This may be useful to associate (at the constraint system level) the set of possible computed answer constraints with each predicate^{5}. In this case, it is easy to see that the computed answer constraint semantics and and the condensed one coincide. However, we believe that axiom C_{2} is essential for a “logical” interpretation of constraints and hiding. This is a key-point in our approach to abstract interpretation of constraint logic programs, where data-flow analysis is computed in a CLP -like way. This task is obtained by requiring that both concrete and abstract constraints share a similar “logical” interpretation. This restriction allows us to join some abstract domain with suitable constraint systems. As shown in Section 4, more concrete observable behaviours (e.g., the set of computed answer constraints) can be obtained at the semantic level, by applying different semantic constructions (e.g., see the semantics in Section 4 modeling sets of computed answer constraints, without condensing). However, notice that some observable properties which are different from success patterns, such as: failure, call patterns and partial answers cannot be modeled by applying directly the semantic construction in Section 4. As for call patterns, both the magic-like transformation in [15] and the semantic-based approximation in [32] can be easily extended to CLP languages in view of the present paper. The machinery of partial answers instead may require an additional layer of abstraction, like the one applied in [16] for the compositional analysis of modular logic programs. We believe that our constraint system notion and abstraction can be easily applied to semantic constructions characterizing different observable behaviours, like those described in [10].

5We thank an anonymous referee for this comment.

8. CONCLUSIONS

We have defined an algebraic framework for a generalized semantics for constraint logic programs. Such an approach to program semantics allows a formal treatment for correctness conditions in any non-standard interpretation, e.g., for abstract interpretation, or reasoning about compiler correctness, and provides a basis for the study of the general algebraic properties of the semantics construction. The ability to represent the condensing process as an operator in the constraint system simplifies the abstract semantic construction, and provides a formal axiomatic treatment of abstraction. Moreover, the use of variable hiding operators (such as cylindrifications) in the T_{P} definition allows the use of finite dimension constraint systems and provides a formal treatment of renaming in abstract interpretation. Finite dimension constraint systems are particularly useful to provide finite upper approximations to the semantics, such as in the case of linear relationships analysis, where the finiteness is strongly related with the (finite) dimension of the space of solutions.

Further generalizations are possible in view of abstract interpretation. Weaker constraint systems can be considered, where for example distributivity does not hold. The distributivity restriction is not applicable to a wide class of static analysis problems including linear relationships, as shown in Section 6.1, and range variable analysis, based on an abstract lattice of intervals specifying the range of program variables [3]. Non-distributive constraint systems can be studied as a more general framework for constraint-based program analysis. A classification of the different constraint systems which are useful in dataflow analysis can be based on the set of properties they hold. A comparison with our framework can be helpful to systematically derive those properties of the semantics construction that may be affected by a different constraint system definition. Moreover, the notion of abstraction can be refined even more by considering semimorphisms of term systems, where terms are ordered by instantiation. This can be suitable to characterize term abstraction in abstract interpretation.

The stimulating discussions with Roberto Bagnara, Roberto Barbuti, Veroniek Dumortier, Maurizio Gabbrielli, Georg Karner, Michael Maher, Nino Salibra, and Gert Smolka are gratefully acknowledged. We thank the anonymous referees for many helpful comments.

A. APPENDIX: PROOFS OF SELECTED RESULTS

Proposition 3.1.

Closed semirings are continuous.

Proof. [sketch] It is easy to prove, from R_{4}, that if {a_{i}}_{i∈I} is a possibly infinite family of objects in C, and a ∈ C then, if a⊕a_{i} = a for all i ∈ I, then a⊕(∑_{i∈I} a_{i}) = a. Therefore, by idempotence, a closed semiring is always continuous or finitary (this claim has been recently proved in [51], Proposition 13).

Proposition 3.2.

C is partially ordered by ≤, and forms a complete lattice.

Proof. [sketch] Since (C, ⊗, ⊕, 1, 0) is a closed semiring, ⊕ is associative, commutative and idempotent, whence it is easy to show that C is partially ordered by ≤. For every c ∈ C, c ⊕ 0 = 0 ⊕ c = c, so 0 ≤ c, i.e., 0 is the least element of the partially ordered set ⟨C, ≤⟩. Consider any family X = {c_{i}}_{i∈I} ⊆ C. By Definition 3, C is closed under finite and infinite applications of ⊕, whence ∑ X ∈ C. From associativity, commutativity, and idempotence of ⊕ we have, for any i ∈ I, c_{i} ⊕ (∑ X) = c_{0} ⊕ … ⊕ c_{i} ⊕ c_{i} ⊕ … = ∑ X, whence c_{i} ≤ (∑ X) for all c_{i} ∈ X, i.e., ∑ X is an upper bound of X. From continuity, ∑ X is also the least upper bound of X. It follows that C is a ⊕-semilattice with a minimal element 0. Thus ⟨C, ≤⟩ is a complete lattice.

Theorem 3.1.

Let A be an arbitrary constraint system. For any c, c′ ∈ C, x ∈ V, X ⊆ V and t, t′, t′′ ∈ τ such that x ind t, the following properties hold:

P1: ∃_{X}∃_{X}c = ∃_{X}c;

P2: c ≤ c′ ⇒ ∃_{X}c ≤ ∃_{X}c′;

P3: ∀c, c′ ∈ C : c′ ≤ ∃_{X}c ⇔ ∃_{X}c′ ≤ ∃_{X}c;

P4: ∀c, c′ ∈ C : c ≤ c′ ∧ c′ ≤ ∃_{X}c ⇒ ∃_{X}c = ∃_{X}c′; P5: ∃_{{x}}c = c iff ∃_{{x}}c̃ = c for some c̃ ∈ C; P6: ∃_{{x}}c = c if x ind c; P7: d_{t,t′} = ∃_{{x}}(d_{t,x} ⊗ d_{x,t′}) where x ind t, t′, P8: c ≤ c′ ⇒ ∂_{x}^{t}c ≤ ∂_{x}^{t}c′; P9: ∂_{x}^{t}∃_{{x}}c = ∃_{{x}}c; P10: ∂_{x}^{t} c = c iff ∂_{x}^{t}c̃ = c for some c̃ ∈ C; P11: ∃_{X}1 = 1; ∃_{X}c = 0 iff c = 0; P12: ∃_{{x}}d_{x,t} = 1; P13: (d_{t,t′} ⊗ d_{t′,t′′}) ⊕ d_{t,t′′} = d_{t,t′′} (transitivity).

Proof. Let c, c′ ∈ C, x ∈ V, X ⊆ V and t, t′, t′′ ∈ τ. It is straightforward to prove the componentwise monotonicity of ⊗ by the axioms.

P1, P2: Straightforward by definition.

P3: By distributivity of ∃ on ⊕ and idempotence: c′ ⊕ ∃_{X}c = ∃_{X}c ⇒ ∃_{X}c′ ⊕

∃_{X}c = ∃_{X}c. The other implication follows by C_{2}. P4: By monotonicity of ∃ and from the previous property we obtain: ∃_{X}c≤ ∃_{X}c′

and ∃_{X}c′ ≤ ∃_{X}c respectively. P5: By idempotence if x is bound in c then ∃_{{x}}c = c. Notice that the set of

fixed-points of ∃_{X} is the range of ∃_{X} itself. The converse is straightforward.

P6: Assume x ind t for some t ∈ τ. This implies ∃_{{x}}c = ∃_{{x}}∂_{x}^{t}c. From the definition of ∂_{x}^{t} and Axiom C_{4}, this is equal to ∃_{{x}}(d_{x,t} ⊗ c), which is nothing but ∂_{x}^{t}c. Since x ind t, we have ∂_{x}^{t}c = c, which proves the result.

P7: Assume t, t′ ∈ τ and x ind t, t′. By Axiom D_{3}: ∃_{{x}}(d_{t,x} ⊗ d_{x,t′}) =

d_{[t/x]x,t′} = d_{t,t′}. P8: From the monotonicity of ∃ and ⊗. P9: Assume x ind t, then by definition ∂_{x}^{t}∃_{{x}}c = ∃_{{x}}(d_{x,t} ⊗ ∃_{{x}}c). From

Axiom C_{3} this is equal to ∃_{{x}}d_{x,t} ⊗ ∃_{{x}}c. From Property P12 (proved below), this in turn is equal to ∃_{{x}}c.

P10: By P9, ∂_{x}^{t} ∂_{x}^{t}c = ∂_{x}^{t}(∃_{{x}}(d_{x,t} ⊗ c)) = ∃_{{x}}(d_{x,t} ⊗ c) = ∂_{x}^{t}c.

P11: Both follow from Axioms C_{1} and C_{2}.

P12: By Axiom D_{1}, for any t′ ∈ τ: ∃_{{x}}d_{x,t} = ∃_{{x}}(d_{x,t} ⊗d_{t′,t′}) = d_{[t/x]t′,[t/x]t′} =

1; P13: Assume x ind t, t′, t′′.

d_{t,t′′} = ∃_{{x}}(d_{t,x} ⊗ d_{x,t′′}) [ P7 ] = ∂_{x}^{t′}∃_{{x}}(d_{t,x} ⊗ d_{x,t′′}) [ x ∉ F V (∃_{{x}}(d_{t,x} ⊗ d_{x,t′′})) and P9 ] ≥∂_{x}^{t′}(d_{t,x} ⊗ d_{x,t′′}) = d_{t,t′} ⊗ d_{t′,t′′} [ ∂-monotonicity (P8) and Axiom D_{4} ]

Lemma 3.1.

For any constraint system A, if c and c′ are A-constraints and X is a set of variables such that X ind c, then ∃_{X}(c ⊗ c′) = c ⊗ ∃_{X}(c′).

Proof. By Theorem 3.1, ∃_{X}c = c, whence ∃_{X}(c ⊗ c′) = ∃_{X}(∃_{X}c ⊗ c′). From Axiom C_{3}, this is equal to ∃_{X}c ⊗ ∃_{X}c′, which is equal to c ⊗ ∃_{X}c′ since ∃_{X}c = c by Theorem 3.1.

Lemma 3.2.

For any constraints c and c′ in a constraint system A, c ⊗ ∃_{{x}}c′ = ∃_{{y}}(c ⊗ c̃′), where y ind c, c′; y ≠ x and c̃′ = ∂_{x}^{y}c′.

Proof. Suppose that y ind c, y ind c′, y ≠ x, and c̃′ = ∂_{x}^{y}c′. Since y ind c, we have ∃_{{y}}(c ⊗ c̃′) = c ⊗ ∃_{{y}}∂_{x}^{y}c′. Since y ≠ x, Axiom C_{4} implies ∃_{{y}}∂_{x}^{y}c′ = ∃_{{x}}∃_{{y}}(d_{x,y}⊗c′). Since y ind c′, this is equal to ∃_{{x}}(∃_{{y}}d_{x,y}⊗c′). From Property P12, this in turn is equal to ∃_{{x}}c′. It follows that c ⊗ ∃_{{x}}c′ = c ⊗ ∃_{{y}}∂_{x}^{y}c′ = ∃_{{y}}(c ⊗ c̃′).

Lemma 4.1.

1 [] p(t̄) ⇝_{P}^{∗} c [] ε iff d_{x̄,t̄} [] p(x̄) ⇝_{P}^{∗} c′ [] ε and ∃_{{x̄}}c′ = c; for x̄ not used in the derivation for c.

Proof. 1 [] p(t̄) ⇝_{P}^{∗} c [] ε if and only if for some clause C ≡ p(t̄_{0}) :− c_{0} [] B_{1}, ..., B_{n} in P,

1 [] p(t̄) ⇝_{P} d_{t̄,t̄_{0}} ⊗ c_{0} [] B_{1}, ..., B_{n} ⇝_{P}^{∗} c [] ε.

This is true if and only if x̄ ind C and

1 [] p(t̄) ⇝_{P} ∃_{{x̄}}(d_{t̄,x̄} ⊗ d_{x̄,t̄_{0}}) ⊗ c_{0} [] B_{1}, ..., B_{n} ⇝_{P}^{∗} c [] ε,

i.e., if and only if x̄ ind C and

1 [] p(t̄) ⇝_{P} ∃_{{x̄}}(d_{t̄,x̄} ⊗ d_{x̄,t̄_{0}} ⊗ c_{0}) [] B_{1}, ..., B_{n} ⇝_{P}^{∗} c [] ε.

Since x̄ is not used in the derivation of c: x̄ ind c, this is true if and only if d_{t̄,x̄} [] p(x̄) ⇝_{P}^{∗} c′ [] ε and ∃_{{x}}c′ = c. The result follows.

Lemma 4.2.

Let G = c_{0} [] p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) be an A-goal and P ∈ CLP (A). J_{P} (G) = c iff there exist p_{i}(x̄_{i}) :− c_{i} ∈ O(P), such that x̄_{i} ind G and x̄_{i} ∩ x̄_{j} = ∅ for 1 ≤ i, j ≤ n, i ≠ j; and c = ∃(c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ c_{1}... ⊗ d_{x̄_{n},t̄_{n}} ⊗ c_{n})_{var(G)}.

Proof. Let P ∈ CLP (A). Let G be a goal. We prove that:

{ ∃(c)_{var(G)} | G ⇝_{P}^{∗} c [] ε } =

\{ ∃(c)_{var(G)} | \begin{matrix}G = c_{0} [] p_{1}(t_{1}), ..., p_{m}(t_{m}) \\ ∀i = 1..m : 1 [] p_{i}(x̄_{i}) ⇝_{P}^{∗} c_{i} [] ε \\ x̄_{i} ind G and x̄_{i} ∩ x̄_{j} = ∅ for j = 1...n i ≠ j \\ c = c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ ∃(c_{1})_{x_{1}}... ⊗ d_{x̄_{m},t̄_{m}} ⊗ ∃(c_{m})_{x_{m}} \end{matrix} \} .

(⊆) The proof is by induction on the length n of the derivation. In the base case, assume G = 1 [] p(t) and G ⇝_{P} c [] ε. By definition, this holds iff p(x) :− c′ ∈ P and c = d_{t,x} ⊗ c′. By Lemma 3.1 and because x ∪ var(c′) ind t we have ∃(d_{t,x} ⊗ c′)_{var(t)} = ∃(d_{t,x} ⊗ ∃(c′)_{x})_{var(t)}. Let V̇ = var(d_{t,x} ⊗ c′), then

∃_{V̇ \var(t)}(d_{t,x} ⊗ c′) = ∃_{V̇ \(var(t)∪x)}∃_{x}(d_{t,x} ⊗ c′) [ Axiom C_{4} ] = ∃_{x}(d_{t,x} ⊗ ∃_{V̇ \(var(t)∪x)}c′) [ Lemma 3.1 ] = ∃_{x}(d_{t,x} ⊗ ∃(c′)_{x}) [ F V (d_{t,x} ⊗ ∃(c′)_{x}) = var(t) ∪ x ]

= ∃(d_{t,x} ⊗ ∃(c′)_{x})_{var(t)}. [ x ⊆ V̇ \ var(t) ]

In the inductive case, let G = c_{0} [] p_{1}(t_{1}), ..., p_{m}(t_{m}) such that G ⇝_{P}^{n} c [] ε. Consider a clause p_{1}(x_{1}) :− c_{1} [] b_{1}(r_{1}), ..., b_{k}(r_{k}) in P and assume:

G ⇝_{P} c_{0} ⊗ d_{t_{1},x_{1}} ⊗ ∃(c_{1})_{vc} [] b_{1}(r_{1}), ..., b_{k}(r_{k}), p_{2}(t_{2}), ..., p_{m}(t_{m}) ⇝_{P}^{n−1} c [] ε

where vc = x_{1} ∪_{i=1}^{k} var(r_{i}). By the inductive hypothesis, for i, l = 1..k and j, w =

2..m, we can define b_{i}(y_{i}) :− c′_{i} and p_{j}(x_{j}) :− c_{j} such that x_{j}, y_{i} ind G; y_{i} ≠ x_{j}; for i ≠ l, j ≠ w: y_{i} ≠ y_{l} and x_{j} ≠ x_{w}; 1 [] b_{i}(y_{i}) ⇝_{P}^{∗} c̃′_{i} [] ε, 1 [] p_{j}(x_{j}) ⇝_{P}^{∗} c̃_{j} [] ε, c′_{i} = ∃(c̃′_{i})_{y_{i}}, c_{j} = ∃(c̃_{j})_{x_{j}} (i.e., F V (c′_{i}) ⊆ y_{i} and F V (c_{j}) ⊆ x_{j}); and, by Lemma 3.1:

∃(c)_{var(G′)} = c_{0} ⊗ d_{t_{1},x_{1}} ⊗ ∃(c_{1})_{vc} ⊗ ∃ ( \begin{matrix}d_{r_{1},y_{1}} ⊗ c′_{1} ⊗ ... ⊗ d_{r_{k},y_{k}} ⊗ c′_{k}⊗ \\ d_{t_{2},x_{2}} ⊗ c_{1} ⊗ ... ⊗ d_{t_{m},x_{m}} ⊗ c_{m} \end{matrix} )_{var(G′)}

where G′ = c_{0} ⊗d_{t_{1},x_{1}} ⊗∃(c_{1})_{vc} [] b_{1}(r_{1}), ..., b_{k}(r_{k}), p_{2}(t_{2}), ..., p_{m}(t_{m}). By definition:

1 [] p_{1}(x_{1}) ⇝_{P}^{∗} c_{1} ⊗ d_{r_{1},y_{1}} ⊗ c̃′_{1} ⊗ ... ⊗ d_{r_{k},y_{k}} ⊗ c̃′_{k} [] ε.

Let c′′ = c_{1} ⊗ d_{r_{1},y_{1}} ⊗ c̃′_{1} ⊗ ... ⊗ d_{r_{k},y_{k}} ⊗ c̃′_{k}. Consider now the constraint:

c_{0} ⊗ ∃(d_{t_{1},x_{1}} ⊗ ∃(c′′)_{x_{1}} ⊗ d_{t_{2},x_{2}} ⊗ c_{1} ⊗ ... ⊗ d_{t_{m},x_{m}} ⊗ c_{m})_{var(G)}.

Because for j = 2..m: F V (c_{j}) ⊆ x_{j}; x_{j} ind t_{j}; x_{1} ind t_{1} and F V (∃(c′′)_{x_{1}}) ⊆ x_{1}, the constraint above is equivalent to

c_{0} ⊗ ∃_{{x_{1}...x_{m}}}(d_{t_{1},x_{1}} ⊗ ∃(c′′)_{x_{1}} ⊗ d_{t_{2},x_{2}} ⊗ c_{1} ⊗ ... ⊗ d_{t_{m},x_{m}} ⊗ c_{m}). (∗)

Let V̇ = var(c). Since V̇ \ var(G) = (V̇ \ var(G′)) ∪ vc where, with an abuse of notation, we denote by var(G′) the set of variables vc∪var(c_{0})∪var(t_{1}) ∪_{i=2}^{m} var(t_{i}),

and for i, l = 1..k and j, w = 2..m: F V (c′_{i}) ⊆ y_{i} and F V (c_{j}) ⊆ x_{j}; x_{j}, y_{i} ind G; y_{i} ≠ x_{j}; for i ≠ l, j ≠ w: y_{i} ≠ y_{l} and x_{j} ≠ x_{w}. From Lemma 3.1 we have:

∃(c)_{var(G)} = ∃_{vc}(∃(c)_{var(G′)})

= ∃_{vc} (c_{0} ⊗ d_{t_{1},x_{1}} ⊗ ∃(c_{1})_{vc} ⊗ ∃_{y_{1}...y_{k},x_{2}...x_{m}} ( \begin{matrix}d_{r_{1},y_{1}} ⊗ c′_{1} ⊗ ⋯ ⊗ d_{r_{k},y_{k}} ⊗ c′_{k} \\ d_{t_{2},x_{2}} ⊗ c_{1} ⊗ ⋯ ⊗ d_{t_{m},x_{m}} ⊗ c_{m} \end{matrix} ))

= c_{0} ⊗ ∃_{x_{1}..x_{m}} ( \begin{matrix}d_{t_{1},x_{1}} ⊗ ∃_{y_{1}...y_{k},vc\x_{1}} ( \begin{matrix}∃(c_{1})_{vc} ⊗ d_{r_{1},y_{1}} ⊗ c′_{1} \\ ⊗... ⊗ d_{r_{k},y_{k}} ⊗ c′_{k} \end{matrix} ) \\ ⊗d_{t_{2},x_{2}} ⊗ c_{1} ⊗ ... ⊗ d_{t_{m},x_{m}} ⊗ c_{m} \end{matrix} )

= c_{0} ⊗ ∃_{x_{1}...x_{m}}(d_{t_{1},x_{1}} ⊗ ∃(c′′)_{x_{1}} ⊗ d_{t_{2},x_{2}} ⊗ c_{1} ⊗ ⋯ ⊗ d_{t_{m},x_{m}} ⊗ c_{m})

which is equivalent to (∗).

(⊇) The proof follows by observing that, because of Lemma 3.2, we can always replace hidden variables with fresh variables in arbitrary, but finite, conjunctions of (complete) constraints (such as those computed for each atomic goal 1 [] p_{i}(x̄_{i})). Assume G = c_{0} [] p_{1}(t̄_{1}), ..., p_{m}(t̄_{m}) and for each i = 1, ..., m: 1 [] p_{i}(x̄_{i}) ⇝_{P}^{∗} c_{i} [] ε, where x̄_{i} ind G; x̄_{i} ∩ x̄_{j} = ∅ for j = 1, ..., n such that i ≠ j. Let

c = c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ ∃(c_{1})x̄_{1}... ⊗ d_{x̄_{m},t̄_{m}} ⊗ ∃(c_{m})x̄_{m}.

Notice that the computed answer constraints c_{i} for i = 1, ..., m are finite constraints. Moreover, since we assume V to be infinite, for each i = 1, ..., m, there are (fresh) variables nv_{i} ⊆ V such that nv_{i} ∩ var(G) = ∅, nv_{i} ind c_{1}, ..., c_{m} and nv_{i} ∩ nv_{j} = ∅ for j = 1, ..., m. Thus, by Lemma 3.2 if v_{i} = var(c_{i}) \ x̄_{i} and c̃_{i} = ∂_{v_{i}}^{nv_{i}}c_{i}:

c = ∃_{nv_{1}..nv_{m}}(c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ c̃_{1}... ⊗ d_{x̄_{m},t̄_{m}} ⊗ c̃_{m}).

It is straightforward to associate a successful derivation for G with renaming variables nv_{1}, ..., nv_{m} such that ∃(c)_{var(G)} = ∃_{x̄_{1}..x̄_{m}}∃_{nv_{1}..nv_{m}}c.

Lemma A.1. Let A be a constraint system, C = p(x̄) :− c [] p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) be an A-clause and I be an A-interpretation. For i = 1, ..., n let p_{i}(x̄′_{i}) :− c′_{i} and p_{i}(x̄′′_{i}) :− c′′_{i} be variants of constrained atoms in I that have been renamed apart from C and from each other. Then: ∃(c ⊗ d_{t̄_{1},x̄′_{1}} ⊗ c′_{1} ⊗ ... ⊗ d_{t̄_{n},x̄′_{1}} ⊗ c′_{n})x̄ = ∃(c ⊗ d_{t̄_{1},x̄′′_{1}} ⊗ c′′_{1} ⊗ ... ⊗ d_{t̄_{n},x̄′′_{1}} ⊗ c′′_{n})x̄.

Proof. Assume, for i = 1, ..., n: p_{i}(x̄′_{i}) :− c′_{i} and p_{i}(x̄′′_{i}) :− c′′_{i} be renamings of some p_{i}(x̄_{i}) :− c_{i}, such that x̄′_{i}, x̄′′_{i}, and x̄′′_{i} do not share any variables with each other or with C. By definition, for i = 1, ..., n: c′′_{i} = ∃x̄_{i}(d_{x̄′_{i},x̄_{i}} ⊗ c_{i}) and c′_{i} = ∃x̄_{i}(d_{x̄′′_{i},x̄_{i}} ⊗ c_{i}). Let c̃′ = ∃(c ⊗ d_{t̄_{1},x̄′_{1}} ⊗ c′_{1} ⊗ ⋯ ⊗ d_{t̄_{n},x̄′_{n}} ⊗ c′_{n})x̄ and V̇ = var(c ⊗ d_{t̄_{1},x̄′_{1}} ⊗ c′_{1} ⊗ ⋯ ⊗ d_{t̄_{n},x̄′_{n}} ⊗ c′_{n}). By applying Theorem 3.1 we can hide variables x̄′_{1}..x̄′_{n} in c̃′, namely:

c̃′ = ∃_{V̇ \\{x̄,x̄′_{1}..x̄′_{n}\}}∃_{x̄′_{1}..x̄′_{n}} ( \begin{matrix}c ⊗ d_{t̄_{1},x̄′_{1}} ⊗ ∃x̄_{1}(d_{x̄′_{1},x̄_{1}} ⊗ c_{1})⊗ \\ ... ⊗ d_{t̄_{n},x̄′_{n}} ⊗ ∃x̄_{n}(d_{x̄′_{n},x̄_{n}} ⊗ c_{n}) \end{matrix} )

[ Axiom C_{4} and definition ]

= ∃_{V̇ \\{x̄,x̄′_{1}..x̄′_{n}\}} ( \begin{matrix}c ⊗ ∃_{x̄′_{1},x̄_{1}}(d_{t̄_{1},x̄′_{1}} ⊗ d_{x̄′_{1},x̄_{1}} ⊗ c_{1})⊗ \\ ... ⊗ ∃_{x̄′_{n},x̄_{n}}(d_{t̄_{n},x̄′_{1}} ⊗ d_{x̄′_{n},x̄_{n}} ⊗ c_{n}) \end{matrix} )

[ independence ]

= ∃_{V̇ \{x̄,x̄′_{1}..x̄′_{n}}}(c ⊗ ∃x̄_{1}(d_{t̄_{1},x̄_{1}} ⊗ c_{1}) ⊗ ... ⊗ ∃x̄_{n}(d_{t̄_{n},x̄_{n}} ⊗ c_{n}))

[ Theorem 3.1 ]

= ∃_{(V̇ \{x̄,x̄′_{1}..x̄′_{n}})∪{x̄_{1}..x̄_{n}}}(c ⊗ d_{t̄_{1},x̄_{1}} ⊗ c_{1} ⊗ ... ⊗ d_{t̄_{n},x̄_{n}} ⊗ c_{n})

[ independence ]

Since x̄′_{1}..x̄′_{n} are independent for (c ⊗ d_{t̄_{1},x̄_{1}} ⊗ c_{1} ⊗ ... ⊗ d_{t̄_{n},x̄_{n}} ⊗ c_{n}), we have

c̃′ = ∃(c ⊗ d_{t̄_{1},x̄_{1}} ⊗ c_{1} ⊗ ... ⊗ d_{t̄_{n},x̄_{n}} ⊗ c_{n})x̄.

The same argument can be applied to prove that c̃′′ = ∃(c ⊗ d_{t̄_{1},x̄_{1}} ⊗ c_{1} ⊗ ... ⊗ d_{t̄_{n},x̄_{n}} ⊗ c_{n})x̄.

Lemma 4.3.

Let A be a constraint system and P ∈ CLP (A). For any I ∈ ℘(B^{A}): (T_{P} (I^{♭}))^{♭} = (T_{P} (I))^{♭}.

Proof. The lemma follows by ∃/meet-distributivity. Because P is a finite set, it is equivalent to prove that for any C ∈ P: (T_{{C}}(I^{♭}))^{♭} = (T_{{C}}(I))^{♭}. Let C = p(t̄) :− c [] p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) and I be an interpretation. Assume p(x̄) :− ∃(c̃)x̄ ∈ (T_{{C}}(I^{♭}))^{♭}. By definition, p_{i}(x̄_{i}) :− c_{i} <<_{C,x̄_{1},...,x̄_{i−1}} I^{♭}; c̃ = d_{x̄,t̄}⊗c⊗c′_{1} ⊗⋯⊗c′_{n}, where c′_{i} = d_{x̄_{i},t̄_{i}} ⊗ c_{i}; and x̄ ind C, c_{1}, ..., c_{n}. By definition, for each i = 1, ..., n there exists a set of indices W_{i} such that p_{i}(ȳ_{k}) :− c̈_{k} <<_{x_{i}} I for any k ∈ W_{i}, and c_{i} = ∑_{k∈W_{i}} ∂_{y_{k}}^{x_{i}} c̈_{k}. Therefore, for each i = 1, ..., n we can choose k_{i} ∈ W_{i} such that

p_{i}(ȳ_{k_{i}}) :− c̈_{k_{i}} <<_{x̄,x̄_{i},C,ȳ_{k_{1}} ,...,ȳ_{k_{i−1}}} I.

Thus, by T_{P} definition, for each k_{1} ∈ W_{1}, ..., k_{n} ∈ W_{n}:

p(x̄) :− ∃(d_{x̄,t̄} ⊗ c ⊗ c′_{1} ⊗ ⋯ ⊗ c′_{n})x̄ ∈ T_{{C}}(I),

where c′_{i} = d_{ȳ_{k_{i}} ,t̄_{i}} ⊗ c̈_{k_{i}}, for i = 1, ..., n. The thesis follows by ∃ and ⊗ distributivity: ∃(c̃)x̄ is equal to

∃(d_{x̄,t̄} ⊗ c⊗ ∑_{k_{1}∈W_{1}} (d_{x̄_{1},t̄_{1}} ⊗ ∃_{{y_{k_{1}} }}(d_{ȳ_{k_{1}} ,x̄_{1}} ⊗ c̈_{k_{1}})) ⊗ ⋯ ⊗

∑_{k_{n}∈W_{n}} (d_{x̄_{n},t̄_{n}} ⊗ ∃ȳ_{kn} (d_{ȳ_{kn} ,x̄_{n}} ⊗ c̈_{k_{n}})))x̄

= ∃(d_{x̄,t̄} ⊗ c⊗ ∑_{k_{1}∈W_{1}} (d_{ȳ_{k_{1}} ,t̄_{1}} ⊗ c̈_{k_{1}}) ⊗ ⋯ ⊗ ∑_{k_{n}∈W_{n}} (d_{ȳ_{kn} ,t̄_{n}} ⊗ c̈_{k_{n}}))x̄

= ∑_{k_{1}∈W_{1}} ... ∑_{k_{n}∈W_{n}} ∃ (d_{x̄,t̄} ⊗ c ⊗ (d_{ȳ_{k_{1}} ,t̄_{1}} ⊗ c̈_{k_{1}}) ⊗ ... ⊗ (d_{ȳ_{kn} ,t̄_{n}} ⊗ c̈_{k_{n}}))x̄ .

Proposition 4.2.

Let A be a constraint system and P ∈ CLP (A). T_{P} is a continuous function on the complete lattice ⟨℘(B^{A}), ⊆⟩ and T_{P}^{♭} is continuous on the complete lattice ⟨℘^{♭}(B^{A}), ⊑⟩.

Proof. The proof of continuity of T_{P} follows the standard lines (e.g. see [2]). The continuity of T_{P}^{♭} is then a straightforward consequence of the continuity of T_{P} and Lemma 4.3.

Theorem 4.1.

Let A be a constraint system with dimension ω, and P ∈ CLP (A), then F(P) = O(P)/∼ and F^{♭}(P) = (O(P)/∼)^{♭}.

Proof. We consider the condensed case only, the other case is similar. The proof is by induction: for each n ∈ N, we show that if p(x̄) :− c is any element of T_{P}^{♭} ↑ n(∅) then c = ∑{∃(c′)_{{x̄}} | 1 [] p(x̄) ⇝_{P}^{∗} c′ [] ε}. The base case is straightforward by the definition of ⇝. For the inductive case, consider a predicate p in P defined by clauses C_{1}, …, C_{k}, with C_{j} = ‘p(t̄_{j}) :− c_{0_{j}} [] p_{1_{j}}(t̄_{1_{j}}), ..., p_{m_{j}}(t̄_{m_{j}}),’ 1 ≤ j ≤ k.

Let p(x̄) :− c ∈ T_{P}^{♭} ↑ n(∅), then by definition: c = ∑_{j=1}^{k} ∃(c_{j})x̄ where x̄ ind C_{j} for

each j = 1, ..., k:

c_{j} = d_{x̄,t̄_{j}} ⊗ c_{0_{j}} ⊗ d_{x̄_{1_{j}} ,t̄_{1_{j}}} ⊗ c_{1_{j}} ⊗ ... ⊗ d_{x̄_{m_{j}} ,t̄_{m_{j}}} ⊗ c_{m_{j}}

and where p_{i_{j}}(x̄_{i_{j}}) :− c_{i_{j}} ∈ T_{P}^{♭} ↑ (n − 1)(∅) (F V (c_{i_{j}}) ⊆ x̄_{i_{j}}); x̄_{i_{j}} ind C_{j}; x̄, x̄_{i_{j}} andx̄_{l_{h}} are mutually variable-disjoint for each i, l = 1, .., m, j, h = 1, .., k such that i ≠ l and j ≠ h.

By the inductive hypothesis: for each i = 1, .., m and j = 1, .., k:

c_{i_{j}} = ∑{∃(ċ)x̄_{i_{j}} | 1 [] p_{i_{j}}(x̄_{i_{j}}) ⇝_{P}^{∗} ċ [] ε}.

Thus, by distributivity of ⊗ over ⊕: c_{j} = ∑ D_{j} where

D_{j} = \{ c_{j} | \begin{matrix}c_{j} = d_{x̄,t̄_{j}} ⊗ c_{0_{j}} ⊗ d_{x̄_{1_{j}} ,t̄_{1_{j}}} ⊗ ∃(ċ_{1_{j}})x̄_{1_{j}} ⊗ ... ⊗ d_{x̄_{m_{j}} ,t̄_{m_{j}}} ⊗ ∃(ċ_{m_{j}})x̄_{m_{j}} \\ 1 [] p_{1_{j}}(x̄_{1_{j}}) ⇝_{P}^{∗} ċ_{1_{j}} [] ε, …, 1 [] p_{m_{j}}(x̄_{m_{j}}) ⇝_{P}^{∗} ċ_{m_{j}} [] ε \end{matrix} \} .

Let G_{j} = d_{x̄,t̄_{j}} ⊗ c_{0_{j}} [] p_{1_{j}}(t̄_{1_{j}}), ..., p_{m_{j}}(t̄_{m_{j}}). Because for j, h = 1, .., k, i, l = 1, .., m: x ind C_{j} and x_{i_{j}} ≠ x_{l_{h}} for each i ≠ l and j ≠ h; we have

∑_{j=1}^{k} ∃(∑ D_{j})x̄ = ∑_{j=1}^{k} (∑{∃(∃(c_{j})_{var(G_{j})})x̄ | G_{j} ⇝_{P}^{∗} c_{j} [] ε}) [ by Lemma 4.2 ]

= ∑{∃(c)x̄ | 1 [] p(x̄) ⇝_{P}^{∗} c [] ε}. [ x̄ ⊆ var(G_{j}) ]

It is sufficient now to prove that 1 [] p(x̄) ⇝_{P}^{n} c [] ε implies that there exists c̃ ∈ C and p(x̄) :− ∃(ċ)x̄ ∈ F^{♭}(P) such that ∃(ċ)x̄ = ∃(c)x̄ ⊕ c̃. We prove this by induction: the base case is straightforward by the definition of T_{P}^{♭}. For the inductive case, assume that if 1 [] p(x̄) ⇝_{P}^{n} c [] ε then there exists c̃ ∈ C and p(x̄) :− ∃(ċ)x̄ ∈ F^{♭}(P) such that ∃(ċ)x̄ = ∃(c)x̄ ⊕ c̃. Consider:

1 [] p(x̄) ⇝_{P} c′ [] p_{1}(t̄_{1}), ..., p_{m}(t̄_{m}) ⇝_{P}^{n} c [] ε

where p(t̄) :− c_{0} [] p_{1}(t̄_{1}), ..., p_{m}(t̄_{m}) is some renamed apart clause in P and c′ = 1 ⊗ d_{x̄,t̄} ⊗ c_{0} = d_{x̄,t̄} ⊗ c_{0}. Consider the atomic goals: 1 [] p_{i}(x̄_{i}) for i = 1, ..., m. By Lemma 4.2:

1 [] p_{i}(x̄_{i}) ⇝_{P}^{k} c̈_{i} [] ε

where k ≤ n and c = d_{x̄,t̄} ⊗ c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ ∃(c̈_{1})x̄_{1} ⊗ ... ⊗ d_{x̄_{m},t̄_{m}} ⊗ ∃(c̈_{m})x̄_{m}. By the inductive hypothesis, for each i = 1, ..., m there exists p_{i}(x̄_{i}) :− ∃(ċ_{i})x̄_{i} ∈ F^{♭}(P) and c̃_{i} ∈ C such that ∃(ċ_{i})x̄_{i} = ∃(c̈_{i})x̄_{i} ⊕ c̃_{i}.

The definition of T_{P}^{♭} implies that

p(x̄) :− ∃(d_{x̄,t̄} ⊗ c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ ∃(ċ_{1})x̄_{1} ⊗ ... ⊗ d_{x̄_{m},t̄_{m}} ⊗ ∃(ċ_{m})x̄_{m})x̄

is in F^{♭}(P). Therefore

p(x̄) :− ∃(d_{x̄,t̄} ⊗ c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ (∃(c̈_{1})x̄_{1} ⊕ c̃_{1}) ⊗ … ⊗ d_{x̄_{m},t̄_{m}} ⊗ (∃(c̈_{m})x̄_{m} ⊕ c̃_{1}))

is in F^{♭}(P). The theorem is proved because ⊗ is associative, distributes on ⊕, and ⊕ is associative and commutative.

Proposition 5.1.

Let A and A′ be constraint systems as specified above. Let also c ∈ C, x ∈ V and

t ∈ τ such that x ind t. If α_{κ} : A ⟶^{s} A′ then α(∂_{x}^{t}c) ≤′ ∂_{κ(x)}^{′κ(t)}α(c).

Proof. Assume the hypothesis.

α(∂_{x}^{t}c) = α(∃_{x}(d_{x,t} ⊗ c))
≤′ ∃′_{κ(x)}α(d_{x,t} ⊗ c)
≤′ ∃′_{κ(x)}(α(d_{x,t}) ⊗′ α(c))
≤′ ∃′_{κ(x)}(d′_{κ(x),κ(t)} ⊗′ α(c)) = ∂_{κ(x)}^{′κ(t)}α(c).

Proposition 5.3.

Let A and A′ be constraint systems with universes C and C′ respectively. If A′ is correct with respect to A by means of a semimorphism α, there exists a mapping γ : C′ → C such that (α, γ) is a Galois insertion of ⟨C′, ≤′⟩ into ⟨C, ≤⟩.

Proof. Assume the hypothesis. Define γ(c′) = ∑{c | α(c) ≤′ c′}. Let c′_{1} ≤′ c′_{2}. Then, from the definition of γ and the monotonicity of α, ∑{c | α(c)≤′ c′_{1}}⊕∑{c | α(c) ≤′ c′_{2}} = γ(c′_{2}), i.e., γ is monotonic. Let c′ ∈ C′ and c ∈ C. From the definition of γ, we have α(γ(c′)) = α(∑{c | α(c) ≤′ c′}). From the additivity of α this is equal to ∑{α(c) | α(c) ≤′ c′}, and this in turn is equal to c′ from the surjectivity of α. Thus, α(γ(c′)) = c′. From the monotonicity of α we have c ≤ ∑{c̃ | α(c̃) ≤′ α(c)}. It follows, from the definition of γ, that c ≤ γ(α(c)).

Theorem 5.1.

Let P ∈ CLP (A) and P′ ∈ CLP (A′) be the corresponding program on A′. If A′ is correct with respect to A, then β(F(P)) ⊑′ F(P′) and β(F^{♭}(P)) ⊑′ F^{♭}(P′), where β : ℘^{♭}(B^{A}) → ℘^{♭}(B^{A′}) is defined as

β(I) = { [p(κ(x̄)) :− α(c)]_{∼} | p(x̄) :− c << I } .

Proof. As before we prove the condensed case as the other is similar. Let A′ be a correct constraint system with respect to A, and α_{κ} be the corresponding semimorphism. Let a << I denote a variant of an object a ∈ I that has been renamed apart from all elements of I. The mapping β : ℘^{♭}(B^{A}) → ℘^{♭}(B^{A′}) defined as

β(I) = { [p(κ(x̄)) :− α(c)]_{∼} | p(x̄) :− c << I }

is continuous by definition. As observed in [5], by β continuity, the proof can be reduced to show that β(T_{P}^{♭} (I)) ⊑′ T_{P}^{♭} (β(I)) for all I ∈ ℘^{♭}(B^{A}). Let I ∈ ℘^{♭}(B^{A}), and {C_{1}^{p}, ..., C_{m}^{p}} be the set of clauses in P defining p, where C_{j}^{p} = ‘p(t̄_{j}) :− c_{j} [] q_{1_{j}}(t̄_{1_{j}}), … q_{n_{j}}(t̄_{n_{j}})’, 1 ≤ j ≤ m. Let {C_{1}^{p′}, ..., C_{m}^{p′}} be the corresponding set of clauses on A′ in the program P′, and

⟨q_{1_{j}}(x̄_{1_{j}}) :− c̃_{1_{j}}, …, q_{n_{j}}(x̄_{n_{j}}) :− c̃_{n_{j}}⟩ <<_{C_{j}^{p}} I

and c_{i_{j}} = d_{x̄_{i_{j}} ,t̄_{i_{j}}} ⊗ c̃_{i_{j}}, 1 ≤ i ≤ n. Then, [p(κ(x̄)) :− c]_{∼} ∈ β(T_{P}^{♭} (I)) where

c = α (∑_{j=1}^{m} ∃(d_{x̄,t̄_{j}} ⊗ c_{j} ⊗ c_{1_{j}} ⊗ ⋯ ⊗ c_{n_{j}})x̄)

From the definition of semimorphism, we have

c ≤ (∑_{j=1}^{m}′∃′(α(d_{x̄,t̄_{j}}) ⊗′ α(c_{j}) ⊗′ α(c_{1_{j}}) ⊗′ ⋯ ⊗′ α(c_{n_{j}}))_{κ(x̄)})

Let ⟨q_{1_{j}}(κ(x̄_{1_{j}})) :− c̃′_{1_{j}}, …, q_{n_{j}}(κ(x̄_{n_{j}})) :− c̃′_{n_{j}}⟩ <<_{C_{j}^{p′}} β(I), and for 1 ≤ i ≤ n c′_{i_{j}} = α(d_{x̄_{i_{j}} ,t̄_{i_{j}}}) ⊗′ c̃′_{i_{j}}. It follows that

c ≤ (∑_{j=1}^{m}′∃′(α(d_{x̄,t̄_{j}}) ⊗′ α(c_{j}) ⊗′ c′_{1_{j}} ⊗′ ⋯ ⊗′ c′_{n_{j}})_{κ(x̄)}) .

By the definition of a semimorphism, for any two terms t_{1}, t_{2}: α(d_{t_{1},t_{2}})≤ d′_{κ(t_{1}),κ(t_{2})}. Then, by definition, β(T_{P}^{♭} (I)) ⊑′ T_{P}^{♭} (β(I)).

Proposition 5.5.

Vrel_{S} is a morphism of term systems. Proof. Rigid terms are mapped to ∅. Denote by s′ the substitution operation on τ_{V}. Let t_{1}, t_{2} ∈ τ and x ∈ V. If x is not a relevant variable in t_{2} then Vrel_{S}(s_{x}(t_{1}, t_{2})) = Vrel_{S}(t_{2}) and s′_{x}(Vrel_{S}(t_{1}), Vrel_{S}(t_{2})) = Vrel_{S}(t_{2}) because x ∉ Vrel_{S}(t_{2}). Assume x to be a relevant variable in t_{2}. By definition Vrel_{S}(s_{x}(t_{1}, t_{2})) = Vrel_{S}(t_{1}) ∪ (Vrel_{S}(t_{2}) \ {x}). The thesis follows from the definition of s′, namely: s′_{x}(Vrel_{S}(t_{1}), Vrel_{S}(t_{2})) = (Vrel_{S}(t_{2}) \ {x}) ∪ Vrel_{S}(t_{1}).

Theorem 5.2.

α is an additive semimorphism from the constraint system H to P rop. Proof. (outline) We prove that α is well defined for the simpler case of the “size” norm (for more details see [34]; a similar condition is also proved in [18]). Let c = ∪{c_{i} | i ∈ I} and c′ = ∪{c′_{i} | i ∈ I′} be equivalent satisfiable constraints. Suppose that ∨_{i∈I} α(c_{i})

is not equivalent to ∨_{i∈I′} α(c′_{i}). Then there must be a truth assignment r for which

there exists i ∈ I such that for each j ∈ I′: α(c_{i})(r) = true but α(c′_{j})(r) = false. Now α(c_{i}) and α(c′_{j}) are both conjunctions of formulae of the form X ↔ Y for X, Y ⊆ V, since the existentially quantified variables can be eliminated by replacing the constraint with the disjunction of all the constraints obtained by replacing the variables with the combinations of all the possible values true and false [21, 55]. Let X_{r}, Y_{r} be a partition of V such that r(X_{r}) = true and r(Y_{r}) = false (obviously, r cannot bind all the variables to true—otherwise both the constraints should be true). For each j ∈ I′, each of the conjunctive subformula of α(c′_{j}) contains X_{j} ↔ Y_{j} for some X_{j} and Y_{j} such that X_{j} ⊆ X_{r} and Y_{j} ∩ Y_{r} ≠ ∅. This is a contradiction because there exists j′ ∈ I′ such that if θ_{X_{j}} is a (grounding) solution for c′_{j′} on the variables X_{j}: y ∈ Y_{j} is ground in (c′_{j′})θ_{X_{j}} iff y is ground in (c_{i})θ_{X_{j}}. The properties of semimorphism are straightforward by the definition.

Lemma 5.2.

Let ρ be an ∃-consistent upper closure operator on the constraint system A with universe C, term system τ and set of variables V. Then:

1. for each c ∈ C, x ∈ V and t ∈ τ such that x ind t: ρ(∂_{x}^{t}c) = ∂_{x}^{t}ρ(∂_{x}^{t}c);

2. for each c ∈ C, X ⊆ V: ρ(∃_{X}c) = ρ(∃_{X}ρ(c)).

Proof. For (1), we have from the definition of ∂_{x}^{t} and the ∃-consistency of ρ that ∂_{x}^{t}ρ(∂_{x}^{t}c) = ∃_{{x}}(d_{x,t} ⊗ ∃_{{x}}ρ(∃_{{x}}(d_{x,t} ⊗ c))). From Axiom C_{3} and Property P12, this is equal to ∃_{{x}}ρ(∃_{{x}}(d_{x,t} ⊗ c)) = ∃_{{x}}ρ(∂_{x}^{t}c). Since ρ is ∃-consistent, this is equal to ρ(∂_{x}^{t}c). The result follows.

The proof of (2) proceeds as follows: Let c ∈ C and X ⊆ V. From the monotonicity of ρ and ∃, we have: ρ(∃_{X}c) ≤ ρ(∃_{X}ρ(c)). By ∃-consistency: ∃_{X}ρ(c) ≤ ∃_{X}ρ(∃_{X}c) = ρ(∃_{X}c). The result then follows from the idempotence and monotonicity of ρ.

Lemma 5.3.

Let ρ be a consistent upper closure operator on the constraint system A, with universe C, term system τ and set of variables V. Then for each c ∈ C, x ∈ V and t ∈ τ such that x ind t: ρ(∂_{x}^{t}c) = ρ(∂_{x}^{t}ρ(c)).

Proof. Let c ∈ C, x ∈ V and t ∈ τ:

ρ(∂_{x}^{t}ρ(c)) = ρ(∃_{{x}}(d_{x,t} ⊗ ρ(c)))  [ definition ]
= ρ(∃_{{x}}ρ(d_{x,t} ⊗ ρ(c)))  [ ρ(∃_{X}c) = ρ(∃_{X}ρ(c)) ]
= ρ(∃_{{x}}ρ(ρ(d_{x,t}) ⊗ ρ(c))) [ by idempotence and ⊗-quasi morphism ]
= ρ(∃_{{x}}ρ(d_{x,t} ⊗ c))  [ by ⊗-quasi morphism ]
= ρ(∂_{x}^{t}c).  [ ρ(∃_{X}c) = ρ(∃_{X}ρ(c)) and definition ]

Proposition 5.6.

Let A and A^{♯} be constraint systems with universes C and C^{♯} respectively, such that A^{♯} is correct with respect to A by means of a surjective and additive semimorphism α. Let γ = λc^{♯}. ∑{c | α(c) ≤^{♯} c^{♯}} and ρ = γ ∘ α. Then:

1. ρ(C) is isomorphic to C^{♯};

2. if α(∃_{X}c) = ∃_{κ(X)}^{♯}α(∃_{X}c) for every X ⊆ V and c ∈ C, then γ ∘ α is ∃-

consistent. Proof. Assume the hypothesis. Let ı : ρ(C) → C^{♯} such that ∀c ∈ C : ı(ρ(c)) = α(ρ(c)). By the hypothesis of Galois insertion: α(ρ(c)) = α(c). ı-surjectivity is straightforward by α-surjectivity. ı-injectivity follows because α(c) = α(c′) ⇒ ρ(c) = ρ(c′). This establishes that ρ(C) is isomorphic to C^{♯}.

For the second part, let c ∈ C and X be a set of variables. We prove that ∃_{X}ρ(∃_{X}c) = ρ(∃_{X}c). By ∃-distributivity: ∃_{X}ρ(∃_{X}c) = ∑{∃_{X}c′ ∈ C | α(c′) ≤^{♯} α(∃_{X}c)} and ρ(∃_{X}c) = ∑{c′ ∈ C | α(c′) ≤^{♯} α(∃_{X}c)}. We show that α(∃_{X}c′) ≤^{♯} α(∃_{X}c) for each constraint c′ such that α(c′) ≤^{♯} α(∃_{X}c), i.e., if c′ ∈ ρ(∃_{X}c) then ∃_{X}c′ ∈ ρ(∃_{X}c). By the hypothesis we have:

α(∃_{X}c′) ≤^{♯} ∃_{κ(X)}^{♯}α(c)
≤^{♯} ∃_{κ(X)}^{♯}α(∃_{X}c)
= α(∃_{X}c)

Thus, by ∃-extensivity (i.e., c ≤ ∃_{X}c for each constraint c and set of variables X) we have:

ρ(∃_{X}c) = ∑ { ∃_{X}c′ | α(c′) ≤^{♯} α(∃_{X}c) } = ∃_{X}ρ(∃_{X}c).

Proposition 5.7.

Let A and A^{♯} be constraint systems with universes C and C^{♯} respectively, such that A^{♯} is correct with respect to A by means of a surjective and additive semimorphism α. Let γ : C^{♯} ⟶ C be defined as γ(c^{♯}) = ∑{c | α(c) ≤^{♯} c^{♯}} and ρ = γ ∘ α. Let X ⊆ V and c, c_{1}, c_{2} ∈ C. If α_{κ} is a morphism on constraint systems then:

1. ∃_{X}ρ(c) = ρ(∃_{X}c)

2. ρ(ρ(c_{1}) ⊗ ρ(c_{2})) = ρ(c_{1} ⊗ c_{2}).

Proof. (1) Let c ∈ C and X be a set of variables. By ∃-extensivity: ρ(∃_{X}c) ≤ ∃_{X}ρ(c). By Proposition 5.6 and by the hypothesis, ρ(∃_{X}c) = ∑{∃_{X}c′ | ∃_{κ(X)}α(c′) = ∃_{κ(X)}α(c)}. However, ∃_{X}ρ(c) = ∑{∃_{X}c′ | α(c′) = α(c)} ≤ ρ(∃_{X}c), which proves the thesis.

(2) From the monotonicity of ρ and ⊗, we have ρ(c_{1} ⊗ c_{2}) ≤ ρ(ρ(c_{1}) ⊗ ρ(c_{2})). The converse is satisfied by definition:

\begin{matrix}ρ(c_{1} ⊗ c_{2}) = ∑\{c | α(c) ≤^{♯} α(c_{1} ⊗ c_{2})\} \\ ρ(ρ(c_{1}) ⊗ ρ(c_{2})) = ∑\{c | α(c) ≤^{♯} α(c′ ⊗ c′′), α(c′) ≤^{♯} α(c_{1}), α(c′′) ≤^{♯} α(c_{2})\}. \end{matrix}

By hypothesis, α is a morphism. Thus, by transitivity, and ⊗^{♯} monotonicity if c ∈ ρ(ρ(c_{1}) ⊗ ρ(c_{2})) then c ∈ { c | α(c) ≤^{♯} α(c_{1} ⊗ c_{2}) }.

Lemma 5.4.

Let ρ be a consistent upper closure operator on the constraint system A, with universe C, term system τ and set of variables V. Then for each c ∈ ρ(C), x ∈ V and t ∈ τ such that x ind t: ˜∂_{x}^{t}c = ρ(∂_{x}^{t}c).

Proof. By Lemma 5.2, ρ(∂_{x}^{t}c) = ρ(∃_{{x}}ρ(d_{x,t} ⊗ c)). From ⊗-quasi morphism, this is equal to ˜∃_{{x}}(ρ(ρ(d_{x,t}) ⊗ ρ(c))), where by definition ˜∃_{X} = ρ ∘ ∃_{X}. Since c ∈ ρ(C) and ρ is a closure operator and therefore idempotent, this is equal to ˜∃_{{x}}(ρ(d_{x,t}) ˜⊗c). The lemma follows.

Theorem 5.3.

Let ρ be a consistent upper closure operator on the constraint system A. ρ(A) is a constraint system.

Proof. Let c, c_{1}, c_{2} ∈ ρ(C), C ⊆ ρ(C), X, Y ⊆ V, x ∈ V t, t_{1}, t_{2} ∈ τ and x ind t. In the following we denote ˜∃_{X} = ρ ∘ ∃_{X} and ˜∂_{x}^{t}c = ρ(∃_{{x}}(ρ(ρ(d_{x,t}) ⊗ c))).

R_{1}: We prove that (ρ(C), ˜⊗, ˜⊕, 1, ρ(0)) is a closed semiring. By ρ idempotence and ⊗/⊕-quasi morphism: ρ(0) ˜⊕c = ρ(ρ(0) ⊕ c) = ρ(0 ⊕ c) = c; 1 ˜⊗c = ρ(1⊗c) = c; ρ(0) ˜⊗c = ρ(ρ(0)⊗c) = ρ(0⊗c) = ρ(0). Distributivity follows by ⊗-quasi morphism:

c ˜⊗( ˜∑C) = ρ(c ⊗ ρ(∑ C))
= ρ(ρ(c) ⊗ ρ(∑ C))
= ρ(∑{ρ(c ⊗ c′) | c′ ∈ C})
= ˜∑{ρ(c ⊗ c′) | c′ ∈ C}
= ˜∑{c ˜⊗c′ | c′ ∈ C}

C_{1}: By Lemma 5.2 ρ(∃_{X}(ρ(0))) = ρ(∃_{X}(0)) = ρ(0);

C_{2}: c ˜⊕˜∃_{X}c = ρ(c ⊕ ρ(∃_{X}c)) = ρ(c ⊕ ∃_{X}c) = ˜∃_{X}ρ(c) = ˜∃_{X}c;

C_{3}: By definition, ˜∃_{X}(c_{1} ˜⊗˜∃_{X}c_{2}) = ρ(∃_{X}ρ(c_{1}⊗ρ(∃_{X}c_{2}))). Since ρ is a consistent upper closure operator, it is a ⊗-quasi morphism, and further, c_{1} = ρ(c_{1}) since c_{1} ∈ ρ(C); thus, ρ(c_{1} ⊗ρ(∃_{X}c_{2})) = ρ(ρ(c_{1})⊗ρ(∃_{X}c_{2})) = ρ(c_{1} ⊗∃_{X}c_{2}). Thus, we have ˜∃_{X}(c_{1} ˜⊗˜∃_{X}c_{2}) = ρ(∃_{X}ρ(c_{1} ⊗ ∃_{X}c_{2})). From Lemma 5.2, this is equal to ρ(∃_{X}c_{1} ⊗ ∃_{X}c_{2}) = ˜∃_{X}c_{1} ˜⊗˜∃_{X}c_{2}.

C_{4}: By Lemma 5.2: ˜∃_{X} ˜∃_{Y} c = ρ(∃_{X}ρ(∃_{Y} c)) = ρ(∃_{X∪Y} c) = ˜∃_{X∪Y} c.

C_{5}: By definition, ˜∃_{X}( ˜∑C) = ρ(∃_{X}ρ(∑ C)). From Lemma 5.2 and Axiom C_{5} this is equal to ρ(∑({∃_{X}c | c ∈ C})). Since ρ is an upper closure operator it is also a quasi-complete join-morphism, whence this is equal to ρ(∑(ρ({∃_{X}c | c ∈ C}))) = ρ(∑{ρ(∃_{X}c) | c ∈ C}). This is nothing but ˜∑{˜∃_{X}c | c ∈ C}.

D_{1}: is straightforward.

D_{2}: is straightforward.

D_{3}: By Lemmata 5.3 and 5.4:

˜∂_{x}^{t}ρ(d_{t_{1},t_{2}}) = ρ(∂_{x}^{t}ρ(d_{t_{1},t_{2}})) = ρ(∂_{x}^{t}d_{t_{1},t_{2}}) = ρ(d_{[t/x]t_{1},[t/x]t_{2}}).

D_{4}: By Lemmata 5.3 and 5.4, and by ⊗-quasi morphism:

˜∂_{x}^{t}(c_{1} ˜⊗c_{2}) = ρ(∂_{x}^{t}(ρ(c_{1} ⊗ c_{2})))
= ρ(∂_{x}^{t}(c_{1} ⊗ c_{2}))
= ρ(∂_{x}^{t}c_{1} ⊗ ∂_{x}^{t}c_{2})
= ρ(ρ(∂_{x}^{t}c_{1}) ⊗ ρ(∂_{x}^{t}c_{2}))
= ˜∂_{x}^{t}c_{1} ˜⊗˜∂_{x}^{t}c_{2}.

Theorem 5.4.

Let ρ be a consistent upper closure operator for a constraint system A with universe of constraints C and let c_{1}, c_{2} ∈ C. ρ(c_{1}) ⊗ ρ(c_{2}) ≤ ρ(c_{1} ⊗ c_{2}). If A is ⊗-idempotent and 1 is the annihilator for ⊕, then ρ(c_{1} ⊗ c_{2}) = ρ(c_{1}) ⊗ ρ(c_{2}).

Proof. Let c_{1}, c_{2} ∈ C. ρ(c_{1}) ⊗ ρ(c_{2}) ≤ ρ(c_{1} ⊗ c_{2}) follows by ρ-extensivity. Assume the hypothesis on A. We prove that: ρ(c_{1}) ⊗ ρ(c_{2}) = ρ(c_{1} ⊗ c_{2}). By the hypothesis, for each constraint c, c′: c⊕(c⊗c′) = c⊗(1⊕c′) = c (i.e., c⊗c′ ≤ c). Let c≤ ρ(c_{1} ⊗c_{2}). By monotonicity: c≤ ρ(c_{1}) and c≤ ρ(c_{2}). Thus: c⊗c≤ ρ(c_{1})⊗ρ(c_{2}). The thesis follows by ⊗-idempotence.

Theorem 6.1.

Let A be a constraint system with universe C, variables V and term system τ. If ρ is an upper closure operator satisfying any existential property and a (possibly empty) combination of properties P_{1}—P_{3}, then ρ(A) is a non-distributive constraint system.

Proof. We prove the non-distributive laws for a generic upper closure operator ρ satisfying either E_{1} or E_{2}. The other claims for any combination of properties P_{1}—P_{3} can be easily derived from them. Let c, c′ ∈ ρ(C), C ⊆ ρ(C), X, Y {x} ⊆ V and t, t_{1}, t_{2} ∈ τ such that x ind t:

R_{3}: ρ(0) ⊗ c ≥ ρ(0 ⊗ c) = ρ(0).

R_{5}:  \begin{aligned}c ⊗ ( ˜∑C) & = & c ⊗ ρ(∑ C) \\ & = & ρ(c ⊗ ρ(∑ C)) \\ & ≥ & ρ(c ⊗ (∑ C)) \\ & = & ρ(∑ \{ (c ⊗ c′) | c′ ∈ C \}) \\ & = & ˜∑ \{ (c ⊗ c′) | c′ ∈ C \} . \end{aligned}

C_{1}: The case where ρ satisfies E_{1} is proved in Theorem 5.3. Otherwise, it is straightforward to prove the non-distributive version of C_{1} by extensivity for any closure operator.

C_{3}: Assume ρ satisfies E_{1}:

ρ(∃_{X}(c ⊗ ρ(∃_{X}c′))) = ρ(∃_{X}(c ⊗ ∃_{X}ρ(∃_{X}c′)))
= ρ(∃_{X}c ⊗ ∃_{X}ρ(∃_{X}c′))
≤ ρ(∃_{X}c) ⊗ ρ(∃_{X}ρ(∃_{X}c′))
= ρ(∃_{X}c) ⊗ ρ(∃_{X}c′).

The case where ρ satisfies E_{2} is straightforward. C_{4}: The case where ρ satisfies E_{1} is proved in Theorem 5.3. Assume ρ satisfies

E_{2}:

ρ(∃_{X}(ρ(∃_{Y} c))) = ρ(∃_{X∪Y} (ρ(c))) = ρ(∃_{X∪Y} c) therefore C_{4} is always distributive.

C_{5}: For a generic upper closure operator ρ:

\begin{aligned}ρ(∃_{X}(ρ(∑ C))) & ≥ & ρ(∑ \{ ∃_{X}c′ | c′ ∈ C \}) \\ & = & ρ(∑ \{ ρ(∃_{X}c′) | c′ ∈ C \}). \end{aligned}

The case where ρ satisfies E_{1} is proved in Theorem 5.3. D_{3}: Straightforward by ρ extensivity. D_{4}: It follows by ⊗ idempotence and commutativity:

ρ(∃_{{x}}(ρ(d_{x,t}) ⊗ ρ(c))) ⊗ ρ(∃_{{x}}(ρ(d_{x,t}) ⊗ ρ(c′))) ≥
ρ(∃_{{x}}(ρ(d_{x,t}) ⊗ ρ(c)) ⊗ ∃_{{x}}(ρ(d_{x,t}) ⊗ ρ(c′))) ≥
ρ(∃_{{x}}(ρ(d_{x,t}) ⊗ ρ(c) ⊗ ρ(d_{x,t}) ⊗ ρ(c′))) =
ρ(∃_{{x}}(ρ(d_{x,t}) ⊗ ρ(c) ⊗ ρ(c′)))

Proposition 6.1.

(τ^{a}, S^{a}, V) is a term system of dimension α, and κ is a morphism from τ into τ^{a}.

Proof. We simplify the notation by assuming w.l.o.g. that V = V. Let t, t′ ∈ τ, a, b ∈ τ^{a} such that κ(t) = a and κ(t′) = b, then we have:

T_{1}: s_{x}^{a}(a, x) = κ(s_{x}(t, x)) = κ(t) = a.

T_{2}: s_{x}^{a}(a, y) = κ(s_{x}(t, y)) = y.

T_{3}: s_{x}^{a}(a, s_{x}^{a}(y, b)) = κ(s_{x}(t, t_{2})) where κ(t_{2}) = κ(s_{x}(y, t′)).

Then: s_{x}^{a}(a, s_{x}^{a}(y, b)) = κ(s_{x}(t, s_{x}(y, t′))) = κ(s_{x}(y, t′)). T_{4}: The proof is analogous to that for T_{3}.

Proposition 6.2.

ρ(A) is a correct R_{5} and D_{4} non-distributive constraint system. Proof. From Theorem 6.1, it is enough to prove the D_{3} distributivity. Let ρ = γ ∘ α, t, t_{1}, t_{2} ∈ τ and x ∈ V. The proof follows by ∃/α additivity and from the basic properties of κ:

ρ(∃_{{x}}(ρ(d_{x,t}) ⊗ ρ(d_{t_{1},t_{2}}))) =
ρ(∃_{{x}} ⊕ {d_{x,t_{1}} ⊗ d_{t_{2},t_{3}} | κ(t) = κ(t_{1}), κ(t_{1}) = κ(t_{2}), κ(t_{2}) = κ(t_{3})}) =
γ(⊕{α(∃_{{x}}d_{x,t_{1}} ⊗ d_{t_{2},t_{3}}) | κ(t) = κ(t_{1}), κ(t_{1}) = κ(t_{2}), κ(t_{2}) = κ(t_{3})}) =
γ(⊕{α(d_{[t_{1}/x]t_{2},[t_{1}/x]t_{3}}) | κ(t) = κ(t_{1}), κ(t_{1}) = κ(t_{2}), κ(t_{2}) = κ(t_{3})}) =
γ(d_{κ([t/x]t_{1}),κ([t/x]t_{2}})) =
ρ(d_{[t/x]t_{1},[t/x]t_{2}})

Correctness is straightforward since ρ is an upper closure operator.

Proposition 6.5.

Rel = (℘(L), ∩, ∪, ℜ^{n}, ∅, ∃_{X}, [t = t′])_{X⊆V_{n};t,t′∈τ_{Exp}} is a constraint system.

Proof. [sketch] Most of this proof follows from the fact that the structure LR_{n} discussed in Example 3.4 is a constraint system (see [34] for details) and from an equivalent result in [41]. It is also straightforward to prove that (℘(L), ∩, ∪, ℜ^{n}, ∅) satisfies the axioms of closed semiring.

REFERENCES

1. A.V. Aho, J.E. Hopcroft, and J.D. Ullman. The Design and Analysis of Computer Algorithms. Addison Wesley Publishing Company, 1974.

2. K. R. Apt. Introduction to Logic Programming. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 495–574. Elsevier, Amsterdam and The MIT Press, Cambridge, 1990.

3. R. Bagnara, R. Giacobazzi, and G. Levi. Static Analysis of CLP Programs over Numeric Domains. In Actes Workshop on Static Analysis, WSA’92, number 81-82 in Bigre, pages 43–50, 1992.

4. R. Bagnara, R. Giacobazzi, and G. Levi. An Application of Constraint Propagation to Data-flow Analysis. In Proc of Ninth IEEE Conference on AI Applications, pages 270–276. IEEE Computer Society Press, 1993.

5. R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework for Semanticsbased Bottom-up Abstract Interpretation of Logic Programs. ACM Transactions on Programming Languages and Systems, 15(1):133–181, 1993.

6. R. Barbuti, M. Codish, R. Giacobazzi, and G. Levi. Modeling Prolog Control. Proc. Nineteenth ACM Symposium on Principles of Programming Languages, Jan. 1992, pages 95–104. ACM Press.

7. R. Barbuti and A. Martelli. A Structured Approach to Semantics Correctness. Science of Computer Programming, 3:279–311, 1983.

8. G. Birkhoff. Lattice Theory. In AMS Colloquium Publication, third ed., 1967.

9. A. Bossi, N. Cocco, and M. Fabris. Proving Termination of Logic Programs by Exploiting Term Properties. In S. Abramsky and T.S.E. Maibaum, editors, Proc. TAPSOFT’91, volume 494 of Lecture Notes in Computer Science, pages 153–180. Springer-Verlag, Berlin, 1991.

10. A. Bossi, M. Gabbrielli, G. Levi, and M. Martelli. The s-semantics approach: theory and applications. Journal of Logic Programming, 19 & 20:149–197, 1994.

11. M. Bruynooghe. A Practical Framework for the Abstract Interpretations of Logic Programs. Journal of Logic Programming, 10:91–124, 1991.

12. M. Bruynooghe, G. Janssens, B. Demoen, and A. Callebaut. Abstract Interpretation: Towards the Global Optimization of Prolog Programs. In Proc. Fourth IEEE International Symp. on Logic Programming, pages 192–204. IEEE Comp. Soc. Press, 1987.

13. J. Cirulis. An Algebraization of First Order Logic with Terms. Colloquia Mathematica Societatis Jànos Bolyai, 54:125–146, 1991.

14. K. L. Clark. Predicate logic as a computational formalism. Technical Report Dept. of Computing, Imperial College, 1979.

15. M. Codish, D. Dams, and E. Yardeni. Bottom-up Abstract Interpretation of Logic Programs. Theoretical Computer Science, 124(1):93–126, 1994.

16. M. Codish, S. K. Debray, and R. Giacobazzi. Compositional Analysis of Modular Logic Programs. In Proc. Twentieth Annual ACM Symp. on Principles of Programming Languages, pages 451–464. ACM Press, 1993.

17. M. Codish and B. Demoen. Analysing logic programs using “prop”-ositional logic programs and a magic wand. In D. Miller editor, Proc. of the 1993 International Logic Programming Symposium, pages 114–129, MIT Press 1993.

18. M. Codish, M. Falaschi, and K. Marriott. Suspension Analyses for Concurrent Logic Programs. Technical Report TR 12/92, Dipartimento di Informatica, Università di Pisa, 1992. To appear in ACM Transactions on Programming Languages and Systems.

19. P. Codognet and G. Filè. Computations, Abstractions and Constraints. In Proc. IEEE International Conference on Computer Languages, ICCL’92, IEEE Press, 1992.

20. M.-M. Corsini, K. Musumbu, A. Rauzy, and B. Le Charlier. Efficient bottomup abstract interpretation of Prolog by means of constraint solving over symbolic finite domains. In M. Bruynooghe and J. Penjam, editors, Programming Language Implementation and Logic Programming - Proceedings PLILP’93, volume 714 of Lecture Notes in Computer Science, pages 75–91. Springer-Verlag, Berlin, 1991.

21. 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.

22. 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.

23. P. Cousot and R. Cousot. A constructive characterization of the lattices of all retracts, pre-closure, quasi-closure and closure operators on a complete lattice. Portugaliæ Mathematica, 38(2):185–198, 1979.

24. P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. Sixth ACM Symp. Principles of Programming Languages, pages 269–282, 1979.

25. 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 (To appear in Acta Informatica).

26. P. Cousot and R. Cousot. Abstract Interpretation and Applications to Logic Programs. Journal of Logic Programming, 13(2 & 3):103–179, 1992.

27. P. Cousot and N. Halbwachs. Automatic Discovery of Linear Restraints Among Variables of a Program. In Proc. Fifth ACM Symp. Principles of Programming Languages, pages 84–96, 1978.

28. P. Dart. On Derived Dependencies and Connected Databases. Journal of Logic Programming, 11(2):163–188, 1991.

29. S. K. Debray and R. Ramakrishnan. Generalized Horn Clause Programs. Technical report, Dept. of Computer Science, The University of Arizona, 1991.

30. S. Eilenberg. Automata, Languages, and Machines. Academic Press, volume A, 1974.

31. M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative Modeling of the Operational Behavior of Logic Languages. Theoretical Computer Science, 69(3):289–318, 1989.

32. M. Gabbrielli and R. Giacobazzi. Goal Independency and Call Patterns in the Analysis of Logic Programs. In E. Deaton, D. Oppenheim, J. Urban and H. Berghel editors, Proc. of the Ninth ACM Symposium on Applied Computing, pages 394–399, ACM Press, Phoenix AZ 1994.

33. M. Gabbrielli and G. Levi. Modeling Answer Constraints in Constraint Logic Programs. In K. Furukawa, editor, Proc. Eighth International Conference on Logic Programming, pages 238– 252. The MIT Press, Cambridge, Mass., 1991.

34. R. Giacobazzi. Semantic Aspects of Logic Program Analysis. Ph.D. Dissertation, Universitá di Pisa, March 1993. Also available as Technical Report TD-18/93, Dip.

di Informatica, Università di Pisa, Pisa, Italy.

35. R. Giacobazzi. “Optimal” collecting semantics for analysis in a hierarchy of logic program semantics. Technical Report LIX, Ecole Polytechnique, LIX/RR/94, 1994.

36. R. Giacobazzi, S. K. Debray, and G. Levi. A Generalized Semantics for Constraint Logic Programs. In Proceedings of the International Conference on Fifth Generation Computer Systems 1992, pages 581–591, 1992.

37. R. Giacobazzi, S. Debray, and G. Levi. Joining Abstract and Concrete Computations in Constraint Logic Programmimg. In M. Nivat, C. Rattray, T. Rus and G. Scollo, editors, Proc. Third International Conference on Algebraic Methodology and Software Technology, AMAST’93, Workshops in Computing Series, pages 109–126. Springer-Verlag, London 1993.

38. J.S. Golan. The theory of semirings with applications in mathematics and theoretical computer science. Longman, Harlow, 1992.

39. M. Hanus. Formal Specification of a Prolog Compiler. In P. Deransart, B. Lorho, and J. Maluszyński, editors, Proc. International Workshop on Programming Languages Implementation and Logic Programming, volume 348 of Lecture Notes in Computer Science, pages 273–282. Springer-Verlag, Berlin, 1988.

40. M. Hanus. Analysis of Nonlinear Constraints in CLP(R). In Proc. Tenth International Conference on Logic Programming, pages 83–99. MIT Press.

41. L. Henkin, J.D. Monk, and A. Tarski. Cylindric Algebras. Part I and II. North-Holland, Amsterdam, 1971.

42. M. Hermenegildo, R. Warren, and S.K. Debray. Global flow analysis as a practical compilation tool. Journal of Logic Programming, 13(4):349–366, 1992.

43. Y.E. Ioannidis and E. Wong. An Algebraic Approach to Recursive Inference. In L. Kerschberg, editor, Proc. First International Conference on Expert Database Systems - Charleston SC, pages 295–309, 1987.

44. D. Jacobs and A. Langen. Static Analysis of Logic Programs for Independent AND Parallelism. Journal of Logic Programming, 13(2 & 3):291–314, 1992.

45. 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.

46. J. Jaffar and M.J. Maher. Constraint Logic Programming: A Survey. Journal of Logic Programming, 19 & 20:503–581, 1994.

47. 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.

48. N. Jørgensen, K. Marriot, and S. Michaylov. Some Global Compile-Time Optimizations for CLP(R). In Proc. 1991 International Symposium on Logic Programming, pages 420–434, 1991.

49. M. Karr. Affine Relationships Among Variables of a Program. Acta Informatica, 6:133–151, 1976.

50. G. Karner. On limits in complete semirings. Semigroup Forum 45:148–165, 1992.

51. G. Karner. A topology for complete semirings. In P. Enjalbert, E.W. Mayr and K.W. Wagner, editors, 11th Annual Symposium on Theoretical Aspects of Computer Science - Proceedings STACS’94, Lecture Notes in Computer Science, pages 389–400. Springer-Verlag, Berlin, 1994.

52. G. Karner. Personal communication. 1994.

53. J.-L. Lassez, M. J. Maher, and K. Marriott. Unification Revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587– 625. Morgan Kaufmann, Los Altos, Ca., 1988.

54. J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second edition.

55. K. Marriott and H. Søndergaard. Notes for a tutorial on Abstract Interpretation of Logic Programs. Informal Proc. of the North American Conference on Logic Programming’89, 1989.

56. K. Marriott and H. Søndergaard. Abstract Interpretation of Logic Programs: the Denotational Approach. In A. Bossi, editor, Proc. Fifth Italian Conference on Logic Programming, pages 399–425, 1990.

57. K. Marriott and H. Søndergaard. Analysis of Constraint Logic Programs. In S. K. Debray and M. Hermenegildo, editors, Proc. North American Conference on Logic Programming’90, pages 531–547. The MIT Press, Cambridge, Mass., 1990.

58. K. Marriott and H. Søndergaard. Precise and Efficient Groundness Analysis for Logic Programs. ACM Letters on Programming Languages and Systems 2(1– 4):181–196, 1993.

59. K. Marriott, H. Søndergaard, and N. D. Jones. Denotational Abstract Interpretation of Logic Programs. ACM Transactions on Programming Languages and Systems 16(3):607–648.

60. A. Melton, D.A. Schmidt, and G.E. Strecker. Galois Connections and Computer Science Applications. In D. Pitt et al., editor, Category Theory and Computer Programming, volume 240 of Lecture Notes in Computer Science, pages 299–312. Springer-Verlag, Berlin, 1986.

61. J. Morgado. A Characterization of the Closure Operators by means of one Axiom. PortugaliæMathematica, 21(3):155–156, 1962.

62. Oystein Ore. Combinations of Closure Relations. Annals of Mathematics, 44(3):514–533, 1943.

63. P. Panangaden, V. A. Saraswat, P. Scott, and R. Seely. A Hyperdoctrinal view of Concurrent Constraint Programming. In J. deBakker and G. Roszenberg and W. deRoever eds. Proc. of the REX Workshop, volume 666 of Lecture Notes in Computer Science, pages 457–476. Springer-Verlag, Berlin, 1992.

64. 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.

65. D. Scott. Domains for Denotational Semantics. In M. Nielsen and E. M. Schmidt, editors, Proc. Ninth International Colloquium on Automata, Languages and Programming, volume 140 of Lecture Notes in Computer Science, pages 577–613. Springer-Verlag, Berlin, 1982.

66. M.B. Smyth. Topology. In S. Abramsky, Dov M. Gabbay and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, Background Mathematical Structures, pages 641–761. Oxford Science Publications, 1992.

67. J. E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, 1977.

68. Jichang Tan and I-Peng Lin. Compiling Dataflow Analysis of Logic Programs. In ACM Programming Language Design and Implementation, volume 27 of SIGPLAN Notices, pages 106–115. ACM Press, 1992.

69. A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math., 5:285–309, 1955.

70. J. W. Thatcher, E. G. Wagner, and J. B. Wright. More on advice on structuring compilers and proving them correct. Theoretical Computer Science, 15:223–249, 1981.

71. M. H. van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. Journal of the ACM, 23(4):733–742, 1976.

72. A. van Gelder. Deriving Constraints Among Argument Sizes in Logic Programs. In Proc. of the eleventh ACM Conference on Principles of Database Systems, pages 47–60. ACM, 1990.

73. K. Verschaetse and D. De Schreye. Derivation of Linear Size Relations by abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Fourth International Symposium on Programming Language Implementation and Logic Programming, Proc. of PLILP’92, volume 631 of Lecture Notes in Computer Science, pages 296– 310. Springer-Verlag, Berlin, 1992.

74. M. Ward. The Closure Operators of a Lattice. Annals of Mathematics, 43(2):191– 196, 1942.

75. E. Zaffanella, R. Giacobazzi, and G. Levi. Abstracting Synchronization in Concurrent Constraint Programming. In M. Hermenegildo and J. Penjam, editors, Proc. Sixth Int’l Symp. on Programming Language Implementation and Logic Programming, PLILP’94, volume 844 of Lecture Notes in Computer Science, pages 57–72. Springer-Verlag, Berlin, 1994.