The Unfolding Semantics for Constraint Logic Programs

Roberto Giacobazzi

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

giaco@dipisa.di.unipi.it

1 Introduction

Pure logic programming is based on the unification algorithm on the Herbrand universe. The unification of a set of equations consists two tasks: deciding if the equations are solvable and simplifying the equations by transforming them into the solved form. The second aspect of this process is not really essential to computing.

We can be interested in extending the domain of terms in order to deal with more appropriate domains of computation, like the uncountable domain of reals. The framework of CLP(X) [5] was proposed to cope with this problem. It leads to the definition of a class of languages based upon constraint solving and the logic-programming paradigm. Each instance of the CLP(X) scheme is obtained by the specifying the computation structure and corresponding solution algorithm.

One of the most interesting aspects of this framework is that it allows to generate a class of languages which are soundly based within a single semantic structure. This structure depends on the intended domain of the computation. This contrasts with working on the Herbrand universe where every semantic object has to be coded into a Herbrand term.

This semantic feature leads to a closer relation between the semantics of the language and the real world of computation. As a consequence, the CLP(X)-scheme provides languages having a superior expressive power. In fact, since the notion of unifiability of a set of equations is a particular instance of constraint solvability, pure logic programming is an instance of CLP. The outstanding aspect of this class of languages is that they have the model-theoretic and fixpoint semantics which are similar to those of pure logic programs [5]. Moreover, since the operational semantics of CLP(X) is always based on constraint solvability on a given structure, it is possible to define an algebraic semantics too, corresponding to the algebraic structure of X.

From a purely theoretical point of view, as in the case of positive logic programs, the declarative semantics of CLP(X) enjoys nice properties such as the equivalence between the three notions of minimal model, success set and least fixpoint of an immediate consequence operator. However, this equivalence is not fully achieved, since the standard operational model of a CLP program does not mirror its observable properties, i.e. the real program behaviour, given in terms of a set of answer constraints, is not reflected in the minimal model. As argued in [7], the key issue consists in a suitable choice of the notion of model. In [4] we can find a reconstruction of the semantics of CLP, obtained by defining various model notions, each corresponding to a specific operationally observable property, as firstly defined in [3] for the pure logic programming case.

In this paper, we extend some results related to the pure logic programming and presented in [8], dealing with an alternative way to characterize the operational behaviour of logic programs. The main idea is that we can consider a possibly infinite collection of unit clauses as an alternative representation of the model. This set is obtained from the original program, via a program transformation technique. Therefore, the declarative meaning of a CLP program is again a possibly infinite CLP program.

The computed answer constraint can be obtained by executing the goal into this set of clauses. The operational semantics is reflected into a program transformation technique which preserves the intended meaning of the program. As stressed in [1] an unfolding transformation technique, appears as intermediary between procedural and fixpoint semantics. They show that it is possible to give a quasi-algebraic characterization of the relationship between these two semantics, which allows to give more simple proofs than usual, (in particular about soundness and completeness theorems). These thoughts increase the importance of such a transformation, both from a purely technical point of view and for a deeper understanding of the logic programs semantics. In particular the immediate consequence operator T_{P} can be defined in terms of the unfolding rule.

The unfolding rule presented in this paper is an extension, in the area of constraint logic programs, of the one presented in [8].

2 Preliminaries

Let us recall some basic concepts about CLP. For a more complete treatment on the subject see [6, 5].

In Constraint Logic Programming, the basic operational step is constraint solvability on a given domain. It follows that the algebraic approach to the semantics is natural for CLP.

Let us consider a many sorted first order language. Let SORT = ⋃_{i} SORT_{i} denotes a finite set of sorts. The signature of an n-ary function, predicate or variable is a sequence of n + 1 elements of SORT.

Let us also denote by:

• Σ, a denumerable collection of function symbols,

• Π, a denumerable collection of predicate symbols, where Π contains the equality symbol.

• V, a denumerable set of variable symbols.

Let τ(Σ) and τ(Σ ∪ V) denote, the ground and the possibly non ground class of terms respectively. Then [6, 5]:

• a (Σ, Π)-atom has the form: p(t_{1}, ..., t_{n}) where p ∈ Π and t_{i} ∈ τ(Σ ∪ V), ∀i = 1, ..., n.

• a (Σ, Π)-constraint is a possibly empty, finite or infinite conjunction of (Σ, Π)-atoms. The empty constraint is denoted by TRUE.

Let us assume that Π = Π_{C} ∪ Π_{A} and Π_{C} ∩ Π_{A} = ∅.

Definition 2.1 A constraint logic program (CLP) is a finite set of constraint rules of the following form: A ← c□. or A ← c□B_{1}, ..., B_{n}. where c is a finite (Σ, Π_{C})-constraint and A (the head), B_{1}, ..., B_{n} (the body) are (Σ, Π_{A})- atoms. A goal is a constraint rule with no head and with a non empty body.

The structure defined on Π and Σ (the alphabet), will be denoted by ℜ(Σ, Π) and consists of

1. a collection of non-empty sets Dℜ_{s}, s ∈ SORT;

2. an assignment of a function Dℜ_{s_{1}} × ... × Dℜ_{s_{n}} → Dℜ_{s} to each n-ary function symbol f ∈ Σ, where (s_{1}, ..., s_{n}, s) is the signature of f;

3. an assignment of a function Dℜ_{s_{1}} × ... × Dℜ_{s_{n}} → {T RUE, F ALSE} to each n-ary predicate symbol p ∈ Π (apart from = which is naturally interpreted as syntactic equality), where (s_{1}, ..., s_{n}) is the signature of p.

A ℜ(Σ, Π)-valuation of a ℜ(Σ, Π)-expression E, is a mapping ϑ from each distinct variable in E, into Dℜ_{s}, where s is the sort associated with each variable symbol. In the following, we will omit the ℜ(Σ, Π) notation in programs, constraints, atoms, structures and valuations, when it is clear from the context.

Let us consider a constraint C, defined as a conjunction of a possibly empty or infinite set of atoms C. ℜ ⊧ Cϑ, where ϑ is an ℜ -valuation of the expressions in C, iff ℜ ⊧ cϑ holds (i.e. cϑ is ℜ-equivalent to TRUE).

Let A = p(t_{1}, ..., t_{n}) be an atom and ϑ a valuation on t_{1}, ..., t_{n}. We denote by Aϑ the atom p(t_{1}ϑ, ..., t_{n}ϑ).

Definition 2.2 A constraint c is ℜ-solvable iff there exists an ℜ-valuation ϑ (the ℜ-solution) such that ℜ ⊧ cϑ.

In this paper we do not consider negation. Thus we can relax one of the conditions on the solution compactness of ℜ-structures, as given in [5, 6]. We will consider only the following condition, namely

• for every sort s and d ∈ Dℜ_{s}, d is uniquely definable in terms of a finite or infinite set of constraints.

Let us give a semantic framework for CLP, based on the previous algebraic structures [4, 6, 5]. In the following we assume that the alphabet (Σ, Π) and the ℜ structure are given. Moreover we will often denote n-tuples of terms t_{1}, ..., t_{n} by t̄.

Definition 2.3 The set of instances [c□p(X̄)] of a constrained atom c□p(X̄) is defined as: [c□p(X̄)] = {p(X̄)ϑ|ϑ is an ℜ-solution of c}.

Definition 2.4 Let A be a set of constrained atoms. We define a preorder ⊑ on A such that: c_{1}□p(X̄) ⊑ c_{2}□p(X̄) iff [c_{1}□p(X̄)] ⊆ [c_{2}□p(X̄)].

We denote by ≡ the equivalence relation induced by the preorder ⊑.

Definition 2.5 Let P be a constraint logic program and A be the set of ℜ-solvable constrained atoms in P. The ℜ-base of interpretation B_{P} is the quotient set of A w.r.t. ≡.

Definition 2.6 An interpretation is any subset of B_{P}.

We recall now the definition of truth as given in [4].

Definition 2.7 Let I be an interpretation.

• A constrained atom c□p(X̄) is true in I iff [c□p(X̄)] ⊆ [I];

• A clause H ← c□B_{1}, ..., B_{n} is true in I iff for each ℜ-solution ϑ of c, {B_{1}ϑ, ..., B_{n}ϑ} ⊆ [I] implies Hϑ ∈ [I].

Thus, a model of a CLP program P is any interpretation in which all the clauses of P are true.

We can observe that the mechanism introduced in [2, 3] to allow non-ground atoms in the Herbrand base may be generalized in CLP, by allowing constrained atoms into the ℜ-base. Each constrained atom c□p(X̄), in fact, represents the set of instances p(X̄)ϑ, where ϑ is an ℜ-solution of the constraint c. Thus, it implicitely represents a possibly infinite set of instances of the variables X̄ on the solution domain of c [4].

Let us summarize now the operational and fixpoint semantics as given in [4].

Operational Semantics

Let P be a CLP program. A (P, ℜ)-derivation step of a goal G: ← c□B_{1}, ..., B_{n} returns a goal of the form ← c̃□B̃_{1}, ..., B̃_{n} if there exist n variants of clauses in P, H_{i} ← c_{i}□B̃_{i}, i = 1, ..., n, with no shared variables with the goal, such that

c̃ = {c, c_{1}, ..., c_{n}, B_{1} = H_{1}, ..., B_{n} = H_{n}} is ℜ-solvable.

The (P, ℜ)-derivation of a goal G is then a finite or infinite sequence of goals, returned by (P, ℜ)-derivation steps, starting from G.

A successful (P, ℜ)-derivation of a goal G is a finite (P, ℜ)-derivation whose last element is the empty clause c□. (c will be the associated answer constraint).

A characterization of the operational behaviour of CLP may be given in terms of the following success set associated with the program [4]:

SS(P, ℜ) = {c□p(X̃)|c□p(X̃) ∈ B_{P},

(true□p(X̃)) ⟶^{(P,ℜ)} c′□. ,

c is finite and c□p(X̃) ≡ c′□p(X̃)}.

Fixpoint Semantics.

The following characterization of the semantics in terms of a continuous transformation map, associated with the program P, may be found in [4]. Let I ⊆ B_{P},

T_{(P,ℜ)}(I) = {c□p(X̃) ∈ B_{P} |
∃ a renamed clause p(t̃) ← c_{0}□p_{1}(t̃_{1}), ..., p_{n}(t̃_{n}) ∈ P
∃c_{i}□p_{i}(X̃_{i}) ∈ I, which share no variables,
c′ = c_{0} ∧ {X̃_{1} = t̃_{1}, ..., X̃_{n} = t̃_{n}} ∧ {c_{1}, ..., c_{n}},
c′ is finite, ℜ − solvable and c = c′ ∧ {X̃ = t̃}}.

T_{(P,ℜ)} satisfies the usual properties of the immediate consequence operator as given in [10, 2, 3, 4, 6]. In particular M_{(P,ℜ)} = T_{(P,ℜ)} ↑ ω is a model.

The following soundness and completeness theorem is the main result on the relation between the operational and the declarative semantics of CLP.

Theorem 2.1 Let P be a CLP program, and G: ← c_{0}□A_{1}, ..., A_{n} be a goal. Then the goal G has a refutation in P with computed answer constraint c_{a} iff there exist

(c_{1}□B_{1}), ..., (c_{n}□B_{n}) ∈ M_{(P,ℜ)},

which share no variables, such that c_{0} ∧ c_{1} ∧ ... ∧ c_{n} ∧ A_{1} = B_{1} ∧ ... ∧ A_{n} = B_{n} and c_{a} have the same solutions for the variables in the goal. ◇

This theorem shows that M_{(P,ℜ)} really models the operational behavior of CLP programs [4].

3 Unfolding of Constraint Logic Programs

In this section we present a transformation rule (the unfolding) on CLP programs. As in the pure logic programming case, this rule is defined in order to satisfy at least the following requirements:

• the unfolding of a CLP program is still a CLP program,

• the rule can always be applied to any procedure call,

• the unfolded program has to be equivalent to the original one w.r.t. the computed answer constraint.

Let us first consider the transformation on single clauses.

Definition 3.1 Let P be a CLP program and C : p(t̄) ← c_{0}□p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) a clause of P. The unfolding of the clause C with respect to the program P, Unf(C,P), is the following set of clauses

• {C} if C is a unit clause (n = 0)

• p(X̄) ← c□p_{1_{1}}(t̄_{1_{1}}), ..., p_{1_{k_{1}}}(t̄_{1_{k_{1}}}), ..., p_{n_{1}}(t̄_{n_{1}}), ..., p_{n_{kn}}(t̄_{n_{kn}}) such that p_{i}(X̄_{i}) ← c_{i}□p_{i_{1}}(t̄_{i_{1}}), ..., p_{i_{k_{i}}}(t̄_{i_{k_{i}}}), i = 1, ..., n are (renamed apart) versions of clauses in P, and

c′ = c_{0} ∧ {X̄_{1} = t̄_{1}, ..., X̄_{n} = t̄_{n}} ∧ {c_{1}, ..., c_{n}} is ℜ-solvable and c = c′ ∧ {X̄ = t̄}.

Definition 3.2 Let P be a CLP program defined as a set of constrained clauses {C_{1}, ..., C_{n}}. The unfolding of P is

Unf(P) = ⋃_{i=1}^{n} Unf(C_{i}, P)

Example 3.1 The following constraint logic program [6] can be seen as a simple integration routine for some arithmetic function f. The symbol ϵ stands for some term 1/n where n is a numeral. The interpretation structure is the Real Arithmetic, with the usual signature and Π_{C} = {=, <}.

integrate(A, B, x) ←

0 < B − A ≤ ϵ, x = (B − A) ∗ f(A + (B − A)/2)□. integrate(A, B, x) ←

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

The unfolding of such a program is

integrate(A, B, x) ←

0 < B − A ≤ ϵ, x = (B − A) ∗ f(A + (B − A)/2)□. integrate(A, B, x) ←

B − A > ϵ, M = A + (B − A)/2, x = x_{1} + x_{2},

0 < M − A ≤ ϵ, x_{1} = (M − A) ∗ f(A + (M − A)/2),

0 < B − M ≤ ϵ, x_{2} = (B − M) ∗ f(M + (B − M)/2)□. integrate(A, B, x) ←

B − A > ϵ, M = A + (B − A)/2, x = x_{1} + x_{2},

M − A > ϵ, M′ = A + (M − A)/2, x_{1} = x1^{′} + x2^{′},

B − M > ϵ, M^{”} = M + (B − M)/2, x_{2} = x_{1}^{”} + x_{2}^{”}□

integrate(A, M′, x1^{′}), integrate(M′, M, x2^{′}),

integrate(M, M^{”}, x_{1}^{”}), integrate(M^{”}, B, x_{2}^{”}).

Since M = A + (B − A)/2, the constraint ...M − A > ϵ, ..., 0 < B − M ≤ ϵ... is inconsistent. Thus, we can not unfold the second clause with respect to the first and the second one in the program, and viceversa.

The following results formally establish the equivalence between the semantics of the unfolding of a program and the semantics of the program itself. It follows from the definition that the unfolding rule replaces each clause of the program with a set of clauses, where the corresponding bodies are the result of a single (P, ℜ)-derivation step, by selecting the whole atoms in the source body. Thus we can argue that the unfolding of a clause is the empty set if and only if each possible (P, ℜ)-derivation, by using such a clause, is always failed [8].

Theorem 3.1 Let P be a CLP program. Then M_{(Unf(P),ℜ)} ⊆ M_{(P,ℜ)}.

Proof. We prove that for each clause C ∈ Unf(P), C is true in M_{(P,ℜ)}. Let n denote the length of the body of C.

• Let n = 0. Since, by the definition, C ∈ P and M_{(P,ℜ)} is a model for P, the theorem trivially holds.

• Let n ≥ 0 and C: p(X̄) ← c□p_{1_{1}}(t̄_{1_{1}}), ..., p_{n_{kn}}(t̄_{n_{kn}}). Then by definition there exists a clause p(t̄) ← c_{0}□p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) in P such that, by considering the following renamed apart versions of clauses in P, p_{1}(X̄_{1}) ← c_{1}□p_{1_{1}}(t̄_{1_{1}}), ..., p_{1_{k_{1}}}(t̄_{1_{k_{1}}}). ................................................ p_{n}(X̄_{n}) ← c_{n}□p_{n_{1}}(t̄_{n_{1}}) ,..., p_{n_{kn}}(t̄_{n_{kn}}). the associated constraint:

c′_{i} = c_{0} ∧ ⋀_{j=1}^{i} c_{j} ∧ {X̄_{1} = t̄_{1}, ..., X̄_{i} = t̄_{i}}

is ℜ-solvable, for each i = 1, ..., n, and c = c′_{n} ∧ {X̄ = t̄}. Let us consider the following clause C′_{i}: p(X̄) ← c′_{i} ∧ {X̄ = t̄}□p_{1_{1}}(t̄_{1_{1}}) ,..., p_{i_{k_{i}}}(t̄_{i_{k_{i}}}), p_{i+1}(t̄_{i+1}),...,p_{n}(t̄_{n}). It is a resolvent of the clauses C′_{i−1} and C_{i}. Thus, for each i = 1, ..., n, C′_{i} is true in M_{(P,ℜ)}. ◇

The next theorem shows that each minimal model of Unf(P) is also a model of P. The equivalence between the program P and its unfolding is then proved in conjunction with the previous result.

Theorem 3.2 Let P be a CLP program, then: M_{(P,ℜ)} ⊆ M_{(Unf(P),ℜ)}.

Proof. We prove by induction on n that: T_{(P,ℜ)} ↑ n ⊆ M_{(Unf(P),ℜ)}.

• Base step: let (c□p(X̄)) ∈ T_{(P,ℜ)} ↑ 1. Thus, by definition p(t̄) ← c_{0}. ∈ P and c = c_{0} ∧ {X̄ = t̄}. By the unfolding rule definition we have that p(t̄) ← c_{0}. ∈ Unf(P), and then the unit clause is true in M_{(Unf(P),ℜ)}.

• Inductive step: let (c□p(X̄)) ∈ T_{(P,ℜ)} ↑ (m + 1) = T_{(P,ℜ)}(T_{(P,ℜ)} ↑ m). Thus, by the T_{(P,ℜ)} definition, ∃ p(t̄) ← c_{0}□p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) ∈ P, ∃ (c_{i}□p_{i}(X̄_{i})) ∈ T_{(P,ℜ)} ↑ m such that

c′ = ⋀_{i=0}^{n} c_{i} ∧ {X̄_{1} = t̄_{1}, ..., X̄_{n} = t̄_{n}}

is ℜ-solvable and c = c′ ∧ {X̄ = t̄}. Moreover, by the hypothesis

c = c_{0} ∧ ⋀_{i=1}^{n} c_{i} ∧ {X̄_{1} = t̄_{1}, ..., X̄_{n} = t̄_{n}} ∧ {X̄ = t̄}

is ℜ-solvable. Since ∃p(t̄) ← c_{0}□p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) ∈ P and (c_{i}□p_{i}(X̄_{i})) ∈ T_{(P,ℜ)} ↑ m for each i = 1, ..., n, there exist: p_{1}(ḡ_{1}) ← c_{0_{1}}□p_{1_{1}}(ḡ_{1_{1}}), ..., p_{1_{k_{1}}}(ḡ_{1_{k_{1}}}) ∈ P ............................................... p_{n}(ḡ_{n}) ← c_{0_{n}}□p_{1_{n}}(ḡ_{1_{n}}), ..., p_{n_{kn}}(ḡ_{n_{kn}}) ∈ P and, by the T_{(P,ℜ)} definition, for each j = 1, ..., k_{i} ∃ (ĉ_{i_{j}}□p_{i_{j}}(X̄_{i_{j}})) ∈ T_{(P,ℜ)} ↑ (m − 1), such that

c_{i} = c_{0_{i}} ∧ ⋀_{j=1}^{k_{i}}{X̄_{i_{j}} = ḡ_{i_{j}}} ∧ ⋀_{j=1}^{k_{i}}{ĉ_{i_{j}}} ∧ {X̄_{i} = ḡ_{i}}

is ℜ solvable, for each i = 1, ..., n. Thus, by the inductive hypothesis (ĉ_{i_{j}}□p_{i_{j}}(X̄_{i_{j}})) ∈ T_{(P,ℜ)} ↑ (m − 1) ⟹ (ĉ_{i_{j}}□p_{i_{j}}(X̄_{i_{j}})) ∈ M_{(Unf(P),ℜ)}. Let us consider the unfolding of p(t̄) ← c_{0}□p_{1}(t̄_{1}), ..., p_{n}(t̄_{n}) in P, p(X̃) ← c_{unf} ∧ {X̃ = t̄}□p_{1_{1}}(ḡ_{1_{1}}),...,p_{n_{kn}}(ḡ_{n_{kn}}) ∈ Unf(P), where

c_{unf} = c_{0} ∧ ⋀_{i=1}^{n}{ḡ_{i} = t̄_{i}} ∧ ⋀_{i=1}^{n} c_{0_{i}}.

Since c is ℜ-solvable, and

c = c_{0} ∧ ⋀_{i=1}^{n}{X̄_{i} = t̄_{i}}∧

∧ ⋀_{i=1}^{n}\{\underbrace{c_{0_{i}} ∧ ⋀_{j=1}^{k_{i}}\{X̄_{i_{j}} = ḡ_{i_{j}}\} ∧ ⋀_{j=1}^{k_{i}}\{ĉ_{i_{j}}\} ∧ \{X̄_{i} = ḡ_{i}\}}_{c_{i}}\} ∧ \{X̄ = t̄\}.

we have that

c = \underbrace{c_{0} ∧ ⋀_{i=1}^{n}\{t̄_{i} = ḡ_{i}\} ∧ ⋀_{i=1}^{n}\{c_{0_{i}}\}}_{c_{unf}} ∧ ⋀_{i=1}^{n} ⋀_{j=1}^{k_{i}}\{X̄_{i_{j}} = ḡ_{i_{j}}\} ∧ ⋀_{i=1}^{n} ⋀_{j=1}^{k_{i}}\{ĉ_{i_{j}}\} ∧ \{X̄ = t̄\}.

is ℜ-solvable. Moreover p(X̃) ← c_{unf}□p_{1_{1}}(ḡ_{1_{1}}),..., p_{n_{kn}}(ḡ_{n_{kn}}) is true in M_{(Unf(P),ℜ)}, and, by definition, this is true if and only if for each ℜ-solution ϑ of c_{unf}, if {p_{1_{1}}(ḡ_{1_{1}})ϑ,..., p_{n_{kn}}(ḡ_{n_{kn}})ϑ} ⊆ [M_{(Unf(P),ℜ)}] then p(X̃)ϑ ∈ [M_{(Unf(P),ℜ)}]. Since, by inductive hypothesis, (ĉ_{i_{j}}□p_{i_{j}}(X̄_{i_{j}})) ∈ M_{(Unf(P),ℜ)}, then for each ℜ-solution σ of c, p_{i_{j}}(X̄_{i_{j}})σ ∈ [M_{(Unf(P),ℜ)}]. Thus, p(X̃)σ ∈ [M_{(Unf(P),ℜ)}], and therefore c□p(X̃) ∈ M_{(Unf(P),ℜ)}. ◇

As a consequence, we have proved the equivalence of P and Unf(P), namely

Corollary 3.3 Let P be a CLP program. Then M_{(P,ℜ)} = M_{(Unf(P),ℜ)}

In the next theorem we will focus on the operational behavior of Unf(P). Since M_{(P,ℜ)} = M_{(Unf(P),ℜ)}, we will see that any refutation of a goal in P, with answer constraint c_{a}, has an equivalent refutation in Unf(P) with answer constraint c′_{a}, having the same solutions w.r.t. the variables in the goal. Moreover, the refutation in Unf(P) is generally shorter than the corresponding in P.

In the following, as in the pure logic programming case [8], we will assume that the computation rule used in the refutation, always selects all the atoms in the goal.

Theorem 3.4 Let ← c□A_{1}, ..., A_{n} be a goal which has a refutation in P of length l, with answer constraint c_{a}. Then:

1. if l = 1, the goal has the same refutation in Unf(P),

2. if l > 1, the goal has a refutation in Unf(P) of length l′ < l with an equivalent (w.r.t. the solutions) answer constraint.

Proof.

1. is trivial since each unit clause in P is also in Unf(P).

2. the proof is given by induction on the refutation length.

• Base step: let l = 2, and let us suppose that

(c□A_{1}, ..., A_{n}) ⟶^{C_{1},..,C_{n}} (c′□G_{1}, ..., G_{n}) ⟶^{C_{i_{j}}} (c′_{a}□.)

where C_{i} : H_{i} ← c_{i}□G_{i} = B_{i_{1}}, ..., B_{i_{k_{i}}}. and C_{i_{j}} : H_{i_{j}} ← c_{i_{j}}□. Moreover, by definition c′ = c ⋀_{i=1}^{n}{c_{i} ∧ H_{i} = A_{i}} and c′_{a} = c′ ⋀_{i=1}^{n} ⋀_{j=1}^{k_{i}}{c_{i_{j}} ∧ B_{i_{j}} = H_{i_{j}}}. are ℜ-solvable. Let us consider the unfolding in P of each clause: H_{i} ← c_{i}□G_{i}, H_{i} ← c_{i} ⋀_{j=1}^{k_{i}}{B_{i_{j}} = H_{i_{j}} ∧ c_{i_{j}}}□. ∈ Unf(P). Since c′_{a} is ℜ-solvable, then there exists in Unf(P) a refutation of the goal of length 1, with an equivalent answer constraint.

• The inductive step is quite similar to the base one. Let us suppose that the thesis holds for l ≥ 2 and that the goal has the following refutation of length l + 1

(c□A_{1}, ..., A_{n}) ⟶^{C_{1},..,C_{n}} (c′□G_{1}, ..., G_{n}) ⟶^{C_{i_{j}}} (c′′□G_{1_{1}}, ..., G_{n_{kn}}) ⟶^{∗} (c′_{a}□.)

Then, for each i = 1, ..., n H_{i} ← c̃_{i}□G_{i_{1}}, ..., G_{i_{k_{i}}} ∈ Unf(P), and c̃_{i} = c′ ⋀_{j=1}^{k_{i}}{B_{i_{j}} = H_{i_{j}}} is ℜ-solvable. Thus, as in the base case (c□A_{1}, ..., A_{n}) ⟶ (⋀_{i=1}^{n} c̃_{i}□G_{1_{1}}, ..., G_{n_{kn}}) is a correct refutation step in Unf(P), which, by the induction hypothesis, leads trivially to the thesis. ◇

4 The Unfolding Semantics

In this section we consider the iterative application of the unfolding rule to a given CLP program. Such an application gives us an alternative way to characterize the semantics of CLP.

Let us consider a CLP program P together with the following inductive definition:

P^{0} = P

P^{i+1} = Unf(P^{i})

Since for each i, j ∈ ω, M_{P^{i}} = M_{P^{j}}, this is a collection of CLP programs which are all equivalent [8]. Thus, by considering the following set

U^{i} = {(c ∧ {X̄ = t̄}□p(X̄)) s.t p(t̄) ← c□. is a clause of P^{i}}, we can define the unfolding semantics of CLP as follows.

Definition 4.1 The unfolding semantics of a CLP program P, denoted by M, is

M = ⋃_{i∈ω} U^{i}.

Roughly speaking, since the unfolding semantics of a CLP program is a possibly infinite set of unit clauses computed by the repeated application of the unfolding rule, we claim that M is the same as the success set of P. This result is formally proved in the following theorem.

Theorem 4.1 Given a CLP program P, M = M_{(P,ℜ)}.

Proof.

• We prove that M ⊆ M_{(P,ℜ)}. This holds trivially, by definition. In fact, since (c□p(X̄)) ∈ M if and only if ∃ i ∈ ω such that p(t̄) ← c_{0}□. ∈ P^{i} and c = c_{0} ∧ {X̄ = t̄}, then (c□p(X̄)) ∈ M_{(P,ℜ)}.

• Let us suppose that M ⊂ M_{(P,ℜ)}. Thus, by definition there exists a constrained atom (c□p(X̄)) ∈ M_{(P,ℜ)} such that (c□p(X̄)) ∉ T_{(P^{i},ℜ)} ↑ 1, for each i ∈ ω (since for each i ∈ ω: U^{i} = T_{(P^{i},ℜ)} ↑ 1).

Moreover, by completeness, the goal ← c□p(X̄). has a refutation in P and its length has to be l_{0} > 0 (otherwise (c□p(X̄)) ∈ T_{(P^{0},ℜ)} ↑ 1).

By theorem 3.4, the same goal has a refutation of length l_{1} < l_{0} in P^{1}, with an equivalent answer constraint, and so on, for i = 2, 3, ..... This leads to a contradiction, from which the thesis follows. ◇

The unfolding rule for the CLP framework, is an extension of a rule originally developed for positive logic programs [8]. Similar results can be obtained by considering other unfolding rules [9] in the framework of CLP.

5 Concluding remarks

We have shown that the operational semantics of CLP leads a suitable transformation rule which allows to define a semantics equivalent to the model-theoretic one. The transformation is strongly related to the immediate consequence operator.

In fact, as in the pure logic programming case, by considering an interpretation I as a set of constrained rules (CLP clauses), we have

T_{(C,ℜ)} = Unf(C, I),

where T_{(C,ℜ)} is the immediate consequence operator associated with the clause C [8]. This result, which is inherited from the theory of pure logic programs, stresses the very close relation between the standard fixpoint semantics of CLP and the unfolding one.

Thus, many of the results on the unfolding semantics theory of pure logic programs, as given in [8], hold in the framework of CLP too. In particular, since we deal with constraints instead of substitutions, many of the previous results are much easier to prove. Many of technical lemmas on the unification theory have, in fact, a more natural and general interpretation by using constraints. Thus, we obtain much simpler and more elegant proofs for tedious theorems, such as 3.1, 3.2 and 3.3. The rational behind this remark has to be found in the role played by unification in substitution based proofs. Unification, in fact, as already argued in the introduction, is somewhat redundant, since it embodies the transformation to solved form in addition to solvability checking. In fact, from the proof viewpoint, we only need to test solvability of sets of constraints (or equations, in the case of pure logic programs).

References

[1] F. Denis and J.-P. Delahaye. Unfolding, Procedural and Fixpoint Semantics of Logic Programs. In Proc. STACS’91, 1991.

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

[3] M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. A Model-Theoretic Reconstruction of the Operational Semantics of Logic Programs. Technical Report TR 32/89, Dipartimento di Informatica, Università di Pisa, 1989. To appear in Information and Computation.

[4] M. Gabbrielli and G. Levi. Modeling answer constraints in Constraint Logic Programs. Technical Report TR 4/91, Dipartimento di Informatica, Università di Pisa, 1991.

[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 J.-L. Lassez. Constraint Logic Programming. Technical report, Department of Computer Science, Monash University, June 1986.

[7] G. Levi. Models, Unfolding Rules and Fixpoint Semantics. In R. A. Kowalski and K. A. Bowen, editors, Proc. Fifth Int’l Conf. on Logic Programming, pages 1649–1665. The MIT Press, Cambridge, Mass., 1988.

[8] G. Levi and P. Mancarella. The Unfolding Semantics of Logic Programs. Technical Report TR-13/38, Dipartimento di Informatica, Università di Pisa, 1988.

[9] H. Tamaki and T. Sato. Unfold/Fold Transformations of Logic Programs. In Sten-Åke Tarnlund, editor, Proc. Second Int’l Conf. on Logic Programming, pages 127–139, 1984.

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