The AND-compositionality of CLP computed answer constraints.

Roberto Bagnara, Marco Comini, Francesca Scozzari and Enea Zaffanella Dipartimento di Informatica, Università di Pisa, Corso Italia 40, 56125 Pisa, Italy

                      {bagnara,comini,scozzari,zaffanel}@di.unipi.it

Abstract

We present a semantic characterization of CLP languages for the class of quick-checking systems. We define a semantics of computed answer constraints which is AND-compositional, does not loose the distinction between active and passive constraints in the answers and has both a top-down and a bottom-up characterization. We also show that an incrementality property we impose on the constraint solver is essential in order to define an AND-compositional atombased semantics.

1 Introduction

The semantics of CLP languages presented in [6] is (at least in its intentions) very general. Real CLP systems, in fact, are often equipped with incomplete constraint solvers and delay mechanisms. For instance, the arithmetic solver employed in the CLP(R) system [7] deals only with linear constraints, whereas non-linear ones are delayed. The languages truly implemented by these “real systems” are not captured by standard semantics constructions such as the original one of [5] and its refinements [4]. These semantics, indeed, refer to the ideal domain of computation, thus pretending that the system is endowed with a complete solver.

The idea of [6] consists in parameterizing the semantics construction with respect to the constraint system and two functions modeling the inferential power of the system’s constraint solver and the delay mechanisms employed. The infer function models the solver’s ability of deriving new information from the constraint store (i.e., the set of active constraints) and from the delayed constraints (which are termed as passive). The consistent function models the solver’s ability of detecting the unsatisfiability of the constraint store. Despite this nice idea, the semantics of [6] has several drawbacks:

• The semantics is defined only for most-general atomic goals. However, it is not clear how it can be used to recover the computed answers for general goals. Indeed, this is not possible in the setting of [6] since the constraint solver is not assumed to be incremental. This property (which we define precisely in Section 3) amounts to say, roughly speaking, that feeding the solver with a set of constraints all-in-one-shot, or giving them to it one-at-a-time does not change the solver’s results (namely, the sets of active and passive constraints will be the same).

• The distinction between active and passive constraints is taken into account only in the transition system used to define the operational semantics. In the end they are merged together so that everything is lost. This way, the two CLP(R) programs {p(X) :- X = 2} and {p(X) :- X*X = 4} are assigned the same semantics. Indeed, they exhibit a quite different behavior: in response to the query ?- p(Y) the first one yields the answer Y = 2 whereas, for the second one, the system’s answer is Y*Y =4 Maybe, indicating that the constraint is still passive. Moreover, the operational semantics of [6] makes use also of the logical-truth relation on the (idealized) constraint domain, which is undesirable.

• The bottom-up characterization of computed answers is given only for the ideal systems (i.e., those endowed with a complete constraint solver).

In this work we present a semantic characterization of CLP languages which overcomes the limitations of the one given in [6]. In particular, for the important class of quick-checking systems (i.e., those in which every resolution step is followed by a satisfiability check, or, in other words, most if not all the existing CLP systems), we define a semantics of computed answer constraints which:

• under the very reasonable hypothesis of incrementality of the constraint solver, is AND-compositional, that is, the answers to general goals can be reconstructed from the answers to most-general atomic goals;

• does not loose the distinction between active and passive constraints in the answers;

• has both a top-down and a bottom-up characterization.

We also show that the incrementality assumption on the constraint solver is so reasonable that it is impossible, without it, to define an atom-based semantics which is both AND-compositional and independent from the computation rule.

2 Preliminaries

In this section, following [6], we briefly review the basic syntax and semantics of constraint systems and CLP languages.

A signature is a set of function and predicate symbols with arities. A Σ-formula is built from variables, function and predicate symbols in Σ by using the classical first order logical connectives and quantifiers. In a closed formula each occurrence of a variable lies in the scope of a quantifier for that variable; ∃(ϕ) denotes the existential closure of all the free variables occurring in formula ϕ. A Σ-structure D is a set D together with an assignment of functions and relations on D to the symbols of Σ. We assume that Σ always contains the predicate symbol = which is interpreted as the identity over D. A Σ-theory is a collection of closed Σ-formulas and a model of a Σ-theory T is a Σ-structure D such that all the formulas of T evaluate to True under the interpretation D. We write T, D ⊧ ϕ to denote that the formula ϕ is valid in all the models of T extending D. The set of constraints L is a subset of the set of Σformulas closed under variable renaming, conjunction and existential quantification. A pair (D, L) is a constraint domain and will be often denoted by D.

A CLP program is a collection of rules of the form A←B where A is an atom and B is a (finite) multiset of atoms and constraints. A goal G is a (finite) multiset of constraints and atoms, representing their conjunction. atoms(G) denotes the multiset of all the atoms in G and constr(G) denotes the multiset of all the constraints in G. Multiset union is denoted by ⊎, whereas {|e|} denotes the singleton multiset containing e. As usual, without any loss of generality, we assume that rules and goals are in standard form, meaning that all the arguments in atoms are variables and each variable occurs in at most one atom.

The operational semantics is given by defining a transition system on states. A state is a triple ⟨G, C, S⟩ where G is a goal and C,S are finite (conjunctive) multisets of constraints, called the active and the passive constraints respectively. There is one additional state denoted fail. The initial state corresponding a goal G is ⟨G, ∅, ∅⟩. The transition system is parametric with respect to the functions consistent and infer. Given a set of constraints C, the function consistent(C) is a consistency check such that D ⊧ ∃(C) implies consistent(C). The function infer applied to a pair of finite multisets of constraints (C, S) yields a new pair of finite multisets of constraints (C′, S′) such that D ⊧ (C ∧ S) ↔ (C′ ∧ S′).

The transition rules are the following:

⟨G ⊎ {|A|}, C, S⟩ ⟶^{r} ⟨G ⊎ B, C, S ⊎ {|A = H|}⟩

where A is the selected atom^{1}, H←B is a renamed apart rule of P^{2}, H and A have the same predicate symbol and {|A = H|} is an abbreviation for the conjunction of equations between the corresponding arguments.

⟨G ⊎ {|A|}, C, S⟩ ⟶^{r} fail

where A is the selected atom and for every rule H←B of P, H and A have different predicate symbols.

⟨G ⊎ {|c|}, C, S⟩ ⟶^{c} ⟨G, C, S ⊎ {|c|}⟩

1We assume as given a computation rule which selects a transition rule and an element of G, if necessary.

2The program P is fixed in ⟶.

if c is the selected constraint.

⟨G, C, S⟩ ⟶^{i} ⟨G, C′, S′⟩  if (C′, S′) = infer (C, S)
⟨G, C, S⟩ ⟶^{s} ⟨G, C, S⟩  if consistent(C)
⟨G, C, S⟩ ⟶^{s} fail  if ¬ consistent(C)

A CLP system is thus defined by giving the constraint domain, the computation rule and definitions for consistent and infer.

Given states s_{0}, …, s_{n} and transitions s_{i} ⟶^{x_{i}} s_{i+1} we will often write s_{0} ⟶^{x_{0}···x_{n−1}}

s_{n} to denote the derivation s_{0} ⟶^{x_{0}} … ⟶^{x_{n−1}} s_{n}. Similarly, we write s ⟶^{x|y} s′ if s ⟶^{x} s′ or s ⟶^{y} s′ holds (according to the computation rule).

A CLP system is called quick-checking if its operational semantics can be described in terms of ⟶^{ris} and ⟶^{cis} (composite) rules only. A successful derivation starting from initial state ⟨G, ∅, ∅⟩ is a finite derivation having ⟨∅, C, S⟩ as the final state; (C, S) is an answer constraint for the initial goal G.

As usual, the syntactic equivalence modulo variance is denoted by ≡. For the sake of simplicity given the syntactic object E, E′, F, we write E ≈_{F} E′ for (F, E) ≡ (F, E′), namely to denote that E can be obtained from E′ by possibly renaming all the variables but those contained in F.

3 From AND-compositionality to incrementality

In this paper we are interested in computed answer constraints of quick-checking transition systems. Formally the set of computed answer constraints with respect to program P and goal G is defined as

Cac(P, G) = { ⟨G, C, S⟩ | ⟨G, ∅, ∅⟩ ⟶^{(r|c)is}^{∗} ⟨∅, C, S⟩ }

As usual computed answer constraints must not depend upon variable names, i.e., computed answer constraints of variant goals must be variant themselves. In the logic programming case this property is a consequence of the renaming apart condition used in SLD-resolution. In the CLP case to ensure this property the infer and consistent operations must compute their results independently upon variable names too, i.e.,

(C, S) ≡ (C′, S′) ⟹ (C, S, infer (C, S)) ≡ (C′, S′, infer (C′, S′))  (3.1)
C ≡ C′ ⟹ consistent(C) ↔ consistent(C′)  (3.2)

An atom-based semantics S is a set of triples of the form ⟨A, C, S⟩ where A is an atom and C, S are finite multisets of constraints. An atom-based semantics differs from the Cac operational behavior defined above in that it gathers the computed answers constraints of atomic goals only. The lower complexity of atom-based semantics make them more suitable for the development of semantics based analysis tools. However, to be really useful, these semantics have to be provided with a mechanism to reconstruct the computed answer constraints of a general goal from the semantics of its components (atoms and constraints). The availability of such a mechanism is the well-known AND-compositionality property of the semantics. Hence, the top-down semantics can be defined using the s-semantics atom-based style [2].

Definition 3.1 Let P be a fixed program, p range over the set of predicate symbols and x be a tuple of distinct variables. Then the top-down semantics of P with respect to the computation rule R is

SS_{P}^{R} = { ⟨p(x), C, S⟩_{/≡} | ⟨p(x), ∅, ∅⟩ ⟶_{R}^{(r|c)is}^{∗} ⟨∅, C, S⟩ }

When it is clear from the context, we will omit the computation rule index R.

Definition 3.2 An atom-based semantics S is AND-compositional w.r.t. computed answer constraints if

⟨G, C, S⟩ ∈ Cac(P, G) ⟺ ∀G_{i} ∈ atoms(G) ∃⟨G′_{i}, C_{i}, S_{i}⟩ renamed apart versions of elements in S and ∃ρ variables substitution s.t. G_{i} = G′_{i}ρ and (C′, S′) = infer (∅, ⨄_{i}(C_{i} ⊎ S_{i})ρ ⊎ constr(G)) and consistent(C′)

where (C, S) ≈_{G} (C′, S′).

In the general case, both the Cac set and the atom-based semantics S depend upon the choice of computation rule. When defining the AND-compositional property we are faced to the following choice: either the AND-compositionality mechanism depends on the computation rule, or the same AND-compositionality mechanism has to be used for all computation rules. Due to its greater formal and computational simplicity, in this paper we will opt for the latter. Moreover this mechanism has to be defined by means of the tools available inside the constraint system, namely in terms of the infer and consistent functions. In this way we avoid using the ⊧ relation, which is only weakly related to the real computation power of the constraint system.

From a technical point of view, all the active and passive constraints coming from the atoms of the composite goal are collapsed into a multiset of passive constraints. The alternative choice of keeping distinct the active and passive parts would fail in that, in general, the union of several consistent active constraints can yield an inconsistency.

Definition 3.3 The operations infer and consistent are incremental if

infer (∅, S) = (C_{1}, S_{1}), consistent(C_{1}), infer (C_{1}, S_{1} ⊎ {| c |}) = (C_{2}, S_{2}),
consistent(C_{2}) ⟺ infer (∅, S ⊎ {| c |}) = (C′_{2}, S′_{2}), consistent(C′_{2})

(3.3)

where (C_{2}, S_{2}) ≈_{S⊎{| c |}} (C′_{2}, S′_{2}) and

infer (∅, ∅) = (∅, ∅), consistent(∅)  (3.4)

Moreover the transition system is incremental if the operations infer and consistent are incremental.

The following Lemma shows that, given an incremental transition system, every quick checking computation rule R_{1} can be simulated by a corresponding computation rule R_{2} which omits all the non final i and s transitions. We call such a computation rule late checking.

Lemma 3.4 Consider an incremental transition system. Then ∀G, n ≥ 0

⟨G, ∅, ∅⟩ ⟶^{(r|c)is}^{n} ⟨∅, C^{q}, S^{q}⟩ ⟺ ⟨G, ∅, ∅⟩ ⟶^{r|c}^{n}⟶^{is} ⟨∅, C^{ℓ}, S^{ℓ}⟩

where (C^{q}, S^{q}) ≈_{G} (C^{ℓ}, S^{ℓ}).

Proof. We prove a stronger result for induction on n ≥ 0, namely

⟨G, ∅, ∅⟩ ⟶^{(r|c)is}^{n} ⟨G^{q}, C^{q}, S^{q}⟩ ⟺ ⟨G, ∅, ∅⟩ ⟶^{r|c}^{n}⟶^{is} ⟨G^{ℓ}, C^{ℓ}, S^{ℓ}⟩

where (G ⊎ G^{q}, C^{q}, S^{q}) ≡ (G ⊎ G^{ℓ}, C^{ℓ}, S^{ℓ}). The n = 0 base case by (3.4) is triv-

ial, while for the inductive case we have ⟨G, ∅, ∅⟩ ⟶^{(r|c)is}^{n} ⟨G^{q}, C^{q}, S^{q}⟩ which is equivalent to

⟨G, ∅, ∅⟩ ⟶^{(r|c)is}^{n−1} ⟨G_{1}, C_{1}, S_{1}⟩ ⟶^{(r|c)is} ⟨G^{q}, C^{q}, S^{q}⟩.

By applying the inductive hypotheses this is equivalent to

⟨G, ∅, ∅⟩ ⟶^{r|c}^{n−1}⟶^{is} ⟨G_{2}, C_{2}, S_{2}⟩ ⟶^{(r|c)is} ⟨G^{ℓ}, C_{3}, S_{3}⟩

where (G ⊎ G_{1}, C_{1}, S_{1}) ≡ (G ⊎ G_{2}, C_{2}, S_{2}) and by (3.1) and (3.2) (G ⊎ G^{q}, C^{q}, S^{q}) ≡ (G ⊎ G^{ℓ}, C_{3}, S_{3}). This in turn is equivalent to

\begin{matrix}⟨G, ∅, ∅⟩ & ⟶^{r|c}^{n−1} ⟨G_{2}, ∅, S_{4}⟩ ⟶^{is} ⟨G_{2}, C_{2}, S_{2}⟩ ⟶^{r|c} \\ ⟨G^{ℓ}, C_{2}, S_{2} ⊎ \{| c |\}⟩ & ⟶^{is} & ⟨G^{ℓ}, C_{3}, S_{3}⟩ \end{matrix}

where infer (∅, S_{4}) = (C_{2}, S_{2}), consistent(C_{2}) and infer (C_{2}, S_{2} ⊎ {| c |}) = (C_{3}, S_{3}), consistent(C_{3}). The constraint {| c |} is the one introduced by the r or c rule in the last derivation step.

Because of the incrementality of the transition system we obtain

infer (∅, S_{4} ⊎ {| c |}) = (C^{ℓ}, S^{ℓ})

and consistent(C^{ℓ}) where (C_{3}, S_{3}) ≈_{S_{4}⊎{| c |}} (C^{ℓ}, S^{ℓ}). Because of the renaming apart property of infer we have that (C_{3}, S_{3}) ≈_{G⊎G^{ℓ}} (C^{ℓ}, S^{ℓ}). Thus we can construct the following derivation

⟨G, ∅, ∅⟩ ⟶^{r|c}^{n−1} ⟨G_{2}, ∅, S_{4}⟩ ⟶^{r|c} ⟨G^{ℓ}, ∅, S_{4} ⊎ {| c |}⟩ ⟶^{is} ⟨G^{ℓ}, C^{ℓ}, S^{ℓ}⟩

By the transitivity of ≡ the proof is so concluded.

Next Lemma follows from the commutativity of multisets’ union.

Lemma 3.5 Let R_{1} and R_{2} be two late checking computation rules.

⟨G, ∅, ∅⟩ ⟶_{R_{1}}^{r|c}^{n}⟶^{is} ⟨∅, C_{1}, S_{1}⟩ ⟺ ⟨G, ∅, ∅⟩ ⟶_{R_{2}}^{r|c}^{n}⟶^{is} ⟨∅, C_{2}, S_{2}⟩

where (C_{1}, S_{1}) ≈_{G} (C_{2}, S_{2}).

An immediate consequence of the two previous lemmata is the independence of the semantics upon quick checking computation rules.

Theorem 3.6 Consider an incremental transition system and let R_{1} and R_{2} be two quick checking computation rules. Then SS_{P}^{R_{1}} = SS_{P}^{R_{2}}.

Lemma 3.7 Consider an incremental transition system. Then ∀G, S_{0}, n ≥ 0

⟨G, ∅, S_{0}⟩ ⟶^{r|c}^{n}⟶^{is} ⟨∅, C, S⟩ ⟺

∀G_{i} ∈ atoms(G) ∃⟨G′_{i}, C_{i}, S_{i}⟩ renamed apart versions of elements in SS_{P} and ∃ρ variables substitution s.t. G_{i} = G′_{i}ρ and (C′, S′) = infer (∅, S_{0} ⊎ ⨄_{i}(C_{i} ⊎ S_{i})ρ ⊎ constr(G)) and consistent(C′)

where (C, S) ≈_{G⊎S_{0}} (C′, S′).

Proof. The proof is by induction on n. The n = 0 base case is trivial, while for n > 0 we have two sub-cases, depending on the rule applied first

c rule] Let c be the selected constraint and G = G_{0} ⊎ {| c |}.

⟨G, ∅, S_{0}⟩ ⟶^{c} ⟨G_{0}, ∅, S_{0} ⊎ {| c |}⟩ ⟶^{r|c}^{n−1}⟶^{is} ⟨∅, C, S⟩

For IH we have ∀G_{i} ∈ atoms(G_{0}) ∃⟨G′_{i}, C_{i}, S_{i}⟩ renamed apart versions of elements in SS_{P} and ∃ρ s.t. G_{i} = G′_{i}ρ and

(C′, S′) = infer (∅, S_{0} ⊎ {| c |} ⊎ ⨄_{i}(C_{i} ⊎ S_{i})ρ ⊎ constr(G_{0}))

and consistent(C′), where (C, S) ≈_{G_{0}⊎S_{0}⊎{| c |}} (C′, S′). The thesis follows immediately from atoms(G_{0}) = atoms(G) and constr(G_{0}) ⊎ {| c |} = constr(G). r rule] Let A be the selected atom, G = G_{0} ⊎{| A |} and H←B be the used (renamed apart) clause of P. Then

⟨G, ∅, S_{0}⟩ ⟶^{r} ⟨G_{0} ⊎ B, ∅, S_{0} ⊎ {| A = H |}⟩ ⟶^{r|c}^{n}⟶^{is} ⟨∅, C, S⟩

For IH we have ∀G_{i} ∈ atoms(G_{0}), ∀B_{j} ∈ atoms(B) ∃⟨G′_{i}, C_{i}, S_{i}⟩, ∃⟨B′_{j}, C_{j}, S_{j}⟩ renamed apart versions of elements in SS_{P} and ∃ρ s.t. G_{i} = G′_{i}ρ, B_{j} = B′_{j}ρ and

(C_{1}, S_{1}) = infer (∅, S_{0} ⊎ {| A = H |} ⊎ ⨄_{i}(C_{i} ⊎ S_{i})ρ ⊎
⨄_{j}(C_{j} ⊎ S_{j})ρ ⊎ constr(G_{0}) ⊎ constr(B))

(Prf.1) where consistent(C_{1}) and (C, S) ≈_{G_{0}⊎B⊎S_{0}⊎{| A=H |}} (C_{1}, S_{1}). Now, let S′ = S_{0} ⊎ {| A = H |} ⊎ ⨄_{i}(C_{i} ⊎ S_{i})ρ ⊎ ⨄_{j}(C_{j} ⊎ S_{j})ρ ⊎ constr(G_{0}) ⊎ constr(B) and S′′ = {| A = H |} ⊎ ⨄_{j}(C_{j} ⊎ S_{j})ρ ⊎ constr(B). Moreover let (C_{2}, S_{2}) = infer (∅, S′′). Because S′′ ⊆ S′ by (3.3) we have consistent(C_{2}). By IH again on B, for some m < n we can

construct the derivation ⟨B, ∅, {| A = H |}⟩(⟶^{r|c})^{m} ⟶^{is} ⟨∅, C_{3}, S_{3}⟩ where

(C_{3}, S_{3}) ≈_{B⊎{| A=H |}} (C_{2}, S_{2}).  (Prf.2)

Hence ⟨A, C_{3}, S_{3}⟩_{/≡} ∈ SS_{P} because we can build the derivation

⟨A, ∅, ∅⟩ ⟶^{r} ⟨B, ∅, {| A = H |}⟩(⟶^{r|c})^{m} ⟶^{is} ⟨∅, C_{3}, S_{3}⟩

Then we can choose a renamed apart ⟨A′, C_{q}, S_{q}⟩ and a suitable variables substitution ρ′ s.t. (Prf.1) holds for ρ′ instead of ρ and

⟨A′, C_{q}, S_{q}⟩ρ′ = ⟨A, C_{3}, S_{3}⟩.  (Prf.3)

Now let S′′′ be S′ − S′′ with ρ′ instead of ρ and let

(C_{4}, S_{4}) = infer (∅, (S′′′) ⊎ C_{3} ⊎ S_{3}).  (Prf.4)

Because of the renaming apart property of ⟨A′, C_{q}, S_{q}⟩ and from (Prf.3) follows (C_{2}, S_{2}) ≈_{G⊎A⊎S_{0}} (C_{q}, S_{q}). Now by Lemma 3.7, (Prf.1), (Prf.2), (Prf.4) and (3.3) several times on S′ − S′′ we obtain (C_{4}, S_{4}) ≈_{G⊎S_{0}} (C, S) This and (3.2) implies consistent(C_{4}). The (3.3) property can be iteratively applied because consistent(C_{1}).

The proof is so concluded.

Theorem 3.8 If the transition system is incremental and R is quick checking then the SS_{P}^{R} semantics is AND-compositional w.r.t. computed answer constraints.

Proof. We can apply Lemma 3.4 and prove the equivalent result

⟨G, ∅, ∅⟩ ⟶^{r|c}^{n}⟶^{is} ⟨∅, C, S⟩ ⟺

∀G_{i} ∈ atoms(G) ∃⟨G′_{i}, C_{i}, S_{i}⟩ renamed apart versions of elements in

SS_{P} and ∃ρ variables substitution s.t. G_{i} = G′_{i}ρ,
(C′, S′) = infer (∅, ⨄_{i}(C_{i} ⊎ S_{i})ρ ⊎ constr(G)) and consistent(C′)

where (C, S) ≈_{G} (C′, S′). The thesis follows immediately from Lemma 3.7.

Theorem 3.9 Let R be a quick checking computation rule. Suppose that SS_{P}^{R} is AND-compositional w.r.t. computed answer constraints and independent with respect to all quick checking computation rules. Then the transition system is incremental.

Proof. Let S = {| c_{1} …, c_{n} |}. For proving (3.4) simply apply the AND-composition-ality of SS_{P} on G = ∅. To prove (3.3) let c be a constraint, infer (∅, S ⊎ {| c |}) = (C_{1}, S_{1}) and consistent(C_{1}). By applying the AND-compositionality of SS_{P} on G = S ⊎ {| c |} this is equivalent to ⟨G, C_{2}, S_{2}⟩ ∈ Cac(P, G) where (C_{1}, S_{1}) ≈_{G} (C_{2}, S_{2}). For the independence of computed answer constraints upon the selection

rule this is equivalent to ⟨S ⊎ {| c |}, ∅, ∅⟩ ⟶^{cis}^{n} ⟨{| c |}, C_{3}, S_{3}⟩ ⟶^{cis} ⟨∅, C_{4}, S_{4}⟩ where

(C_{2}, S_{2}) ≈_{G} (C_{4}, S_{4}). This is equivalent to

⟨S, ∅, ∅⟩ ⟶^{cis}^{n} ⟨∅, C_{5}, S_{5}⟩  (Prf.1)

and ⟨{| c |}, C_{5}, S_{5}⟩ ⟶^{cis} ⟨∅, C_{6}, S_{6}⟩ where (C_{3}, S_{3}) ≈_{S} (C_{5}, S_{5}) and (C_{4}, S_{4}) ≈_{{| c |}}

(C_{6}, S_{6}). By applying the AND-compositionality of SS_{P} on (Prf.1) this is equivalent to

(C_{7}, S_{7}) = infer (∅, S), consistent(C_{7})

where (C_{5}, S_{5}) ≈_{S} (C_{7}, S_{7}). Hence for cis rule definition

(C_{6}, S_{6}) = infer (C_{5}, S_{5} ⊎ {| c |}), consistent(C_{6}).

Now let (C_{8}, S_{8}) = infer (C_{7}, S_{7} ⊎ {| c |}), then for (3.1) we have

(C_{7}, S_{7}, C_{8} ⊎ S_{8}) ≡ (C_{5}, S_{5}, C_{6} ⊎ S_{6})

and by (3.2) consistent(C_{8}). By ≡ transitivity (C_{8}, S_{8}) ≈_{G} (C_{1}, S_{1}). Finally from (3.2) we have that consistent(C_{1}) which is the claim.

Note that, from Theorem 3.8 and Theorem 3.9 it follows that, under the hypothesis of independence upon the computation rule, the incrementality condition is equivalent to the AND-compositionality of SS_{P}^{R}. However, it is possible to relax our notion of AND-compositionality, by combining the atoms according to a fixed computation rule, thus obtaining a weaker incrementality condition.

4 Bottom-up semantics

In this section we show a bottom-up characterization of our semantics and prove that, for every incremental transition system, it is equivalemnt to the top-down construction.

The immediate consequences operator is defined by exploiting the properties of incremental transition system, namely Lemma 3.4 and 3.7.

Definition 4.1 The immediate consequences operator of the program P is

T_{P} (I) = { ⟨p(x), C, S⟩_{/≡} |

x are new variables, H←B ∈ P, ∀B_{i} ∈ atoms(B)

∃⟨B′_{i}, C_{i}, S_{i}⟩ renamed apart versions of elements of I and a variables substitution ρ s.t. B_{i} = B′_{i}ρ, (C, S) = infer (∅, {|p(x) = H|} ⊎ constr(B) ⊎ ⨄_{i}(C_{i} ⊎ S_{i})ρ) and consistent(C) } The following lemma can be proved using standard techniques.

Lemma 4.2 The T_{P} operator is continuous.

Proof. It is easy to see that T_{P} is monotone. We have to prove that is also finitary, i.e., T_{P} (⋃^{∞}I_{n}) ⊆ ⋃^{∞}T_{P} (I_{n}).

Let I_{0} ⊆ I_{1} ⊆ … I_{n} ⊆ … be a chain. If g ∈ T_{P} (⋃^{∞}I_{n}) then for T_{P} definition there must exist a finite number of goals g_{1}, …, g_{n} ∈ ⋃^{∞}I_{n} from which g is built. In particular it must exist a finite k s.t. g_{1}, …, g_{n} ∈ I_{k} and then, applying T_{P} definition again g ∈ T_{P} (I_{k}) which implies g ∈ ⋃^{∞}T_{P} (I_{n}).

Definition 4.3 Let P be a program. The bottom-up semantics of P is F_{P} = T_{P} ↑ ω.

Theorem 4.4 Consider an incremental transition system. For any quick checking computation rule R we have SS_{P}^{R} = F_{P}

Proof. Let’s prove the two inclusions separately.

SS _{P} ⊆ F_{P} ] Let ⟨p(x), C^{q}, S^{q}⟩ ∈ SS_{P}, that is, for some n there exists the quick

checking derivation ⟨p(x), ∅, ∅⟩ ⟶^{(r|c)is}^{n} ⟨∅, C^{q}, S^{q}⟩. From Lemma 3.4 there exists

the late checking derivation ⟨p(x), ∅, ∅⟩ ⟶^{r|c}^{n}⟶^{is} ⟨∅, C^{ℓ}, S^{ℓ}⟩ where (C^{q}, S^{q}) ≈_{p(x)}

(C^{ℓ}, S^{ℓ}).

We prove the inclusion by induction on the number of r or c transitions of the late checking system. Note that the first rule is always an r rule. For n = 1 there exists a renamed apart clause H. of P such that

⟨p(x), ∅, ∅⟩ ⟶^{r} ⟨∅, ∅, {|p(x) = H|}⟩ ⟶^{is} ⟨∅, C^{ℓ}, S^{ℓ}⟩

By definition of T_{P} we have that ⟨p(x), C^{ℓ}, S^{ℓ}⟩_{/∼} ∈ T_{P} ↑ 1.

For n > 1 without loss of generality consider the following derivation where H←B is a renamed apart version of clause of P.

⟨p(x), ∅, ∅⟩ ⟶^{r} ⟨B, ∅, {|p(x) = H|}⟩ ⟶^{r|c}^{n−1} ⟨∅, ∅, S_{0}⟩ ⟶^{is} ⟨∅, C^{ℓ}, S^{ℓ}⟩

Note that for n = 1 the body B is empty and most of the following formulas became trivial. The derivation

⟨B, ∅, {|p(x) = H|}⟩ ⟶^{r|c}^{n−1} ⟨∅, ∅, S_{0}⟩

does not depend on the accumulated constraints because no i and s transitions are applied. So we can build the derivation

⟨B, ∅, ∅⟩ ⟶^{r|c}^{n−1} ⟨∅, ∅, S_{0} − {|p(x) = H|}⟩ ⟶^{is} ⟨∅, C_{1}, S_{1}⟩

where, if we let (C_{2}, S_{2}) = infer (∅, {|p(x) = H|} ⊎ C_{1} ⊎ S_{1}), (C^{ℓ}, S^{ℓ}) ≈_{B} (C_{2}, S_{2}) by (3.3). Then, by Theorem 3.8, for each atom B_{i} ∈ atoms(B) there exists ⟨B′_{i}, C_{i}, S_{i}⟩ renamed apart versions of elements in SS_{P} and ρ such that B_{i} = B′_{i}ρ and

(C_{3}, S_{3}) = infer (∅, constr(B) ⊎ ⨄_{i}(C_{i} ⊎ S_{i})ρ)

where consistent(C_{3}) and (C_{1}, S_{1}) ≈_{B} (C_{3}, S_{3}). All the previous derivations are smaller than n so applying the IH we obtain ⟨B′_{i}, C_{i}, S_{i}⟩ ∈ T_{P} ↑ ω. In particular, because of the finiteness of B, there exists some k such that for each i ⟨B′_{i}, C_{i}, S_{i}⟩ ∈ T_{P} ↑ k. Moreover

infer (∅, {|p(x) = H|} ⊎ (constr(B) ⊎ ⨄_{i}(C_{i} ⊎ S_{i})ρ)) ≈_{p(x)}  [ by (3.3) ]
infer (∅, {|p(x) = H|} ⊎ C_{3} ⊎ S_{3}) ≈_{p(x)}  [ by (3.1) ]
infer (∅, {|p(x) = H|} ⊎ C_{1} ⊎ S_{1}) ≈_{p(x)}
(C^{ℓ}, S^{ℓ}) ≈_{p(x)}
(C^{q}, S^{q})

and consistent(C^{q}). Hence by T_{P} definition ⟨p(x), C^{q}, S^{q}⟩_{/∼} ∈ T_{P} ↑ (k + 1). The thesis then follows by T_{P} monotonicity.

SS _{P} ⊇ F_{P} ] We prove by induction on n that T_{P} ↑ n ⊆ SS_{P}.

The n = 0 case is trivial, because T_{P} ↑ 0 = ∅ ⊆ SS_{P}. For n ≥ 1 let ⟨p(x), C, S⟩ ∈ T_{P} ↑ n. Then for some clause H←B ∈ P ∀B_{i} ∈ atoms(B) ∃⟨B′_{i}, C_{i}, S_{i}⟩ renamed apart versions of elements of T_{P} ↑ (n − 1) and ρ s.t. consistent(C) and (C, S) = infer (∅, U ⊎ constr(B) ⊎ ⨄_{i} K_{i}) where U = {|p(x) = H|} and K_{i} = (C_{i} ⊎ S_{i})ρ. Note that for n = 1 the body B is empty and most of the following formulas become trivial.

By applying Lemma 3.7 with S_{0} = U we have that ⟨B, ∅, U⟩ ⟶^{∗} ⟨∅, C′, S′⟩ where (C, S) ≈_{B⊎U} (C′, S′). Then ⟨p(x), ∅, ∅⟩ ⟶^{∗} ⟨∅, C′, S′⟩ which is the thesis.

5 Conclusions

In this paper we have presented a semantic characterization of “real” CLP languages. This is made possible by parameterizing the semantic construction with respect to functions which model the behavior of the actual constraint solver employed. This idea is due to [6]. However, the semantics presented in [6] suffers from several drawbacks. We have overcome these limitations, presenting a semantics for quick-checking systems which is AND-compositional (under the assumption of incrementality of the constraint solver), captures both active and passive constraints, and has natural top-down and bottom-up construction processes. Our incrementality assumption (which is missing in [6]) does not exclude any reasonable system. Moreover, we have shown that if the incrementality assumption does not hold then no atom-based semantics can be both AND-compositional and independent from the computation rule.

The semantic treatment presented in this paper is not the only way to characterize CLP systems employing incomplete constraint solvers. For instance, the delay mechanism can be captured at the constraint system level, instead of carrying over a distinguished set of delayed (or passive) constraints in the semantics. In [1] a class of constraint systems is introduced, where constraints are cc agents [8]. In this approach, the CLP(R) constraint X = Y ∗ Z is considered as a shorthand for

ask(ground(Y) ∨ ground(Z)) → tell(X = Y ∗ Z),

expressing the fact that X = Y ∗ Z (being non-linear) is delayed until it becomes linear, namely, until either Y or Z are constrained to take a single value.

If we are interested in complete constraint solvers only, then the semantics defined in [6] boils down to the CLP version of the s-semantics [4]. In this case the ANDcompositionality problem has been deeply studied, even with respect to a much more concrete semantics, yielding stronger results [3].

References

[1] R. Bagnara. A hierarchy of constraint systems for data-flow analysis of constraint logicbased languages. Technical Report TR-96-10, Dipartimento di Informatica, Università di Pisa, 1996. To appear on a special issue of “Science of Computer Programming”.

[2] A. Bossi, M. Gabbrielli, G. Levi, and M. Martelli. The s-semantics approach: Theory and applications. Journal of Logic Programming, 19-20:149–197, 1994.

[3] M. Comini and G. Levi. An algebraic theory of observables. In M. Bruynooghe, editor, Proceedings of the 1994 Int’l Symposium on Logic Programming, pages 172–186. The MIT Press, Cambridge, Mass., 1994.

[4] M. Gabbrielli, G. M. Dore, and G. Levi. Observable semantics for constraint logic programs. J. Logic Computation, 5(2):133–171, 1995.

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

[6] J. Jaffar and M. J. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 19-20:503–581, 1994.

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

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