Joining Abstract and Concrete Computations in Constraint Logic Programming ^{∗}

Roberto Giacobazzi and Giorgio Levi

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

                     {giaco,levi}@di.unipi.it

Saumya K. Debray

Department of Computer Science, The University of Arizona Tucson, AZ 85721

                      debray@cs.arizona.edu

Abstract

The use of standard instances of the CLP framework (e.g. CLP (Bool) and CLP (R)) for non-standard (possibly abstract) interpretations, weakens the distinction between concrete and abstract computations in semantics and analysis. We formalize this idea by applying the well known approximation techniques (e.g. the standard theory of closure operators) in conjunction with a generalized notion of constraint system, supporting any program evaluation. The “generalized semantics” resulting from this process, abstracts 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. Both top-down and a bottom-up semantics are considered.

1 Introduction

Constraint logic programming (CLP) is a generalization of the pure logic programming paradigm, having similar model-theoretic, declarative and operational semantics [15]. CLP is then a general programming paradigm which may be instantiated on various semantic domains. The fundamental linguistic aspect of constraint logic programming is the ability of computing constraints by means of Horn-like rules. Since this aspect can be separated from the details specific to particular constraint systems, it seems natural to parameterize the semantics of CLP languages with respect to the underlying constraint system. We refer to such a semantics as generalized semantics [12]. It turns out that the generalized semantics provides 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.

∗The work of R. Giacobazzi and G. Levi was supported by the Esprit Basic Research Action 3012 - Compulog and by “Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo” of C.N.R. under grants no. 9100880.PF69. The work of S. Debray was supported in part by the National Science Foundation under grants CCR-8901283 and CCR-9123520.

In this paper we show how abstract and concrete interpretations for logicbased languages can be joined into the unifying framework of constraint logic programming. We apply the generalized semantics introduced in [12], intended to generalize the notion of constraint logic programs as firstly introduced in [15]. The algebraic approach we take to constraint interpretation makes it easy to identify a suitable set of operators which 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 a main technical contributions: to show how a wide class of analysis techniques developed for pure and constraint-based logic programs can themselves be viewed as instances of the constraint logic programming paradigm. This is obtained by considering a general notion of constraint systems which is weak enough to have general applicability and at the same time strong enough to ensure that relevant properties of the standard semantics construction for logic programs are preserved. 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 in the field of program analysis both as a tool for the formal specification of abstract domains of approximate relations and for the rapid prototyping of static analysis systems. This approach has some interesting practical applications, such as the ability to compile the data-flow analysis directly to an abstract machine for constraint logic programs. This approach, which is a logical extension of the “abstract compilation” scheme discussed in [14], removes the overhead of program interpretation incurred by keeping separate abstract and concrete interpretations, and leads to significant improvements in the speed of analysis (e.g. see [14, 22]).

The paper is structured as follows: in Section 2 we introduce the basic mathematical notations used throughout the paper. Section 3 introduces the main results in [12], thus providing an incremental step-by-step algebraic specification for constraint systems and semantics. In Section 4 we consider generalized semantics for constraint logic programs as a framework for semantics-based analyses for constraint logic programs. An example, namely ground dependency 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 ground dependency analysis; and, as shown in Section 5: CLP (R)^{1}, where a weaker notion of constraint system supporting program analysis is introduced. This is accomplished by focusing on a specific application of constraint programming to data-flow analysis, namely: linear relationships analysis, which associates linear constraints with standard equations on terms. Section 6 contains a survey of the most important related works.

1CLP (R) denotes the CLP (ℜ) (constraint logic programs on the domain of real numbers) implementation described in [16].

2 Preliminaries

The set of natural and real numbers are denoted by N and ℜ respectively. 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. We denote by Σ^{∗} the family of finite-length strings (sequences) from symbols in Σ, including the empty string Λ. Sequences are typically denoted by ⟨a_{1}, ..., a_{n}⟩ or simply a_{1}, ..., a_{n} for a_{i}’s symbols in Σ. The length of s sequence s is denoted |s|. The set 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. Let R ⊆ A × A be a binary transitive relation on A, then the transitive closure of R is denoted by R^{∗}. Syntactic identity is denoted ≡.

A set P equipped with a partial order ≤ is said to be partially ordered, and sometimes written ⟨P, ≤⟩. 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. 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, ≤, ⊥, ⊤, ∨, ∧).

To specify function parameters in function definitions we often make use of Church’s lambda notation. We write f : A → B to mean that f is a total function of A into B. 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. Let (L, ≤, ⊥, ⊤, ∨, ∧) be a non-empty complete lattice. Let f : L → L be a function. The upper ordinal powers of f are defined as follows: 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 ω.

An algebraic structure ([13]) 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 a (possibly infinite non-denumerable) 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 Q_{i} operations, 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. Morphisms σ of algebraic structures (A, Q_{A}) and (B, Q_{B}), provided with a common set of basic operators, are denoted σ : (A, Q_{A}) ⟶^{m} (B, Q_{B}).

3 Generalized semantics

In this section we recall some of the basic results on the generalized semantics in [12].

3.1 Term systems

A term system is an algebra of terms provided with a binary operator which realizes substitutions [4]. We are interested in term systems where every term depends only on a finite number of variables (also called finitary term systems). They represent the first basic definition in the semantic construction.

Definition 3.1 [term systems [4]] A term system τ is an algebraic structure (τ, S, V) where we refer to the elements of τ as τ-terms (terms for short); V is a countable set^{2} of τ-variables (variables, for short) in τ; 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′ ∈ τ. 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).

Intuitively, s_{x}(t, t′) denotes the operation “substitute t for every occurrence of the variable x in t′.” For notational convenience, we often denote s_{x}(t, t′) as [t/x] t′. This notation can be extended to substitutions on multiple variables. Notice that, 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 imposing that the dimension set [4]: {x ∈ V | [t/x] t′ ≢ t′ for some t ∈ τ} is finite for every t′ ∈ τ. A renaming of a variable x in a term t is [y/x] t for some y ≠ x. Standard properties of term systems and substitutions, such as the properties of composition, can be found in [4].

Example 3.1 Let Σ be a finite collection of function symbols. The standard term system τ_{(Σ,V)} = (T (Σ, V), Sub, V) is a term system provided that substitutions in Sub perform standard substitutions. In this case v ind t iff the variable v does not occur in t.

Notice that the substitution operators in S do not perform in general idempotent substitutions.

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} ∈ τ, ∀i = 1, ..., n. 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. Let ō = (o_{1}, ..., o_{n}) and ō′ = (o′_{1}, ..., o′_{n}) be tuples (sets) of syntactic objects. We write ō ≠ ō′ to denote o_{i} ≠ o′_{j} for each i, j.

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

2A more general definition that considers sets of arbitrary cardinalities is given in [4]: for our purposes, it suffices to consider countable sets.

s_{σ}(Δ_{1}, Δ_{2}) = \{ \begin{matrix}(Δ_{2} \ \{σ\}) ∪ Δ_{1} & if σ ∈ Δ_{2} \\ Δ_{2} & otherwise \end{matrix}

In this case, for each σ ∈ Σ and finite set Δ ⊆ Σ: σ ind Δ iff σ ∉ Δ. τ_{Σ} is a term system.

3.2 Constraint systems

The process of building constraints in any fixpoint evaluation of a given CLP program is mainly based on set-union and conjunction. We now give an algebraic characterization of this process in order to provide a framework for generalized interpretations of constraint logic programs. We consider closed semirings to summarize, in an algebraic framework, all the aspects dealing with composition of terms like unification (conjunction) and set union. A weaker structure, namely a non-distributive closed semiring, will be considered in Section 5.

Definition 3.2 [closed semirings [1]] A Closed Semiring is an algebraic structure (C, ⊗, ⊕, 1, 0) satisfying the following:

1. (C, ⊗, 1) and (C, ⊕, 0) are monoids.

2. ⊕ is commutative and idempotent.

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

4. for any countable sequence of elements a_{1}, …, a_{n}, … in C: a_{1} ⊕ a_{2} ⊕ ⋯ ⊕ a_{n} ⊕ ⋯ exists and is unique. Moreover associativity, commutativity and idempotence of ⊕ apply to countably infinite as well as to finite applications of ⊕.

5. ⊗ is left/right-distributive over finite and countably infinite applications of ⊕, i.e., if C = {a_{1}, …, a_{n}, …} is a countable sequence of elements in C and c ∈ C, then c ⊗ (⊕C) = ⊕({c ⊗ c′ | c′ ∈ C}) and (⊕C) ⊗ c = ⊕({c′ ⊗ c | c′ ∈ C}), where ⊕C denotes a_{1} ⊕ a_{2} ⊕ ⋯ ⊕ a_{n} ⊕ · · ·. A semantic definition necessarily implies some notion of “observable behav-

ior”: programs that have the same semantics are considered to not be observably different. Modeling the semantics of constraint logic programs in terms of answer constraints corresponds to considering answer constraints as the appropriate observable property [10]. Thus, the notion of solution for a given answer constraint has to be restricted (projected) to the variables of the corresponding query (output variables). Closed semirings are too weak to capture the notion of variable projection. We handle this notion by means of a family of “hiding” operators on the underlying algebra. The intuition here is that given a constraint c, the cylindrification operation ∃_{S}(c) yields the constraint obtained by “projecting out” information about the variables in S from c. Diagonal elements [13] are considered as a way to provide parameter passing [21]. In constraint logic programming the equality symbol “=” is assumed to provide term unification in any constraint system. However, cylindric algebras, which are oriented to first-order languages without function symbols, are not adequate as an algebraic semantic framework for general constraint logic programs, so we extend diagonal elements to deal with generic terms, following the approach in [4]. Finally, for each variable x and term t, a unary operator ∂_{x}^{t} extends the substitution operation to idempotent substitutions on constraints.

Definition 3.3 [constraint systems] A constraint system A is an algebraic structure (C, ⊗, ⊕, 1, 0, ∃_{Δ}, ∂_{x}^{t}, d_{t,t′})_{{x},Δ⊆V;t,t′∈τ} where C is a set of A-constrai-nts generated by a given set of atomic constraints, and is called the universe of A; V is a countable set of variables; τ is a term system; 0, 1, d_{t,t′} are distinct (atomic) elements of C, for each t, t′ ∈ τ; {∃_{Δ}}_{Δ⊆V} and {∂_{x}^{t}}_{x∈V;t∈τ} are unary operations on C the latter being defined for x ind t; ⊗, ⊕ are binary operations on C; such that the following postulates are satisfied for any c, c′ ∈ C; Δ, Ψ ⊆ V and t, t′, t′′ ∈ τ:

R_{1}. the structure (C, ⊗, ⊕, 1, 0) is a closed semiring; C_{1}. c ⊕ ∃_{Δ}c = ∃_{Δ}c; C_{2}. ∃_{Δ}(c ⊗ ∃_{Δ}c′) = ∃_{Δ}(∃_{Δ}c ⊗ c′) = ∃_{Δ}c ⊗ ∃_{Δ}c′; C_{3}. ∃_{Δ}∃_{Ψ}c = ∃_{(Δ∪Ψ)}c; C_{4}. ∃_{Δ} distributes over finite and countably infinite joins; D_{1}. d_{t,t} = 1; D_{2}. ∃_{{x}}d_{x,t} = 1; D_{3}. d_{t,t′} = d_{t′,t}; S_{1}. ∂_{x}^{t}(c) = ∃_{{x}}(d_{x,t} ⊗ c);

S_{2}. ∂_{x}^{t}(d_{t′,t′′}) = d_{[t/x]t′,[t/x]t′′};

S_{3}. ∂_{x}^{t}(c ⊗ c′) = ∂_{x}^{t}c ⊗ ∂_{x}^{t}c′.

With an abuse of notation, when clear from the context, we denote ∂_{x}^{t}(c) as [t/x] c. The meaning of cylindrification is given by the axioms from C_{1} to C_{4}, while diagonal elements and substitutions are specified by the axioms from D_{1} to S_{3}. Notice that Axiom S_{1} and S_{2} 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. Recursively, a simple constraint is any atomic constraint, or the cylindrification (substitution) of a simple constraint, or a finite conjunction (meet) of simple constraints. 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. A variable 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 the constraint ∂_{x}^{y}c such that x ≠ y. It is renamed apart if also y ind c. Let {x_{1}, ..., x_{n}} ⊆ V, in the following we will denote ∃_{var(c)\{x_{1},...,x_{n}}}c, i.e. hiding from all the variables in c except {x_{1}, …, x_{n}}, as ∃(c)_{{x_{1},...,x_{n}}}. We often omit brackets 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} ∈ τ, and denote A an arbitrary constraint system (C, ⊗, ⊕, 1, 0, ∃_{Δ}, ∂_{x}^{t}, d_{t,t′})_{{x},Δ⊆V;t,t′∈τ}. c_{1} ≤ c_{2} denotes the relation c_{1} ⊕ c_{2} = c_{2}, for c_{1}, c_{2} ∈ C. C is partially ordered by ≤, and forms a complete lattice.

A number of important properties are shared by constraint systems. In particular, for each Δ ⊆ V, ∃_{Δ} defines an additive upper closure operator on C^{3}, while the substitution operator on constraints defines an additive retraction on C^{4}. Notice that the substitution is not, in general, extensive. Moreover, if x is bound in c then x ind c, and if c is a renaming apart of c′ with respect to x, then x ind c; and if Δ ind c then ∃_{Δ}(c ⊗ c′) = c ⊗ ∃_{Δ}c′. An important property on the relation between cylindrification and renaming (with fresh variables) allows us to extend the standard approach to the semantic construction of logic programs to constraint-based programs: c ⊗ ∃_{{x}}c = ∃_{{y}}(c ⊗ ĉ′) where y ind c, c′, y ≠ x and ĉ′ = ∂_{x}^{y}c′.

Example 3.3 (CLP (H)) Let Σ = {a, b, ..., f, g, ...} be a finite collection of function symbols. Atomic constraints are (one-sorted) equations on the term system τ_{(Σ,V)} (see Example 3.1). The Herbrand constraint system A_{H}, is the quotient algebra

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

where: E_{H} is the set of possibly existentially quantified finite conjunctions of equations over τ_{(Σ,V)} and H is intended to represent the Herbrand interpretation structure, interpreting diagonal elements as unification [15]. 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 bounded variables X: σ, and s_{1}σθ ≡ t_{1}σθ , ..., s_{n}σθ ≡ t_{n}σθ. 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 the 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. ∂_{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}} { ϑ | H ⊧ E_{i}ϑ } = ∪_{i∈I_{2}} { ϑ | H ⊧ E′_{i}ϑ } .

Example 3.4 (CLP (R_{n})) In the following x⃗ = (x_{1}...x_{n}) is a vector (point) in ℜ^{n} and x_{i} is its i-th element. A hyperplane is the set of points x⃗ ∈ ℜ^{n} satisfying a_{1}x_{1} +...+a_{n}x_{n} = b, with not all a’s equal to zero. Any hyperplane 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 R_{n}, is:

3An upper closure operator ρ on a partially ordered set ⟨A, ≤⟩ is a monotonic, idempotent and extensive (i.e. ρ(x) ≥ x) operator.

4A retraction on a partially ordered set ⟨A, ≤⟩ is an operator ϱ that is idempotent and monotonic.

(P, ∩, ∪, ℜ^{n}, ∅, ∂_{x}^{t}, ˆ∃_{Δ}, [t_{1} = t_{2}])_{{x},Δ⊆V_{n};t,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} 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 [13]: 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. The substitution operator is: ∂_{x}^{t} = λc.ˆ∃_{{x}}([x = t] ∩ c). R_{n} is a constraint system.

3.3 Operational and fixpoint 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 the approach in [12] by defining Horn-like clauses on constraint systems. Constraint logic programs are defined in the usual way: let A be a constraint system on the 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 simple 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. A (generalized) constraint logic program, also called A-program, is a finite set of clauses. For notational simplicity, we will sometimes omit the superscript from the various semantic functions where the constraint system under consideration is obvious from the context. The family of A-programs is denoted by CLP (A). Finally, the renamings of variables in constraints and terms extend their meaning in the obvious way to any syntactic object (atoms, goals, clauses, programs etc.); as well as the notion of independence.

Let A be a constraint system and P ∈ CLP (A). Define ⇝_{P} (an Aderivation step) to be the least relation on A-goals such that G ⇝_{P} G′ iff • G = c_{0} □ p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}),

• there exists a renamed version of a clause in P: p_{1}(x̄_{1}) :− c_{1} □ B̄_{1}, such that var(G) ∩ var(B̄_{1} ∪ x̄_{1}) = ∅,

• G′ = c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ ∃(c_{1})_{x̄_{1}∪var(B̄_{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 Aderivation step. A successful derivation is a finite sequence whose last element has an empty body. The operational semantics is then defined in terms of the success set, namely the set of successful computations specified by the transitive closure of the transition relation on atomic A-goals, where ε denotes the empty sequence of goals:

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

Goal dependent success set semantics is defined in terms of a function J_{P} that yields the computed answer constraint for any A-goal, such that J_{P} (G) = ⊕{∃(c)_{var(G)} | G ⇝_{P}^{∗} c □ }. The following lemma proves the AND-compositio-nality for the operational semantics of constraint logic programs.

Lemma 3.1 ([12]) 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^{A}(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)}.

Since a constraint system can be non-meet-commutative, it is straightforward to notice that the independence on the selection rule does not hold in general in these semantic characterizations. For this reason we have assumed a left-to-right selection rule.

The fixpoint semantics is defined by allowing constrained atoms into the base of interpretations as suggested in [10]. Each constrained atom ‘p(x̄) :− c’ represents the set of instances p(x̄)ϑ, where ϑ is a solution of the constraint c. We assume F V (c) ⊆ var(A). It can be shown that the unfolding of a clause is independent on the variable names used in constrained atoms. This can be expressed in the semantics by a relation ∼ that captures the notion of equivalence upto renaming on constrained atoms. Let B^{A} be the set of constrained atoms of a constraint system A. 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̄′, i.e. such that x̄′ ≠ x̄_{1} and x̄′ ≠ x̄_{2} (x̄′ ind c_{1}, c_{2}); and ∂x̄′ ; x̄_{1}c_{1} = ∂x̄′ ; x̄_{2}c_{2}. The A-base of interpretations is B^{A}/∼ (denoted B^{A}).

In the following, given a syntactic object o, we denote by p(x̄) :− c <<_{o} I a constrained atom p(x̄) :− c such that [p(x̄) :− c]_{∼} ∈ I and x̄ ind o. We extend this to specify tuples of renamed apart syntactic objects.

Just as ⊕ expresses the notion of “merging together” the information present in two constraints, the operator ⊔ captures the notion of merging together the information present in two sets of constrained atoms; i.e. the operator ⊔ : ℘(B) × ℘(B) ⟶ ℘(B) is defined as follows:

I_{1} ⊔ I_{2} = {[p(x̄) :− ⊕ {∂x̄ ; x̄′c′ | p(x̄′) :− c′ <<x̄ I_{1} ∪ I_{2}}]_{∼}} for any

I_{1}, I_{2} ∈ ℘(B).

The relation ⊑, expressing the notion of a set of constrained atoms containing less information than another, is defined as follows: for any I_{1}, I_{2} ∈ ℘(B), I_{1} ⊑ I_{2} iff I_{1} ⊔ I_{2} = I_{2}. An A-interpretation is an element in ℘(B^{A}) containing at most one constrained atom for each predicate symbol. The set of Ainterpretations is denoted ℑ^{A}. ⟨ℑ^{A}, ⊑⟩ is a complete lattice.

The fixpoint semantics of a program P over a constraint system A, F^{A}(P), is defined in terms of a continuous immediate consequence operator in the style of [23], i.e. F^{A}(P) = lfp(T_{P}^{A}) = T_{P}^{A} ↑ω(∅), where the mapping T_{P}^{A} : ℑ^{A} → ℑ^{A}, is defined as follows:

T_{P}^{A}(I) = ⨆_{C∈P} \{ [p(x̄) :− ∃(c̃)x̄]_{∼} | \begin{matrix}C : p(t) :− c □ p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}), \\ 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} \}

The fixpoint semantics construction requires, potentially, only a finite set of variables. This follows from the elementary properties of cylindrification with respect to substitution. Intuitively, the hiding allows to define “local environments” which cannot be influenced by substitution. As a consequence, any hidden variable in each of the c_{i} can be (re)used outside the scope of the hiding, thus making applicable renamings by means of the same variables. The number of variables needed to compute the semantics depends from the program structure. Example 3.5 Consider the following program over the Herbrand constraint system:

\begin{aligned}p(x) & :− & x = []. \\ p(x) & :− & x = [h|y] □ p(y). \end{aligned}

The fixpoint computation for T_{P} returns the following interpretation for p (we denote by , and ; conjunction and disjunction (set-union) of constraints):

p(x) :− x = [];

∃_{h,y,x′}(x = [h|y], y = x′, x′ = []);

∃_{h,y,x′′}(x = [h|y], y = x′′, ∃_{h,y,x′}(x′′ = [h|y], y = x′, x′ = []));

∃_{h,y,x′} ( \begin{matrix}x = [h|y], y = x′, \\ ∃_{h,y,x′′} ( \begin{matrix}x′ = [h|y], y = x′′, \\ ∃_{h,y,x′}(x′′ = [h|y], y = x′, x′ = []) \end{matrix} ) \end{matrix} );

etc....

The set of variables needed to compute the fixpoint is {x, x′, x′′, h, y}.

The following result states the equivalence between the operational and the fixpoint semantics, for any constraint system A. We need that V is a denumerable set of variables. Theorem 3.2 ([12]) Let A be a constraint system and P ∈ CLP (A), then F(P) = O(P)/∼.

4 Abstract constraint systems

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 semantics correctness” in [3]. Correctness of non-standard semantic specifications can be handled in an algebraic way through the notion of morphism. However, 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 a weaker notion of morphism between algebraic structures, capturing the approximation possibly induced by abstract interpretations or by any approximate semantics defined in the framework.

A morphism of term systems, κ : τ ⟶^{m} τ′, is a function mapping terms of τ to terms of τ′ such that ∀t_{1}, t_{2} ∈ τ and x ∈ V: κ(s_{x}(t_{1}, t_{2})) = s′_{κ(x)}(κ(t_{1}), κ(t_{2})), where s and s′ are the substitution operators in τ and τ′ respectively. Let A and A′ be constraint systems (A′ = (C′, ⊗′, ⊕′, 1′, 0′, ∃′_{Δ}, ∂_{x}^{′t}, d′_{t_{1},t_{2}})_{{x},Δ⊆V′;t,t_{1},t_{2}∈τ′}) be constraint systems. There exists a semimorphism α : A ⟶^{s} A′ iff there exists a morphism of term systems κ : τ ⟶^{m} τ′ such that for each c, c_{1}, c_{2} ∈ C, C ⊆ C, {x}, Δ ⊆ V and t, t_{1}, t_{2} ∈ τ such that x ind t: α(0) = 0′, α(1) ≤′ 1′, α(⊕C) ≤′ ⊕′α(C), α(∃_{Δ}c) ≤′ ∃′_{κ(Δ)}α(c), α(c_{1} ⊗ c_{2}) ≤′ α(c_{1}) ⊗′ α(c_{2}) and α(d_{t_{1},t_{2}}) ≤′ d′_{κ(t_{1}),κ(t_{2})}. Semimorphisms of constraint systems will be often

denoted as α_{κ}. Notice that α(∂_{x}^{t}c) ≤′ ∂_{κ(x)}^{′κ(t)}α(c).

Definition 4.1 Let A and A′ be constraint systems with universes C and C′ and term systems τ and τ′ respectively. A′ is correct with respect to A iff there exists a semimorphism α_{κ} (κ : τ ⟶^{m} τ′ and α : A ⟶^{s} A′) which is a surjective and additive mapping of ⟨C, ≤⟩ into ⟨C′, ≤′⟩.

Additivity and surjectivity allow the semimorphism to associate the “best” approximating constraint in A′ with any concrete constraint in A. As usual, this is captured by the notion of Galois insertion, as specified by the following, where a pair of functions (α, γ) is a Galois insertion of ⟨C′, ≤′⟩ into ⟨C, ≤⟩ iff α and γ are monotonic, α(γ(c′)) = c′ and c ≤ γ(α(c)) for each c ∈ C and c′ ∈ C′ [7, 8]. If A′ is correct with respect to A by means of a semimorphism α_{κ}, there exists a Galois insertion of ⟨C′, ≤′⟩ into ⟨C, ≤⟩.

In the framework of abstract interpretation, correctness of fixpoint approximations require in addition some conditions on correctness of the non-standard semantics operators [7]. With the assumption of additivity, semimorphisms are adequate to specify both Galois insertions, and correctness of constraint systems. Let A′ be a constraint system which 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′ 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 in the obvious way on tuples of terms. The following theorem relates the semantics of a program with the (non-standard) semantics of the corresponding program defined on a correct constraint system. Theorem 4.1 Let P ∈ CLP (A) and P′ ∈ CLP (A′) be the corresponding program on A′. Assume A′ be correct with respect to A. There exists β : ℑ^{A} → ℑ^{A′} such that β(F^{A}(P)) ⊑′ F^{A′}(P′).

Given a (fixpoint) concrete semantics, data-flow analysis usually requires computing the limit of Kleene chains. Convergence to the least fixpoint can either be obtained by forcing the abstract domain to satisfy the ascending chain condition or to use widening and narrowing operators to accelerate convergence for fixpoint approximations, as suggested in [7]. In the following we consider the conditions on the constraint system that ensure the resulting abstract domain to satisfy the ascending chain condition. Definition 4.2 A constraint system A is noetherian iff its universe C does not contain any infinite chain of free-variable bounded constraints^{5}. The free-variable-boundedness condition here is crucial, 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 freevariable-bounded. Given a noetherian constraint system A, the domain ℑ^{A} is noetherian, and F^{A}(P) can be computed by iterating T_{P} a finite number of times.

5A set of constraints {c1, ..., cn, ..} is said to be free-variable bounded iff there exists a finite set of variables Ṽ such that F V (ci) ⊆ Ṽ for each i ≥ 1.

We illustrate this technique by means of a simple example of data-flow analysis for ground dependences in pure logic programs [2, 6].

Consider the (concrete) term system τ_{(Σ,V)} being defined over a finite set of variables V. Let us consider the term system τ_{V} as defined in Example 3.2. Terms are finite sets of variables. Ground terms are denoted with the empty set of variables. It is straightforward to notice that var 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. This domain can be expressed as an instance of our framework using the algebra of propositional formulae with disjunction. Let A_{P rop} = (P rop_{V} , ∧, ∨, true, false, ∃_{X}, ∂_{x}^{t}, ∧(t) ↔ ∧(t′))_{{x},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 var(t) = {x, y, z} and var(t′) = {w, v}; x ∧ y represents a term whose groundness depends upon variables x and y; while x∨y represents a set of terms whose groundness depends upon variables x or y. Local variables are hidden by existential quantification. Since x ↔ true is equivalent to x, a variable x instantiated with ground term is denoted x (i.e. the expression x denotes that x is ground). Substitution is defined in the obvious way. It is easy to prove that, because of the finiteness of V, A_{P rop}/ ↔ is a finite (and then noetherian) constraint system.

The analysis is obtained by associating with each equational constraint in A_{H}, a boolean expression specifying groundness relationships among variables in predicates. The following example shows this technique. Example 4.1 Consider the following program to reverse a list:

   nrev([], []).
   nrev([H|L], R) :- nrev(L, L1), append(L1, [H], R).
   append([], L, L).
   append([H|Y], X2, [H|Z]) :- append(Y, X2, Z).

The corresponding Prop program for groundness analysis is:

nrev(x_{1}, x_{2}) :− x_{1} ∧ x_{2}.

nrev(x_{1}, x_{2}) :− x_{1} ↔ (h ∧ l) □ nrev(l, r1), append(r_{1}, h, r).

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

append(x_{1}, x_{2}, x_{3}) :− x_{1} ↔ (h ∧ y) ∧ x_{3} ↔ (h ∧ z)□append(y, x_{2}, z). The reader may verify that the abstract semantics for append and nrev can be derived by evaluating the modified program in CLP (A_{P rop}) (which corresponds to the standard CLP (Bool)). They are given by:

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

{ nrev(x_{1}, x_{2}) : − x_{1} ↔ x_{2}} . which correspond precisely with the behavious of the program with respect to groundness: in append the third argument is ground iff the first two is ground, while in nrev the first argument is ground iff the second is ground.

4.1 The approximation operator on constraint systems

It is well known that the space of approximate constraints can be specified using upper closure operators ([8]). In the following we introduce the basic properties of upper closure operators on a constraint system. These properties allow the resulting algebraic structure to be a constraint system as well. In particular we characterize the approximation induced when the semimorphism α_{κ} behaves as a morphism of constraint systems. Section 5 discusses weaker conditions that are more useful for abstract interpretation. Following this approach, most of the well known techniques for specifying abstract domains can be extended to constraint systems.

Any upper closure approximation of a constraint system defines a partition of the universe of constraints into convex sets of constraints. 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 4.3 Let A be a constraint system with universe C. An upper closure operator ρ on ⟨C, ≤⟩ is ∃-consistent if for each c ∈ C: ρ(∃_{Δ}c) = ∃_{Δ}ρ(∃_{Δ}c). ∃-consistency for an upper closure operator ensures that the approximation (induced by the operator) of a constraint which is hidden on a set of variables, is still hidden on the same set of variables. From this condition we prove that ρ satisfies the ∂-consistency, the ∃-quasi morphism condition (see Lemma 4.2) and that ρ ∘ ∃_{Δ} is an upper closure operator. Notice that ∃_{Δ} ∘ ρ is not idempotent, unless ∃_{Δ} and ρ commute. This is in accordance with a classical result of closure theory saying that any composition of two upper closure operators is an upper closure operator iff they commute [20]. Lemma 4.2 Let ρ be an ∃-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}ρ(∂_{x}^{t}c); and for each c ∈ C, Δ ⊆ V: ρ(∃_{Δ}c) = ρ(∃_{Δ}ρ(c)). In the remainder of this section we discuss some conditions for systematically deriving abstract constraint systems from a concrete one using closure operators. As we will see, this programme is not applicable to a number of abstract interpretations. This problem is addressed in Section 5. Definition 4.4 Let A be a constraint system with universe C. A consistent upper closure operator ρ 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′)). Since a consistent upper closure operator is a closure operator, it maps each constraint to one that approximates it. 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 joinmorphism, namely for each D ⊆ C, ρ(⨁_{c∈D} c) = ρ(⨁_{c∈D} ρ(c))). It is easy to prove that for consistent upper closure operators, for each c ∈ C, x ∈ V and t ∈ τ such that x ind t: ρ(∂_{x}^{t}c) = ρ(∂_{x}^{t}ρ(c)). Notice that cylindrifications, which are (commuting) upper closure operators, are not consistent as they do not satisfy the ⊗-quasi morphism condition (see Axiom C_{2}).

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

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

where ρ(C) = {c ∈ C | c = ρ(c)}, and for each c_{1}, c_{2} ∈ ρ(C): c_{1} ˜⊗c_{2} = ρ(c_{1} ⊗ c_{2}) and ˜⊕ = λC ⊆ C.ρ(⊕C). Theorem 4.3 Let ρ be a consistent upper closure operator on the constraint system A. ρ(A) is a correct constraint system (wrt A).

As observed in [8], any Galois insertion (α, γ) defines an upper closure operator ρ = γ ∘ α on the corresponding (concrete) complete lattice. In the following we characterize the consistency of upper closures induced by a Galois insertion. Theorem 4.4 Let A and A^{a} be constraint systems with universes C and C^{a} respectively, such that A^{a} is correct with respect to A by means of a surjective and additive morphism α. Let γ = λc^{a}. ⊕ {c | α(c) ≤^{a} c^{a}} and ρ = γ ∘ α. Then: ρ(C) is isomorphic to C^{a} and, if α(∃_{Δ}c) = ∃_{κ(Δ)}^{a}α(∃_{Δ}c) for every Δ ⊆ V and c ∈ C, then ρ is ∃-consistent. Let A be a constraint system and A^{a} be correct with respect to A by means of a surjective and additive semimorphism α_{κ}. Let γ = λc^{a}. ⊕ {c | α(c) ≤^{a} c^{a}} and ρ = γ ∘ α. Theorem 4.5 Let Δ ⊆ V and c, c_{1}, c_{2} ∈ C. If α_{κ} is a morphism on constraint systems then:

(1) ∃_{Δ}ρ(c) = ρ(∃_{Δ}c) and (2) ρ(ρ(c_{1}) ⊗ ρ(c_{2})) = ρ(c_{1} ⊗ c_{2}).

In most of abstract interpretations, the concrete semantics is defined on a constraint system which is ⊗-idempotent and where 1 is the annihilator for ⊕. For this family, any meet of closed constraints is still closed: i.e., ρ(c_{1}) ⊗ ρ(c_{2}) = ρ(ρ(c_{1}) ⊗ ρ(c_{2})) (i.e. any consistent abstraction becomes a ⊗-morphism). This behaviour is too restrictive for most of the abstract interpretations, where the intended meet approximation does not support the ⊗-quasi morphism condition. In the following we will consider ⊗-idempotent and commutative constraint systems where 1 is annihilator for ⊕, as these conditions are satisfied in most of the “concrete” constraint systems (e.g. in CLP (H)). In particular, we show that some properties (the distributivity properties) of constraint systems are affected by non-consistent closure operators.

5 Non-distributive analysis

Assume a constraint system A with universe C, where the axiom of distributivity is replaced by the weaker relation: c ⊗ (⊕C) ≤ ⊕{c ⊗ c′ | c′ ∈ C} for c ∈ C and C ⊆ C (in the remainder of this section we refer to them as non-distributive constraint systems). The axiom of distributivity was introduced to prove the continuity of T_{P}^{A}. However, by monotonicity of ∃ and ⊗, it is easy to prove that T_{P}^{A} is monotone in any non-distributive constraint system A. It follows that for noetherian non-distributive constraint systems, T_{P}^{A} is continuous. Distributivity was also used to prove the equivalence between the fixpoint and operational semantics. 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 fixpoint 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 [18]). 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). We show the applicability of non-distributive constraint systems by means of an example.

Linear relationships analysis The inference of linear size relationships between the arguments of procedures 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 [9, 17, 11, 24]. The approach of Verschaetse and De Schreye 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)}). Substitutions are performed as standard substitutions. It is easy to see τ_{Exp} is a term system and that the mapping Exp_{S} : τ_{(Σ,V)} → τ_{Exp} which associates a linear expression with each terms in τ_{(Σ,V)}:

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

is a morphism.

Example 5.1 With the length and size norms:

|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}),

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

Karr ([17]) shows that linear relationships analysis among variables of programs 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: the universe is a set of affine subspaces K on a fixed n-dimensional space; the meet operation ⊗ is simply intersection of affine subspaces; the join of two affine subspaces A_{1} and A_{2}, given by A_{1} ˆ⊕A_{2}, is the smallest affine subspace containing A_{1} and A_{2} (since the union of two affine subspaces is not, in general, an affine subspace); cylindrification, which corresponds to the variable restriction of Verschaetse and De Schreye, corresponds to “projection” parallel to an axis; and substitution is defined as follows: Let S be an affine subspace and x ∈ V, t ∈ τ_{Exp}, then the substitution of x with t in S is defined as the affine subspace ˆ∃_{{x}}(x = t ∩ S). The elements 0 and 1 are defined as ∅ and the entire space ℜ^{n} (for some sufficiently large n) respectively. 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}}. Diagonal elements are (single) equations on the term system τ_{Exp}. Proposition 5.1 (K, ∩, ˆ⊕, ℜ^{n}, ∅, ˆ∃_{Δ}, ˆ∂_{x}^{t}, [t = t′])_{{x},Δ⊆V_{n};t,t′∈τ_{Exp}} is a non-distributive, ∩-idempo-tent and commutative constraint system, where ℜ^{n} is annihilator for ˆ⊕. As pointed out in [17], there are no infinitely ascending chains of free-variable bounded constraints (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}. The resulting constraint system is therefore noetherian. Example 5.2 Consider the logic program defining the predicate append in Example 4.1, together with the norm length. The corresponding abstract program is:

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). The abstract semantics can be computed in ℜ^{3}:

T_{P}^{K} ↑0(∅) = ∅ T_{P}^{K} ↑1(∅) = {append(x_{1}, x_{2}, x_{3}) :− x_{1} = 0, x_{2} = x_{3}} T_{P}^{K} ↑2(∅) = {append(x_{1}, x_{2}, x_{3}) :− (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. A possible implementation can be obtained by slightly modifying the CLP (R) interpreter in [16] to cope with affine subspaces. 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.

6 Related work

Abstract interpretation of constraint logic programs is considered by Marriott and Søndergaard [19]. 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 data-flow 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 by appropriately modifying the underlying constraint system. In this way, data-flow analyses of logic-based languages can be specified as a standard constraint computation. No difference is introduced between the concrete programming language and the abstract one. They both derive from the same general specification of the CLP paradigm.

A related approach is also considered by Codognet and Filè, who give an algebraic definition of constraint systems and consider abstract interpretation of constraint logic programs [5]. However, the algebraic structure considered by these authors is very different: only ⊗-composition is considered. The notion of “computation system” is introduced but 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, a loop-checker consisting in a “tabled” interpreter is needed. 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 (abstract) constraint system.

Acknowledgments

The stimulating discussions with Roberto Bagnara, Roberto Barbuti, Suzanne Dietrich, Maurizio Gabbrielli, Michael Maher, Nino Salibra, Gert Smolka, and David S. Warren are gratefully acknowledged.

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] R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs. ACM Transactions on Programming Languages and Systems, 15(1):133–181, 1993.

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

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

[5] P. Codognet and G. Filè. Computations, Abstractions and Constraints in Logic Programs. In Proc. Fourth Int. Conf. on Programming Languages, 1992.

[6] 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.

[7] 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.

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

[9] 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.

[10] M. Gabbrielli and G. Levi. Modeling Answer Constraints in Constraint Logic Programs. In K. Furukawa, editor, Proc. Eighth Int’l Conf. on Logic Programming, pages 238– 252. The MIT Press, Cambridge, Mass., 1991.

[11] 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.

[12] 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.

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

[14] 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.

[15] 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.

[16] 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.

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

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

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

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

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

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

[23] 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.

[24] K. Verschaetse and D. De Schreye. Derivation of Linear Size Relations by abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proc. of PLILP’92, volume 631 of Lecture Notes in Computer Science, pages 296–310. Springer-Verlag, Berlin, 1992.