A Generalized Semantics for Constraint Logic Programs ^{∗}

Roberto Giacobazzi^{1}, Saumya K. Debray^{2}, Giorgio Levi^{1}

1) Dipartimento di Informatica

Università di Pisa Corso Italia 40, 56125 Pisa

{giaco,levi}@di.unipi.it 2) Department of Computer Science

The University of Arizona Tucson, AZ 85721 debray@cs.arizona.edu

In FGCS’92 proceedings

Abstract

We present a simple and powerful generalized algebraic semantics for constraint logic programs that is parameterized with respect to the underlying constraint system. “Generalized semantics” abstract away from standard semantics objects, by focusing on the general properties of any (possibly non-standard) semantics definition. In constraint logic programming, this corresponds to a suitable definition of the constraint system supporting the semantics definition. An algebraic structure is introduced to formalize the constraint system notion, thus making applicable classical mathematical results and both a top-down and bottom-up semantics are considered. Non-standard semantics for CLP can then be formally specified by means of the same techniques used to define standard semantics. Different non-standard semantics for constraint logic languages can be specified in this framework: e.g. abstract interpretation, machine level traces and any computation based on an instance of the constraint system.

1 Introduction

Constraint logic programming (CLP) is a generalization of the pure logic programming paradigm, having similar model-theoretic, fixpoint and operational semantics [Jaffar and Lassez 87]. Since the basic operational step in program execution is a test for solvability of constraints in a given algebraic structure, CLP has in addition an algebraic semantics. CLP is then a general paradigm which may be instantiated on various semantic domains, thus achieving a good expressive power. One relevant feature is the distinction between testing for solvability and computing a solution of a given constraint formula. In the logic programming case, this corresponds to the unification process, which tests for solvability by computing a solution (a set of equations in solved form or most general unifier). In CLP, the computation of a solution of a constraint is left to a constraint solver, which does not affect the semantic definition of the language. This allows different computational domains, e.g. real arithmetic, to be considered without requiring complicated encodings of data objects as first order terms. Since the fundamental linguistic aspects of CLP 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 [Saraswat et al. 91]. We refer to such a semantics as generalized semantics. It turns out that 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 of CLP programs: this provides a foundation for dataflow analysis and program manipulation of CLP programs. In this paper we address the problem of defining a generalized semantics for constraint logic programs. This can also be the base to specify non-standard semantics for other logic-based languages (e.g. in [Barbuti et al. 92] Prolog control features are expressed in terms of a constraint logic language). 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 the definition of different non-standard semantics. An interesting aspect of such a development is that non-standard interpretations such as abstract interpretations can be developed entirely within an algebraic framework: for example, the notion of “abstraction” can be characterized simply via additional axioms that specify which terms are to be considered “equal” under the abstract interpretation, and relationships between different abstract interpretations can be characterized in terms of homomorphisms between the corresponding algebras.

∗The work of R. Giacobazzi and G. Levi was supported by “Progetto Finalizzato Sistemi Informatici e Calcolo Parallelo”

of C.N.R. under grant n. 9100880.PF69 and by the Esprit Basic Research Action 3012 - Compulog. The work of S. Debray was supported in part by the National Science Foundation under grant number CCR-8901283.

In this paper, two kinds of generalized semantics top-down and bottom-up, are considered. Since computations are always performed in the algebra of constraints, the two approaches represent just two ways to perform possibly non-standard computations. The reader is assumed to be acquainted with the basic notions of lattice theory and sorted algebras. Full proofs, not included due to space limitations, are present in the full version of this paper.

2 Constraint Algebras

As defined in [Jaffar and Lassez 87], the semantics of constraints is given in terms of an algebraic structure which interprets constraint formulas, while the semantics of a constraint logic program is given in terms of the well known fixpoint, model-theoretic and operational characterizations. In this section we introduce an incremental algebraic specification for constraint systems.

2.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 [Cirulis 88]. We are interested in term systems where every term depends only on a finite number of variables^{1}. They represent the first basic definition in the semantics construction.

Definition 2.1 A term system T is an algebraic structure (T , S, V) where we refer to the elements of T as T -terms (terms in short); V is a countable set of T -variables (variables, for short) in T ; S_{V} is a countable set of binary operations on T , indexed by V; and the following conditions hold, for all x, y ∈ V and t, t′, t′′ ∈ T :

T_{1}. s_{x}(t, x) = t, (identity)

T_{2}. s_{x}(t, y) = y, if x ≠ y, (annihilation)

T_{3}. s_{x}(t, s_{x}(y, t′)) = s_{x}(y, t′) if x ≠ y, (renaming)

T_{4}. s_{x}(t′, s_{y}(t′′, t)) = s_{y}(s_{x}(t′, t′′), t) if x ≠ y and y ind t′ (independent composition)

where a T -term t is independent on the T -variable x, denoted as “x ind t,” if s_{x}(t′, t) = t for every t′ ∈ T . We say that a variable v occurs in a term t if ¬(x ind t).

Intuitively, s_{x}(t, t′) denotes the operation “substitute t for every occurrence of the variable x in t′.” For notational convenience, we denote s_{x}(t, t′) as [t/_{x}] t′. This notation can be extended to substitutions on multiple 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.

Example 2.1 Let Σ be a denumerable collection of function symbols. We denote by τ(Σ, V) the set of possibly non-ground terms defined on Σ. The standard term system T_{(Σ,V)} = (τ(Σ, V), Sub, V) is a term system provided that substitutions in Sub perform idempotent substitutions. In this case v ind t iff the variable v does not occur in t. □

Let Π be a finite collection of predicate symbols. A (T , Π)-atom has the form p(t_{1}, ..., t_{n}) where p ∈ Π and t_{i} ∈ T , ∀i = 1, ..., n. We denote by W_{1}\W_{2} the set W_{1} where the elements in W_{2} have been removed. The powerset of a set S is denoted by 2^{S}, and any tuple of syntactic objects (terms, atoms, etc.) o_{1}, ..., o_{n} is denoted by ⟨o_{1}, ..., o_{n}⟩.

2.2 An Algebraic Framework

We give now a formal algebraic specification for the language of constraints on a given term system.

Definition 2.2 A Closed Semiring [Aho et al. 74] is an algebraic structure (C, ⊗, ⊕, 1, 0), such that: (1) (C, ⊕, 0) is a (join-)idempotent and commutative monoid; (2) (C, ⊗, 1) is a (meet-)monoid; (3) 0 is an annihilator for ⊗; (4) if a_{1}, ..., a_{n}, .. is a countable sequence of elements in C, a_{1} ⊕a_{2} ⊕...⊕a_{n} ⊕.. exists and is unique; (5) associativity, commutativity and idempotence of ⊕ apply to infinite as well as finite joins; and (6) ⊗ distributes over finite and counably infinite joins.

Example 2.2 [[Aho et al. 74]] Let A_{ℜ} = (ℜ^{+}, +, min, 0, +∞) where ℜ^{+} is the set of non-negative reals including +∞, and A_{Σ} = (Σ^{∗}, ·, ∪, {ϵ}, ∅) where Σ^{∗} is the family of sets of finite-length strings of symbols from the finite alphabet Σ (including the empty string ϵ) and · denotes concatenation. Both A_{ℜ} and A_{Σ} are closed semirings. Notice that in A_{Σ} · is not commutative. □

Any semantics definition supports the notion of observable behaviour for a given program. Modelling answer constraints in constraint logic programming corresponds to consider answer constraints as the observable property for any CLP program. 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, as in [Saraswat et al. 91]. Cylindric algebras [Henkin et al. 85] provide a suitable framework to enhance our algebraic structures. A cylindric algebra is formed by enhancing a Boolean algebra by means of a family of unary operations called cylindrifications. 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. They are necessary here because when we solve a goal in a constraint logic program, we are interested only in constraints on the variables that appear in that goal: thus, any additional constraints that may have been imposed on other variables during the course of the computations should be projected away in the representation of the final answer constraint. This is accomplished using cylindrification. 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. The machinery of cylindric algebras is not quite adequate for this, but the problem can be handled using polyadic algebras [Henkin et al. 85], which allow possibly countably many cylindrifications.

1A more general definition that considers sets of arbitrary cardinalities is given in [Cirulis 88]: for our purposes, it suffices to consider denumerable sets.

Diagonal elements [Henkin et al. 85] are considered as a way to provide parameter passing [Saraswat et al. 91]. In constraint logic programming the equality symbol “=” is assumed in any constraint system to provide term unification. However, cylindric algebras were introduced to provide an algebraic formalization of first-order-logic, actually oriented to first-order-languages without operation symbols; thus ignoring all terms but variables. This framework is not adequate to provide an algebraic semantic framework for constraint logic programs. We extend diagonal elements to deal with generic terms, following the approach in [Cirulis 88]. Diagonal elements represent equations on a given term system T . This approach results in introducing “term-unification” (i.e. equations on terms) as distinguished elements in the algebra.

Definition 2.3 A cylindric closed semiring is an algebraic structure (C, ⊗, ⊕, 1, 0, ∃_{Δ}, d_{t,t′})_{Δ⊆V;t,t′∈T} where C is a set called the universe of semiring, V is a countable set of variables, T is a term system; 0, 1, d_{t,t′} are distinct elements of C, for each t, t′ ∈ T ; {∃_{Δ}}_{Δ⊆V} are unary operations on C; ⊗, ⊕ are binary operations on C; such that the following postulates are satisfied for any c, c′ ∈ C; Δ, Ψ ⊆ V and t, t′ ∈ T :

S_{1}. the structure (C, ⊗, ⊕, 1, 0) is a closed semiring,

C_{1}. ∃_{Δ}0 = 0, C_{2}. c ⊕ ∃_{Δ}c = ∃_{Δ}c,

C_{3}. ∃_{Δ}(c ⊗ ∃_{Δ}c′) = ∃_{Δ}c ⊗ ∃_{Δ}c′,

C_{4}. ∃_{Δ}∃_{Ψ}c = ∃_{(Δ∪Ψ)}c,

C_{5}. ∃_{Δ} distributes over finite and countably infinite joins,

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

D_{2}. d_{t,t′} = ∃_{{x}}(d_{t,x} ⊗ d_{x,t′}) where x ind t, t′,

D_{3}. d_{z,[t/_{x}]t′} = ∃_{{x}}(d_{z,t′} ⊗ d_{x,t}), where z ≠ x and x ind t, z ind t′.

Notice that Axiom D_{3} relates the notion of substitution in the term system T with diagonal elements of C (which intuitively correspond to the notion of equality constraints) in the expected way.

The notions of “independence” and “occurrence” of variables extends in the obvious way from terms in T to constraints in 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 also denote as 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} ∈ T . Any closed semiring can be extended to a cylindric closed semiring by letting d_{t,t′} = 1 for each t, t′ ∈ T and ∃_{Δ}c = c for each c ∈ C and Δ ⊆ μ. Following [Henkin et al. 85] we refer to them as discrete cylindric closed semirings.

In the general theory of cylindric algebras, the commutative and transitive properties of diagonal elements (i.e. d_{t,t′} = d_{t′,t} and (d_{t,t′}⊗d_{t′,t′′})⊕d_{t,t′′} = d_{t,t′′}) are derived by the axioms. Because of the weakness of cylindric closed semirings, these properties are not derivable from the axioms. However they are not required in proving the semantic results given below. They can be added to provide the theory of equality.

Given a closed semiring, we can induce a partial ordering relation ⊑_{⊕} on C, such that c_{1} ⊑_{⊕} c_{2} iff c_{1} ⊕ c_{2} = c_{2}. As a consequence, (C, ⊑_{⊕}) is a complete lattice.

2.3 Constraint Systems

In this section we formalize the notion of constraint system, based on the above algebraic framework.

Definition 2.4 A constraint interpretation structure is any cylindric closed semiring. Given a constraint interpretation structure A with universe C, an Aconstraint (constraint for short) is any element in C.

Idempotence, associativity and commutativity are the least set of properties [Barbuti et al. 91,Debray and Ramakrishnan 91] which allow ⊕ to model the set union operation. ⊗ corresponds to the constraint conjunction and plays the important role of collecting the information during the computation. Distributivity allows to represent constraints as possibly infinite joins of finite meets (also called simple constraints). Closure on (possibly infinite) countable elements in C allows to denote infinite joins of constraints.

Example 2.3 Let us assume that Π = Π_{C} ∪ Π_{P} and Π_{C} ∩ Π_{P} = ∅. We refer to Λ_{(Σ,Π_{C})} as the free algebra of formulas in the sorted vocabulary (S, Σ, Π_{C}): where S (sort) is a set of symbols, Σ a specified set of operations with a corresponding signature on S and Π_{C} a set of predicate symbols with a signature on S; enhanced with the disjunction symbol ∨, the conjunction symbol ∧, the existential quantifier ∃, the identity symbol =, the truth and falsehood symbols T and F and closed under countably infinite disjunctions of formulas in Λ_{(Σ,Π_{C})}. Equations and possibly existentially quantified (T_{(Σ,V)}, Π_{C})-atoms are called atomic constraints.

Let us consider the solution compact many sorted algebraic structure R_{(Σ,Π_{C})} [Jaffar and Lassez 87], defined over the many sorted alphabet (S, Σ, Π_{C}), consisting of: a collection DR of non-empty sets denoted {DR_{s}}_{s}, where s ∈ S; an assignment of a function DR_{s_{1}} × ... × DR_{s_{n}} → DR_{s} to each n-ary function symbol f ∈ Σ, where (s_{1}, ..., s_{n}, s) is the signature of f; an assignment of a function DR_{s_{1}} × ... × DR_{s_{n}} → {true, false} to each n-ary predicate symbol p ∈ Π_{C}, where (s_{1}, ..., s_{n}) is the signature of p.

Let us consider a constraint c in Λ_{(Σ,Π_{C})}. R ⊧ c, iff there exists a mapping ϑ (the solution of the constraint) from each distinct free variable x in c into Dℜ_{s}, (free variables in a constraint c are denoted F V (c)) where s is the sort associated with x, and cϑ is R-equivalent to T (R ⊧ cϑ).

Let c_{1} = ∨_{i∈I_{1}} c′_{i} and c_{2} = ∨_{i∈I_{2}} c′′_{i} denote possibly infi-

nite disjunctions of conjunctions of atomic constraints c′_{i} and c′′_{i}, where i ranges over I_{1} and I_{2} being sets of possibly infinite indexes. The equivalence relation ≈_{R} on Λ_{(Σ,Π_{C})} is defined as follows

c_{1} ≈_{R} c_{2} iff ∪_{i∈I_{1}} {ϑ | R ⊧ c′_{i}ϑ} = ∪_{i∈I_{2}} {ϑ | R ⊧ c′′_{i}ϑ}.

≈_{R} is a congruence relation on the one sorted algebra (Λ_{(Σ,Π_{C})}, ∧, ∨, T, F, ∃_{X}, t = t′)_{X⊆V;t,t′∈T_{(Σ,V )}}. The standard constraint interpretation structure is then given by the quotient algebra, denoted as A_{st} = (Λ_{(Σ,Π_{C})}, ∧, ∨, T, F, ∃_{X}, t = t′)_{X⊆V;t,t′∈T_{(Σ,V )}}/_{≈_{R}}. It is trivially a meet-idempotent and commutative cylindric closed semiring. □

Example 2.4 [CLP (H)] Let us consider the following signature associated with the usual Herbrand universe definition, Σ = {a, b, ..., f, g, ...}. Atomic constraints are one sorted equations on the term system T_{(Σ,V)}. The corresponding Herbrand interpretation structure A_{H}, is the quotient algebra (C_{H}, ∧, ∨, T, F, ∃_{X}, t = t′)_{X⊆V;t,t′∈T_{(Σ,V )}}/_{≈_{EQ}}, modulo ≈_{EQ}, where C_{H} = { t = t′ | t, t′ ∈ T_{(Σ,V)} } and ≈_{EQ} is the equivalence relation induced by the algebraic structure interpreting diagonal elements as unification [Jaffar and Lassez 87]. It is straightforward to prove that this corresponds to the pure logic programming case. □

To relate constraint interpretation structures, we follow the approach to “static semantics correctness” in [Barbuti and Martelli 83]. Correctness of nonstandard semantics 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 involved algebras be partially ordered sets. We introduce a weaker notion of morphism, capturing the approximation possibly induced by abstract interpretations or any approximate semantics defined in the framework.

Definition 2.5 Let A_{Σ} and B_{Σ} be (many sorted) algebraic structures over the sorted alphabet (S, Σ). Let us assume that for each s ∈ S, (DB_{s}, ⪯_{DB_{s}}) is a partially ordered set. A weak morphism σ : A → B is a family of functions σ_{s} : DA_{s} → DB_{s}, for s ∈ S, such that: σ_{s}(f_{A}) ⪯_{DB_{s}} f_{B}, for each constant symbol f :→ s in Σ and σ_{s}(f_{A}(a_{1}, ..., a_{n})) ⪯_{DB_{s}} f_{B}(σ_{s_{1}}(a_{1}), ..., σ_{s_{n}}(a_{n})), for each operation symbol f : s_{1}...s_{n} → s in Σ.

Definition 2.6 Let A be a constraint interpretation structure. A constraint interpretation morphism is a weak morphism ε from (Λ_{(Σ,Π_{C})}, ∧, ∨, T, F, ∃_{X}, t = t′)_{X⊆V;t,t′∈T_{(Σ,V )}} in A.

Example 2.5 The standard constraint interpretation morphism ε_{st} is a morphism which associates with any formula in Λ_{(Σ,Π_{C})}, the corresponding equivalence class modulo ≈_{R}. □

In general, a constraint system is an interpretation (in a closed semiring) for constraint formulas.

Definition 2.7 A constraint system is a pair Γ = ⟨A, ε⟩ where A is a constraint interpretation structure and ε is a corresponding constraint interpretation morphism.

Similar algebraic structures for the definition of constraint systems have been introduced in [Saraswat et al. 91] to specify the semantics of the more complex class of concurrent constraint languages characterized by the ask/tell paradigm.

Constraint systems are specified as systems of partial information in the style of Scott’s information systems [Scott 82], (simple constraint systems), which are tuples (C, Δ, ⊢), where C is an non-empty set of “primitive” constraints and ⊢⊆ 2^{C} × C is an entailment relation such that ∀u, v ∈ 2^{C}: (1) u ⊢ Δ, (2) u ⊢ X whenever X ∈ u and (3) if v ⊢ Y for all Y ∈ u and u ⊢ X, then v ⊢ X. The relation ⊢ can be extended on 2^{C} × 2^{C} as follows: ∀u, v ∈ 2^{C}, u ⊢ v iff u ⊢ X for every X ∈ v.

Composition of constraints is defined in terms of set-union, which is a well known commutative and idempotent operator. Hiding and parameter passing are handled by cylindrification (only finite-variable cylindrifications are allowed) and diagonal elements. The difference is then in the underlying algebraic structure: while information systems provide an elegant framework to develop the (standard) semantics for concurrent constraint languages, we are interested in more appropriate algebraic structures to generalize standard semantics results on CLP. In our case, the constraint system is parametric with respect to a given term system. This introduces a more structured approach (two steps) to non-standard constraint system definition (e.g. abstract interpretation). As for the basic algebraic structure, the choice of closed semirings results more natural in the context of the present paper. We are interested in possibly non-commutative/idempotent compositions (meets) of constraints (see A_{Σ} in Example 2.2). Moreover (see Prop in Section 4.1 below) standard logical and arithmetic operators (e.g. ∨, ∧, T and F) can be specified more naturally as an instance of a closed semiring instead of as an instance of an information system. Nevertheless, it is easy to associate an information system with any ⊗-commutative and idempotent closed semiring. Let (C, ⊗, ⊕, 1, 0) be a ⊗-commutative and idempotent closed semiring. The corresponding information system (C, Δ, ⊢) is defined as follows Δ = 0 and ∀u, v ∈ 2^{C}: u ⊢ v iff v ⊑_{⊕} u.

The key difference is in the semantics definition. In [Saraswat et al. 91] the semantics of constraint languages is specified as closures on the constraint system, thus amalgamating the semantics construction and data-objects. We follow the standard approach (see section below) in generalizing the standard operational and fixpoint semantics characterizations, already known in logic programming. A more structured approach to the generalization process can be obtained by separating the domain of constraints with the various techniques to construct models (e.g. fixpoints of continuous transformations) for constraint logic programs. The independence of the semantics constructions from the underying constraint systems focuses the generalization process on the constraint system definition, thus simplifying the specification of non-standard semantics.

Generalized constraint logic programs are defined in the usual way. Let A be a constraint interpretation structure on the term system T . An A-clause is a formula of the form H :− c□B_{1}, ..., B_{n} with n ≥ 0 where H (the head) and B_{1}, ..., B_{n} (the body) are (T , Π_{P})-atoms, c is an A-constraint and :− and “,” denote logic implication and conjunction respectively. An A-goal is a formula c□B_{1}, ..., B_{n}, where c is constraint and each B_{i} is (T , Π_{P})-atom. A (generalized) constraint logic program, also called A-program is a finite set of A-clauses.

3 Generalized Semantics

The mechanism introduced in [Falaschi et al. 89] to model computed answer substitutions is generalized in CLP, by allowing constrained atoms into the base of interpretations [Gabbrielli and Levi 91]. Each constrained atom p(x̄) :− c, in fact, represents the set of instances p(x̄)ϑ, where ϑ is a solution of the constraint c.

Definition 3.1 Let A be an interpretation structure. A constrained atom has the form p(x̄) :− c where c is an A-constraint, p(x̄) is a (T , Π_{P})-atom and F V (c) = x̄.

Definition 3.2 Let A be an interpretation structure and ℑ be the corresponding set of constrained atoms. We define a partial order ⪯ on ℑ such that p(x̄_{1}) :− c_{1} ⪯ p(x̄_{2}) :− c_{2} iff there exists x̄′ such that ∃_{{x̄_{1}}}(d_{x̄′,x̄_{1}} ⊗ c_{1}) ⊑_{⊕} c_{2}.

The equivalence relation induced by the partial order ⪯ is denoted by ∼. The A-base of interpretations B, is ℑ/_{∼}.

Definition 3.3 Ξ ⊆ 2^{B} is the collection of sets of constrained atoms I such that I ∈ Ξ iff I ⨄ ∅ = ∅ ⨄ I = I, where ⨄ is defined as:

λI_{1}, I_{2}. \{ p(x̄) :− ∑_{j} c̃_{j} | \begin{matrix}p(x̄_{j}) :− c_{j} ∈ I_{1} ∪ I_{2}, \\ c̃_{j} = ∃x̄_{j}(d_{x̄,x̄_{j}} ⊗ c_{j}) \\ and x̄ ind c_{j} \end{matrix} \}.

An A-interpretation is any element of Ξ. ⨄ is strongly related to ⊕. As usual we define I_{1} ⊑_{⊎} I_{2} iff I_{1} ⨄ I_{2} = I_{2} such that (Ξ, ⊑_{⊎}) is a complete lattice. Each interpretation always consists of a finite set of constrained atoms, containing at most one constrained atom for each program predicate symbol: p(x̄) :− ∑_{j∈W} c_{j} ∈ I, where for each j ∈ W, c_{j} represents the set of admissible (i.e. computable in the program) solutions for the predicate symbol p, on the variables x̄. As a consequence infinite joins of constraints are allowed in constrained atoms. This is well defined by the closure of C. In the following we will often omit A in specifying programs, goals, etc.

3.1 Operational Semantics

Let Γ = ⟨A, ε⟩ be a constraint system and P be an A-program. Define ⇝_{P} ⊆ A-Goals × A-Goals (an A-derivation step) to be the smallest relation such that G^{A} ⇝_{P} G^{′A} iff G^{A} = c_{0}□p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}); there exist n (renamed apart) versions of clauses in P: p_{i}(x̄_{i}) :− c_{i}□Ḡ_{i}, i = 1..n; G^{′A} = c_{0} ⊗ c̃_{1} ⊗ ... ⊗ c̃_{n}□Ḡ_{1}, ..., Ḡ_{n}, where for each i = 1..n, c̃_{i} = d_{x̄_{i},t̄_{i}} ⊗c_{i}.

An A-derivation from an A-goal G^{A} is a finite or infinite sequence of (different) A-goals such that every A-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 operational semantics is then defined in terms of the successful computations specified by the transitive closure of the transition relation on A-goals:

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

Goal dependent semantics is defined in terms of a function G that yields the computed answer constraint for any A-goal, such that

G(G^{A}) = ∃(c)_{var(G^{A})} iff G^{A} ⇝_{P}^{∗} c□ .

Theorem 3.1 Let G^{A} = c_{0}□p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) be a goal. G(G^{A}) = c iff there exist p_{i}(x̄_{i}) :− c_{i} ∈ O^{Γ}(P), for i = 1, ..., n and c = ∃(c_{0} ⊗ d_{x̄_{1},t̄_{1}} ⊗ c_{i}... ⊗ d_{x̄_{n},t̄_{n}} ⊗ c_{n})_{var(G^{A})}.

3.2 Fixpoint Semantics

In this section we define a fixpoint semantics which is proved to be equivalent to the operational semantics.

Definition 3.4 Let P be an A-program, the mapping T_{P}^{A} : Ξ → Ξ, is defined as follows T_{P}^{A}(I) = ⨄_{C∈P}

T_{C}^{A}(I) where if C : p(t) :− c□p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) then

T_{C}^{A}(I) = \{ p(x̄) : −∃(c̃)x̄ | \begin{matrix}for each i = 1...n : \\ p_{i}(x̄_{i}) : −c_{i} ∈ I \\ c′_{i} = d_{x̄_{i},t̄_{i}} ⊗ c_{i} \\ c̃ = d_{x̄,t̄} ⊗ c ⊗ c′_{1}.. ⊗ ..c′_{n} \\ x̄ ind c, c′_{1}, ..., c′_{n} \end{matrix} \}

T_{P}^{A} is a continuous function on the complete lattice (Ξ, ⊑_{⊎}). Let lfp(f) denote the least fixpoint of a function f and F^{Γ}(P) = lfp(T_{P}^{A}) = T_{P}^{A} ↑ ω. The following result states the equivalence between the operational and the fixpoint semantics, for any constraint system Γ.

Theorem 3.2 Let P be a program and Γ a constraint system. Then F^{Γ}(P) = O^{Γ}(P).

4 Abstract Interpretation of CLP

The definition of an abstract constraint system is performed in two steps: term abstraction and constraint abstraction. In the first step new syntactic objects are introduced to represent sets of concrete terms. In the second one, constraints on the abstracted term system are abstracted. Since the complete lattice of interpretations is induced by the closed semiring structure, any abstract interpretation will correspond to a suitable definition of a constraint system associated with a particular application.

Definition 4.1 Given a constraint system Γ = ⟨A, ε⟩, a constraint system Γ′ = ⟨A′, ε′⟩, is correct with respect to Γ iff there exists a weak algebraic morphism α_{c} (α_{c} : A → A′) which is a monotonic mapping of (C, ⊑_{⊕}) into (C′, ⊑_{⊕′}).

Notice that, since α_{c} is monotonic, it behaves as an algebraic morphism with respect to the ⊕ operator. Termination has been guaranteed by requiring that all chains be finite.

Definition 4.2 A constraint interpretation structure A is Noetherian iff (C, ⊑_{⊕}) does not contain any infinite chain. A constraint system ⟨A, ε⟩ is Noetherian iff A is Noetherian.

Given a Noetherian constraint system Γ, it is easy to prove that (Ξ, ⊑_{⊎}) is Noetherian. An abstract constraint system is a Noetherian constraint system Γ^{♯} which is correct with respect to the standard one Γ_{st}. It is straightforward to show that in any abstract constraint system ⟨A^{♯}, ε^{♯}⟩, ε^{♯} = α_{c} ∘ ε_{st}. Moreover, by weakness and monotonicity, the composition of two monotonic weak morphisms is still a monotonic weak morphism. Let Γ^{♯} be a correct abstract constraint system. The mapping α : Ξ → Ξ^{♯} such that α(I) = { p(x) :− α_{c}(c) | p(x) :− c ∈ I } is continuous. Abstract interpretations for constraint logic programs correspond to the definition of an abstract constraint system together with a program evaluation strategy. The first defines what an abstract computation is, while the second one deals with a specific evaluation strategy to collect abstract information. Top-down abstract interpretations correspond to the abstraction of the operational semantics. Bottomup evaluations instead allow to compute a finite abstract approximation of the fixpoint semantics associated with a given constraint logic program. Goalindependence is an attractive feature of bottom-up evaluations. Global program analysis, especially useful in type inference, can then be specified as a bottomup evaluation in a suitable constraint system.

Proposition 4.1 Given a program P and an abstract constraint system Γ^{♯} = ⟨A^{♯}, ε^{♯}⟩, there exists a finite positive k such that F^{Γ^{♯}}(P) = T_{P}^{A^{♯}} ↑ k.

The correctness of the analysis is reduced to the correctness of the constraint system.

Theorem 4.2 Let P and Γ^{♯} be a program and an abstract constraint system respectively. Then α(O^{Γ}(P)) ⊑_{⊎}^{♯} O^{Γ^{♯}}(P) and α(F^{Γ}(P)) ⊑_{⊎}^{♯} F^{Γ^{♯}}(P).

Example 4.1 The closed semiring A_{ℜ} developed in Example 2.2 can be used to define a simple complexity analysis tool for constraint logic programs on reals, CLP (ℜ) [Jaffar and Lassez 87]. Let |.|_{τ} : τ(Σ, V) → N be a mapping associating a “weight” with any term, where N is the set of natural numbers. Let us consider a morphism ε such that for each constraint c : t_{1} < t_{2}, ε(c) = |t_{1}|_{τ} + |t_{2}|_{τ}.

The interpretation structure (N , +, min, 0, +∞), where cylindrifications are defined as in the discrete case and diagonal elements are natural numbers d_{t_{1},t_{2}} = |t_{1}|_{τ} + |t_{2}|_{τ}, is trivially Noetherian. A lowerbound complexity analysis can be performed returning a lower bound estimation of the costs in arithmetic computations, as in the following example for a simple integration routine:

int(A, B, x) :− 0 < B − A ≤ ϵ,

x = (B − A) ∗ f(A + (B − A)/2)□ E(ϵ). int(A, B, x) :− B − A > ϵ,

M = A + (B − A)/2, x = x_{1} + x_{2} □ int(A, M, x_{1}), int(M, B, x_{2}), E(ϵ).

E(x) :− x = 1/n□N(n). N(n′) :− n′ = n + 1□N(n). N(n′) :− n′ = 1□.

Let, for instance, c_{+}, c_{∗} and c_{f} be the costs of addition, multiplication/division and f respectively. Variables and constants have a zero cost. Thus, denoting Γ_{τ} such constraint system:

F^{Γ_{τ}} (P) = \{ \begin{matrix}int(A, B, x) :− 4c_{+} + 3c_{∗} + c_{f}, \\ E(n′) :− c_{∗}, \\ N(n′) :− 0 \end{matrix} \} .

□

A space of approximate constraints can be specified by defining an auto-weak morphism ρ which is an upper closure operator (i.e. an idempotent, monotonic and extensive operator) on (C, ⊑_{⊕}). As shown in [Cousot and Cousot 79] the approximation process essentially consists in partitioning the space of constraints so that no distinction is made between equivalent constraints, all approximated by a representant of their equivalence class. The equivalence relation is induced by an upper closure operator ρ: c_{1} ≡_{ρ} c_{2} iff ρ(c_{1}) = ρ(c_{2}). In [Cousot and Cousot 79] different equivalent methods for specifying abstract domains (i.e. upper closure operators) are presented. However, there are standard techniques in algebraic specifications that allow the definition of abstract constraint systems. For example, cylindrifications can be interpreted as abstractions on the algebra of constraints.

Proposition 4.3 Let Δ ⊆ V; ∃_{Δ} is an auto-weak morphism and upper closure operator on (C, ⊑_{⊕}).

Existential quantification is then a way to define abstract domains. The space of approximate constraints can also be specified by adding axioms to the underlying constraint system A. These additional axioms extend the meaning of the diagonal elements d_{t,t′} of the algebra, in effect specifying which objects are to be considered “equivalent” from the perspective of the analysis. This is illustrated by the following example:

Example 4.2 Consider the logic program P

p(0).
p(s(x)) :− q(x).
q(s(x)) :− p(x).

and a simple type (parity) analysis for P. Interpreting P as a constraint logic program on the Herbrand constraint system A_{H}, the type analysis can be specified by extending the axioms specifying the constraint system with the additional axiom: s(s(x)) = x. The resulting constraint system, denoted by A_{H}^{ex}, is trivially Noetherian. The semantics of P in A_{H} is

{p(x) :− x = 0 ∨_{n≥1} x = s^{2n}(0); q(x) :− ∨_{n≥1} x =

s^{2n−1}(0)}; whereas the interpretation in A_{H}^{ex} returns {p(x) :− x = 0; q(x) :− x = s(0)}. The meaning of P in A_{H}^{ex} captures the type of the predicate p and q, computing even and odd numbers respectively. □

A very useful analysis on the relationships among variables of a program can be specified in our framework [Cousot and Halbwachs 78]. The automatic derivation technique in [Verschaetse and De Schreye 91] for linear size relations among variables in logic programs can be suitably specified as a constraint computation. A constraint system of affine relationships (i.e. linear equalities of the form c_{0} = c_{1}X_{1} + ... + c_{n}X_{n}) can be defined by specifying intersection, disjunction and cylindrification (restriction) as given in [Verschaetse and De Schreye 91]. Generalizations considering linear inequalities, as proposed in [Cousot and Halbwachs 78], can still be defined in our framework, thus making explicit the strong connection between automatic detection of linear relationships among variables and CLP (ℜ) computations. Applications of this analysis are: compile time overflow, mutual exclusion, constraint propagation, termination etc. [Jørgensen et al. 91].

4.1 Generalized Rigidity Analysis

There exists a wide class of abstract interpretation techniques for the analysis of ground dependences (also named covering) of pure logic programs [Barbuti et al. 91, Cortesi et al. 91]. In this section we extend the ground dependence notion by means of the notion of rigidity.

A norm is a function weighting terms. Let us recall some basic concepts about norms. For a more accurate treatment on this subject see [Bossi et al. 90].

Definition 4.3 Let T ba a term system. A norm on T is a function |..|_{ζ} : T → N, mapping any term t ∈ T into a natural number.

Example 4.3 The following weighting map is a norm on the Herbrand term system: |t|_{size} = 0 if t is a variable or t = [], |t|_{size} = 1 + |tail|_{size} if t = [h|tail]. □

In order to extend the notion of groundness and ground dependences [Barbuti et al. 91, Cortesi et al. 91] to deal with a more refined one, able to take into account only the relevant subterms of a given (possibly non-ground) term t, we address the notion of rigidity as introduced in [Bossi et al. 90].

Definition 4.4 Let |..|_{ζ} be a norm on the term system T . A term t ∈ T is rigid with respect to |..|_{ζ} iff for any substitution of variables σ: |σt|_{ζ} = |t|_{ζ}.

The rigidity of terms turns out to be important in simplifying termination proofs. If a term is rigid, its weight will not be modified by further substitutions. Rigidity is then strongly related to groundness. Any ground term can not change its weight by instantiation, thus it is always rigid. This notion allows to identify those subterms which are relevant for the analysis purposes. Notice that given a norm |..|_{ζ}, and a nonrigid term t ∈ T , there must exist some variable in t whose instantiation affects the weight of t. In the Herbrand case, results in [Bossi et al. 90] allow to restrict our attention to a particular class of norms: semilinear norms on Herbrand.

Definition 4.5 A norm on T_{(Σ,V)} is semilinear iff it may be defined according to the following structure: |t|_{ζ} = 0 if t is a variable; |t|_{ζ} = c_{0} + |t_{i_{1}}|_{ζ} + ... + |t_{i_{m}}|_{ζ} if t = f(t_{1}, ..., t_{n}), where c_{0} ≥ 0 and {i_{1}, ..., i_{m}} ⊆ {1, ..., n}.

Note that the position of the subterms which allow the principal term to change its weight by instantiation depends on the outermost term constructor only (i.e. f). These subterms are then relevant from the analysis viewpoint. All the non-relevant subterms are discarded by the analysis. Semilinear norms allow to reduce the rigidity notion to a syntactical property of terms. Let

V rel_{ζ}(t) = { v ∈ V | ∃ σ such that |σt|_{ζ} ≠ |t|_{ζ} } .

As shown in [Bossi et al. 90], given a semilinear norm |..|_{ζ}, a term t ∈ T_{(Σ,V)} is rigid iff V rel_{ζ}(t) = ∅. The notion of semilinear norms can be generalized to arbitrary term systems in a straightforward way, as follows: given a term system T , we define a function w : T ⟶ N; for each t ∈ T , an associated finite set of functions F_{t} : t ⟶ T ; and an associative and commutative function ⋈: N × N ⟶ N.

Intuitively, for any term t, the value of w(t) is the “initial weight” of the term t, the set of functions F_{t} correspond to the set of selectors for the “relevant” subterms, and ⋈ indicates how the sizes of the subterms of a term are to be combined. Then, generalized semilinear norms can be defined as follows:

|t| = w(t)+ ⋈_{f∈F_{t}} |f(t)|.

Example 4.4 The “usual” notion of semilinear norms for Herbrand constraint systems can now be generalized as follows, let c_{0} ∈ N: w(t) = 0 if t is a variable, c_{0} otherwise; if t is a variable then F_{t} = ∅; otherwise F_{t} consists of selectors for the relevant positions of t; ⋈ is summation.

The “depth norm”, which could not be expressed as a semilinear norm in the development of [Bossi et al. 90], can be defined as follows: w(t) = 0 if t is a variable, 1 otherwise; if t is a variable then F_{t} = ∅; otherwise if t = f(t_{1}, …, t_{n}) then F_{t} = {f_{i}|1 ≤ i ≤ n}, where f_{i}(t) = t_{i}, i.e. f_{i} is the selector for the subterm at the i^{th} position; and ⋈ is max. □

Let us consider the set C(V) of finite conjunctions of variables in V (the empty conjunction is denoted ϵ) and a term abstraction map α_{T} : T → C(V) such that, given a semilinear norm |..|_{ζ} and t ∈ T , α_{T} (t) = { x_{1} ∧ ... ∧ x_{m} | V rel_{ζ}(t) = {x_{1}, ..., x_{m}} }. Let T_{ζ} be the corresponding abstract term system where substitutions are performed as usual. Marriott and Søndergaard have proposed an elegant domain, named Prop, further studied in [Cortesi et al. 91], to represent ground dependences among arguments in atoms. In [Codognet and Filè 91] an interesting application is introduced. Prop is formalized as a constraint system, and both groundness and definiteness analysis are specified by executing programs in CLP(Bool). The corresponding constraint system does not allow disjunctions of varables, without fully exploiting the expressive power of Prop. The general notion of ground dependence corresponding with any Prop formula (including disjunctions) cannot be specified.

Let A_{ζ} = (P rop_{ζ}, ∨, ∧, T, F, ∃_{X}, t ↔ t′)_{X⊆V;t,t′∈T_{ζ}} be the algebra of possibly existentially quantified formulas defined on the term system T_{ζ}; including the set of connectives ∨, ∧, ↔. Intuitively, the formula x ∧ y ∧ z ↔ w ∧ v represents an equation t = t′ where V rel_{ζ}(t) = {x, y, z} and V rel_{ζ}(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 [Codognet and Filè 91].

Let Bool be a boolean algebraic structure; c ≈_{Bool} c′ iff Bool ⊧ c ↔ c′. It is easy to prove that A_{ζ}/_{≈_{Bool}} is an abstract constraint system.

Example 4.5 Let us consider the semilinear norm “size” and the following constraint logic program on the Herbrand constraint system

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 corresponding abstract model is: {append(x_{1}, x_{2}, x_{3}) :− x_{1} ↔ ϵ ∧ x_{2} ↔ x_{3}}, generalizing the standard ground behavior (where V rel(t) = var(t): and the abstract model is {append(x_{1}, x_{2}, x_{3}) :− x_{3} ↔ x_{1} ∧ x_{2}}) vs. sizerigidity behavior: “the second argument list-size can change iff the third argument does”. □

5 Machine-level Traces

In this section, we consider an example non-standard semantics for constraint logic programs, that of machine-level traces (for a discussion of similar nonstandard semantics in a denotational context, see [Stoy 77]). Such a semantics is essential, for example, if we wish to reason formally about the correctness of a compiler (e.g. see [Hanus 88]) or the behavior of a debugger or profiler. In this section, we show how the semantics described in earlier sections may be instantiated to describe such low-level behaviors. Instead of constrained atoms where each atom is associated with a constraint, this semantics will associate each atom with a set of machine states (equivalently, instruction sequences) that may be generated on an execution of that atom.

The code generated by a compiler for a constraint language must necessarily depend on both the constraint system and the target machine under consideration. Suppose that each “primitive” constraint op(t_{1}, …, t_{n}) in the language under consideration corresponds to (an instance of) a (virtual) machine instruction op(t_{1}, …, t_{n}).^{2} For example, corresponding to a constraint ‘X = Y +5’ in the language under consideration, we might have a virtual machine instruction ‘eq(X, Y + 5)’. Each such machine instruction defines a transformation on machine states, representing the changes that are performed to the heap, stack, registers, etc. of the machine by the execution of that instruction (e.g., see [Hanus 88] for a discussion of the WAM along these lines). In other words, let S be the set of all possible states of the machine under consideration, then an instruction I denotes a function I : S ⟶ S ∪ {fail}, where fail denotes a state where execution has failed.

Given a set S, let S^{∞} denote the set of finite and infinite sequences of S. Intuitively, with each execution we want to associate a set of finite and infinite sequences of machine states, that might be generated by an OR-parallel interpreter. Thus, we want the universe of our algebra to be 2^{S^{∞}}, the set of sets of finite and infinite sequences of machine states. One subtlety, however, is that instructions may “fail” at runtime because some constraints may be unsatisfiable. To model this, it is necessary to handle failure explicitly, since “forward” execution cannot continue on failure. To deal with this, we define the notion of concatenation of sequences of machine states as follows: given any two sequences s_{1} and s_{2} of states in S ∪ {fail}, their concatenation s_{1} ⊙ s_{2} is given by s_{1} ⊙ s_{2} = if s_{1} contains fail then s_{1} else concat(s_{1}, s_{2}), where concat(s_{1}, s_{2}) denotes the “usual” notion of concatenation of finite and countably infinite sequences. Thus, the cylindric closed semiring in this case is (C, ⊗ , ⊕ , 1, 0, ∃_{Δ}, d_{t,t′})_{Δ⊆V;t,t′∈T} where: C = 2^{(S∪{fail})^{∞}} is the set of finite and infinite sequences of machine states; for any S_{1}, S_{2} ∈ C, S_{1} ⊗ S_{2} = {s_{1} ⊙ s_{2} | s_{1} ∈ S_{1}, s_{2} ∈ S_{2}}; ⊕ = ∪; 1 = {ε}, where ε is the empty sequence; 0 = ∅; ∃_{Δ} corresponds to the function that, given any machine state S, yields the machine state obtained by discarding all information about the variables in Δ; and for any t, t′ ∈ T , d_{t,t′} corresponds to the function that, given any machine state S, yields the machine state resulting from constraining t and t′ to be equal, and fail if this is not possible.

2In an actual implementation, each such virtual machine instruction may, of course, “macro-expand” to a sequence of lower-level machine instructions.

A simple variation on this semantics is one where failed execution sequences are discarded silently. To obtain such a semantics, it suffices to redefine the operation ⊕ as follows: S_{1} ⊕ S_{2} = { s | s ∈ S_{1} ∪ S_{2} ∧ fail is not in s }.

6 Related Work

A related framework is considered in [Codognet and Filè 91] where an algebraic definition of constraint systems is given. Program analysis based on abstract interpretation techniques are considered, like groundness analysis and definiteness analysis for CLP programs. Only ⊗-composition is considered. The notion of “computation system” is introduced but it is neither formalized as a specific algebraic structure nor extended with the join-operator. In particular, because of the underlying semantics construction, mainly based on a generalization of the topdown SLD semantics, a loop-checker consisting in a “tabled”-interpreter is introduced. The use of tabled interpreters allows to keep separate the notion of abstraction from the finiteness required by any static analysis. As a consequence, static analysis can be performed by “running” the program in the standard CLP interpreter with tabulation. In our framework, no tabulation is considered. This makes the semantics construction more general. Finiteness is a specific property of the constraint system (expressed in terms of ⊕-chains), thus allowing to specify non-standard computations as standard CLP computations over an appropriate non-standard constraint system. Both the traditional top-down and bottom-up semantics can then be specified in the standard way thus allowing the definition of goal-independent static analysis as an abstract fixpoint computation, without loop-checking. If the constraint system is not Noetherian, a widening/narrowing technique [Cousot and Cousot 91] can be applied in the fixpoint computation to get a finite approximation of the T_{P}^{A} fixpoint.

In a related paper, Marriott and Søndergaard consider abstract interpretation of CLP. A meta-language is defined to specify, in a denotational style, the semantics of logic languages. Abstract interpretation is performed by abstracting such a semantics [Marriott and Søndergaard 90]. In this framework, both standard and non-standard semantics are viewed as an instance of the meta language specification.

Acknowledgment

The stimulating discussions with Maurizio Gabbrielli, Michael Maher and Nino Salibra are gratefully acknowledged.

References

[Aho et al. 74] A.V. Aho, J.E. Hopcroft, and J.D. Ullman. The Design and Analysis of Computer Algorithms. Addison Wesley Publishing Company, 1974.

[Barbuti et al. 92] R. Barbuti, M. Codish, R. Giacobazzi, and G. Levi. Modelling Prolog Control. In Proc. Nineteenth Annual ACM Symp. on Principles of Programming Languages, pages 95–104, 1992.

[Barbuti et al. 91] R. Barbuti, R. Giacobazzi, and G. Levi. A General Framework for Semantics-based Bottom-up Abstract Interpretation of Logic Programs. Technical Report TR 12/91, Dipartimento di Informatica, Università di Pisa, 1991. To appear in ACM Transactions on Programming Languages and Systems.

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

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

[Cirulis 88] J. Cirulis. An Algebraization of First Order Logic with Terms. Colloquia Mathematica Societatis Jànos Bolyai, 54, 1991.

[Codognet and Filè 91] P. Codognet and G. Filè. Computations, Abstractions and Constraints. Technical Report 13, Dipartimento di Matematica Pura e Applicata, Università di Padova, Italy, 1991.

[Cortesi et al. 91] A. Cortesi, G. Filè, and W. Winsborough. Prop revisited: Propositional Formulas as Abstract Domain for Groundness Analysis. In Proc. Sixth IEEE Symp. on Logic In Computer Science, pages 322– 327. IEEE Computer Society Press,1991.

[Cousot and Cousot 77] 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.

[Cousot and Halbwachs 78] 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.

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

[Cousot and Cousot 91] P. Cousot and R. Cousot. Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation. Preliminary draft, ICLP’91 Pre-conference workshop, Paris, 1991.

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

[Falaschi et al. 89] 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.

[Gabbrielli and Levi 91] 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.

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

[Henkin et al. 85] L. Henkin, J.D. Monk, and A. Tarski. Cylindric Algebras. Part I and II. North-Holland, Amsterdam, 1971. (Second edition 1985)

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

[Jørgensen et al. 91] N. Jørgensen, K. Marriott, and S. Michaylov. Some Global Compile-Time Optimizations for CLP(ℜ). Technical report, Department of Computer Science, Monash University, 1991.

[Kemp and Ringwood 90] R. Kemp and G. Ringwood. An Algebraic Framework for the Abstract Interpretation of Logic Programs. In S. Debray and M. Hermenegildo, editors, Proc. North American Conf. on Logic Programming’90, pages 506–520. The MIT Press, Cambridge, Mass., 1990.

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

[Saraswat et al. 91] 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, 1991.

[Scott 82] D. Scott. Domains for Denotational Semantics. In Proc. ICALP, volume 140 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1982.

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

[Verschaetse and De Schreye 91] K. Verschaetse and D. De Schreye. Automatic Derivation of Linear Size Relations. Technical report, Dept. of Computer Science, K.U. Leuven, 1991.