Theoretical Computer Science 122 (1994) 3-47 3

Elsevier

A compositional semantics
for logic programs
A. Bossi
Dipartimento di Matematica Pura ed Applicata, Universitir di Padoua, Via Belzoni 7, I-35131 Padoua,
Italy

M. Gabbrielli, G. Levi and M.C. Meo

Dipartimento di Informatica, Uniuersitir di Piss, Corso Italia 40. 56125 Piss, Italy

Abstract

Bossi, A., M. Gabbrielli, G. Levi and M.C. Meo, A compositional semantics for logic programs,
Theoretical Computer Science 122 (1994) 3-47.

This paper considers open logic programs originally introduced as a tool to build an OR-composi-
tional semantics of logic programs. We extend the original semantic definitions in the framework of
the general approach to the semantics,of logic programs described by Gabbrielli and Levi (1991). We
first define an operational semantic$Lno6P) which models computed answer substitutions and which
is compositional w.r.t. the union 6f programs. Next, we consider the semantic domain of
Q-denotations, which are sets of clauses with a suitable equivalence relation. The fixpoint semantics
F;(P) given by Bossi and Menegus (1991) is proved equivalent to the operational semantics. From
the model-theoretic viewpoint, an Q-denotation is mapped onto a set of Herbrand interpretations,
thus leading to a definition of an R-model based on the classical notion of truth. Moreower, we
consider a particular kind of Q-models (compositional modelsL and we show that I”,(P) is
a (nonminimal) compositional Q-model. A suitable abstraction oq0,( P) is compositional and fully
abstract w.r.t. the equivalence induced by successful derivations! Finally, some applications of our
semantics are discussed. In particular, $J,( P) can be viewed as the foundation of modular program
analysis.

1. Introduction

According to a popular view on logic programming, the problem of the semantics

was solved once and for all by logicians before logic programming was even born.

Correspondence to: A Bossi, Dipartimento di Matematica Pura ed Applicata, Universita di Padova, Via
Belzoni 7, I-35131 Padova, Italy. Email addresses of the authors: bossi(@pdmatl.unipd.it, {gabbri, levi,
meo}@di.unipi.it.

0304-3975/94/$07.00 0 1994-Elsevier Science Publishers B.V. All rights reserved

4 A. Bossi et al

Namely, the only three important concepts are the program itself, the intended
interpretation (declarative semantics) and the theorem prover (operational semantics).
The program is a logic theory. The declarative semantics formalizes the application
that the program is trying to capture. It is an interpretation in the conventional logic
sense and a model of the program. Finally, the theorem prover is a proof procedure
which must be sound and complete with respect to the declarative semantics. Is that
really all there is to it?
The above view is appealing but too simple-minded to capture the difference
between theorem proving and programming. In fact, it applies to any formal system
for which there exists a sound and complete theorem prover. Theorem proving
becomes logic programming when we restrict the class of theories, for example, to
definite Horn clauses, so as to obtain a declarative semantics and a proof procedure
similar to the denotational and the operational semantics of conventional program-
ming languages. This is exactly what van Emden and Kowalski did in their seminal
paper [5.5], where the proof procedure was SLD resolution and the representative
model was the least Herbrand model. According to [SS], the semantics is a mathemat-
ical object which is defined in model-theoretic terms and which can be computed both
by a top-down and a bottom-up construction. Is the above classical and elegant result
a satisfactory solution?
The answer can be found if we first consider a different and more basic question.
What a semantics is used for? The first application of any semantics is to help
understanding the meaning of programs. Other useful applications include areas such
as program transformation and program analysis. One can argue that tens of thou-
sands of logic programmers were really helped by the declarative understanding of
their programs. One can also argue that semantics-based program transformation
and analysis do require deeper results and more elaborate theories, but still only using
basically the above-mentioned simple and straightforward semantics. The above
arguments can become more technical only if we understand which is the basic
semantic property of such formal activities as program transformation and analysis.
The answer coming from computer science is program equivalence, i.e. program
understanding is based on our ability to detect when two programs cannot be
distinguished by looking at their behaviors.
Defining an equivalence on programs = and a formal semantics Y(P) are two
strongly related tasks. A semantics Y(P) is correct w.r.t. z., if Y(P1)=9’(P2) implies
P1 zP2. Y(P) is fully abstract w.r.t. z, if the converse holds, i.e. if PI z P2 implies
Y(P,)= Y(P2). While full abstraction is known to be a desirable property for any
semantics, correctness is a must. The question on the adequacy of the van Emden and
Kowalski’s semantics can then be rephrased as follows. Is that semantics correct w.r.t.
a “natural” notion of program equivalence? And this in turn raises the problem of
choosing a satisfactory notion of program equivalence.
Equivalences can be defined by using logical arguments only. For example, one can
use model-theoretic properties, such as the set of models, the set of logical conse-
quences or the least Herbrand model, and proof-theoretic properties, such as the set of
 A compositional semantics for logic programs 5

derivable atoms. However, this would lead us nowhere, since the equivalence we need
must be based on the operational behavior and on what we can observe from
a computation. In other words, we have to learn more from computer science than
from mathematical logic! From a computer science viewpoint, once we have a formal-
ization of program execution, we have a choice for the equivalence. One important
aspect of the formalization, in addition to the inference rules which specify how
derivations are made, is the concept of observable, i.e. the property we observe in
a computation. In logic programs we can be interested in different observable
properties such as successful derivations, finite failures, computed answer substitu-
tions, partial computed answer substitutions, etc. A given choice of the observable
X induces an observational equivalence c x on programs. Namely, P, cx P2 iff P, and
Pz are observationally indistinguishable according to X. For example, if the observ-
able s denotes successful derivations, PI zS P2 iff for any goal G, G is refutable in PI iff it
is refutable in P2. If the observable c denotes computed answer substitutions, PI z:, Pz
iff for any goal G, G has the same (up to renaming) computed answers in PI and in P2.
Since the observable is the property which allows us to distinguish programs and is
also the property we want to preserve in program transformations, the most natural
choice in the case of logic programs is computed answer substitutions, which are exactly
the result of a logic program execution. Other less abstract observables, such as partial
computed answers and call patterns, might be useful in some applications, for example
in semantics-based analysis and transformation. However, a more abstract observable
like success&l derivations would fail in capturing the essence of logic programming,
even if it is the most adequate to the case of first-order theorem proving, where there is
nothing to be returned as a result of the computation.
We can now note that, as first shown in [18, 191, the van Emden and Kowalski’s
semantics is not correct w.r.t. the observational equivalence based on computed answer
substitutions, while it is correct w.r.t. the one based on successful derivations. Namely,
there exist programs which have the same least Herbrand model and yet compute
different answer substitutions. While trying to understand the meaning of programs,
when analyzing and transforming programs, this semantics cannot be taken as the
reference semantics. This is the reason why the need for a different formal semantics,
correct w.r.t. answer substitutions, was recognized by many authors, giving rise to
several new definitions (see e.g. [lo, 21,57, 18, 311). The need for better semantics was
also recognized in the case of semantics-based abstract interpretation [48, 37, 11, 31
and transformation [36, 51, where, as already mentioned, less abstract observables,
such as partial computed answers or call patterns, have sometimes to be modeled.
The same problem was recognized even earlier in relation to some extensions of
pure logic programming. In fact, the weakness of the traditional semantics is even
more serious when trying to model the behavior of extensions such as constraint or
concurrent logic programs, where the observables play a more important role. For
example, finding definitions modeling the observable behavior was, from the very
beginning, the aim of most of the research on the semantics of concurrent logic
languages (see e.g. [43, 29, 24, 53, 131). This was primarily motivated by the fact that
6 A. Bossi et al

these languages closely resemble traditional concurrent languages, whose semantics

usually model observables such as traces of input-output interactions, deadlocks, etc.
However, one additional motivation was the fact that the “logical” declarative reading
did not help the understanding of programs. Something similar took place in the case
of constraint logic programming. In fact, even if the aim was not finding a semantics
modeling the observable behavior, most of the constructions proposed by Jaffar and
Lassez [34] are different from the van Emden and Kowalski construction (i.e. they are
not %-models) and one of the proposed semantics was later proved [22] to correctly
model the answer constraint observable.
It is worth noting that it is exactly the declarative reading of logic programs which
fails in capturing the computed answers observable. In fact, even if we move from the
least Herbrand model to the set of all the models, we find that there exist programs
which have the same set of models and can still be distinguished by looking at their
computed answers (and the converse holds too). Therefore, logical equivalence is not
the same as the equivalence w.r.t. computed answers. The same statement is true for
all the equivalence relations considered in [46].
In addition to the problem of modeling observational equivalences, there exists
a very important property which does not hold in the traditional least Herbrand
model semantics, i.e. compositionality. Compositionality has to do with a (syntactic)
program composition operator 0, and holds when the semantics of the compound
construct Ci 0 C2 is defined by (semantically) composing the semantics of the constitu-
ents Ci and CZ. In the case of logic programs, the construct which raises a composi-
tionality problem is the union of clauses. The related property is sometimes called
OR-compositionality. People got interested in OR-compositional semantics [39, 49,
47,30,3 l] both for theoretical and practical purposes, such as defining the semantics
for modular versions of logic programs.
When compositions of programs is taken into account, for a given observable
property we obtain different equivalences, depending on which kind of program
composition we consider. Given an observable X and a program composition oper-
ator 0, the induced congruence Z:(~,~) is defined as follows. Pi c.(~,~)P~ iff for any
program Q, PI0Q %x P20Q,i.e. iff PI and P2 are observationally indistinguishable
under any possible context allowed by the composition operator. If the observable
property is successful derivations, we find out that the least Herbrand model is not
even OR-compositional. Still, OR-compositionality can be understood in logical
terms. In fact, the set of all the models is correct w.r.t. successful derivations and
OR-compositional [46].
Over the last few years we have developed a general approach to the semantics [23],
whose aim was modeling the observable behaviors, possibly in a compositional way,
for a variety of logic languages, ranging from positive logic programs [18-20,7], to
general logic programs [54, 271, constraint logic programs [22,32] and concurrent
constraint programs [24]. Our approach is based on the idea of choosing (equivalence
classes of) sets of clauses as semantic domains. Our denotations are then defined by
syntactic objects, as in the case of Herbrand interpretations. Denotations, that we
 A compositional semantics for logic programs I

sometimes call rc-interpretations, have some nice model-theoretic properties. How-

ever, they are not interpretations in the conventional mathematical logic sense, even if
rc-interpretations used in [18-201 can indeed be viewed as interpretations as done in
[52,38], where they were called canonical realizations. As in the case of the traditional
van Emden and Kowalski semantics, our denotations can be computed both by
a top-down construction (a success set) and by a bottom-up constructions (the least
fixpoint of suitable continuous immediate consequence operators on rc-interpreta-
tions). It is worth noting that our aim is not to define a new (artificial and futile) notion
of model. We are simply unhappy with the traditional declarative semantics, because
it characterizes the logical properties only, and we look for new notions of program
denotation useful from the programming or computer science point of view. A satis-
factory solution, even to the simple case of positive logic programs, is needed to gain
a better understanding of more practical languages, such as real Prolog [2] and its
purely declarative counterparts. A partial solution was the s-semantics [18,19], which
was the first (noncompositional) semantics correct w.r.t. computed answers and which
used sets of unit clauses as semantic domain.
In this paper we extend the s-semantics approach to compositionality, starting from
the results in [7]. Note that all the existing OR-compositional semantics (apart from
those in [31,7]) are correct w.r.t. successful derivations only [39,49,47,46,30]. Gaifman
and Shapiro [30] first introduced an OR-compositional semantics in a proof-theoretic
framework. OR-compositionality is achieved by using sets of nonunit clauses as
semantic domain. This semantics was then extended to model computed answers in
[3 11. The resulting denotation, which is also fully abstract, uses semantic domains more
complex than sets of clauses. However, the main reason why we are not happy with the
above semantics is that we want to characterize our denotations according to the van
Emden and Kowalski’s style, namely by a top-down and a bottom-up computation
process. These characterizations are in fact useful to effectively compute approxima-
tions of the denotation, as in the case of abstract interpretation. The Q-semantics [7]
was the first real compositional generalization of the s-semantics and was defined by
a fixpoint construction. This semantics is based on the notion of an Q-open program.
An Q-open program P is a program in which the predicate symbols belonging to the set
Sz are considered partially defined in P. P can be composed with other programs which
may further specify the predicates in Q. Such a composition is a generalization of
program union and is formally defined later (Definition 2.3). A typical partially defined
program is a program where the intensional definitions are completely known while
extensional definitions are only partially known and can be further specified.

Example 1.1. Let us consider the following program:

Qi = { ancestor(X, Y) :-parent(X, Y).

ancestor(X, Z) :-parent(X, Y), ancestor( Y, Z).

parent (isaac, jacob).

parent( jacob, benjamin). 1

8 A. Bossi et al.

New extensional information defining new parent tuples can be added to Q1 as

follows:
Q2 = { parent(unna, elizabeth).

parent(elizabeth, j&n). } .

The semantics of open programs must be compositional w.r.t. program union, i.e.
the semantics of Pi uP2 must be derivable from the semantics of PI and PZ.
As already noted, the least Herbrand model semantics, as originally proposed
in [55], and the computed answer substitution semantics in [l&20], are not com-
positional w.r.t. program union. For example, in Example 1.1, the atom unces-
tor(unnu, elizubeth), which belongs to the least Herbrand model of Qr u Qz, cannot be
obtained from the least Herbrand model of Q1 and Qz (see also Example 2.1). Note
that here we are interested in a composition of programs which extends the definition
of a predicate already existing, and we do not consider any overriding mechanisms. Of
course, such mechanisms are also interesting. For example, when considering pro-
grams structured by using inheritance operators, in some cases we want the new
information to replace the old one. The specific semantic treatment for inheritance by
extension and/or overriding is described in [4], and is obtained by a modification of
the framework we show here.
In this paper we generalize the semantics given in [7] for !&open programs,
following the general approach in [23]. In the specific case of L&open programs,
rc-interpretations are called n-denotations and are sets of conditional atoms, i.e.,
clauses such that all the atoms in the body are open. We give a fixpoint semantics,
which is a variation of the one proposed in [7], described in terms of Q-denotations
and an equivalent operational semantics. The resulting denotation is then character-
ized from the model-theoretic viewpoint, by defining a set of denotations which
encompass standard Herbrand models. Particular denotations are called L&models,
and are based on the standard notion of truth and on the fact that each Q-denotation
represents the set of Herbrand interpretations that can be obtained by composing the
open program with a definition for the open predicates. !&models of open programs
are introduced to obtain a unique representative denotation, computable as the least
fixpoint of a suitable continuous operator, in cases where no such representative exists
in the set of Herbrand models. Our C&models are related to the &-models defined in
[7] by means of an ad hoc notion of truth.
The rest of this paper is organized as follows. Section 1.1 contains notation and
useful definitions on the semantics of logic programs. In Section 2 we define an
operational semantics O,(P) modeling computed answer substitutions which is OR-
compositional. Section 3 introduces a suitable semantic domain for the O,(P) semantics
and defines Q-denotations which are sets of clauses modulo a suitable equivalence
relation. In Section 4 the jixpoint semantics FQ(P) is proved equivalent to the
operational semantics. Section 5 is concerned with model theory. From the model-
theoretic viewpoint, an &denotation is mapped onto a set of Herbrand interpreta-
tions, thus leading to a definition of an Q-model based on the classical notion of truth.
 A compositional semantics for logic programs 9

Moreover, we consider a particular kind of Q-models (compositional models). gfi(P)

is a (nonminimal) compositional Q-model equivalent to the model-theoretic seman-
tics defined in [7] in terms of S,-models. A suitable abstraction of O&P) is a composi-
tional Q-model which is fully abstract w.r.t. the equivalence induced by successful
derivations. A comparison between Q-models and the S,-models is made in Section 6.
Finally, Section 7 discusses some applications of our semantics and points out some
connections with other works. Some proofs are deferred to the appendix. A prelimi-
nary short version of this paper appeared in [6].

1.1. Preliminaries

The reader is assumed to be familiar with the terminology of and the basic results in
the semantics of logic programs [44,1]. Let the signature S consist of a set F of
function symbols, a finite set II of predicate symbols, a denumerable set V of variable
symbols. All the definitions in the following will assume a given signature S. Let T be
the set of terms built on F and V. Variable-free terms are called ground terms.
A substitution is a mapping 9: V+ T such that the set D( 8) = {X 13(X) #X} (domain
of 9) is finite. If WC V, we denote by 91w the restriction of 8 to the variables in W, i.e.
81w( Y) = Y for Y$ W. E denotes the empty substitution. The composition $a of the
substitutions 9 and o is defined as the functional composition. A renaming is a substi-
tution p for which there exists the inverse p-r such that pp-l =~-lp=~. The
preordering < (more general than) on substitutions is such that 96 g iff there exists 9’
such that ,%‘=a. The result of the application of the substitution 9 to a term t is an
instance of t denoted by t9. We define t < t’ (t is more general than t’) iff there exists
8 such that t9= t’. A substitution 9 is grounding for t if t9 is ground. The relation ,< is
a preorder. - denotes the associated equivalence relation (variance). A substitution
9 is a unijier of terms t and t’ if t9- t’9. It is well known that if two terms are unifiable
then they have an idempotent most general unifier which is unique up to renaming.
Therefore, mgu(t,, tz) will denote such a most general unifier of tl and t2. All the
above definitions can be extended to other syntactic expressions in the obvious way.
An atom is an object of the form p(tl, . . . . t,), where PEG, tl, . . . . &ET. A clause is
a formula of the form H :- L1, . . , L, with n 3 0, where H (the head) and L1, . . . , L, (the
body) are atoms. “:-” and “,” denote logic implication and conjunction, respectively,
and all variables are universally quantified. If the body is empty, the clause is a unit
clause. A clause H :- B1, . . , B, subsumes the clause K :-D,, . . , D, iff there exists
a substitution 9 such that H9= K and (B, 8,. .., B, 8} E (DI, . . . . Dm}. A program is
a finite set of clauses. A goal is a formula L1, . . . . L,, where each Li is an atom. By
Var(E) and Pred(E) we denote, respectively, the sets of variables and predicates
occurring in the expression E. A Herbrand interpretation I for a program P is a set of
ground atoms. The intersection M(P) of all the Herbrand models of a program P is
a model (least Herbrand model). M(P) is also the least fixpoint of a continuous
transformation Tp (immediate consequences operator) on the complete lattice of
Herbrand interpretations. If G is a goal, G A’p,R B1 , . . . , B, denotes an SLD derivation
10 A. Bossi et al.

of the resolvent B,, . . . , B, from G in the program P which uses the selection rule R and
where 9 is the composition of the mgu’s used in the derivation. If R is omitted, we
mean that any selection rule is used (and the definition is independent from the
selection rule). q denotes the empty clause, therefore G A,o denotes the refutation of
G in the program P. The computed answer substitution of a refutation G A,o is the
substitution obtained by the restriction of 9 to the variables occurring in G. G &
will denote explicitly the refutation of G in P with computed answer substitution
p. The notations 2 and r? will be used to denote tuples of terms and variables,
respectively, while B”denotes a (possibly empty) conjunction of atoms.

2. Computed answer substitution semantics for !&open programs

The operational semantics of logic programs with computed answer substitutions

as observable [l&20] can be defined as

o(P)=(P(x,, .... X,)SlP(X,,...,X,)~,O}.

The denotation of a program is a set of nonground atoms, which can be viewed as

a possibly infinite program. More precisely, a denotation is a (possibly infinite) set of
equivalence classes of clauses, or a n-interpretation according to [23]. The equiva-
lence is needed to abstract from irrelevant syntactic differences and in the above
semantics it is simply the variance relation.
The denotation of a program P is a z-interpretation I, which has the following
property. P and I are observationally equivalent with respect to any goal G. This is the
property which allows us to state that the semantics does indeed capture the observ-
able behavior [19]. The above semantics (as well as the least Herbrand model
semantics), however, is only compositional w.r.t. the conjunction of atoms in a goal or
in a clause body. In fact, the denotation of a conjunction can be obtained from the
denotation of its conjuncts. The following example shows that when considering
OR-composition (i.e. union of sets of clauses), nonground atoms (or unit clauses) are
no longer sufficient to define a compositional semantics.

Example 2.1. Let us consider the following programs:

PI ={dX):-P(X). P*={P(b).l

r(X):-s(X).

s(b).

p(a). 1.

According to the previous definition of O(P), Lo(P,)= {p(a),q(a),r(b),s(b)} and

O(P,)={p(b)}. Since 0(PluP2)={p(a),p(b),q(a),q(b),r(b),s(b)}, the semantics of
 A compositional semantics for logic programs 11

the union of the two programs cannot be obtained from the semantics of the
programs. Note that also the least Herbrand model is not compositional w.r.t.
u since, for previous programs Pi, P2 and Pi u P2, M(P) is the same as 0(P).

In order for a semantics to be compositional it must contain information in the

form of a mapping from sets of atoms to sets of atoms. This is indeed the case of the
semantics based on the closure operator [39] and on the T, operator [49,47]. If we
want a semantics expressed by the program syntax, compositionality w.r.t. union of
programs can only be obtained by choosing as semantic domain a set of (equivalence
classes of) clauses. In Example 2.1, for instance, the semantics of P, should also
contain the clause q(X):-p(X). Let us formally give the definition of the program
composition we consider.

Definition 2.2 (Q-open program). An Q-open program @-program for short) is a logic
program P together with a set 52 of predicate symbols. A predicate symbol occurring
in Sz is considered to be only partially defined in P.

Definition 2.3 (Q-union). Let PI be an S2,-program and Pz be an Q2,-program. If

(1) 52~52ius2~ and
(2) (Pred(P,)nPred(P2))z(Q2, nQ,),
then PI uR P2 is the C&open program PI u P2. Otherwise, PI uQ P2 is not defined.

The definition of any predicate symbol p~!2 in an C&open program P can always be
extended or refined. For instance, in Example 1.1 program Q1 is open w.r.t. the
predicate parent and this predicate is refined in program Q2. Therefore, a deduction
concerned with a predicate symbol of an R-open program P can be either complete
(when it takes place completely in the program P) or partial (when it terminates in
P with an atom p(E) such that p~s2 and p(f) does not unify with the head of any clause
in P). A partial deduction can be completed by the addition of new clauses. Thus, we
have a hypothetic deduction, conditional on the extension of predicate p.
Let us consider again the program PI of Example 2.1 and assume Sz= { p}. Then, the
goal r(X) produces a complete deduction only, computing the answer substitution
{X/b}. The goal q(X) produces a complete deduction computing the answer substitu-
tion {X/a}, and a hypothetical deduction returning any answer that could be com-
puted by a definition of p external to PI. The goal q(b) has one hypothetical deduction
only, conditional on the provability (outside P,) of p(b). We want to express this
hypothetical reasoning, i.e. that q(b) is refutable if p(b) is refutable. Hence, we will
consider the following operational semantics.

Definition 2.4. Let CSibe a set of predicate symbols. We define

Zd*={p(X,, . ..) X,):-p(X,, . . . ,X,) 1p~sZ, the arity of p is n and X1, . . . . X,

are distinct variables}.
12 A. Bossi et al

Definition 2.5 (Q-compositional operational semantics). Let P be a program and 52 a set

of predicate symbols. Moreover, let P* = P u I& and let R be a fair selection rule.
Then we define

Of2(P)={A:-B, )...) B,(p(X, )...) X/&&Il )...) A$+pRB1 )..., B,,

X 1, ..., Xk are distinct variables, A = p(X1, . . . , X,) $y and
Pred(B1, . . . , B,) C !2}.

Moreover, if P is an Q-open program, O,(P) is also Q-open.

Note that, for s2 = @,i.e. when all the predicates are considered completely defined,
the previous definition boils down to the definition of the s-semantics [18]. On(P) is
a set of resultants [45] obtained from goals of the form p(g) in P and is essentially the
result of the partial evaluation of P, where derivations terminate at open predicates
(i.e. predicates in Q). The set of clauses Ida in the previous definition is used to delay
the evaluation of open atoms. As shown by Proposition 2.6, this is a trick which allows
one to obtain, by using a fixed fair selection rule R, all the derivations
P(X lr ...Txk) ‘%,R I B,, . . , B, which use any selection rule R’ for Pred(B1, . . . , B,) E ~2.
Therefore, the previous definition is independent from the fair selection rule con-
sidered. Note that in the first step of the derivations we use clauses from P (instead of
from P*) because we want O,(P) to contain a clause p(g):-p(g) if and only if
p(X) App(X). The proof of the following proposition is in the appendix.

Proposition 2.6. Let R be a fair selection rule, let P* = Pvld,, x” a tuple of distinct
variables and Pred(B1, . . . . B,)GQ. Then there exists a rule R’ such that
p(Jf)z*p,R,B1 ,..., B, ifsp($&,.D, ,..., Dm&I,RB1 ,..., B, and p(Z?)ya=p(r?)S.

Example 2.7. Let PI, P2 be the Q-open programs of Example 2.1, where 52= { p}. Then

s,(P,)=(p(a),q(a),r(b),s(b),q(X):-p(X)),

%(P,)= {p(b)).
0, contains enough information to compute the semantics of the composition. In fact,

~(PluP,)~O,(PluPz)={p(a),p(b),q(a),q(b),r(b), s(b),q(X):-p(X)1
and

~n(pl~pz)=~*(~n(p1)~~n(Pz))
(see Theorem 2.13).

The congruence (z n) on programs induced by the computed answer substitution

observable when considering also the programs union, can formally be defined as
follows.
 A compositional semanticsfor logic programs 13

Definition 2.8. Let PI, P2 be Q-open programs. Then PI z R Pz if for every goal G and
for every Q-program Q s.t. PiuaQ, i= 1,2, is defined, G %P,Uoeu iff G %p,vnao and
G$r = G$ up to renaming.

Co, allows one to characterize a notion of answer substitution which enhances the
usual one, since (unresolved) atoms, with predicate symbols in Sz, are also considered.
Therefore, it is able to model computed answer substitutions in an OR-compositional
way. Indeed, Theorem 2.10 shows that a program P and its operational semantics
O,(P) are %:R equivalent. As a consequence, the semantics Q,(P) correctly captures
the computed answer substitution observable when considering also the programs
union, i.e. Co,(P) is correct w.r.t. the equivalence z R (Corollary 2.11). Theorem 2.13
shows the compositionality of the semantics w.r.t. the operator uo. The proof of
Lemma 2.12 is also in the appendix.
The proof of Lemma 2.9 is in the appendix and is an extension of the proof of the
completeness Theorem in [ 191.

Lemma 2.9. Let P be a program. Then p(?) 2,,, G1 if

l p(g) 2p,. Gz and
l there exists o=mgu(p(&p(X”)&), p(i)& =p(x”)A$o and G2a=G1

Theorem 2.10. Let P be an R-open program. Then P zfi O,(P).

Proof. We have to show that for every R-open program Q such that Lo,(P) uR Q and
P un Q are defined, G ~c,cPjva q iff G 2 PUa q, where Gy, = Gy, (up to renaming) (note
that if P un Q is defined then On(P) uR Q is also defined but the converse is not true).
By the independence from the selection rule for SLD refutations [44,1], we can
assume that the selection of the atoms is performed according to the following rule
denoted by Y:
(1) first select the nonopen atoms (i.e. the ~(2)‘s such that p$sZ),
(2) among the nonopen atoms, first select those which are added to the current
resolvent by the last inference step (i.e. those in the body of the last used clause).
We will show that, when considering successful derivations, G %Eno.JuQ,Y R in one
step iff there exists n such that G 2 PUp,y R in n steps and G9, = Ga2 (up to renaming).
The thesis follows from the above result by a straightforward inductive argument and
by definition of %a. In the following we consider resolvents as multisets, and we
denote by (G\A), B the multiset obtained from the multiset of atoms G by deleting the
atom A and by adding the multiset of atoms B. Let p(t) be the atom selected in G. If
p(f) is reduced by using a clause in Q, the thesis follows with n = 1. Otherwise let R be
defined as follows:
(1) (R = G\p(f)) 9,) B is the first resolvent (f G) in the derivation G GPUa,, q such
that Y(R)=A& and either Pred(A)ESZ or AEG. Note that by definition of Y,
Pred(B) C 52.
14 A. Bossi et al.

(2) If there does not exist an R as specified in (l), then R is the empty resolvent.
Such an R exists since we are considering finite (successful) derivations. For R as
specified in (l), we have
$1
G -'P~Q,Y R iff (by definition of R and of 9)

P(t”) %P, 9 B iff (by Lemma 2.9)

P(X) 2P,.Y & iff (by Definition 2.5 and Proposition 2.6)

p(X”)S,:-B,&!&(P) iff (by definition of -+en(PJ,Y)

G %n~~w@\p(f)b, Bzo,

where 0 = mgu( p(x)&, p(E)), Go = G9i and B2 o = B (by Lemma 2.9). For R as in (2)
the same holds with R,B,B2 and G\p(t”)=@ and this completes the proof. 0

Corollary 2.11 (Correctness). Let P, , P2 be O-open programs. Zf O,( PI) = O,( Pz) then
P1 =:R P2.

Proof. Straightforward by Theorem 2.10. 0

Lemma 2.12. Let P be a program and G be a goal. Then G Ap, R N i. G Ap, RCN, where
8’
$1VW(G)= Q’bar(G) and the derivation G -+P,Rs N is obtained from G zp,R N by changing
the order in which the atoms are selected.

Theorem 2.13 (Compositionality). Let PI be an Q,-open program, P, an S2,-open

program and let PI u,P, be dejined. Then Ofl(Onl(P1) uQOR2(P2))=OQ(P1 u,P,).

Proof. First note that, by Definition 2.5, Pred(Oo(P))cPred(P). Therefore, by

Definition 2.3, if PI uo Pz is defined then S,,(P,) uQ Lo,,(P,) is also defined.
Moreover, recall that if PI un Pz is defined, then P, u,P, is the Q-open program
PI u Pz. By Definition 2.5 and by Proposition 2.6, it is then sufficient to show that 3 R
such that

iff 3R’ such that

with Pred(B1, . . . , B2) E 52.

Let us prove the two implications separately.
 A compositional semantics for logic programs 1.5

“If”: Assume, without loss of generality, that

A l,...,Ai-1,~(t),Ai+l,...,A,~,,,(p~).~,

(A 1,...,Ai-l,B1,...,B,,Ai+l, . . ..A.)$

in one step, using the clause p( 11:-B i, . . ..B.EO~~(P~) with S=m&p(~),p(~). By

Definition 2.5 and by Proposition 2.6, 3 R such that p(g) &:P1,R Bi, . . . . B, with
p(X)y =p(l) (and hence 8=m~u(p(X”)y,p(t))). Then, by Lemma 2.9,
P(t”)%, .R B; , . . . . BL with p(t)yi =p(g)yS and B;, . . . . Bh=(B,, . . . . B,)9. Hence, in
P, there exists the derivation
A l,...,Ai-l,~(t)rAi+l,...,A,~pl,~

(A ...,Ai-l)yl,
1, B’I, . . ..BX.(Ai+l, ...,Arn)yl.
By definition of B;, . . . . Bi and since the bindings for variables in Al, . . . . A, are
determined by the variables in p(t), we have

(A 1, . . ..Ai-l.P(t”),Ai+l,...,A,)yl=(A1, . . ..Ai-l.p(t”),Ai+l,...,A,)$

and

(Al,...,At_l)lu’l,B;,...,Bb(Ai+l,...,A,)1/1.
Therefore, the thesis holds by a straightforward inductive argument.

Only if: Assume that G zp, UP2,R B1 , . . . , B, with Pred(B,, . . . , B,) c 0, and, without
loss of generality, assume that the first atom selected is p(Z) and the first clause used in
the derivation is in Pi. Since Pred(Bi , . . . , B,)cQ, by Lemma 2.12 we can assume that
the selection rule R is Y as specified in the proof of Theorem 2.10, considering as
nonopen atoms the p($s such that ~$52,. Also, the notation (G \A), B is the same as in
such a proof. Let N be defined as follows:
(1) N = (G \ p(f)) 9,) B is the first resolvent (# G) in the derivation

such that Y(N)= A&$ and either Pred(A)~Cl, or A is an atom in G,

(2) N = B1, . . , B, if there does not exist any N as specified in (1).
Note that, by definition of un, if P, v,P, is defined, then
Pred(P,) n Pred( P2) G (a, n Q,) c ~2~. Therefore, every atom A selected before N is
rewritten using a clause in PI. Moreover, note that, by definition of Y, Pred( N) E Q, .
Therefore, we can repeat the argument of the proof of Theorem 2.10 to show that
16 A. Bossi et al.

iff
0
G-, CO,(Pl),YN,

where Ga = G& . Then we have the following implications:

3
G-t PIUP2,.Iy B 1, ..., Bn iff (by definition of N and of 9’)
3, V
G -YP,,YN -+P,~P~,.YBI, . . ..B. iff (by previous iff)
$1 Y
G-t CD,(PI),Y N-P,“P~,Y&, . . ..B.,

where G9, y = G9. Therefore, by symmetry and a straightforward inductive argument,

we have that p(X)~p,,pl,yB1,...,B, iff P(~)~~,“,(~~~“~“,(~*~.~B~,...,B~ with
p(g)/I = p(x) 9, Pred(B, , . , B,) G Q and this completes the proof. 0

Note that when considering 52= 8, Theorem 2.18 is the completeness theorem of the
s-semantics in [ 1S].

3. Semantic domain for Q-open programs

In this section we formally define the semantic domain which characterizes the
above-introduced operational semantics On. Since On contains clauses (whose body
predicates are all in a), we have to accommodate clauses in the semantic domain
we use. The n-interpretations of Q-open programs will be called !2-denotations.
An Q-denotation can be viewed as a function from interpretations to interpreta-
tions since it contains conditional atoms. As usual, in the following, 52 is a set of
predicates.

Definition 3.1 (Conditional atoms). An Q-conditional atom is a clause A :-B,, . . , B,

such that Pred(B1, . . , B,) E Sz.

In order to abstract from the purely syntactical details, we have to use an equiva-
lence on conditional atoms. We use variance, considering bodies as multisets. Coarser
definitions (correct w.r.t. z*) can be used. = denotes syntactic identity.

Definition 3.2. Let c1 =A1 :-B1, . . . . B,, c2 =A2 :-D,, . . . . D, be two clauses. Then
c1 d c c2 iff there exists a substitution o and there exists ( il, . . . , in} c { 1, . . , m} such
that (A,:-Bl,..., B,)~TEA~:-D;, )..., Di,. We denote by = the equivalence induced
by f,. Moreover, we denote still by N the equivalence on sets of clauses defined as
follows. P, N P2 iff Vc2~P23cI~P1 such that c1 ?c2 and vice versa.
 A compositional semantics for logic programs 17

It is straightforward to show that <, is a preorder and therefore ‘v is an equiva-

lence. The extension of <c to N -equivalence classes is then an ordering, and in the
following will still be denoted by Q,. Note that, by the previous definition, if ci =c2
then there exists a renaming p such that the clauses tip and c2 have the same heads
and the same bodies, by considering bodies as multisets of atoms (instead of
sequences). The following is an example of the previous definitions.

Example 3.3. Let us consider the clauses

Cl PV, Y):-q(W n

c2 P(X, Y):-q(K Y),q(Z, Y),

c3 P(X, b) :+q(a, b), r(X, Y).
Then cl d Cc3, while c2 6 Cc3. Note that both ci and c2 subsume c3.

Note also that considering bodies of clauses as sets instead of multisets in the
definition of d E(i.e. considering subsumption equivalence as N) would not be correct
w.r.t. computed answer substitutions. The following is a simple counterexample.

Example 3.4. Let us consider the clauses

cl P(X, Y) :-4(X, Y), 4(X, Y),
c2 P(X, Y):-q(X, Y).
Let Pr = {cr } and P2 = {c2} be Q-open programs with s2 = {q}. If bodies of clauses are
viewed as sets, c1 and c2 could be considered equivalent (obviously ci subsumes c2 and
vice versa). However, Pr #zR P2. In fact, let Q be the program (q(X, b), q(a, Y)}. Then
P(X, Y) 4 p, up q where 9= {X/u, Y/b}, while the goal p(X, Y) in the program P2 u Q
can compute either {X/a} or {Y/b} only. Note that c1 7ic2.

Obviously N is finer than FZ~, i.e. N equivalent clauses cannot be distinguished in

any context w.r.t. the computed answer substitutions semantics. As a consequence, we
can use N in the definition of the semantic domain as follows.

Definition 3.5. The Gconditional base, GF?~,is the quotient set of all the C&conditional
atoms w.r.t. N.

Remark 3.6. In the following we will denote the equivalence class of a conditional
atom c by c itself. Moreover, any (semantic) subset I of %?*will implicitly be considered
also as an arbitrary (syntactic) a-open program ~(1) obtained by choosing for each
equivalence class CEI an arbitrary element ,u(c) as representative of c. The basic
derivation step (unfolding) is independent from the choice of p(I), i.e., N is a congru-
ence w.r.t. the unfolding operator. All the semantic operators that we will use on
subsets of (Zfi (such as Tf) can be reduced to several applications of this basic step.
Therefore, we can define any semantic operator on 1~9~ in terms of its syntactic
counterpart defined in p(Z), independently from the specific p(Z). In general, all the
18 A. Bossi et al.

definitions where a syntactic program associated with a subset of %‘* is (implicitly)

used will be independent from the choice of the syntactic object. To simplify the
notation, we will denote p(Z) by I and we will denote the syntactic and the semantic
operators by the same name.
Let us now give the formal definition of Q-denotation.

Definition 3.7 (Cl-denotations). An Q-denotation I is any subset of Ce,. The set of all
the Q-denotations is denoted by 9%.

Remark 3.8. In the following the operational semantics 0, will be formally con-
sidered as an Gdenotation. All the previously stated results for O,(P) hold also with
such a definition. In fact, in every proof we can consider syntactic clauses as represent-
atives of --equivalence classes, and hence we can obtain a proof for the case of
Q-denotations also. This is correct since, as previously discussed, the derivation step is
independent from the choice of the representative of the equivalence class.

Remark 3.9. As shown by the following example, the converse of Corollary 2.11 does
not hold, i.e. the semantics O,(P) is not fully abstract w.r.t. z R. In fact, in general, it is
not sufficient to define denotations as sets of equivalence classes of clauses. A full
abstractness result (w.r.t. z n) was obtained in [31]. However, denotations in [31] are
not sets of clauses and the result is obtained by saturating the denotation of a program
using essentially the definition of zfi (restricted to union with atoms). A similar full
abstractness result could be obtained in our case by using the zQ equivalence on the
domain.

Example 3.10. Let us consider the clauses

cl P(X) :-4(X, @,
c2 P(X) :-4(X, 0,
c3 P(X) :-dX> &I( y, 4
and let us consider the programs P1 = {cl, c2) and P2 = {c2, c3}. Note that for sZ= {q},
6J,( Pi) = Pi for i = 1,2 (considering clauses as E -equivalence classes). According to
Definition 3.2, c,$c2, c1$:c3 and ~231.~3, and hence O,( Pr ) # O,(P,). Moreover,
c1 + R c2, c1 $ R c3 and c2 #zR c3. Therefore, no equivalence on single clauses correct
w.r.t. E R can be used to identify P, and Pz. However, PI x R P2 since every answer
that can be computed using c1 can be computed using either c2 or c3.

4. Fixpoint semantics

In this section we define a fixpoint semantics .!FD(P) which is proved in Section 4.1,
to be equivalent to Co,(P). This can be achieved by defining an immediate conse-
quence operator TF on the lattice (99, G) of Q-denotations. F,(P) is the least fixpoint
of TF.
 A compositional semantics for logic programs 19

The immediate consequences operator Tf is strongly related to the derivation rule

used for C&open programs. Indeed, we define it in terms of the unfolding rule. As we
will show in Section 4.1, this allows an elegant and concise proof of the equivalence
between the operational (top-down) and the fixpoint (bottom-up) semantics. Since
T,” models the computed answers in an OR-compositional way, it can be useful for
modular (i.e. OR-compositional) bottom-up program analysis.

Definition 4.1 (Unfolding). Let P and Q be C&open programs. Then the unfolding of
P w.r.t. Q is defined as

unfp(Q)=((A:-~1,...,2,)9I~A:-B1,...,B,~P,3BI:-Zi~Q,renamedapart
for i= 1) . ..) n, s.t. 9=mgu((B1, . . . . B,), (B;, . ..) Bb))}.

Example 4.2. Let us consider the following program:

P = {p(X, Y) :-r(X), s(Y).

r(X) :-s(X).

s(Y):+q(Y).

s(a). 13

unf,(P)=(p(X, Y):-@),q(Y).

p(X, a) :-s(X).

r(X) :-q(X).

r(a).

s(a). 1.

Definition 4.3 (Immediate consequences operator) (Bossi and Menegus [7]). Let P be
an a-open program and let I be an C&denotation. Then we define

T;(Z) = unf,(Z u Idn).

Note that, for C2= 8, TF is the immediate consequence operator introduced in [ 181
whose least fixpoint is the s-semantics.

Proposition 4.4 (Bossi and Menegus [7]). TF is monotonic and continuous on the
complete lattice (9, C).

The notion
of ordinal powers for TF is defined as usual, namely
T,“TO=& TgTn+
1= TF(TFfn) and TgTo= U.aO(Tgtn). Since Tg is continuous
on (9, G), well-known results of lattice theory allow one to prove the following
proposition.
20 A. Bossi et al.

Proposition 4.5. TFro is the least fixpoint of Tp on the complete lattice (9, G).

We can then define the fixpoint semantics as follows.

Definition 4.6 (Bossi and Menegus [7])( Fixpoint semantics). Let P be an Q-open
program. The fixpoint semantics PO(P) of P is defined as FQ(P)= Tzto.

Example 4.7. Let P be the program of Example 4.2 and Sz= (4).

TFTl =u&(Z&)= {s(Y):-q(Y). s(a).},

T~~2=unf,(T~f1uZdn)={r(X):-q(X). r(a).

s(Y):-q(Y). s(a).>,

TFf3 =unf,(T; f2uZd,)= (P(X, Y):-4(X), q(Y). p(X,a):-q(X).

p(a, U-q(Y). p (a, a).

r(X) :-q(X). r(a).

s(Y):-q(Y). s(a). 1.

@-c(P)= TFf3

4.1. Unfolding semantics and equivalence results

The equivalence between the operational and the fixpoint semantics can be proved
by introducing the intermediate notion of unfolding semantics q*(P) [41,42,14].
%a( P) is obtained as the limit of the (top-down) unfolding process. Since the unfolding
rule preserves computed answers in a compositional way, aa is equivalent to the
operational semantics &&n(p).The proof of this equivalence is straightforward, since
O,(P) and aD(P) are based on the same inference rule (applied in sequence and in
parallel, respectively). On the other hand, the equivalence between aa and the
bottom-up semantics FQ(P) can be based on the relation T;(Z) = unfp(Z u I&). Let us
first formally define the unfolding semantics.

Definition 4.8. Let P be a set of clauses. Then we define

L*(P)={cEPlcEG?&}.

Definition 4.9 (Unfolding semantics). Let P be an Q-open program. Then we define the
collection of programs

PI =P,
 A compositional semantics for logic programs 21

The unfolding semantics C&(P) of the program P is defined as

Example 4.10. Let P be the program of Example 4.2 and 52= 14).

P,=P,

P2=unf,,(Puld,)={p(X, Y):-s(X),q(Y). p(X,a):ps(X).

r(X) :-q(X). r(a).

s(Y):-q(Y). s(a). 1,

P3=Ffp*(PuIdn)={p(X, Y):-q(X),q(Y). p(u, Y):-q(Y).

p(X, a) :-q(X). P(a>u).

r(X) :-q(X). r(a).

s(Y):-q(Y). s(u). 1,

&(P)=P,.

In order to prove the equivalence we need two lemmata. The first one states the
associativity of the unfolding operator.

Lemma 4.11 (Denis and Dalahaye [14]). Let P,Q, W be programs. Then
un!(unfa(W))= un?JIspcQ,(W).

Lemma 4.12. Let P be an Q-open program and let P,, be us in Dejinition 4.9. Let
W be a set of clauses and let us define unf i( W)=unf,( W) and, for n> 1,
unf F( W) = unfp(unf ;-‘( W)). Then, for n 2 1, we have
(1) unfp(unf F’(W)=unf F’(unf4W)),
(2) unfP~+,(W)=~nfp(unf~,Id,(W)),
(3) unf “,,,,n(lda) = Ida u T; t n,
(4) TfTn=l,(PJ.

Proof. All the proofs are by induction on n.

(1) Straightforward.
(2) For n= 1, we have the equalities

u~f~z(W)=unf~u,f,(pv~do) (W) (by Definition 4.9)

= unfp(unfpUId,( W)) (by Lemma 4.11).

22 A. Bossi et al.

For n>, 1, assume unfP,( W) = ~nfp(unfF;:~, ( W)). Then

w~P,+ I ( W = ~~f,n~pn~~v~~,~(
W V-v Definition 4.9)

= nnfP,WPUrd,(W) (by Lemma 4.11)

= unfp(unf~;:d,,(unfp”,d”
( W))) (by inductive hypothesis)

=~nfp(unf~~r~,(W)) (by definition of unf” and part 1).

and the thesis holds.

(3) For n= 1, we have the equalities

unfpUId,(IdR) = unfp(Zdn) u unfI,,o(Zd,) (by definition of unfolding)

= unf,(Zd,) u Zdn (by definition of Id*)

=Zd,u Tgrl (by definition of 7 and by Definition 4.3).

For nb 1, assume unf”pUId,(ZdR)=ZdRu TFtn.

unf::&,(Zdn)= unfp,Id,(Unf”Pvld,(ZdR)) (by definition of unf”+ ‘)

= unfpUId,(ZdRu TFTn) (by inductive hypothesis)

=unfp(ZdQu T~~n)uw&(Zdnu TFtn)

(by definition of unfolding)

=unfp(Zd,uT~fn)uunfId,(T~~n)uZd,
(by definition of ZdQ)

= TFTn+ 1 uZdnuunfld,(T~fn)
(by definition of t and by Definition 4.3)

= rgtn + 1 u Ido (by the following remark).

The last equality holds because, by definition of Id* and the unfolding rule,
unf&(T~fn)G T:lr~ and, since TF is monotonic, TFtns TF t n+ 1.
(4) First note that, by Definitions 4.9 and 4.3, lo(P,)= unfp,(Zdn)= TFn(@). Since
PI = P, ln(P1) = T!(O) = TFt 1. For n > 1 note that, by definition of r and by Definition
4.3, TFrn = unfp(ZdQ u Tg t n - 1). Then for n > 1 the following equalities hold:

TFtn = unfp(ZdQu TF 1 n - 1) (by the previous remark)

= unfp(unf$;&,(ZdR)) (by part 2 of Lemma 4.12)

=unfpm(Zdn) (by part 1 of Lemma 4.12)

= z,(P,) (by the previous remark)

and this completes the proof. 0

 A compositional semantics for logic programs 23

The following theorem shows the equality of the unfolding and the fixpoint
semantics.

Theorem 4.13. Let P be a program. Then gO( P) = ain( P).

Proof. By definition, FO(P)= TFfw. Note that c~T:fo iff 3n such that c~T:fn and
G@*(P) iff 3n such that CEZ~(P,J. Then the thesis follows from part (4) of Lemma
4.12. 0

The following theorem states the equality of the unfolding and the operational
semantics. The proof (in the appendix) is straightforward since both the semantics are
top-down and are based on the same inference rule.

Theorem 4.14. Let P be an Gopen program. Then O,(P)=@!,(P).

Corollary 4.15 (Equivalence). Let P be a program. Then YQ( P) = oon(P).

Proof. Straightforward by Theorems 4.13 and 4.14. q

As previously discussed, the semantics pQ(P) is zQ-equivalent to the program

P, i.e. given a program P, such that P unP, is defined, each answer computed
in Pun P, can be computed also in p*(P) un PI. Note that such a semantics
is also closed under unfolding, i.e. it contains all the results of (partial) unfoldings
performed by using clauses in it (see Definition 4.16). As a consequence, given a
set of atoms Q with Pred(Q) cf2, each answer computed in P un Q can be computed
in 9,JP) unQ by using a single “parallel” derivation step (note that, by
Theorem 5.20, considering only atoms is not a restriction). The following propositions
formalize these properties. Recall that by I7 we denote the set of all the predicate
symbols.

Definition 4.16. A set of clauses (a subset of 9,) I is u-closed iff unfI(luldn)cZ.

Lemma 4.17. Let P be a program. Then T,“ro is u-closed.

Proof. To simplify the notation let us denote TFro by F, and TFrn by F,. By
Definition 4.16, we have to prove that unfF,(F,uIdn)=F,. We show the two inclu-
sions separately.
unfF,(F,uZd,)EF,: Note that CEF, iff 3n such that CEF,,. We then prove, by
induction on n, that Vn 3 0, unfF,(F,u Idn) s F,.
For n=O, the proof is straightforward, since F,, =8 and unf(FouIdn)=@
24 A. Bossi et al.

For n > 0, we have

unfF,(F,uzd,)=unf,(un~F~_,“ldn(Fwuzdn))

(by definition of t and by Lemma 4.11)

c_unfp(Fw u Id,)
(by inductive hypothesis and by definition of I&)

= F, (by Definition 4.3 and since F, is a fixpoint).

unf,(F, u Idn) 1 Fw: We prove, by induction on n, that Q n > 0, unf,(F, u Zdn) 2 F,,.
For n = 0, the proof is straightforward, since F,, = 8.
For n>O, we have

F. = unf,(F,,_ 1u Ido) (by Definition 4.3)

c unfp(unfFa(FO u Zdn) u Id,) (by inductive hypothesis)

E unfp(unfFoUId, (F, u Idn)) (by definition of unfolding)

=unf,,s,(~,~ld,)(F~uIdn) (by Lemma 4.11)

= unfF_(Fwu Id,) (by Definition 4.3 and since F, is a fixpoint)

and this concludes the proof. Cl

Proposition 4.18. Let IEW~. Then Tyrw is the least (w.r.t. set inclusion) subset of
%?owhich is u-closed and which contains I.

Proof. T: f o is u-closed by Lemma 4.17. Note that, by Definition 4.3, for

ZG’G&,I=T~(~). Then by definition of t, 1~T~~o. Let Hc%?o, such that H is
u-closed and I G H. Let us show by induction on n that Qn, T:TnsH.
For n=O, it is obvious since T:fO=@.
For n>O, let us assume by inductive hypothesis that Tyync H. Then

TFTn+ 1 = Ty(TyTn) (by definition of 7)

c T:(H) (by inductive hypothesis)

c T;(H) (since I E H)

=H (since H is u-closed).

Since T:fo= u,,<, Tytn, the thesis holds. 0

Lemma 4.19. Let P be a u-closed set of clauses and let Q be a set of atoms with
Pred(Q)cSZ. Then, for any n> 1, TcUQtn= T$(Q)“Q.
 A compositional semantics for logic programs 25

Proof. The proof is by induction on IZ.For n=2, by Definition 4.3, we have to prove
that

~rlfp,~(~nfp,~(0))=~n~(Q)uQ.
We show the two inclusions separately. By definition of unfolding,

unfp,n(unfpua(8))=unfp(unfp(8))uQ)uQzunfp(Q)uQ.
On the other hand,

unfp,a(~nfp,a(~))=unfp(unfp(8)uQ)uQ (by definition of unfolding)

G unfp(unfp(Q) u Q) u Q (by definition of unfolding)

= unfp(unfpurd,(Q)) u Q (by definition of Zdn)

=WY,n~,~Pu~~n~(Q)uQ
(byLemma 4.11)
=efp(Q)uQ (since P is u-closed)

and the thesis holds for the base case. The proof for the inductive case is identical and
thus omitted. 0

Proposition 4.20. Let P be an Q-open program and let Q be a set of atoms with
Pred(Q)Gfi. Then for any goal G=A1,...,A,, G4’Pu,Q~ ifs there exists
B 1,...,~n4~pd~~~~ such that Y=mga((A,, . . ..A.), (B,, . . ..B.)) and
YIVnr(G)=QIVar(G).

Proof. The completeness theorem of s-semantics [lS] can be obtained as the particu-
lar case g=$!l of Theorem 2.10 and can be stated as follows. G AP q iff there exists
B l,...,B,~T$tw such that Y=mgu((A1,...,A,)(B,,...,B,)) and YIv~~(~)=QIv~~,G).
By definition of F*(P) (and a straightforward inductive argument), T!,qtco=
T”F,>:,p),,afw. Since F&P) is u-closed, by Lemma 4.19 and by definition of T,
T%,,(P&~= T!&,P, (Q)uQ and the thesis holds. 0

5. Model theory

As we have shown, the operational and fixpoint semantics of a program P define an

O-denotation IP. Let J be any set of ground atoms defining the open predicates in P.
Then (the Herbrand model) J can be viewed as a program which closes P, i.e. which
completely specifies the open predicates of P. Now Ip is a representative, in terms of
clauses, of a function which when applied to a Herbrand model J closing P, returns
the least Herbrand model of the composition Pu J. If we consider a class of possible
closures J of P, we can view ZP as a syntactic notation for the set X(ZP) of the least
Herbrand models of all the programs P u J. By abuse of notation, we will then say that
26 A. Bossi et al.

Zp is a “model” (O-model) of P iff all the Herbrand interpretations in #(lp) are models
of P. Depending on which sets J we allow to use as closures for Q-denotations we
obtain different classes of Q-models.
In this section, we first define Q-models which are obtained by using a restricted
definition %‘(Zp). Such a restriction allows to obtain a large class of !&models which
includes the standard Herbrand models. We show that the least upper bound of the
u-closed Q-models of a program P (according to a suitable ordering) is the least
Herbrand model of P. We then introduce a particular class of Q-models which are
obtained by using the more general definition of X(lp), and hence are compositional
w.r.t. uQ. We show that FQ( P) is a compositional Q-model. Finally, we prove the full
abstractness of a (compositional) model-theoretic semantics w.r.t. the equivalence
induced by the successful derivation notion of observable.

5.1. Q-models

In the following we denote by BQ the R-denotation { p(QIp~s2). We denote by

M(K) the least Herbrand model of the set of clauses K. Moreover, if I is an
Q-denotation, we denote also by M(I) the least Herbrand model of I’= {P(c) 1CEZ>,
where P(c) is any element of the equivalence class c. Clearly, M(I) is well defined since
it does not depend on the element chosen in the ‘v equivalence classes. Analogously,
we call Herbrand model of I any Herbrand model of I’.
Let us now define the Q-models.

Definition 5.1. Let I be an Q-denotation for an O-open program. Then

~‘(Z)={M(luJ)IJcA,(Z)},

where An(l)={ p(olp~SZ and p(?j is a ground instance of an atom, in a body of

a clause in I}.

Example 5.2. Let I = (p(a) :-q(b)} be an Q-denotation. Then

(1) for a=(q) ~‘(I)={~,(P(a),q(b)}},
(2) for Q=(P,q} ~‘(z)=(~,{P(a),q(b))).

Definition 5.3 (Q-model). Let P be an Q-open program and I be an Q-denotation.

I is an &?-model of P iff VJEX’(I), J is a Herbrand model of P.
Let us show an example of Q-model.

Example 5.4. Let us consider the following program:

P={q(X):-P(X)
r(X):-s(X).

s(b).

P(a). ).
 A compositional semantics for logic programs 27

Let us assume Q= { p> and consider the Q-denotation O,(P), which, according to
Definition 2.5 is

~,(P)=(q(X):-p(X),~(a),q(a),r(b),s(b)).

By Definition 5.1, &@‘(OQ(P,))=(H1, Hz, H3, . ..}. where, denoting by [p(X)] the set
of ground instances of p(X),

Hr = {p(a), q(a), r(b), s(Q),

H,= {r(b),s(b))u CPWI u CqWl.

Since HI, Hz, . . . . H, are all Herbrand models of P, by Definition 5.3 Lo,(P) is an
Q-model of P, .

In general, we can prove that O,(P) is an Q-model of P. The proof follows from
a more general result that we will give in Section 5.2 (see corollary 5.24).
Note that in Definition 5.1 we impose a restriction on the set J of ground atoms
which are added to the R-denotation I in order to completely specify the “open”
predicates. Namely, we require that J contains only atoms which unify with atoms
already in bodies of clauses in 1. The reason for such a restriction is that we want that
standard Herbrand models are also Q-models (Proposition 5.5). Clearly, if M is
a Herbrand model of the program P and N is an arbitrary set of ground atoms, Mu N
could be not a model of P. Therefore, as shown by Example 5.6, if we drop our
restriction in Definition 5.1, Proposition 5.5 does not hold anymore.

Proposition 5.5. Let P be an Q-open program. Then every Herbrund model of P is an

Q-model of P.

Proof. The proof is straightforward, since for any Herbrand interpretation I,

%‘(I) = (I}. 0

Example 5.6. Let us consider the Q-open program P = { p(u) :-q(u)}, where Q= {q}.
Then 8 is a (the least) Herbrand model of P. If, by violating the condition J c An(Z),
Ma)WV)9 8 would not be an Q-model of P because (q(u)} is not a Herbrand
model of P.

A relevant property of standard Herbrand models states that the intersection of

a set of models of a program P is always a model of P. This allows one to define the
model-theoretic semantics of P as the least Herbrand model obtained by intersecting
all the Herbrand models of P. The following example shows that this important
28 A. Bossi et al.

property does not hold any more when considering Q-models with set-theoretic
operations.

Example 5.7. Let Q= {q} and P be the following &open program:

464 1.
The O,(P)={p(b):-q(b),p(X),q(a)} and M(P)=(q(a)}u{p(~)lfis a ground term}.
By Definition 5.3 O,(P) and M(P) are Q-models of P. However, O,(P)n M(P) =
{q(a)} is not an Q-model of P.

Intuitively, the Q-model intersection property does not hold because set-theoretic
operations do not adequately model the operations on conditional atoms. Namely,
the information of an Q-denotation Ii may be contained in Z2 without Ii being
a subset of Z2. In order to define the model-theoretic semantics for Q-open programs
as a unique least u-closed Q-model, we then need a suitable partial order & on
Q-denotations. c should model the meaning of Q-denotations, in such a way
that (9, L) is a complete lattice. This can be obtained by considering c as
given in Definition 5.8. It is worth noting that the least u-closed Q-model is the
standard least Herbrand model (Proposition 5.17). Moreover, the most expressive
Q-model O,(P) is a nonminimal Q-model (see Section 5.2). The following definitions
are similar to those given in [20] for the noncompositional semantics of positive logic
programs.

Definition 5.8. Let II, I2 be Q-denotations. We define:

l I1 ~~1~ iff Vci~Zi 3~~1~ such that c2 d,ci.
l I1 EZ, iff (I, GdZ2) and (I, GdZl implies I, GZ,).
where <C is defined in Definition 3.2.

The proof of the following proposition is the same of the analogous in [20].

Proposition 5.9. The relation <d is a preorder and the relation E is an ordering.

NotethatifZ,cZz,thenZ,cZ,,sinceZ,~Z2impliesZ, ddZ2.Toshowthattheset
of Q-denotations with c is a complete lattice we need two more propositions.

Definition 5.10. Let Z be an Q-denotation. We define

 A compositional semantics for logic programs 29

Example 5.11. (a) If I= {p(X),p(a):-q(b),q(b),p(a)} then Min(Z)= {p(X), q(b)},

(b) J={q(X):-p(X),r(X)

q(b) :-p(b)

4(b):-P(X)

Min(J)={q(X):-p(X),?.(X)

q(b) :-p(X)

r(b) 1.

Proposition 5.12. Let I1 and I, be Q-denotations. Then I1 <,I2 and Z2 ddZl iff
Min(Z,)=Min(Z,).

Proof. “If”: First observe that, by Definition 3.2, if c1 = H1 :-B,, . . . , B,,

c2=H2:-D1,...,Dm and ci Gcc2, then there exists a substitution (T such that
HI o= H2 and the multiset { +B1 0, . . . , B,,G}+ is contained in the multiset
('Dl , . . . , D,} +. Considering bodies as multisets, given a clause c there exists only
a finite number up to renaming of clauses c’ which are less instantiated than c.
Moreover, the number of the atoms in the body of a clause is finite. Therefore, there
exists only a finite number of clauses which are dc than the clause c and which are not
equal up to renaming. Since an Q-denotation Z contains N equivalences classes of
clauses, Z contains no infinite descending chains c1 > c c2 > c c3.. . (where ci > c cj iff
cj Gc ci and Cj#ci). Then the thesis follows from Definitions 5.10 and 5.8.
Only if: Assume Min(Z,)#Min(Zz) and let cr~Min(Z,) \Min(Zz). Since Ii GdZ2,
3c2~Min(Z2) such that c2#c1 and c2 <Ccl. Moreover, since Z2GdZl, 3c~Min(Z,)
such that c <c c2 #cr. Then c # c1 (recall that the ccs are equivalence classes), which
contradicts the hypothesis cl~Min(Z,). 0

Definition 5.13. Let ,4 be a set of Q-denotations. We introduce the following

notations.
l VA=U,,,Z,
0 Min(/1) = Min(V/l),
0 &l=A where A=Min(/l)uV{ZEnIMin(n)~Z}.

Note that Min(/l)=Min(U/1). We can now prove the following proposition. The
proof is essentially that one in [20], rephrased by using Proposition 5.12.

Proposition 5.14. For any set A ofQ-denotations there exists the least upper bound of

A, lub(A), and lub(A)= u/i holds.

30 A. Bossi et al.

Proof. (1) U,4 is an upper bound of A: If Z is an element of A, then Z Gd 1”; in

fact VCEZ, CEU~~~ I, thus 3c’EMin(n) such that c’ 6, c, and so I <d u”, since
Min(A) s UA. Moreover, if U” <d I, then by Proposition 5.12, Mm(A)=
Min(UA) = Min(Z)~l. Therefore, by definition of DA, Z c Un.
(2) U,4 is the least upper bound of A: Let H be an upper bound of A. Since, for
every ZEA, I dd H, then UIE,, I GdH and UA ddH. Assume now H G~UA, then
Min(H)= Min(UA), and therefore Min(A)=Min(UA)~ H. Moreover, for any ZE,~
such that Min(n)~Z, Min(H)cZ, and therefore (since IL H) Zc H. Then
V{ZEAIM~~(A)GZ)GH, and therefore UASH holds. 0

Proposition 5.15. The poset of all the Q-denotations (9, E) is a complete lattice with lub
operator given by UX (Dejnition 5.13). Wo is the top element and 0 is the bottom
element.

Proof. For any set n of !&denotations, the existence of its least upper bound is
ensured by Proposition 5.14. The greatest lower bound of n is then given by
glb(A)=lub({Z~9~VZ’~A, ZEZ’}). 0

We show now that according to c ordering, the least u-closed R-model is

the standard least Herbrand model. This fact justifies our choice of the ordering
relation. Note that, also with the F ordering the glb of a set of Q-models is not an
Q-model. However, for the set of all the u-closed R-models such a property holds.
Recall that an u-closed set (Definition 4.16) of clauses S contains the set S, of all the
unit clauses which can be obtained by iterated unfoldings of clauses in S. The least
Herbrand model of S can then be obtained by considering the ground instances of the
unit clauses in S. As a consequence, each u-closed set is greater, according to
c ordering, than its least Herbrand model. This allows us to obtain the result in
Proposition 5.17.

Proposition 5.16. For any u-closed Q-model I of a program P there exists a standard
Herbrand model I’ of P such that I’ c 1.

Proof. Define I’= M(Z)EX’(Z). Then, I’ is a standard Herbrand model of P. We show

now that 1’~ I. By definition of X’(Z), since I is u-closed, I’ d d I. Assume now Z d d I’.
Then I’ = Min(Z’) = Min(Z) c Z (by Proposition 5.12). 0

Proposition 5.17. Let P be a program. Then glb( {ZEN 1I is an S&model of P>)= M(P)
(the least standard Herbrand model of P).

Proof. Note that the standard Herbrand models are ordered by set inclusion, then
apply Propositions 5.9 and 5.16. 0
 A compositional semantics for logic programs 31

5.2. Compositional models

As previously discussed, when considering model theory we are no more concerned

with computed answers, whose meaning cannot be reflected by purely logical notions
such as truth, logical consequence, etc. However, we can still be interested in the
“compositional” aspects of the (model-theoretic) semantics. Note that Q-models are
not compositional w.r.t. un. Indeed, the standard least Herbrand model M(P) is an
a-model (Proposition 5.5) and, as shown by Example 2.1, in general, M(Pi uP2)
cannot be obtained from M(P,) and M(P,). Moreover, as shown in Example 5.6, the
composition of an a-model of P1 and of an G-model of Pz is not an a-model of
PI UPZ.
Among Q-models we could then be interested in identifying a particular class of
“compositional !&?-models” for which the above properties hold. This can be achieved
by using the more general and natural definition of &?(I).

Definition 5.18 (compositional Q-model). Let P be an S&open program and I be an

Q-denotation. We define

~(Z)={M(zuJ)~Js~‘n}.

Then I is a compositional n-model of P iff VJES+‘(Z), J is a Herbrand model of P.

Clearly, since %‘(Z)S z(Z), if Z is a compositional &model then it is also an

a-model according to Definition 5.3. The vice versa does not hold. For example, in the
program P = (p(a) :-q(a)} with Sz= {q} of Example 5.6,8 (the least Herbrand model of
P) is an Q-model but is not a compositional R-model since (q(a)}EX(@).
In the following we will show some properties of compositional Q-models. We first
need the formal definition of the equivalence obtained by considering successful
derivations as observable and un as composition.

Definition 5.19. Let PI, P2 be Q-open programs. Then PI z~,~P~ iff for any Q-open
program Q such that PI uo Q and P2 uoQ are defined and for any goal G,
8
G-t Plu,Q 0 iff G ‘Pz”,Q. 0

The following theorem generalizes the result given in [31] for the case R = ZZ.

Theorem 5.20 (Gabbrielli et al. [25] ). Let PI, P2 be programs. Then PI $ o P2 ifs there
exists a set of atoms Q ~69, such that PI uoQ $@Pz uo Q. Moreover, PI +og PZ
ifs there exists a set of (ground) atoms Qz@o such that PI unQ $:,,,Pz u~Q.

Corollary 5.21 (Gabbrielli et al. C2.51). Let PI and P2 be &open programs and let
assume that programs are defined on a signature containing infinite constant symbols.
Then for any Q~47o and for any goal G, G ~P,,,Q q implies G &VnQ q iff for every
set Q C B* of (ground) atoms M( PI u Q) E M( P2 u Q).
32 A. Bossi et al.

The following proposition shows that compositional S2-models satisfy the pre-
viously sketched compositional properties. Note that the proposition does not hold
for Gmodels.

Proposition 5.22. Let PI be an S2,-open program and P2 be an R,-open program such

that PI uoPz is defined. Let Mi be a compositional ai-model of Pi such that
Pred(Mi) s Pred(P;), i = 1,2. Then
(1) MI uo Mz is defined and is a compositional Q-model of PI unPz.
(2) Let M; be a compositional S2,-model of PI. Then for any Q G&I~, and for any
goal G, G :r , u,a q implies G AM; vno q .

Proof. (1) Since P, unPz is defined, then Q,UQ,Z!LJ and

Pred(M,)nPred(Mz)~Pred(Pl)nPred(P2)zS2,nC?,. Then MI unMz is defined.
Now, let JE%‘(M, unMz). By definition of Z’, J=M(M,uM,uZ), where ZG~?~.
Observe that J is a Herbrand model of PI iff Jn%YPredCP,)= M(M1 u( JnS?‘,,,,,,,,))
= M(M1 uZl) is a Herbrand model of PI, where II = JnBa, (the last equality holds
since VA:+LEM,, Pred(L)cQ2,). Then M(M,uZ,)~%‘(M,) and since MI is a com-
positional 52,-model of PI, then M(M1 u II) and, by the previous observation, J are
Herbrand models of P, . Analogously we can prove that J is a Herbrand model of P2.
Therefore, J is a Herbrand model of PI u P2 and this completes the proof.
(2) Straightforward, by Corollary 5.21 and by observing that VQE&?~,,
M(M;uQ)E#(P~). Then, since M; is a compositional 52,-model of PI, M(M;uQ)
is a Herbrand model of P,uQ and so M(P,uQ)cM(M;uQ). 0

We show now that O,,(P) is a compositional Q-model (and hence an Gmodel).

Note that M(P)& On(P) since M(P) is the least u-closed n-model and O,(P) is
u-closed. Clearly, this ordering is strict, i.e. in general U0 (P)$ M(P). Consider for
example the program P= { p(X), p(b)}. Then O@(P)=P (considered as a denotation)
and P#M(P).

Theorem 5.23. Let P be an n-open program. Then O,(P) is a compositional R-model

of P.

Proof (by contradiction). Assume that O,(P) is not a compositional !&model of P.

Then ~JE%‘(O,(P)) such that J is not a Herbrand model of P. Then
3c=A:-B r, . . . . B,EP and 3a such that Aa is ground, Bio~J, Vi= 1, . . . . n and AafJ.
Since JEH(O,(P)),

J=M(O,(P)uZ)

=Z’u(D8109is ground, D:-D1,...,Dk~Oa(P)uZdn

and Di8EZ’, i=l,...,k 13

 A compositional semantics for logic programs 33

where ZsBo and Z’={p(f)lp~52 and p(t”)~J). Since V’i=l, . . ..n. BioEJ, there exists
Bi:-Di,l, ..., Di, k, variants of clauses in cOo(P) u I& and 3oi such that B:ai = Bio and
Di,joiEZ’, Vj= 1, ...) ki. Then, by definition of Q&P), 3(A:-D1.1, . . . . Dl,k,, . . . .
Dn,l, . . . . D,,k,)y~On(P) and 30’ such that Aya’=Aa and Vi= 1, . . . . n, Vj= 1, ...) ki,
Di,jyo’~Z’. Thus, Aya’=.4o~J which contradicts the hypothesis. 0

Corollary 5.24. Let P be an O-open program. Then O,(P) is an a-model (according to

Dejinition 5.3) of P.

Proof. The proof is straightforward from Theorem 5.23, Definitions 5.3 and 5.18. 0

In the following, we use the notation [ ] also for SZ-denotations, i.e. we denote by
[Z] the n-denotation (c~%?oj ~c’EZ, c=p(c’)S and c is ground}, where ,u(c) gives one
element of the equivalence class c. Clearly, the definition of [Z] is independent from
the choice of the element ,u(c’).
We have shown that Be(P) is a compositional Q-model. Clearly, since the
zo equivalence is finer than z~,~, the semantics Co,(P) is correct w.r.t. ~o,~, i.e. if
O,(P,)=Bn(Pz) then PI z R,gP2. Obviously, since O,(P) also models computed
answers, this semantics contains too much information to achieve also full abstract-
ness w.r.t. zR,g. In order to achieve such a result, we then need an abstraction on
O,(P).
First note that a goal G has a successful derivation iff a ground instance of G has
a successful derivation. Therefore, for successful derivations it is sufficient to consider
the ground version [I] of the denotation Z of a program. Note also that if a clause
c subsumes c’ then each successful derivation can be performed by using c instead of
c’. Moreover, tautological clauses can be deleted. Indeed, since a tautology contains in
the body, a copy of the head, if a successful derivation for the goal G in a program
P uses a tautology c then there exists also a successful derivation for G which does not
use c. All these observations allow to formally define the abstraction J&‘~(P) of @o(P)
as follows. We say that a clause c properly subsumes the clause c’ iff c subsumes c’ and
c’ does not subsume c.

Definition 5.25. Let Q be a set of ground clauses. Then we define

wcf(Q)=(c(c=A:-B1,..., B,E%‘~, Bi#Bj for 1 <i# j<n

3,4-D, ,..., D,EQ s.t. {B, ,..., B,}={D, ,..., Do>

c is not a tautology,

Jc’EQ such that c’ properly subsumes c 1.

Definition 5.26 (Model-theoretic compositional semantics). Let P be an Q-open

program. Then we define ~&‘o(P) = wcf ([cO,( P)]).
34 A. Bossi et al

For a set Q of ground clauses, wcf(Q) returns the clauses in Q, modified by deleting
repetitions of atoms in the body, which are not subsumed by other clauses in Q, and
which are not tautologies. Note that wcf(Q) is the weak canonical form [46] of Q. The
(weak) canonical form of a set P of (possibly nonground) clauses can be obtained [46]
by “partitioning the clauses of P according to subsumption equivalence, by choosing
the reduced clause for each equivalence class and then deleting those clauses which are
subsumed by some other clauses (and tautologies)“. A clause c is reduced [Sl] if it
contains no identical atoms in the body and cannot be subsumed by a nonrenaming
instance of c. Reference [46] shows that each clause is subsumption-equal (up to
renaming) to a reduced clause and that the (weak) canonical form is unique up to
renaming (considering bodies as sets). The following theorem shows the relation of
these notions with the Tp operator. Recall that two sets of clauses P and Q are weakly
subsumption equivalent if for every CEP which is not a tautology there exists C’EQ
such that c’ subsumes c and vice versa. Moreover in the following by Tp + id = T, + id
we mean that for every set of ground atoms X, Tp(X)uX = TQ(X)uX (id is the
identity).

Theorem 5.27 (Maher [46]). Let P, Q be sets of clauses. P and Q are weakly subsump-
tion equivalent ifs Tp + id = T, + id.

Lemma 5.28. Let P, Q be (possibly injinite) sets of ground clauses. Then P is weakly
subsumption equivalent to Q ifs wcf(P) = wcf(Q).

Proof. By definition of wcf, if wcf(P) is subsumption equivalent to wcf(Q) then

wcf(P)= wcf(Q). Then to prove the thesis we only need to show that wcf(P) and
P are weakly subsumption equivalent (w.s.e.). Since we are considering ground
clauses, c = A :- B, , . . . , B,subsumesc’=A:-D1 ,..., D,iff {B, ,..., B,}G(D, ,..., II,>,
and hence c and c’ are subsumption equivalent iff {B,, . . . , B, > = {Ill, . . . , Dm}. There-
fore, P and P’ are subsumption equivalent, where P’ is obtained from P by consider-
ing bodies of clauses as sets, and we have to show that wcf(P) and P’ are w.s.e. First
note that, by definition of wcf; wcf(P) = wcf(P’)cP’. Hence, we only have to show
that VC’EP’~CEWC~(P’) such that c subsumes c’. Note that since we are considering
ground clauses, for every c’ = A :- {D 1, . . . , Dm} there exists only a finite number of
different clauses ci = A :- {B1, . . . , B,} (where bodies are considered as sets) such that
(B1,...,B,}c{D1,...,D,) 1 e c i su b sumes c and not vice versa). Therefore, in P’
(‘.
there are no infinite chains c1 > c2 > ... , where c1 > cz means c1 is properly subsumed
by c2. Then, by definition of wcf, VC’EP’, 3 CEwcf( P’) such that c subsumes c’ and the
thesis holds. 0

For finite sets, the nonground version of the previous lemma was proved in [46]
(i.e. two finite sets of possibly nonground clauses are weakly subsumption equivalent
iff they have the same weak canonical form). However, note that Lemma 5.28 does not
 A compositional semantics for logic programs 35

hold if we consider possibly nonground clauses, and therefore we consider kvcf as the
weak canonical form as in [46]. A counter example can be obtained by considering
the program P given in [30]

P=(c,)A:-R(X,,X,)

c2)A:-R(X1,X*),R(X2,X1)

since in this case we have an infinite chain c1 >cz> ‘.I (cl properly subsumed by
c2 . . . ).
Theorem 5.31 shows the full abstraction result. A different fully abstract invariant
w.r.t. z~,~ was already given in [30].

Lemma 5.29. Let PI, P2 be programs. Then PI z R,g Pz ifs [PI] z R,~[ Pz].

Proof, Note that, in general, M(PuQ)=M([P]uQ) (since M(PuQ)=T,,,To=

~pl,aT~=M([P]~Q)). By Corollary 5.21, PI FZ~,~P, iff VQG&I~ M(P,uQ)=
M(P,uQ), and hence the thesis holds. 0

Lemma 5.30. Let .C?be a set of predicates and let P, W be u-closed sets of ground
clauses such that if H :-~EPU W then Pred(g)s 52. Then P %n,s W iff
wcf(P)= wcf( W).

Proof. By Lemma 5.28, since P and Ware sets of ground clauses, wcf( P) = wcf( W) iff
P and Ware weakly subsumption equivalent. By Theorem 5.27, P and Ware weakly
subsumption equivalent iff T, + id = T, + id. Moreover, by Corollary 5.21, P NN~,~W
iff VQ c 91n, M (P u Q) = M( WV Q). By hypothesis all the predicate symbols appearing
in the bodies of clauses in P and Ware contained in R. Then to prove the thesis we
only need to prove that VQC-W,, M(PuQ)=M(WuQ) iff T,+id=T,+id. We
prove the two implications separately.
“If”: SinceT,,,(X)=T,(X)uT,(X),ifT,+id=T,+idthenT,,~+id=Tw,,+id.
Since M(P)=T,to=T,+idtw, M(PuQ)=M(WuQ).
“Only if”: Let us consider a set Q of ground atoms. Note that, since P is u-closed,
M(PuQ)=TpUa(Q)=T,(Q)uQ. Analogously M(WuQ)=T,(Q)uQ. Then, since
VQ,M(PuQ)=M(WuQ), VQ set of ground atoms Tp(Q)uQ=Tw(Q)uQ, i.e.
T,+id= T,+ id and this completes the proof. 0

Theorem 5.31 (Full abstraction). Let PI, Pz be C&open programs. Then,

dn(P1)=An(P*) $7”PI =$2,sPz.
36 A. Bossi et al.

Proof. First note that, by (a particular case of) Theorem 2.10, P zOn,gOn(P) and
hence PI z,,~P, iff cO,(P,) x~,~ O,(P,). Therefore, we have the following implica-
tions:

P2 =zn,gp2 iff (by the previous observation),

flAPI) =Iz,,c”dP2) iff (by Lemma 5.29),

C~dPI)l ~:n,sr_~n(Pz)l iff (by Lemma 5.30 since [O,(P)] is

u-closed and ground),

wcf( [On(P1)]) = wcf( [O,(P,)]) iff (by Definition 5.25),

~n(P1)=~n(P2)7

and this completes the proof. q

Let us finally show that A,(P) is a compositional O-model. Then A,(P) can be
considered as the compositional model-theoretic semantics of the program P.

Lemma 5.32. Let I be an Q-denotation. Then l?(Z)=~(wcf([I])).

Proof. Note that, by definition of Herbrand model, M(Z u J) = M( [I] u J) and there-
fore X(Z)=X([Z]). Then to prove the thesis, we only need to show that
s( [Z])= ~Y(wcf( [I])). Note that, by definition of wcf, [I] and wcf( [I]) are weakly
subsumption equivalent (i.e. they have the same weak canonical form). Then, by
Theorem 5.27, Trrl+ id = TwCfC[rlJ + id. Note that, in general, T,,,(X) = T,..(X) u Tp(X).
Then, V.Z set of atoms qIIUJ +id=TwCf,,,,,,J+id, and therefore M([Z]u.Z)=
M(wcf( [Z]) u .Z) (since M(P) = Tpru). Then &‘( [Z]) = X’(wcf( [Z])), and the thesis
holds. 0

Proposition 5.33. Let P be an Q-open program. Then &o(P) is a compositional

Q-model.

Proof. By Lemma 5.32, %(0,(P))= 2(wcf([O,(P)])). By Theorem 5.23, On(P) is

a compositional Q-model of P. Therefore, by Definition 5.18, A!n(P)=wcf([Bn(P)])
is a compositional Q-model of P. 0

6. SO-models

We will now consider the relation between Q-models (Definition 5.3) and the
So-models defined in [7] on the same set of denotations. Both the Q- and &-models
are intended to capture specific operational properties, from a model-theoretic point
of view. However, S,-models are based on an ad hoc notion of truth (S,-truth) and the
 A compositional semantics for logic programs 37

least &-model is exactly F*(P). Conversely, !&models are based on the usual notion
of truth in a Herbrand interpretation through the function 2’. FQ(P) is a nonmini-
ma1 a-model.

Definition 6.1 (Bossi and Menegus [7]) (Sn-truth). Let 52 be a set of predicate symbols
and I be an Q-denotation. A definite clause c = A :- B1, . , B,, m 2 0 is SO-true in I iff
u&(Z u Zdo) E I.

SO-models are defined in the obvious way. Note that, by definition of SQ-truth, ZEN
is an &-model of P iff unfp(Z u ZdQ)E I.

Proposition 6.2. Every &-model is an Q-model (according to Definition 5.3).

Proof. The proof is similar to that of Theorem 5.23. 0

Proposition 6.3 (Bossi and Menegus [7]). If n is a nonempty set of So-models of an

C&open program P, then nMEnM is an Sn-model of P.

Proposition 6.3 allows to define the model-theoretic semantics As,(P) for a pro-
gram P in terms of the &-models as follows.

Definition 6.4 (Bossi and Menegus [7]). Let P be an Q-open program and S be the set
of all the S,-models of P. Then M,,(P)= nMESM.

Corollary 6.5. Let A be a nonempty set of So-models of an Q-open program P. Then

n MEnM is an Q-model of P.

By definition and by Proposition 6.3, Msn(P) is the least SQ-model in the lattice
(9, G) (recall that 9 is the set of all the Q-denotations). The following proposition
shows that M,“(P) is also the least S,-model in the lattice (9, c).

Proposition 6.6. Let P be a program and let S be the set of all the Sn-models of P. Then
MsO(P)=glb(S) (according to the c ordering).

Proof. By Lemma 6.3 M,,(P) is an S,-model. Moreover, since I EJ implies I FJ,

&s,(P) is a lower bound (w.r.t. c) of S. Therefore, MsII(P)=glb(S). Cl

The following theorem shows the equivalence of the least &-model M,,(P) and the
fixpoint semantics (Definition 4.6).

Theorem 6.7 (Bossi and Menegus [7]). Let P be an Q-open program. Then
6(P) = M,,(P).
38 A. Bossi et al.

Corollary 6.8. Let P be an Q-open program. Then FD(P) is an Q-model of P.

Proof. The proof is straightforward from Theorem 6.7 and Proposition 6.2. 0

It is worth noting that, since cO,( P) = FQ( P) = Ms,( P), Theorem 2.13 shows that the
least So-model Mso( P) is compositional w.r.t. Q-union of programs when considering
computed answer substitutions as observables. This result was already proved in [7]
for the MsO( P) model. Finally note that, as shown by the following example, TF is not
monotonic (and therefore it is not continuous) on the complete lattice (9, E).
However, Proposition 6.10 ensures us that gD(P) is still the least fixpoint of TF on
(9, c).

Example 6.9. Consider the program P= {p(x) :-q(x), r(b)}. Let !Z=@, Ii = (q(a), q(x)}
and 12=(r(b),q(x)}. Then Z,EZ, while T~(Il)={p(x),p(a),r(b)}$T~(12)={p(x),r(b)}.

Proposition 6.10. TFro is the least jixpoint of T; on the complete lattice (9, c).

Proof. (a) U,,,(TFfn) is a jxpoint of T g: The proof is straightforward by Proposi-

tion 4.5.
(b) UnaO TFrn is the least fixpoint of Tg: By continuity of TF, UnsO TFTn is the
least fixpoint with respect to set inclusion. Then the thesis follows, since I G J implies
IFJ. 0

7. Related work and applications

The result of our semantic construction has several similarities with the proof-
theoretic semantics defined in [30,31]. Our construction, however, is closer to the
usual characterization of the semantics of logic programs. Namely, we define a top-
down operational and a bottom-up fixpoint semantics and, last but not least, a model-
theoretic semantics which allows us to obtain a declarative characterization of
syntactically defined models. The semantics in [30] does not characterize computed
answer substitutions, while the denotation defined by the fully abstract semantics in
[31] is not a set of clauses (i.e. a program). The framework of [30,31] can be useful for
defining a program-equivalence notion, even if our more declarative (model-theoretic)
characterization is even more adequate. Moreover, the presence of an operational or
a fixpoint semantics makes our construction useful as a formal basis for program
analysis.
Another related paper is [S], where Q-open logic programs are called open theories.
Open theories are provided with a model-theoretic semantics which is based on ideas
very similar to those underlying our Definition 5.1. However, [S] does not consider
semantic definitions in the style of our U,(P) which gives a unique denotation to any
open program and does not consider computed answers as observables.
 A compositional semantics for logic programs 39

Our Q-semantics O,(P) has already been used for several applications. Let us
briefly discuss some of them.
l Suitable abstractions of the open semantics can be used to model nonstandard
observables useful for program analysis. For example, in [28] a fully abstract
semantics for partial answers is obtained essentially by considering the heads of the
clauses in U),(P). Moreover, [28] defines also an extension of the Q-semantics
which takes into account the selection rule and which allows to correctly model
those observables which depend on it. on(P) is also useful for studying new
equivalences of logic programs [26,25] based on computed answer substitutions
which are not considered in [46].
l The open semantics is useful to model incomplete knowledge bases, where new
chunks of knowledge can incrementally be assimilated, and logic languages pro-
vided with a module-like structure. Modified versions of Co,(P) allow to obtain
semantics compositional w.r.t. various composition operators. A semantic com-
positional w.r.t. a generalized inheritance operator is obtained in [4]. Static and
dynamic extension/overriding mechanisms can be expressed using the generalized
operator. Since the semantic domains are (equivalence classes of) clauses, we have
a uniform treatment of static and dynamic inheritance which in other composi-
tional semantics [9] require different semantic objects to coexist. Moreover, the
semantics in [4] is the first compositional semantics of units and inheritance which
correctly models computed answer substitutions.
l The open semantics can be considered as the semantic base for modular program
analysis. It may happen that in a system under development, not all the pieces of
the program are available for analysis at some point, but we might want to do some
analysis in any case. Clearly, this is possible only if the base semantics is modular,
i.e. compositional. Modularity helps considerably in reducing the complexity of
analysis and in proving correctness of programs, since it allows an incremental and
structured specification and verification of the software. A first use of our semantics
for modular analysis is in [12].
Let us finally remark some other interesting properties of the Q-semantics on(P)
which could be further investigated.
l By means of a syntactic device, we obtain a unique representation for a possibly
infinite set of Herbrand models when a unique representative Herbrand model does
not exist. A similar device was used in [ 1535,271 to characterize logic programs
with negation. A combination of these results with our semantics could be con-
sidered to develop a compositional semantics for programs with negation.
l Our framework is strongly related to abduction [17]. If R is the set of abducible
predicates, the abductive consequences of any goal G can be found by executing
G in Lo,(P).
l The delayed evaluation of open predicates which is typical of O,(P) can easily be
generalized to other logic languages, to achieve compositionality w.r.t. the union of
programs. In particular, this matches quite naturally the semantics of CLP and
concurrent constraint programs given in [22].
40 A. Bossi et al.

l The modification of the Bn( P) semantics developed in [4] could be used to develop
a modular analysis for programs which are structured by using inheritance mech-
anisms, according to the usual object-oriented style.

Appendix

In this appendix we give the proofs of some lemmata and theorems. Let us first
introduce some definitions about substitutions and equations. The interested reader
can see [16,40,50]. An equation is an atom s = t, where s, t are terms and = is
a predicate symbol which is interpreted as the syntactic equality over the Herbrand
universe. Given a set of equations E = {sl = tl, . . . , s, = t,}, the (most general) unifier of
(E) is a (most general) unifier of ((sl, . . . ,sn)(tl, . . . . t,)). It is well known that the
idempotent mgu of a set of equations (terms) is unique up to renaming (see e.g. [16]).
Moreover, if a set of equations E is unifiable, then there exists an idempotent mgu of E.
A solution of E is a grounding unifier of E. Two sets of equations El, E2 are equivalent
(E, =.e E,) if they have the same solutions. The lattice structure on idempotent
substitutions [16] is isomorphic to the lattice structure on equations introduced in
[40] ([SO] extends this result to include also the trivial Herbrand universe). Therefore,
we can use indifferently equations or idempotent mgu’s. In the following we will
always implicitly consider idempotent mgu’s and a nontrivial Herbrand universe.
Moreover, idempotent mgu’s are considered equal up to renaming, i.e. if 9, p = Q2,
where p is a renaming, we write (by a slight abuse of notation) 9, = QZ. 7=S denotes
a set of equations.

Definition A.l. Let 9= (Xl/tl, ..,, X,/t,} be a substitution. Then a($)= {X1 =tl, ....
x,= tn}.

Lemma A.2 (Palamidessi [SO]). Let S1, Q2 be idempotent substitutions. Then

mgu(~(4)u&%))=4mgu(&(W4)=Q2mgu(J?4)W.

Theorem A.3 (Lassez [40]). If the Herbrand universe is non trivial, then 8 is an
idempotent mgu of E if a($) z:e E.

If 9 is an idempotent mgu of E, a(8) is called the solved form of E [40].

Corollary A.4. Zf the Herbrand universe is nontrivial and El z:e EZ, then for any set of
equations E, mgu(E u El)= mgu(E u E,).

Proof. By definition of solution, if El z e E2 then E u El z e E u E2. Then the thesis

follows from Theorem A.3.

Corollary A.5. Let El, E2 be sets of equations with mgu(El)= 8 and mgu(E, 9)= y.
Then mgu(El u E2)= 9~.
 A compositional semantics for logic programs 41

Proof. We have the following equalities

mgu(E, uE,)=mgu(b(9)uE2) (by Corollary A.4, and by Theorem A.3)

= Smgu(E, 9) (by Lemma A.2)

=9y (by Definition of y)

and this completes the proof. 0

In order to prove the following results we will consider a CLP-like [33] version of
SLD derivation, denoted by -+;,R, which uses equations instead of mgu’s. The
previous stated isomorphism allows to prove the equivalence of the two versions of
SLD (see below). More precisely, given a goal p(S), G, E, where G is a set of atoms, E is
a set of equations and p(F) is the selected atom, and given a clause
c=p(Z):-B,,..., B,~P,wecandefinep(&G,E-+;,~s”=i,E,B, ,..., B,,Ginonestep
(using clause c) iff the set E u (i= t”>is unifiable. Provided that no equational atom is
considered (and hence chosen) by the selection rule and by replacing the atom p(Z) by
p(g), x”=t (where 2 are new distinct variables), we can then replace a derivation
d=(p(f) 2 P,RG’) by the equivalent derivation p(x), z=f-+;,R G, E, which uses the
same clauses as d. The equivalence is formally proved by the following result.

Lemma A.6 (Wolfram et al. [56]). Let P be a program, let -+* be defined as before and
let G=A 1, . . . . Ak be a goal, where Ai=pi(~i), i= 1, . . . . k. Let H=pl(X”,), . . . . pk(_Ck),
E={X”,=!~U...UX~,=~~) and let B={X/tIx=tE~i=ti, l<i<k}, with x”l,...,r?k
3
new distinct variables. Then G -+P,RG’ if H, E~Y~*,~H’, E’, with fl$=mgu(E’) and
G’=H’PS. Moreover, mgu(E’)(,,rC,,= QIVarCGj.

Note that the previous lemma holds for any selection rule. Then we have the
following lemma.

Lemma A.7 (Lemma 2.12). Let P be a program and let G be a goal. Then G 2r,R N ifs
8 8’
G -+P,R,N, where SIVarCG,=QiVarCG,
and the derivation G +P,R, N is obtained from
G A,,,. N by changing the order in which the atoms are selected.

Proof. Straightforward from Lemma A.6, by noting that in +;,R derivations the
computation is performed by accumulating equations and, since equations are con-
sidered as sets, the ordering in which equations are added is not relevant. 0

Proposition A.8 (Proposition 2.6). Let R be a given fair selection rule, let P * = P v Ida,
2 be new distinct variables and Pred(B,; . . . . B,)&Q. Then there exists
aruleR’suchthatp(X”)$,,,.B, ,..., B,ifSp(X”)-+,,nD, ,..., D,%:P*,RB1 ,..., B,and
p(Xl)ya=p(X)IP.
42 A. Bossi et al.

Proof. (+) The proof is straightforward by considering R’ as the selection rule

obtained from R, by eliminating in the derivation,

P(s+*p,RDl>...>
kPb+,R~l,..., B,

all the selections of atoms which are rewritten by clauses in Id,\P.

(3) In order to prove the thesis, we consider -+* derivations. By hypothesis and by
Lemma A.6, there exists a derivation d1 = p(z) -+p*,R.E, B;, . . . , Bi such that E is a set
of equations, S=mgu(E) and Bi, . . . . B,=(B;, . . . . Bk)9. Then we can define a deriv-
ation d,=p(X”) -+j!*,RF, B;, . . . , BL as follows. The first clause used in d2 is the same
clause of program P which is used to rewrite p(x) in the first step of the derivation d, .
For each atom Aj that is selected by R in a step of the derivation &, if Aj is selected by
R’ in di , then we use the same input clause, used in d, (recall that PEP *). Note that if
Aj is not selected by R’, then Pred(Aj)El& since Pred(B1,. . . , B,) c Q. Therefore, if Aj is
not selected by R’, we can use, to rewrite Aj, the input clause Pj(X”j):-pj(Xj)Elda,
where pj = Pred(Aj). Then the derivation d2 uses only clauses which are used in dl and
some clauses in Id*. Moreover, since the selection rule R is fair, if an atom Ai is
selected in a step of the derivation dl , then in the derivation d2 the atom Ai is selected
within a finite number of steps (recall that we can always rewrite an atom q(f), where
q~s2 in the derivation d2 by means of the input clause q(P) :- q( 9)). Thus, F= E u E’,
where E’ is a set of the equation (2, = f i ,..., t”,=FS},where,fori=l ,..., s, fiarenew
distinct variables, which do not occur in E. Then it is easy to check that 3a= mgu(F),
0=/?9, where p=(?,/fi, . . . . f&). Therefore, by Lemma A.6,

P(x”) -%*,&WI 3. . ..%)a.

where B1, . . . ,B,=(B;, . . ..Bh)o and p(r?)cr=p(r?)pS=p(g)S, and this concludes the
proof. 0

Lemma A.9 (Lemma 2.9). Let P be a program. Then p(Z) %p,R G1 ifs the following hold

. ~(2) %,, Gz>

l there exists a=mgu(p@),p(_?)S,), p(~)91=p(x)S20 and G20=G1.

Proof. Let us define /I = {f/f}. By Lemma A.6

~(2) %, R G2

iff
~(2) -:, R E> G

where g2 = mgu(E), G& = G2 and

P(S) %.. GI
 A compositional semantics for logic programs 43

iff
p(X),X=E ,&G,E,~==

where /?,9i = y=mgu(Eu {x”= t”}) and Gy= G1 . By definition of the unification algo-
rithm and by definition of mgu, E u {r? = f} is unifiable iff t”= x9, is unifiable iff there
exists o = mgu (p(f), p(X) Q2). Therefore, by the previous equivalence of derivations -P *
and -+,

iff

~(0 %,, GI

and there exists c = mgu( p(F),p(&&). By definition of jJ,9,, y, p(r)& =

p(&?S, =p(x”)y. Now

8*0=QngU({2q=f}) (by definition of c)

= 92mgu(({X”=5)})82) (by definition of &)

=mgu(Eu(X=f}) (by Corollary AS)

=Y (by definition of y).

Therefore, ~(~)IP,a=p(r?)y=p(t”)9~. Moreover, by definition of Gi, G, and

y, G1 = Gy = G& cr= G2 g and this completes the proof. 0

In the proof of the following theorem we use a parallel derivation and its equiva-
lence to the SLD derivation with a fair rule. Note that the equivalence of the fair SLD
derivations and the parallel derivation was already proved in [56]. In the proof we
show a simple argument for such an equivalence for the sake of completeness.

Theorem A.10 (Theorem 4.14). Let P be an Q-open program. Then O,(P) =aQ(P).

Proof. Let us denote by Ai, . . . . A, &,, B1 , . . ,, B, a parallel derivation step where

the m atoms Al,..., A, are rewritten by the m clauses Hi:-B”iEP such that
8=mgu((A,, . . . . A,) (H,, . . . . H,)) and (B”,, . . . . &,J9=B1, . . . . B,. Let us define
P* =PuZd,. By Definition 4.9 (and by a straightforward inductive argument)
p(X)&, ,, Al, . . .) A, 2p*, B Ir . . . . l3, in k steps iff p(X)yS:-Bi, . . . . B,EP,. By defini-
tion of On(P) and eQ(P), to prove the thesis it is then sufficient to show that, for
Pred(B,, . . . . B,)cQ,

p(z) Ap,#,Al, . . . . A, &*,, B1, . . . . B, iff

44 A. Bossi et al.

for a fair selection rule R. By Proposition 2.6, we can assume that R is a fair rule such
that if it selects an atom Aj in the resolvent G = A 1, . . . , A,,,, all the atoms derived by
Aj are evaluated (i.e. selected) after the atoms Ai for i = 1, . . , m, i # j. Formally, we can
define such a rule R, as follows.
Let 4 be a given bijection on the set of natural numbers. Then R, selects in every
resolvent the atom A with the minimum value $(A), where the function $(A) is defined
inductively on the length h of derivation as follows.
For h=O: If Go=A,,...,A,is the goal then t,!/(Aj)=+(j)for l<j<n.
For h>O: Assume a given value I for the atoms in G,,= Al, . . . . A,,, and let
G,+, =(A,, . . . . Ai-i,Bl, ...,B,,Ai+l, ... , A,) 9 be the resolvent obtained by replacing
Ai=&(Gh+l) by Bi, ...y B,. Then for l<k<r, ~(Bk)=~(k)+max,_<j,,(~(Aj)).
It is clear from the definition that R, is a fair rule. To simplify the notation
we assume in the following that the function C$selects atoms from left to right. Note
that

in one step iff c=p(x”)y :-Al, . . . . A,cP. Moreover, observe that if

A 1, ..., A, %*,~a&, . . ..B.

and the length of such a derivation is m, then by definition of R, for i = 1, . . , m each

atom Ai is selected in such a derivation and rewritten by a clause in P*.
Therefore, by (a slight modification of) Lemma 2.12,

P(X)~,,R~A~,...,A,~~*,R,
B1, . . ..B. in m+l steps iff

p(r?)~,p,llA1 ,..., A,A,*,,,B, ,..., B, in two steps

Observe also that if

in k<m+ 1 steps and Pred(B1, . . . . B,, Ak, . . . , A,)cQ then we can obtain an equiva-
lent derivation whose length is m + 1 steps by simply rewriting the atoms Ak, . . . , A, by
clauses in I&. Therefore, by a straightforward inductive argument, we can prove that,
for Pred(B1, . . . . B,.,Ak, . . . . A,)EQ,

p(X”)&,,A,, . . . . A,~,P*,llB1,...,B, iff

P(~?)~~,R*A~,...,A,~~‘,R,B~,...,B,

and this completes the proof. 0

 A compositional semantics for logic programs 45

References

[l] K.R. Apt, Introduction to logic programming, in: J. van Leeuwen, ed., Handbook of Theoretical
Computer Science, Vol. B: Formal Models and Semantics (Elsevier, Amsterdam, 1990) 493-574.
[2] R. Barbuti, M. Codish, R. Giacobazzi and G. Levi, Modelling prolog control, in: Proc. 19th Ann.
ACM Symp. on Principles of Programming Languages (1992) 955104.
[3] R. Barbuti, R. Giacobazzi and G. Levi, A general framework for semantics-based bottom-up
abstract interpretation of logic programs, ACM Trans. Programming Languages Systems 15 (1993)
1333181.
[4] A. Bossi, M. Bugliesi, M. Gabbrielli, G. Levi and M.C. Meo, Differential logic programming, in: Proc.
20th Ann. ACM Symp. on Principles of Programming Languages (1993) 359-370.
[S] A. Bossi and N. Cocco, Basic transformation operations which preserve computed answer substitu-
tions of logic programs, J. Logic Programming 16 (1993) 47-87.
[6] A. Bossi, M. Gabbrielli, G. Levi and M.C. Meo, Contributions to the semantics of open logic
programs, in: Proc. Internat. Conf on Fifth Generation Computer Systems 1992 (1992) 570-580.
[7] A. Bossi and M. Menegus, Una semantica composizionale per programmi logici aperti, in: P. Asirelli,
ed., Proc. 6fh Italian Conf on Logic Programming (1991) 95-109.
[S] A. Brogi, E. Lamma and P. Mello, Composing open logic programs, J. Logic and Computation, to
appear.
[9] M. Bugliesi, A declarative view of inheritance in logic programming, in: K. Apt, ed., Proc. Joint
Internat. Conf and Symp. on Logic Programming (MIT Press, Cambridge, MA, 1992) 113-130.
[lo] K.L. Clark, Predicate logic as a computational formalism, Research Report DOC 79/59, Imperial
College, Dept. of Computing, London, 1979.
[1 l] M. Codish, D. Dams and E. Yardeni, Bottom-up abstract interpretation of logic programs, Technical
Report, Dept. of Computer Science, The Weizmann Institute, Rehovot, 1990; Theoret. Comput. Sci.
124, to appear.
[12] M. Codish, SK. Debray and R. Giacobazzi, Compositional analysis of modular logic programs, in:
Proc. 20th Ann. ACM Symp. on Principles of Programming Languages (1993) 451-464.
1133 F.S. de Boer and C. Palamidessi, Concurrent logic languages: asynchronism and language compari-
son, in: S. Debray and M. Hermenegildo, eds., Proc. North American Conf on Logic Programming ‘90,
(MIT Press, Cambridge, MA, 1990) 99-114.
1141 F. Denis and J.-P. Delahaye, Unfolding, procedural and fixpoint semantics of logic programs, in:
C. Choffrut and M. Jantzen, eds., STACS 91, Lecture Notes in Computer Science, Vol. 480 (Springer,
Berlin, 1991) 51 l-522.
[15] P.M. Dung and K. Kanchanasut, A fixpoint approach to declarative semantics of logic programs, in:
E. Lusk and R. Overbeck, eds., Proc. North American Conf on Logic Programming ‘89 (MIT Press,
Cambridge, MA, 1989) 604625.
[16] E. Eder, Properties of substitutions and unifications, J. Symbolic Comput. 1 (1985) 31-46.
1171 K. Eshghi and R.A. Kowalski, Abduction compared with negation by failure, in: G. Levi and M.
Martelli, eds., Proc. 6th Internat. Conf on Logic Programming (MIT Press, Cambridge, MA, 1989)
234-254.
[lS] M. Falaschi, G. Levi, M. Martelli and C. Palamidessi, A new declarative semantics for logic languages,
in: R.A. Kowalski and K.A. Bowen, eds., Proc. 5th Internat. Conf on Logic Programming (MIT Press,
Cambridge, MA, 1988) 993-1005.
1191 M. Falaschi, G. Levi, M. Martelli and C. Palamidessi, Declarative modeling of the operational
behavior of logic languages, Theoret. Comput. Sci. 69 (1989) 2899318.
[20] 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,
Universita di Pisa, 1989; Inform. and Comput., to appear.
1213 G. Ferrand, Error diagnosis in logic programming, an adaptation of E.Y. Shapiro’s method, J. Logic
Programming 4 (1987) 1777198.
[22] M. Gabbrielli and G. Levi, Modeling answer constraints in constraint logic programs, in:
K. Furukawa, ed., Proc. Eighth Internat. Conf on Logic Programming (MIT Press, Cambridge, MA,
1991) 238-252.
46 A. Bossi et al.

~231 M. Gabbrielli and G. Levi, On the semantics of logic programs, in: J. Leach Albert, B. Monien and M.
Rodriguez-Artalejo, eds., Automata, Languages and Programming, 18th Internat. Colloquium, Lecture
Notes in Computer Science, Vol. 510 (Springer, Berlin, 1991) 1-19.
~241 M. Gabbrielli and G. Levi, Unfolding and Fixpoint Semantics of Concurrent Constraint Programs,
Theoret. Comput. Sci. 105 (1992) 85-128.
WI M. Gabbrielli, G. Levi and M.C. Meo, Observable behaviors and equivalences of logic programs,
Research Report HAS-RR-92-9E, International Institute for Advanced Study of Social Information
Science, FUJITSU LAB. Ltd., 1992.
WI M. Gabbrielli, G. Levi and M.C. Meo, Observational equivalences for logic programs, in: K. Apt, ed.,
Proc. Joint Internat. Conf: Symp. on Logic Programming (MIT Press, Cambridge, MA, 1992) 131-145.
1271 M. Gabbrielli, G. Levi and D. Turi, A two steps semantics for logic programs with negation, in: Proc.
Internat. Con& on Logic Programming and Automated Reasoning, Lecture Notes in Artificial Intelli-
gence, Vol. 624 (Springer, Berlin, 1992) 297-308.
WI M. Gabbrielli and M.C. Meo, Fixpoint semantics for partial computed answer substitutions and call
patterns, in: H. Kirchner and G. Levi, eds., Proc. 3rd Internat. Conf: on Algebraic and Logic
Programming, Lecture Notes in Computer Science, Vol. 632 (Springer, Berlin, 1992) 84-99.
~291 H. Gaifman, M.J. Maher and E.Y. Shapiro, Reactive behavior semantics for concurrent constraint
logic programs, in: E. Lusk and R. Overbeck, eds., Proc. North American Conf on Logic Programming
‘89 (MIT Press, Cambridge, MA, 1989) 553-572.
c301 H. Gaifman and E. Shapiro, Fully abstract compositional semantics for logic programs, in: Proc. 16th
Ann. ACM Symp. on Principles of Programming Languages (1989) 1344142.
c311 H. Gaifman and E. Shapiro, Proof theory and semantics of logic programs, in: Proc. 4th IEEE
Symp. on Logic In Computer Science (IEEE Computer Society Press, Silver Spring, MD, 1989)
50-62.
~321 R. Giacobazzi, SK. Debray and G. Levi, A generalized semantics for constraint logic programs, in:
Proc. Internat. Con& on Fifth Generation Computer Systems 1992 (1992) 581-591.
D31 J. Jaffar and J.-L. Lassez, Constraint logic programming, in Proc. 14th Ann. ACM Symp. on Principles
ofProgramming Languages (1987) 111-119.
c341 J. Jaffar and J.-L. Lassez, Constraint logic programming, Technical Report, Department of Computer
Science, Monash University, June 1986.
c351 K. Kanchanasut and P. Stuckey, Eliminating negation from normal logic programs, in: H. Kirchner
and W. Wechler, eds., Proc. 2nd Internat. Conf: on Algebraic and Logic Programming, Lecture Notes in
Computer Science, Vol. 463 (Springer, Berlin, 1990) 217-231.
[36] T. Kawamura and T. Kanamori, Preservation of stronger equivalence in unfold/fold logic program-
ming transformation, in: Proc. Internat. Conf on Fifth Generation Computer Systems (Institute for
New Generation Computer Technology, Tokyo, 1988) 413-422.
[37] R. Kemp and G. Ringwood, An algebraic framework for the abstract interpretation oflogic programs,
in: S. Debray and M. Hermenegildo, eds., Proc. North American Conf: on Logic Programming ‘90 (MIT
Press, Cambridge, MA, 1990) 506-520.
1381 G. Kreisel and J.L. Krivine, Elements of Mathematical Logic (Model Theory) (North-Holland,
Amsterdam, 1967).
[39] J.-L. Lassez and M.J. Maher, Closures and fairness in the semantics of programming logic, Theoret.
Comput. Sci. 29 (1984) 167-184.
[40] J.-L. Lassez, M.J. Maher and K. Marriott, Unification revisited, in: 3. Minker, ed., Foundations of
Deductive Databases and Logic Programming (Morgan Kaufmann, Los Altos, CA, 1988) 587-625.
[41] G. Levi, Models, Unfolding rules and fixpoint semantics, in: R.A. Kowalski and K.A. Bowen, eds.,
Proc. 5th Internat. Conf on Logic Programming (MIT Press, Cambridge, MA, 1988) 1649-1665.
1421 G. Levi and P. Mancarella, The unfolding semantics of logic programs, Technical Report TR-13/88,
Dipartimento di Informatica, Universita di Pisa, 1988.
[43] G. Levi and C. Palamidessi, An approach to the declarative semantics of synchronization in logic
languages, in: J.-L. Lassez, ed., Proc. 4th Internat. Co@ on Logic Programming (MIT Press,
Cambridge, MA, 1987) 877-893.
[44] J.W. Lloyd, Foundations of Logic Programming (Springer, Berlin, 2nd ed., 1987).
[45] J.W. Lloyd and J.C. Shepherdson, Partial evaluation in logic programming. J. Logic Programming 11
(1991) 2177242.
 A compositional semantics for logic programs 47

[46] M.J. Maher, Equivalences of logic programs, in: J. Minker, ed., Foundations of Deductive Databases
and Logic Programming (Morgan Kaufmann, Los Altos, CA, 1988) 627-658.
[47] P. Mancarella and D. Pedreschi, An algebra of logic programs, in: R.A. Kowalski and K.A. Bowen,
eds., Proc. 5th Internat. Conf on Logic Programming (MIT Press, Cambridge, MA, 1988) 100661023.
[48] K. Marriott and H. Ssndergaard, Semantics-based dataflow analysis of logic programs, in: G. Ritter,
ed., Information Processing 89 (North-Holland, Amsterdam, 1989) 601-606.
[49] R.A. O’Keefe, Towards an algebra for constructing logic programs, in: Proc. IEEE Symp. on Logic
Programming (1985) 1522160.
[SO] C. Palamidessi, Algebraic properties of idempotent substitutions, in: M.S. Paterson, ed., Proc. 17th
Internat. Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science,
Vol. 443 (Springer, Berlin, 1990) 3866399.
[Sl] G. Plotkin, A note on inductive generalization, Machine Intelligence, 5 (1970) 153-165.
[52] H. Rasiowa and R. Sikorski, Tne Mathematics of Metamathematics (North-Holland, Amsterdam,
1963).
1531 V.A. Saraswat and M. Rinard, Concurrent constraint programming, in: Proc. 17th ACM Symposium
on Principles of Programming Languages (1990) 232-245.
[54] D. Turi, Extending S-models to logic programs with negation, in: K. Furukawa, ed., Proc. 8th
Internat. Conf on Logic Programming (MIT Press, Cambridge, MA, 1991) 397-411.
[55] M.H. van Emden and R.A. Kowalski, The semantics of predicate logic as a programming language,
J. ACM 23 (1976) 7333742.
[56] D.A. Wolfram, M.J. Maher and J-L. Lassez, A unified treatment of resolution strategies for logic
programs, in: Sten-Ake Tarnlund, ed., Proc. 2nd Internat. Con{ on Logic Programming (1984)
263-276.
[57] S. Yamasaki, M. Yoshida and S. Doshita, A fixpoint semantics of Horn sentences based on
substitution sets, Theoret. Comput. Sci. 51 (1987) 309-324.