arXiv:cs/0107014v1 [] 10 Jul 2001

Transformations of CCP programs
SANDRO ETALLE
University of Twente and CWI
MAURIZIO GABBRIELLI
Università di Udine
and
MARIA CHIARA MEO
Università di L’Aquila
We introduce a transformation system for concurrent constraint programming (CCP). We define
suitable applicability conditions for the transformations which guarantee that the input/output
CCP semantics is preserved also when distinguishing deadlocked computations from successful
ones and when considering intermediate results of (possibly) non-terminating computations.
The system allows us to optimize CCP programs while preserving their intended meaning: In
addition to the usual benefits that one has for sequential declarative languages, the transformation
of concurrent programs can also lead to the elimination of communication channels and of synchronization points, to the transformation of non-deterministic computations into deterministic
ones, and to the crucial saving of computational space. Furthermore, since the transformation
system preserves the deadlock behavior of programs, it can be used for proving deadlock freeness
of a given program with respect to a class of queries. To this aim it is sometimes sufficient to apply
our transformations and to specialize the resulting program with respect to the given queries in
such a way that the obtained program is trivially deadlock free.
Categories and Subject Descriptors: I.2.2 [Artificial Intelligence]: Automatic Programming—
Program transformation; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages—algebraic approaches to semantics; D.1.3 [Programming Techniques]:
Concurrent Programming; D.3.2 [Programming Languages]: Language Classifications—concurrent, distributed, and parallel languages
General Terms: Languages, Theory
Additional Key Words and Phrases: Optimization, Concurrent Constraint Programming, Deadlock freeness

Author’s address: S. Etalle, Distributed and Embedded Systems group, Faculty of Computer Science, University of Twente, P.O. Box 217 7500AE Enschede - The Netherlands.
M. Gabbrielli, Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze
206, 33100 Udine, Italy, gabbri@dimi.uniud.it.
Maria Chiara Meo, Dipartimento di Matematica Pura e Applicata, Università di L’Aquila,
Loc. Coppito, 67010 L’Aquila, Italy, meo@univaq.it
Permission to make digital/hard copy of all or part of this material without fee for personal
or classroom use provided that the copies are not made or distributed for profit or commercial
advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and
notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish,
to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.
c 1999 ACM 0164-0925/99/0100-0111 $00.75
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year, Pages 1–57.

2

·

Sandro Etalle et al.

1. INTRODUCTION
Optimization techniques, in the case of logic-based languages, fall into two main
categories: on one hand, there exist methods for compile-time and low-level optimizations such as the ones presented for constraint logic programs by [Jørgensen
et al. 1991], which are usually based on program analysis methodologies (e.g. abstract interpretation). On the other hand, we find source to source transformation
techniques such as partial evaluation [Mogensen and Sestoft 1997] and more general
techniques based on the unfold and fold or on the replacement operation.
Unfold/fold transformation techniques were first introduced for functional programs in [Burstall and Darlington 1977], and then adapted to logic programming
(LP) both for program synthesis [Clark and Sickel 1977; Hogger 1981], and for program specialization and optimization [Komorowski 1982]. Tamaki and Sato [1984]
proposed a general framework for the unfold/fold transformation of logic programs,
which has remained in the years the main historical reference of the field, and has
later been extended to constraint logic programming (CLP) in [Maher 1993; Etalle
and Gabbrielli 1996; Bensaou and Guessarian 1998] (for an overview of the subject,
see the survey by Pettorossi and Proietti [1994]). As shown by a number of applications, these techniques provide a powerful methodology for the development and
optimization of large programs, and can be regarded as the basic transformations
techniques, which might be further adapted to be used for partial evaluation.
Despite a large literature in the field of declarative sequential languages, unfold/fold transformation sequences have hardly been applied to concurrent languages. Notable exceptions are the papers of Ueda and Fukurawa [1988], Sahlin
[1995], and of de Francesco and Santone [1996] (their relations with this paper are
discussed in Section 7). Also when considering partial evaluation we find only very
few recent attempts [Hosoya et al. 1996; Marinescu and Goldberg 1997; Gengler
and Martel 1997] to apply it in the field of concurrent languages.
This situation is partially due to the fact that the non-determinism and the
synchronization mechanisms present in concurrent languages substantially complicate their semantics, thus complicating also the definition of correct transformation
systems. Nevertheless these transformation techniques can be very useful also for
concurrent languages, since they allow further optimizations related to the simplification of synchronization and communication mechanisms.
In this paper we introduce a transformation system for concurrent constraint
programming (CCP) [Saraswat 1989; Saraswat and Rinard 1990; Saraswat et al.
1991]. This paradigm derives from replacing the store-as-valuation concept of von
Neumann computing by the store-as-constraint model: Its computational model
is based on a global store, which consists of the conjunction of all constraints established until that moment and expresses some partial information on the values
of the variables involved in the computation. Concurrent processes synchronize
and communicate asynchronously via the store by using elementary actions (ask
and tell) which can be expressed in a logical form (essentially implication and conjunction [Boer et al. 1997]). On one hand, CCP enjoys a clean logical semantics,
avoiding many of the complications arising in the concurrent imperative setting;
as argued in the position paper [Etalle and Gabbrieli 1998] this aspect is of great
help in the development of effective transformation tools. On the other hand,
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

3

differently from the case of other theoretical models for concurrency (e.g. the πcalculus), there exist “real” implementations of concurrent constraint languages
(notably, the Oz language [Smolka 1995] and the related ongoing Mozart project
http://www.mozart-oz.org/); thus, in contrast to other models for concurrency,
in this framework transformation techniques can be readily applied to practical
problems.
The transformation system we are going to introduce is originally inspired by
the system of Tamaki and Sato [1984]. Compared to its predecessors, it improves
in three ways: Firstly, we managed to eliminate the limitation that in a folding
operation the folding clause has to be non-recursive, a limitation which is present
in many other unfold/fold transformation systems, this improvement possibly leads
to the use of new more sophisticated transformation strategies. Secondly, the applicability conditions we propose for the folding operation are now independent from
the transformation history, making the operation much easier to understand and
to implement. In fact, following [Francesco and Santone 1996], our applicability
conditions are based on the notion of “guardedness” and can be checked locally
on the program to be folded. Finally, we introduced several new transformation
operations. It is also worth mentioning that the declarative nature of CCP allows
us to define reasonably simple applicability conditions which ensure the correctness
of our system.
We will illustrate with a practical example how our transformation system for
CCP can be even more useful than its predecessors for sequential logic languages.
Indeed, in addition to the usual benefits, in this context the transformations can also
lead to the elimination of communication channels and of synchronization points, to
the transformation of non-deterministic computations into deterministic ones, and
to the crucial saving of computational space. These improvements were possible
already in the context of GHC programs by using the system defined in [Ueda and
Furukawa 1988].
Our results show that the original and the transformed program have the same
input/output semantics in a rather strong sense, which distinguishes successful,
deadlocked and failed derivations. As a corollary, we obtain that the original program is deadlock free iff the transformed one is and this allows us to employ the
transformation system as an effective tool for proving deadlock-freeness: if, after
the transformation, we can prove or see that the process we are considering never
deadlocks (in some cases the transformation simplifies the program’s behavior so
that this can be immediately checked), then we are also sure that the original process does not deadlock either. We also consider non-terminating computations by
proving three further correctness results. The first one shows that the intermediate
results of (possibly non-terminating) computations are preserved up to logical implication, while the second one ensures full preservation of (traces of) intermediate
results, provided we slightly restrict the applicability conditions for our transformations. The third result shows that this restricted transformation system preserves
a certain kind of infinite computations (active ones). We discuss the extension of
this result to the general case, claiming that our system does not introduce any
new infinite computation.
This paper is organized as follows: in the next section we present the notation and
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

4

·

Sandro Etalle et al.

the necessary preliminary definitions, most of them regarding the CCP paradigm.
In Section 3 we define the transformation system, which consists of various different
operations (for this reason the section is divided in a number of subsections). We
will also use a working example to illustrate the application of our methodology.
Section 4 states the first main result, concerning the correctness of the transformation system, while Section 5 contains the results for non-terminating computations.
Further examples are contained in Section 6. Section 7 compares this paper to
related work in the literature and Section 8 concludes. For the sake of readability
we include in this paper only proof sketches of several results, the (rather long)
technical details being deferred to the (on-line only) Appendix.
A preliminary version of this paper appeared in [Etalle et al. 1998].
2. PRELIMINARIES
The basic idea underlying the CCP paradigm is that computation progresses via
monotonic accumulation of information in a global store. The information is produced (in form of constraints) by the concurrent and asynchronous activity of several agents which can add a constraint c to the store by performing the basic action
tell(c). Dually, agents can also check whether a constraint c is entailed by the store
by using an ask(c) action. This allows the synchronization of different agents.
Concurrent constraint languages are defined parametrically with respect to the
notion of constraint system, which is usually formalized in an abstract way following the guidelines of Scott’s treatment of information systems (see [Saraswat and
Rinard 1990]). Here, we consider a more concrete notion of constraint which is
based on first-order logic and which coincides with the one used for constraint logic
programming (e.g. see [Jaffar and Maher 1994]). This will allow us to define the
transformation operations in a more comprehensible way, while retaining a sufficient expressive power. We could equally well define the transformations in terms
of the abstract notion of constraint system given in [Saraswat and Rinard 1990]1.
Thus, assume given a signature Σ defining a set of function and predicate symbols
and associating an arity with each symbol. A constraint c is a first-order Σ-formula
built by using symbols of Σ, variables from a given (countable) set V and the logical connectives and quantifiers (∧, ∨, ¬, ∃) in the usual way. The interpretation
for the symbols in Σ is provided by a Σ-structure D consisting of a set D and an
assignment of functions and relations on D to the symbols in Σ which respect the
arities. So, D defines the computational domain on which constraints are interpreted. Usually, in order to model parameter passing, Σ is assumed to contain the
binary predicate symbol = which is interpreted as the identity in D. We will follow
this assumption, which allows us to avoid the use of most general unifiers (indeed,
for many computation domains D the most general unifier of two terms does not
exist).
The formula D |= c states that c is valid in the interpretation provided by D, i.e.
that it is true for every valuation of the free variables of c. The empty conjunction
of primitive constraints will be identified with true. We also denote by Var (e) the
set of free variables occurring in the expression e.
1 To this aim, essentially we should replace equations of the form X = Y for diagonal elements
dXY .

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

5

In the sequel, constraints will be considered up to equivalence in the domain D,
i.e. we write c1 = c2 in case D |= c1 ↔ c2 . Terms will be denoted by t, s, . . .,
variables with X, Y, Z, . . ., further, as a notational convention, t̃ and X̃ denote a
tuple of terms and a tuple of distinct variables, respectively. ∃−X̃ c stands for the
existential closure of c except for the variables in X̃ which remain unquantified.
We also assume that the reader is acquainted with the notion of substitution and
of most general unifier (see [Lloyd 1987]). We denote by eσ the result application
of a substitution σ to an expression e. Given a substitution σ, the domain of σ,
Dom(σ), isSthe finite set of variables {X | Xσ 6= X}, the range of σ is defined as
Ran(σ) = X∈Dom(σ) Var (Xσ).
The notation and the semantics of programs and agents is virtually the same
one of [Saraswat and Rinard 1990]. In particular, the k operator allows one to
express parallel composition of two agents and it is usually described in terms of
interleaving,
while non-determinism
Pn
Pn arises by introducing a (global) choice operator
ask(c
)
→
A
:
the
agent
i
i
i=1
i=1 ask(ci ) → Ai nondeterministically selects one
ask(ci ) which is enabled in the current store, and then behaves like Ai . Thus, the
syntax of CCP declarations and agents is given by the following grammar:
Declarations D ::=
ǫ | p(t̃) ← A | D,
PD
n
Agents
A ::=
stop | tell(c) |
i=1 ask(ci ) → Ai |A k A | p(t̃)
Processes
Proc ::= D.A
where c and ci ’s are constraints. Note that here we allow terms both as formal and
actual parameters.
Usually this is not the case, since the procedure call p(t̃) can be equivalently
written as p(X̃) k tell(X̃ = t̃), while the declaration p(t̃) ← A is equivalent to
p(X̃) ← A k tell(X̃ = t̃). We make this assumption only because this simplifies the
writing of programs in the examples.
Due to the presence of an explicit choice operator, as usual we assume (without
loss of generality) that each predicate symbol is defined by exactly one declaration.
A program
Pis a set of declarations. In the following examples we assume that the
operator
binds tighter than k (so, ask(a) → A k ask(b) → B + ask(d) → C means
(ask(c) → A) k (ask(b) → B + ask(d) → C)). In case some ambiguity arises we will
use brackets to indicate the scope of the operators.
An important aspect for which we slightly depart from the usual formalization
of CCP regards the notion of locality. In [Saraswat and Rinard 1990] locality is
obtained by using the operator ∃, and the behavior of the agent ∃X A is defined
like the one of A, with the variable X considered as local to it. Here we do not
use such an explicit operator: analogously to the standard CLP setting, locality is
introduced implicitly by assuming that if a process is defined by p(t̃) ← A and a
variable Y occurs in A but not in t̃, then Y has to be considered local to A.
The operational model of CCP is described by a transition system T = (Conf, →)
where configurations (in) Conf are pairs consisting of a process and a constraint
(representing the common store), while the transition relation → ⊆ Conf × Conf
is described by the (least relation satisfying the) rules R1-R4 of Table I which
should be self-explanatory. Here and in the following we assume given a set D
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

6

·

Sandro Etalle et al.
R1

hD.tell(c), di → hD.stop, c ∧ di

R2

hD.

R3

R4

Pn

i=1

ask(ci ) → Ai , di → hD.Aj , di

if j ∈ [1, n] and D |= d → cj

hD.A, ci → hD.A′ , c′ i
hD.(A k B), ci → hD.(A′ k B), c′ i
hD.(B k A), ci → hD.(B k A′ ), c′ i
hD.p(t̃), ci → hD.A k tell(t̃ = s̃), ci
Table I.

if p(s̃) ← A ∈ defnD (p)

The (standard) transition system.

of declarations and we denote by defnD (p) the set of variants2 of the (unique)
declaration in D for the predicate symbol p. Due to the presence of terms as
arguments to predicates symbols, differently from the standard setting in rule R4
parameter passing is performed by a tell action. We also assume the presence of a
renaming mechanism that takes care of using fresh variables each time a declaration
is considered3 .
We denote by →∗ the reflexive-transitive closure of the relation → defined by
the transition system, and we denote by Stop any agent which contains only stop
and k constructs. A finite derivation (or computation) containing only satisfiable
constraints is called successful if it is of the form hD.A, ci →∗ hD.Stop, di 6→ while
it is called deadlocked if it is of the form hD.A, ci →∗ hD.B, di 6→ with B different
from Stop (i.e., B contains at least one suspended agent). A derivation producing
eventually false is called failed. Note that we consider here the so called “eventual
tell” CCP, i.e. when adding constraints to the store (via tell operations) there
is no consistency check. Our results could be adapted to the CCP language with
consistency check (“atomic tell” CCP) by minor modifications of the transformation
operations.
3. THE TRANSFORMATION
In order to illustrate the application of our method we will adopt a working example.
We consider an auction problem in which two bidders participate: bidder a and
bidder b; each bidder takes as input the list of the bids of the other one and produces
as output the list of his own bids. When one of the two bidders wants to quit
the auction, it produces in its own output stream the token quit. This protocol
is implemented by the following program AUCTION. Here and in the following
examples we do not make any assumption on the specific constraint domain being
used, apart from the fact that it should allow us to use lists of elements. This
is the case for most existing general purpose constraint languages, which usually
incorporate also some arithmetic domain (see [Jaffar and Maher 1994]).
auction(LeftBids,RightBids) ← bidder a([0|RightBids],LeftBids) k bidder b(LeftBids,RightBids)
2A

variant of a declaration d is obtained by replacing the tuple X̃ of all the variables appearing
in d for another tuple Ỹ.
3 For the sake of simplicity we do not describe this renaming mechanism in the transition system.
The interested reader can find in [Saraswat and Rinard 1990; Saraswat et al. 1991] various formal
approaches to this problem.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

7

bidder a(HisList, MyList) ←
ask(∃HisBid,HisList′ HisList = [HisBid|HisList’] ∧ HisBid = quit) → stop
+ ask(∃HisBid,HisList′ HisList = [HisBid|HisList’] ∧ HisBid 6= quit) →
(tell(HisList = [HisBid|HisList’]) k
make new bid a(HisBid,MyBid) k
ask(MyBid = quit) → (tell(MyList = [MyBid|MyList’]) k broadcast(“a quits”))
+ ask(MyBid 6= quit) → (tell(MyList = [MyBid|MyList’]) k
tell(MyBid 6= quit) k
bidder a(HisList’,MyList’)))
plus an analogous definition for bidder b.

Here, the agent make new bid a(HisBid,MyBid) is in charge of producing a new offer
in presence of the competitor’s offer HisBid; the agent will produce MyBid = quit if
it evaluates that HisBid is too high to be topped, and decides to leave the auction.
This agent could be further specified by using arithmetic constraints. In order to
avoid deadlock, auction initializes the auction by inserting a fictitious zero bid in
the input of bidder a. Notice that in the above program the agent tell(HisList =
[HisBid|HisList’]) is needed to bind the local variables (HisBid, HisList’) to the global
one (HisList): In fact, as a result of the operational semantics, such a binding is
not performed by the ask agent. On the contrary the agent tell(MyBid 6= quit)
is redundant: We have introduced it in order to slightly simplify the following
transformations (the transformations remain possible also without such a tell).
The introduction of redundant tell’s is a transformation operation which will be
formally defined in Subsection 3.4.
3.1 Introduction of a new definition
The introduction of a new definition is virtually always the first step of a transformation sequence. Since the new definition is going to be the main target of the
transformation operation, this step will actually determine the very direction of the
subsequent transformation, and thus the degree of its effectiveness.
Determining which definitions should be introduced is a very difficult task which
falls into the area of strategies. To give a simple example, if we wanted to apply
partial evaluation to our program with respect to a given agent A (i.e. if we wanted
to specialize our program so that it would execute the partially instantiated agent
A in a more efficient way), then a good starting point would most likely be the
introduction of the definition p(X̃) ← A, where X̃ is an appropriate tuple of variables
and p is a new predicate symbol. A different strategy would probably determine
the introduction of a different new definition. For a survey of the other possibilities
we refer to [Pettorossi and Proietti 1994].
In this paper we are not concerned with the strategies, but only with the basic
transformation operations and their correctness: we aim at defining a transformation system which is general enough so to be applied in combination with different
strategies.
In order to simplify the terminology and the technicalities, we assume that these
new declarations are added once for all to the original program before starting the
transformation itself. Note that this is clearly not restrictive. As a notational convention we call D0 the program obtained after the introduction of new definitions.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

8

·

Sandro Etalle et al.

In the case of program AUCTION, we assume that the following new declarations
are added to the original program.
auction left(LastBid) ← tell(LastBid 6= quit) k bidder a([LastBid|Bs],As) k bidder b(As,Bs).
auction right(LastBid) ← tell(LastBid 6= quit) k bidder a(Bs,As) k bidder b([LastBid|As],Bs).

The agent auction left(LastBid) engages an auction starting from the bid LastBid
(which cannot be quit) and expecting the bidder “a” to be the next one in the bid.
The agent auction right(LastBid) is symmetric.
3.2 Unfolding
The first transformation we consider is the unfolding. This operation consists essentially in the replacement of a procedure call by its definition. The syntax of CCP
agents allows us to define it in a very simple way by using the notion of context. A
context, denoted by C[ ], is simply an agent with a “hole”, where the hole can contain
any expression of type agent. So, for example, [ ] k A and ask(c) → A + ask(b) → [ ]
are contexts, while ask(a) → A + [ ] is not. C[A] denotes the agent obtained by
replacing the hole in C[ ] for the agent A, in the obvious way.
Definition 3.1 (Unfolding). Consider a set of declarations D containing
d : H ← C[p(t̃)]
u : p(s̃) ← B
Then unfolding p(t̃) in d consists in replacing d by
d′ : H ← C[B k tell(t̃ = s̃)]
in D. Here d is the unfolded definition and u is the unfolding one; d and u are
assumed to be renamed so that they do not share variables.
After an unfolding we often need to simplify some of the newly introduced tell’s
in order to “clean up” the resulting declarations. This is accomplished via a tell
elimination. Recall that a most general unifier σ of the terms t and s is called
relevant if (Dom(σ) ∪ Ran(σ)) ⊆ Var(t, s).
Definition 3.2 (Tell Elimination and Tell Introduction). The declaration
d : H ← C[tell(s̃ = t̃) k B]
can be transformed via a tell elimination into
d′ : H ← C[Bσ]
where σ is a relevant most general unifier of s̃ and t̃, provided that the variables in
the domain of σ do not occur neither in C[ ] nor in H. This operation is applicable
either when the computational domain D admits a most general unifier, or when s̃
and t̃ are sequences of distinct variables, in which case σ is simply a renaming. On
the other hand, the declaration
d : H ← C[Bσ]
can be transformed via a tell introduction into
d′ : H ← C[tell(X̃ = X̃σ) k B]
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

9

provided that σ is a substitution such that X̃ = Dom(σ) and Dom(σ) ∩ (Var (C[ ], H)∪
Ran(σ)) = ∅.
Notice that, in particular, we can always exchange C[tell(true) k A] with C[A]
and vice-versa. The presence of Ran(σ) in the above condition is needed to ensure
that σ is idempotent: in fact, using substitutions σ of the form X/f (X) would
not be correct in general. In practice, the constraints on the domain of σ can be
weakened by appropriately renaming some local variables; this is also shown in the
upcoming example. In fact, if all the occurrences of a local variable in C[ ] are in
choice branches different from the one the “hole” lies in, then we can safely rename
apart each one of these occurrences.
In our AUCTION example, we start working on the definition of auction right, and
we unfold the agent bidder b([LastBid|As], Bs) and then we perform the subsequent
tell eliminations (we eliminate the tells introduced by the unfolding). The result of
these operations is the following program.
auction right(LastBid) ← tell(LastBid 6= quit) k
bidder a(Bs, As) k
ask(∃HisBid,HisList′ [LastBid|As] = [HisBid|HisList’] ∧ HisBid = quit) → stop
+ ask(∃HisBid,HisList′ [LastBid|As] = [HisBid|HisList’] ∧ HisBid 6= quit) →
tell([LastBid|As] = [HisBid|HisList’]) k
make new bid b(HisBid,MyBid) k
ask(MyBid = quit) → tell(Bs = [MyBid|Bs’]) k broadcast(“b quits”)
+ ask(MyBid 6= quit) → tell(Bs = [MyBid|Bs’]) k
tell(MyBid 6= quit) k
bidder b(HisList’,Bs’)

3.3 Backward Instantiation
The new operation of backward instantiation, is somehow similar to the one of
unfolding. We immediately begin with its definition.
Definition 3.3 (Backward instantiation). Let D be a set of definitions and
d : H ← C[p(t̃)]
b : p(s̃) ← tell(c) k B
be two definitions of D. The backward instantiation of p(t̃) in d consists in replacing
d by d′ , which is either
d′ : H ← C[p(t̃) k tell(c) k tell(t̃ = s̃)]
or
d′ : H ← C[p(t̃) k tell(t̃ = s̃)]
(it is assumed here that d and b are renamed so that they have no variables in
common).
More generally, the operation can also be applied when b is not of the form
p(s̃) ← tell(c) k B by considering c to be true.
Intuitively, this operation can be regarded as a “half-unfolding” for the following
reason: performing an unfolding is equivalent to applying a derivation step to the
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

10

·

Sandro Etalle et al.

atomic agent under consideration, here we do not quite do it, yet we carry out (part
of) the two first phases that the derivation step requires.
In the Section 6 we will show an application of this operation (Example 6.2).
3.4 Ask and Tell Simplification
A new important operation is the one which allows us to modify the ask guards
and the tell’s occurring in a program. Let us call produced constraint of C[ ] the
conjunction of all the constraints appearing in ask and tell actions which can be
evaluated before [ ] is reached (in the context C[ ]). Now, if a is the produced
constraint of C[ ] and D |= a → c, then clearly we can simplify an agent of the form
C[ask(c) → A+ask(d) → B] to C[ask(true) → A+ask(d) → B]4 . Moreover, under the
previous hypothesis, we can clearly transform C[tell(c) k A] to C[A] and, conversely,
C[A] to C[tell(c) k A] (as previously mentioned, this latter transformation consisting
in the introduction of a redundant tell might be needed to prepare a program for
the folding operation).
In general, if a is the produced constraint of C[ ] and for some constraint c′ we
have that D |= ∃−Z̃ (a ∧ c) ↔ (a ∧ c′ ) (where Z̃ = Var (C, A)), then we can replace
c with c′ in C[ask(c) → A] and in C[tell(c)]. In particular, if we have that a ∧ c
is unsatisfiable, then c can immediately be replaced with false (the unsatisfiable
constraint). In order to formalize this intuitive idea, we start with the following
definition.
Definition 3.4. Given an agent A, the produced constraint of A is denoted by
pca(A) and is defined by structural induction as follows:
pca(tell(c)) = c
pca(A k B) = pca(A) ∧ pca(B)
pca(A)
= true for any agent A which is neither of the form tell(c)
nor a parallel composition.
By extending the definition we use for agents to contexts, given a context C[ ]
the produced constraint of C[ ] is denoted by pc(C[ ]) and is inductively defined as
follows:
pc([ ])
= true
′
pc(C
[
]
k
B)
= pc(C′ [ ]) ∧ pca(B)
Pn
pc( i=1 ask(ci ) → Ai ) = cj ∧ pc(C′ [ ]) where j ∈ [1, n] and Aj = C′ [ ]
The following definition allows us to determine when two constraints are equivalent within a given context C[ ].
Definition 3.5. Let c, c′ be constraints, C[ ] be a context, and Z̃ be a set of
variables. We say that c is equivalent to c′ within C[ ] and w.r.t. the variables in Z̃
iff D |= ∃−Z̃ (pc(C[ ]) ∧ c) ↔ ∃−Z̃ (pc(C[ ]) ∧ c′ )
This definition is employed in the following operation, which allows us to simplify
the constraints in the ask and tell guards.
4 Note that in general the further simplification to C[A + ask(d) → B] is not correct, although we
can transform C[ask(true) → A] into C[A].

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

11

Definition 3.6 (Ask and Tell Simplification). Let D be a set of declarations.
Pn
(1) Let d : H ← C[ i=1 ask(ci ) → Ai ] be a declaration of D. Suppose that c′1 , . . . , c′n
are constraints such that for j ∈ [1, n], c′j is equivalent to cj within C[ ] and
w.r.t. the variables in Var (C, H, Aj ).
Pn
Then we can replace d with d′ : H ← C[ i=1 ask(c′i ) → Ai ] in D. We call this
an ask simplification operation.
(2) Let d : H ← C[tell(c)] be a declaration of D. Suppose that the constraint c′ is
equivalent to c within C[ ] and w.r.t. the variables in Var (C, H).
Then we can replace d with d′ : H ← C[tell(c′ )] in D. We call this a tell
simplification operation.
In our AUCTION example, we can consider the produced constraint of tell(LastBid
6= quit), and modify the subsequent ask constructs as follows:
auction right(LastBid) ← tell(LastBid 6= quit) k
bidder a(Bs, As) k
ask(∃HisBid,HisList′ [LastBid|As] = [HisBid|HisList’] ∧ LastBid 6= quit ∧ HisBid = quit) →
stop
+
ask(∃HisBid,HisList′ [LastBid|As] = [HisBid|HisList’]) →
tell([LastBid|As] = [HisBid|HisList’]) k . . .

Via the same operation, we can immediately simplify this to.
auction right(LastBid) ← tell(LastBid 6= quit) k bidder a(Bs, As) k
ask(false) → stop
+ ask(true) → tell([LastBid|As] = [HisBid|HisList’]) k . . .

3.5 Branch Elimination and Conservative Ask Elimination
In the above program we have a guard ask(false) which of course will never be
satisfied. The first important application of the guard simplification operation
regards then the elimination of unreachable branches.
Definition 3.7 (Branch Elimination). Let D be a set of declarations and let
Pn
d : H ← C[ i=1 ask(ci ) → Ai ]

be a declaration of D. Assume that n > 1 and that for some j ∈ [1, n], we have
that cj = false, then we can replace d with
Pj−1
Pn
d′ : H ← C[( i=1 ask(ci ) → Ai ) + ( i=j+1 ask(ci ) → Ai )].

The condition that n > 1 means that we cannot eliminate all the branches of a
choice and it is needed to ensure the correctness of the system (otherwise one could
transform a deadlock into a success: For example, the agent tell(c) k ask(false) →
stop when evaluated in the empty store produces the constraint c and deadlocks,
while the agent tell(c) produces c and succeeds).
By applying this operation to the above piece of example, we can eliminate
ask(false) → stop, thus obtaining
auction right(LastBid) ← tell(LastBid 6= quit) k
bidder a(Bs, As) k
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

12

·

Sandro Etalle et al.

ask(true) → tell([LastBid|As] = [HisBid|HisList’]) k
...

Now we do not see any reason for not eliminating the guard ask(true) altogether.
This can indeed be done via the following operation.
Definition 3.8 (Conservative Ask Elimination). Consider the declaration
d : H ← C[ask(true) → B]
We can transform d into the declaration
d′ : H ← C[B].
This operation, although trivial, is subject of debate. In fact, Sahlin [1995] defines
a similar operation, with the crucial distinction that the choice might still have
more than one branch, in other words, in the system of [Sahlin 1995] one is allowed
to simplify the agent C[ask(true) → A + ask(b) → B] to the agent C[A], even if b
is satisfiable. Ultimately, one is allowed to replace the agent C[ask(true) → A +
ask(true) → B] either with C[A] or with C[B], indifferently. Such an operation is
clearly more widely applicable than the one we have presented but is bound to be
incomplete, i.e. to lead to the loss of potentially successful branches. Nevertheless,
Sahlin argues that an ask elimination such as the one defined above is potentially
too restrictive for a number of useful optimization. We agree with the statement
only partially, nevertheless, the system we propose could easily be equipped also
with an ask elimination as the one proposed by Sahlin (which of course, if employed,
would lead to weaker correctness results).
In our example program, the application of these branch elimination and conservative ask elimination leads to the following:
auction right(LastBid) ← tell(LastBid 6= quit) k
bidder a(Bs, As) k
tell([LastBid|As] = [HisBid|HisList’]) k
make new bid b(HisBid,MyBid) k
ask(MyBid = quit) → (tell(Bs = [quit|Bs’]) k broadcast(“b quits”))
+ ask(MyBid 6= quit) → (tell(Bs = [MyBid|Bs’]) k
tell(MyBid 6= quit) k
bidder b(HisList’,Bs’))

Via a tell elimination of tell([LastBid|As] = [HisBid|HisList’]), this simplifies to:
auction right(LastBid) ← tell(LastBid 6= quit) k
bidder a(Bs, As) k
make new bid b(LastBid,MyBid) k
ask(MyBid = quit) → (tell(Bs = [quit|Bs’]) k broadcast(“b quits”))
+ ask(MyBid 6= quit) → (tell(Bs = [MyBid|Bs’]) k
tell(MyBid 6= quit) k
bidder b(As,Bs’))

3.6 Distribution
A crucial operation in our transformation system is the distribution,Pwhich consists
of bringing an agent inside a P
choice as follows: from the agent A k i ask(ci ) → Bi ,
we want to obtain the agent i ask(ci ) → (A k Bi ). This operation requires delicate

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

13

applicability conditions, as it can easily introduce deadlocks: consider for instance
the following contrived program D.
p(Y) ← q(X) k ask(X >= 0) → tell(Y=0)
q(0) ← stop

In this program, the process D.p(Y) originates the derivation hD.p(Y), truei →∗
hD.Stop, Y = 0i. Now, if we blindly apply the distribution operation to the first
definition we would change D into:
p(Y) ← ask(X >= 0) → (q(X) k tell(Y=0))

and now we have that hD.p(Y), truei generates only deadlocking derivations. This
situation is avoided by demanding that the agent being distributed will not be able
to produce any output, unless it is completely determined which branches of the
choices might be entered.
To define the applicability conditions for the distribution operation we then need
the notion of productive configuration. Here and in the following we say that a
derivation hD.A, ci →∗ hD.A′ , c′ i is maximal if hD.A′ , c′ i 6→.
Definition 3.9 (Productive). Given a process D.A and a satisfiable constraint
c, we say that hD.A, ci is productive iff either it has no (finite) maximal derivations
or there exists a derivation hD.A, ci →∗ hD.A′ , c′ i such that D |= ¬(∃−Z̃ c → ∃−Z̃ c′ ),
where Z̃ = Var(A).
So, a configuration is productive if its evaluation can (strictly) augment the
information contained in the global store. For technical reasons which will be clear
after the next definition, we call productive also those configurations which have
no finite maximal derivations.
We can now provide the definition of the distribution operation.
Definition 3.10 (Distribution). Let D be a set of declarations and let
P
d : H ← C[A k ni=1 ask(ci ) → Bi ]

be a declaration in D, where e = pc(C[ ]). The distribution of A in d yields as result
the definition
Pn
d′ : H ← C[ i=1 ask(ci ) → (A k Bi )]

provided that for every constraint c such that Var (c) ∩ Var(d) ⊆ Var (H, C), if
hD.A, c ∧ ei is productive then both the following conditions hold:

(a) There exists at least one i ∈ [1, n] such that D |= (c ∧ e) → ci ,
(b) for each i ∈ [1, n], either D |= (c ∧ e) → ci or D |= (c ∧ e) → ¬ci .
Pn
Intuitively, the constraint c models the possible ways of “calling” A k i=1 ask(ci ) →
Bi . Condition (b) basically requires that if the store c is such that A might produce
some output (that is, the configuration hD.A, c ∧ ei is productive), then for each
branch of the choice it is already determined whether we can follow it or not. This
guarantees that the constraints possibly added to the store by the evaluation of
A cannot influence the choice. Moreover, condition (a) guarantees that we do not
apply the operation to a case such as tell(X = a) k ask(false) → stop, which would
clearly be wrong. If hD.A, c ∧ ei is not productive then we do not impose any
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

14

·

Sandro Etalle et al.

condition, since the evaluation of hD.A, c ∧ ei cannot affect the choice. As previously mentioned, we call productive also those configurations which have no finite
maximal derivations, that is, those configurations which originate non-terminating
computations only (possibly with no output). In fact, also in this case we need conditions (a) and (b), since otherwise bringing A inside the choice might transform a
looping program into a deadlocking one.
The above applicability conditions are a strict improvement on the ones we presented in [Etalle et al. 1998], in which we used the concept of required variable. We
now report this definition, both for simplifying the explanation for some examples
and for comparing the above definition of distribution with the one in [Etalle et al.
1998].
Definition 3.11 (Required Variable). We say that the process D.A requires
the variable X iff, for each satisfiable constraint c such that D |= ∃X c ↔ c, hD.A, ci
is not productive.
In other words, the agent A requires the variable X if, in the moment that the
global store does not contain any information on X, A cannot produce any information which affects the variables occurring in A and has at least one finite maximal
derivation. Even though the above notion is not decidable in general, it is easy
to find wide-applicable (decidable) sufficient conditions guaranteeing that a certain variable is required. For example it is immediate to see that, in our program,
bidder a(Bs, As) requires Bs: in fact the derivation starting in bidder a(Bs, As) suspends (without having provided any output) after one step and resumes only when
more information for the variable Bs has been produced.
The following remark clarifies how the concept of required variable might be used
for ensuring the applicability of the distributive operation. Its proof is straightforward.
Remark 3.12. Referring to Definition 3.10. If A requires a variables which does
not occur in H, C[ ], then the distribution operation is applicable.
Proof. In this case, there exists no constraint c such that Var (c) ∩ Var (d) ⊆
Var (H, C) and hD.A, c ∧ ei is productive.
In our example, since the agent bidder a(Bs, As) requires the variable Bs, which
occurs only inside the ask guards, we can safely apply the distributive operation.
The result is the following program.
auction right(LastBid) ← tell(LastBid 6= quit) k make new bid b(LastBid,MyBid) k
ask(MyBid = quit) → tell(Bs = [quit|Bs’]) k broadcast(“b quits”) k bidder a(Bs, As)
+ ask(MyBid 6= quit) → (tell(Bs = [MyBid|Bs’]) k
tell(MyBid 6= quit) k
bidder a(Bs, As) k
bidder b(As, Bs’))

In this program we can now eliminate the construct tell(Bs = [MyBid|Bs’]): In
fact, even though the variable Bs here occurs also elsewhere in the definition, we
can assume it to be renamed since it occurs only on choice-branches different than
the one on which the considered agent lies. Thus we obtain:
auction right(LastBid) ← tell(LastBid 6= quit) k make new bid b(LastBid,MyBid) k
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

15

ask(MyBid = quit) → tell(Bs = [quit|Bs’]) k broadcast(“b quits”) k bidder a(Bs, As)
+ ask(MyBid 6= quit) → (tell(MyBid 6= quit) k
bidder a([MyBid|Bs’], As) k
bidder b(As, Bs’))

Before we introduce the fold operation, let us clean up the program a bit further:
we can now first apply a tell elimination to tell(Bs = [quit|Bs’]), and then properly
transform (by unfolding, and simplifying the result) the agent bidder a([quit|Bs’],
As) in the first ask branch. We easily obtain:
auction right(LastBid) ← tell(LastBid 6= quit) k make new bid b(LastBid,MyBid) k
ask(MyBid = quit) → broadcast(“b quits”) k stop
+ ask(MyBid 6= quit) → (tell(MyBid 6= quit) k
bidder a([MyBid|Bs’], As) k
bidder b(As, Bs’))

The just introduced stop agent can safely be removed (see Proposition 4.2) and we
are left with:
auction right(LastBid) ← tell(LastBid 6= quit) k make new bid b(LastBid,MyBid) k
ask(MyBid = quit) → broadcast(“b quits”)
+ ask(MyBid 6= quit) → (tell(MyBid 6= quit) k
bidder a([MyBid|Bs’], As) k
bidder b(As, Bs’))

3.7 Folding
The folding operation has a special role in the suite of the transformation operations.
This is due to the fact that it allows us to introduce recursion in a definition,
often making it independent from the definitions it depended on. As previously
mentioned, the applicability conditions that we use here for the folding operation
do not depend on the transformation history, nevertheless, we require that the
declarations used to fold an agent appear in the initial program. Thus, before
defining the fold operation, we need the following.
Definition 3.13. A transformation sequence is a sequence of programs D0 , . . . , Dn ,
in which D0 is an initial program and each Di+1 is obtained from Di via one of the
following transformation operations: unfolding, backward instantiation, tell elimination, tell introduction, ask and tell simplification, branch elimination, conservative ask elimination, distribution and folding.
Recall that we assume that the new declarations introduced by using the definition introduction operation are added once for all to the original program D0
before starting the transformation itself. We also need the notion of guarding context. Intuitively, a context C[ ] is guarding if the “hole” appears in the scope of an
ask guard.
Definition 3.14 (Guarding Context). We call C[ ] is a guarding context iff
Pn
C[ ] = C′ [ i=1 ask(ci ) → Ai ] and Aj = C′′ [ ] for some j ∈ [1, n].
So, for example, ask(c) → (A k [ ]) is a guarding context, while (ask(c) → A) k [ ] is
not. We can finally give the definition of folding:
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

16

·

Sandro Etalle et al.

Definition 3.15 (Folding). Let D0 , . . . , Di , i ≥ 0, be a transformation sequence.
Consider two definitions.
d : H ← C[A] ∈ Di
f : B←A
∈ D0
If C[ ] is a guarding context, B contains only distinct variables as arguments and
Var (A) ∩ Var (C,H) ⊆ Var (B) then folding A in d consists of replacing d by
d′ : H ← C[B]

∈ Di+1

(it is assumed here that d and f are suitably renamed so that the variables they
have in common are only the ones occurring in A).
In many situations this operation is actually applicable also in absence of a guarding
context as discussed below.
Remark 3.16. We can apply the fold operation also in case C[ ] is not guarding
context (referring to the notation of the previous definition), provided that the
definition H ← C[A] was not modified nor used during the transformation. In fact,
in this case we can simply assume that the original definition of H ← C[A] contained
a dummy ask guard as in
H ← ask(true) → C[A]
that the folding operation is applied to this definition, and that the guard ask(true)
will eventually be removed by an ask elimination operation.
Actually, in many cases this reasoning can be applied also to definitions that are
used during the transformation. This kind of folding is called propagation folding
(as opposed to the recursive folding): it is not employed to introduce recursion,
but to propagate to other contexts the efficiency that was hopefully gained by the
transformation. Usually, transformation systems provide a special condition for
the propagation folding operation. For instance, in [Tamaki and Sato 1984], a
distinction is made between new and old predicates. Here we decided not to do so.
This allows us to have a definition of folding operation which is particularly simple.
We refer to the end of Example 6.2 for an example of application of folding
without guarding context.
The reach of the folding operation is best shown via our example. We can now
fold auction left(MyBid) in the above definition, and obtain:
auction right(LastBid) ← tell(LastBid 6= quit) k make new bid b(LastBid,MyBid) k
ask(MyBid = quit) → broadcast(“b quits”)
+ ask(MyBid 6= quit) → auction left(MyBid)

Now, by performing an identical optimization on auction left, we can also obtain:
auction left(LastBid) ← tell(LastBid 6= quit) k make new bid a(LastBid,MyBid) k
ask(MyBid = quit) → broadcast(“a quits”)
+ ask(MyBid 6= quit) → auction right(MyBid)

This part of the transformation shows in a striking way one of the main benefits
of the folding operation: the saving of synchronization points. Notice that in the
initial program the two bidders had to “wait” for each other. In principle they
were working in parallel, but in practice they were always acting sequentially, since
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

17

one had always to wait for the bid of the competitor. The transformation allowed
us to discover this sequentiality and to obtain an equivalent program in which the
sequentiality is exploited to eliminate all suspension points, which are known to
be one of the major overhead sources. Furthermore, the transformation allows a
drastic saving of computational space. In fact, in the initial definition the parallel
composition of the two bidders leads to the construction of two lists containing all
the bids done so far. After the transformation we have a definition which does not
build the list any longer, and which, by exploiting a straightforward optimization
can employ only constant space.
Concerning the syntax of the operation, in our setting the folding operation reduces to a mere replacement. To people familiar with this operation, this might
seem restrictive: one might wish to apply the folding also in the case that the definition to be folded contains an instance of A, i.e. when d has the form H ← C[Aσ]
(in this case the folding operation is applicable only if σ satisfies specific conditions
described in [Tamaki and Sato 1984] for logic programs and in [Etalle and Gabbrielli 1996] for CLP). This extended operation would actually correspond to the
(most) usual definition of folding as in [Tamaki and Sato 1984; Etalle and Gabbrielli
1996; Bensaou and Guessarian 1998]. In our system such an extended operation
is formally not needed, as it can be obtained by combining together the folding
operation with the tell introduction.
In fact, assume that we would like to fold the definition
d : H ← C[Aσ]

∈ Di

by using the definition
f : B←A

∈ D0

In the first place, via a tell introduction, we can modify definition d as follows
d∗ : H ← C[A k tell(X̃ = X̃σ)],
Clearly, we assume here that X̃ and σ fulfill the applicability conditions given in
Definition 3.2. Then, via a normal folding operation we obtain
d∗∗ : H ← C[B k tell(X̃ = X̃σ)]
(provided that the applicability conditions for the folding are satisfied) which is
equivalent to the definition
d′ : H ← C[Bσ].
obtained in the case of the folding operation as defined in [Tamaki and Sato 1984;
Etalle and Gabbrielli 1996; Bensaou and Guessarian 1998]. Actually, in case the
constraint domain admit most general unifiers, the definition d′ can be obtained
from d∗∗ by using a tell elimination operation (also in this case we assume that the
applicability conditions for the tell elimination are satisfied).
For the sake of simplicity, we do not give the explicit definition of this (derived)
extended folding operation and of its applicability conditions. Therefore, the occurrences of this operation in the last example of Section 6 have to be considered
as a shorthands for the sequence of operations described above.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

18

·

Sandro Etalle et al.

4. CORRECTNESS
Any transformation system must be useful (i.e. allow useful transformations and
optimization) and – most importantly – correct, i.e., it must guarantee that the
resulting program is in some sense equivalent to the one we have started with.
Having at hand the transition system in Table I, we provide now the intended
semantics to be preserved by the transformation system by defining a suitable notion
of “observables”. We start with the following definition which takes into account
terminating and failed computations only. In the next Section we will consider also
non-terminating computations. Here and in the sequel we say that a constraint c
is satisfiable iff D |= ∃ c.
Definition 4.1 (Observables). Let D.A be a CCP process. We define
O(D.A) = {hc, ∃−Var (A,c) d, ssi | c and d are satisfiable, and there exists
a derivation hD.A, ci →∗ hD.Stop, di}
∪
{hc, ∃−Var (A,c) d, ddi | c and d are satisfiable, and there exists
a derivation hD.A, ci →∗ hD.B, di 6→, B 6= Stop}
∪
{hc, false, ffi
| c is satisfiable, and there exists
a derivation hD.A, ci →∗ hD.B, falsei}.
Thus what we observe are the results of terminating computations (if consistent),
abstracting from the values of the local variables in the results, and distinguishing
the successful computations from the deadlocked ones (by using the termination
modes ss and dd, respectively). We also observe failed computations, i.e. those
computations which produce an inconsistent store.
Having defined a formal semantics for our paradigm, we can now define more
precisely the notion of correctness for the transformation system: we say that a
transformation sequence D0 , . . . , Dn is partially correct iff, for each agent A, we
have that
O(D0 .A) ⊇ O(Dn .A)
holds, that is, nothing is added to the semantics of the initial program. Dually, we
say that D0 , . . . , Dn is complete iff, for each agent A, we have that
O(D0 .A) ⊆ O(Dn .A)
holds, that is, no semantic information is lost during the transformation. Finally a
transformation sequence is called totally correct iff it is both partially correct and
complete.
In the following we prove that the our transformation system is totally correct.
As previously mentioned, for the sake of readability some proofs are only sketched
and their full versions can be found in the Appendix.
The proof of this result is originally inspired by the one of Tamaki and Sato for
pure logic programs [Tamaki and Sato 1984] and has retained some of its notation,
in particular we also use the notions of weight and of split derivation. Of course the
similarities do not go any further, as demonstrated by the fact that in our transformation system the applicability conditions of folding operation do not depend on
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

19

the transformation history (while allowing the introduction of recursion), and that
the folding definitions are allowed to be recursive (the distinction between Pnew
and Pold of [Tamaki and Sato 1984] is now superfluous).
We start with the following proposition allows us to eliminate stop agents in
programs.
Proposition 4.2. For any agent A and set of declarations D, O(D.A k stop) =
O(D.A).
Proof. The proof follows immediately from the definition of observables by
noting that, according to rules R1-R4, the agent stop has no transition and hD.A k
stop, ci →∗ hD.B k stop, di iff hD.A, ci →∗ hD.B, di, where obviously B k stop is
equal to Stop iff B = Stop (recall that Stop is the generic agent containing only k
and stop).
The following notion of mode will be useful to shorten the notation.
Definition 4.3. Let D0 , . . . , Dn be a transformation sequence, A be an agent and
d be a constraint. We define the mode m(A, d) of the agent A w.r.t. the constraint
d as follows

 ss if d is satisfiable and A = Stop
dd if d is satisfiable, hD0 .A, di 6→ and A 6= Stop
m(A, d) =

ff if d is not satisfiable
Note that the notion of mode does not depend on the set of declarations Di we
are considering, that is, in the above definition we could equivalently use Di rather
than D0 . This is the content of the following.
Proposition 4.4. Let D0 , . . . , Dn be a transformation sequence, A be an agent
and d be a constraint. Then hD0 .A, di 6→ iff hDi .A, di 6→, for any i ∈ [1, n].
Proof. Immediate by observing that a procedure call can be evaluated in D0 iff
it can be evaluated in Di , for any i ∈ [1, n].
In what follows, we are going to refer to a fixed transformation sequence D0 , . . . , Dn .
We start with the following result, concerning partial correctness.
Proposition 4.5 (Partial Correctness). If, for each agent A, O(D0 .A) =
O(Di .A) holds then, for each agent A, O(Di .A) ⊇ O(Di+1 .A).
Proof. (Sketch). We show that given an agent A and a satisfiable constraint
cI , if there exists a derivation ξ = hDi+1 .A, cI i →∗ hDi+1 .B, cF i, with m(B, cF ) ∈
{ss, dd, ff}, then there exists also a derivation ξ ′ = hDi .A, cI i →∗ hDi .B′ , c′F i with
∃−Var (A,cI ) c′F = ∃−Var (A,cI ) cF and m(B′ , c′F ) = m(B, cF ). By Definition 4.1, this will
imply the thesis. The proof is by induction on the length l of the derivation.
(l = 0). In this case ξ = hDi+1 .A, cI i. By the definition hDi .A, cI i is also a
derivation of length 0 and then the thesis holds.
(l > 0). If the first step of derivation ξ does not use rule R4, then the proof
follows from the inductive hypothesis.
Now, assume that the first step of derivation ξ uses rule R4 and let d′ ∈ Di+1
be the declaration used in the first step of ξ. If d′ was not modified in the transformation step from Di to Di+1 (that is, d′ ∈ Di ), then the result follows from the
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

20

·

Sandro Etalle et al.

inductive hypothesis. We assume then that d′ 6∈ Di , d′ is then the result of the
transformation operation applied to obtain Di+1 . The proof proceeds by distinguishing various cases according to the operation itself. Here we consider only the
operations of unfolding, tell elimination, tell introduction and folding. The other
cases are deferred to the Appendix.
Unfolding: If d′ is the result of an unfolding operation then proof is immediate.
Tell elimination and introduction: If d′ is the result of a tell elimination or of
a tell introduction the thesis follows from a straightforward analysis of the possible
derivations which use d or d’. First, observe that for any derivation which uses a
declaration H ← C[tell(s̃ = t̃) k B], we can construct another derivation such that
the agent tell(s̃ = t̃) is evaluated before B. Moreover for any constraint c such
that ∃dom(σ) c = ∃dom(σ) cσ, (where σ is a relevant most general unifier of s̃ and t̃),
there exists a derivation step hDi .B1 σ, cσi → hDi .B2 σ, c′ i if and only if there exists
a derivation step hDi .B1 , c ∧ (s̃ = t̃)i → hDi .B2 , c′′ i, where, for some constraint e,
c′ = eσ, c′′ = e ∧ (s̃ = t̃) and therefore c′ = ∃dom(σ) c′′ . Finally, since by definition σ
is idempotent and the variables in the domain of σ do not occur neither in C[ ] nor
in H, for any constraint e we have that ∃−Var (A,cI ) eσ = ∃−Var (A,cI ) (e ∧ (s̃ = t̃)).
Folding: If d′ is the result of a folding then let
- d : q(r̃) ← C[H] be the folded declaration (∈ Di ),
- f : p(X̃) ← H be the folding declaration (∈ D0 ),
- d′ : q(r̃) ← C[p(X̃)] be the result of the folding operation (∈ Di+1 )
where, by hypothesis, Var (d)∩Var (X̃) ⊆ Var (H) and Var(H)∩(Var (r̃)∪Var (C)) ⊆
Var (X̃). In this case ξ = hDi+1 .CI [q(ṽ)], cI i → hDi+1 .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗
hDi+1 .B, cF i and we can assume, without loss of generality, that Var (CI [q(ṽ)], cI ) ∩
Var (H) = ∅.
By the inductive hypothesis, there exists a derivation
χ = hDi .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗ hDi .B′′ , c′′F i,
with ∃−Var (C [C[p(X̃)] k tell(ṽ=r̃)],c ) c′′F = ∃−Var (C [C[p(X̃)] k tell(ṽ=r̃)],c ) cF and
I

I

I

′′

m(B

, c′′F )

I

= m(B, cF ).

(1)

Since Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[p(X̃)] k tell(ṽ = r̃)], cI ), we have that
∃−Var (CI [q(ṽ)],cI ) c′′F = ∃−Var (CI [q(ṽ)],cI ) cF .
′

′

(2)

′

Since by hypothesis for any agent A , O(D0 .A ) = O(Di .A ), there exists a derivation
ξ0 = hD0 .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗ hD0 .B0 , c0 i
such that ∃−Var (C [C[p(X̃)] k tell(ṽ=r̃)],c ) c0 = ∃−Var (C [C[p(X̃)] k tell(ṽ=r̃)],c ) c′′F and m(B0 , c0 )
I

I

I

I

= m(B′′ , c′′F ).
By (1), (2) and since Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[p(X̃)] k tell(ṽ = r̃)], cI ), we have
that
∃−Var (CI [q(ṽ)],cI ) c0 = ∃−Var (CI [q(ṽ)],cI ) cF and m(B0 , c0 ) = m(B, cF ).

(3)

Let f ′ : p(X̃′ ) ← H′ be an appropriate renaming of f, which renames only the
variables in X̃, such that Var(d) ∩ Var(f ′ ) = ∅ (note that this is possible, since
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

21

Var (H) ∩ (Var (r̃) ∪ Var (C)) ⊆ Var (X̃)). By hypothesis, Var (CI [q(ṽ)], cI ) ∩ Var (H) =
∅. Then, without loss of generality we can assume that Var(ξ0 ) ∩ Var (f ′ ) 6= ∅ if and
only if the procedure call p(X̃) is evaluated, in which case declaration f ′ is used.
Thus there exists a derivation
hD0 .CI [C[H′ k tell(X̃ = X̃′ )] k tell(ṽ = r̃)], cI i →∗ hD0 .B′0 , c0 i,
where m(B′0 , c0 ) = m(B0 , c0 ). By (3) we have
m(B′0 , c0 ) = m(B, cF ).

(4)

′

′

We now show that we can substitute H for H k tell(X̃ = X̃ ) in the previous derivation. Since f ′ : p(X̃′ ) ← H′ is a renaming of f : p(X̃) ← H, the equality X̃ = X̃′
is conjunction of equations involving only distinct variables. Then, by replacing the variables X̃ with X̃′ and vice versa in the previous derivation we obtain
the derivation χ0 = hD0 .CI [C[H k tell(X̃′ = X̃)] k tell(ṽ = r̃)], cI i →∗ hD0 .B′′0 , c′0 i
where ∃−Var (C [C[H k tell(X̃′ =X̃)] k tell(ṽ=r̃)],c ) c′0 = ∃−Var (C [C[H k tell(X̃′ =X̃)] k tell(ṽ=r̃)],c ) c0
I

I

I

I

and m(B′′0 , c′0 ) = m(B′0 , c0 ).
¿From (4) it follows that
m(B′′0 , c′0 ) = m(B, cF ).

(5)
′

Then, from (3) and since Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[H k tell(X̃ = X̃)] k tell(ṽ =
r̃)], cI ) we obtain
∃−Var (CI [q(ṽ)],cI ) c′0 = ∃−Var (CI [q(ṽ)],cI ) cF .

(6)

Moreover, we can drop the constraint tell(X̃′ = X̃), since the declarations used
in the derivation are renamed apart and, by construction, Var (CI [C[H] k tell(r̃ =
ṽ)], cI ) ∩ Var(X̃′ ) = ∅. Therefore there exists a derivation hD0 .CI [C[H] k tell(ṽ =
r̃)], cI i →∗ hD0 .B̄0 , c̄0 i which performs exactly the same steps of χ0 , (possibly) except for the evaluation of tell(X̃′ = X̃), and such that ∃−Var (C [C[H] k tell(ṽ=r̃)],c ) c̄0 =
I

I

∃−Var (C [C[H] k tell(ṽ=r̃)],c ) c′0 and m(B̄0 , c̄0 ) = m(B′′0 , c′0 ). From (5), (6) and since
I

I

Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[H] k tell(ṽ = r̃)], cI ), it follows that
m(B̄0 , c̄0 ) = m(B, cF ) and ∃−Var (CI [q(ṽ)],cI ) c̄0 = ∃−Var (CI [q(ṽ)],cI ) cF .

(7)

Since O(D0 .A′ ) = O(Di .A′ ) holds by hypothesis for any agent A′ , there exists a
derivation
hDi .CI [C[H] k tell(ṽ = r̃)], cI i →∗ hDi .B′ , c′F i
where
∃−Var (C [C[H] k tell(ṽ=r̃)],c ) c′F = ∃−Var (C [C[H] k tell(ṽ=r̃)],c ) c̄0
I

′

I

I

I

, c′F )

and m(B
= m(B̄0 , c̄0 ).
¿From (7) and since Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[H] k tell(ṽ = r̃)], cI ), we obtain
m(B′ , c′F ) = m(B, cF ) and ∃−Var (CI [q(ṽ)],cI ) c′F = ∃−Var (CI [q(ṽ)],cI ) cF .

(8)

Finally, since d : q(r̃) ← C[H] ∈ Di , there exists a derivation
ξ ′ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H] k tell(ṽ = r̃)], cI i →∗ hDi .B′ , c′F i
and then the thesis follows from (8).
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

22

·

Sandro Etalle et al.

In order to prove total correctness we need the following.
Definition 4.6 (Weight). Let ξ be a derivation. We denote by wh(ξ) the number of derivation steps in ξ which use rule R2. Given an agent A and a pair of
satisfiable constraints c, d, we then define the success weight wss (A, c, d) of the agent
A w.r.t. the constraints c and d as follows
wss (A, c, d) = min{n | n = wh(ξ) and ξ is a derivation
hD0 .A, ci →∗ hD0 .Stop, d′ i 6→
with ∃−Var (A,c) d′ = ∃−Var (A,c) d }
Analogously, we define the deadlock weight wdd (A, c, d) of the agent A w.r.t. the
constraints c and d
wdd (A, c, d) = min{n | n = wh(ξ) and ξ is a derivation
hD0 .A, ci →∗ hD0 .B, d′ i 6→
with B 6= Stop and ∃−Var (A,c) d′ = ∃−Var (A,c) d }
and the failure weight wff (A, c, d′ ) of the agent A w.r.t. the constraints c and d′
wff (A, c, d′ ) = min{n | n = wh(ξ) and ξ is a derivation hD0 .A, ci →∗ hD0 .B, d′ i
with d′ = false
}
Notice that wss (A, c, d′ ) is undefined in case there is no successful derivation corresponding to the given constraints (and analogously for wdd and wff ). Also, both
wss (A, c, false) and wdd (A, c, false) are undefined, as the success and deadlock weight
consider only non failed derivations (i.e. derivations which do not produce the
constraint false).
As previously mentioned, this notion of weight is rather different from the one
in [Tamaki and Sato 1984], since the latter is based on the number of nodes in a
proof tree for an atom, by taking into account the fact that the predicate symbol
appearing in that atom is “new” or “old”.
In the total correctness proof we also make use of the concept of split derivations.
Intuitively, these are derivations which can be split into two parts: the first one, up
to the first ask evaluation, is performed in the program Di while the second one is
carried out in D0 .
Definition 4.7 (Split derivation). Let D0 , . . . , Di be a transformation sequence.
We call a derivation in Di ∪ D0 a successful split derivation if it has the form
hDi .A1 , c1 i →∗ hDi .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .Stop, cn i 6→
where cn is a satisfiable constraint, m ∈ [1, n]5 and the following conditions hold:
(a) the first m − 1 derivation steps do not use rule R2;
(b) the m-th derivation step hDi .Am , cm i → hD0 .Am+1 , cm+1 i uses rule R2;
(c) wss (A1 , c1 , cn ) > wss (Am+1 , cm+1 , cn ).
A deadlocked split derivation is defined analogously, by replacing wss for wdd and
Stop for a generic agent B 6= Stop in the last configuration of the derivation above.
5 If m = n we can write indifferently hD .Stop, c i or hD .Stop, c i to denote the last configuration
n
n
0
i
of the derivation.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

23

Finally a failed split derivation is defined by replacing wss for wff and Stop for a
generic agent (which is not necessarily terminated) and by assuming that cn = false
in the last configuration of the derivation above.
In the following we call split derivations both successful, deadlocked and failed
split derivations. The previous definition is inspired by the definition of descent
clause of [Kawamura and Kanamori 1988]; however, here we use a different notion
of weight and rather different conditions on them. We need one final concept.
Definition 4.8. We call the program Di weight complete iff, for any agent A, for
any satisfiable constraint c and for any constraint d, the following hold: if there
exists a derivation
hD0 .A, ci →∗ hD0 .B, di
such that m(B, d) ∈ {ss, dd, ff} then there exists a split derivation in Di ∪ D0
hDi .A, ci →∗ hD0 .B′ , d′ i
where ∃−Var (A,c) d′ = ∃−Var (A,c) d and m(B′ , d′ ) = m(B, d).
So Di is weight complete if we can reconstruct the semantics of D0 by using only
(successful, deadlocked and failed) split derivations in Di ∪ D0 . We now show that if
Di is weight complete then no observables are lost during the transformation (i.e.,
the transformation is complete). This is the content of the following.
Proposition 4.9. If Di is weight complete then, for any agent A, O(D0 .A) ⊆
O(Di .A).
Proof. We consider only the case of successful derivations, since the case of
deadlocked (failed) derivations can be proved analogously by considering the notions of deadlock (failure) weight and deadlocked (failed) split derivation. Assume
that there exists a (finite, successful) derivation hD0 .A, ci →∗ hD0 .Stop, di. We
show, by induction on the success weight of (A, c, d), that there exists a derivation
hDi .A, ci →∗ hDi .Stop, d′ i, where ∃−Var (A,c) d′ = ∃−Var (A,c) d.
Base Case. If wss (A, c, d) = 0 then, since Di is weight complete, from Definition 4.7
and Definition 4.8 it follows that there exists a (successful) split derivation in Di ∪D0
of the form hDi .A, ci →∗ hDi .Stop, d′ i where ∃−Var (A,c) d′ = ∃−Var (A,c) d, rule R2 is
not used and therefore each derivation step is done in Di .
Inductive Case. Assume that wss (A, c, d) = n. Since Di is weight complete there
exists a (successful) split derivation in Di ∪ D0
ξ : hDi .A, ci →∗ hD0 .Stop, d′ i,
where ∃−Var (A,c) d′ = ∃−Var (A,c) d. If rule R2 is not used in ξ then the proof is the
same as in the previous case. Otherwise ξ has the form
hDi .A, ci →∗ hDi .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .Stop, d′ i
where wss (A, c, d′ ) > wss (Am+1 , cm+1 , d′ ). Let ξ ′ be the derivation
ξ ′ : hDi .A, ci →∗ hDi .Am , cm i → hDi .Am+1 , cm+1 i.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

24

·

Sandro Etalle et al.

By the inductive hypothesis, there exists a derivation
ξ ′′ : hDi .Am+1 , cm+1 i →∗ hDi .Stop, d′′ i
where ∃−Var (Am+1 ,cm+1 ) d′′ = ∃−Var (Am+1 ,cm+1 ) d′ . Without loss of generality, we can
assume that Var (ξ ′ ) ∩ Var (ξ ′′ ) = Var (Am+1 , cm+1 ) and hence there exists a derivation
hDi .A, ci →∗ hDi .Stop, d′′ i.
Finally, by our hypothesis on the variables and by construction,
∃−Var (A,c) d′′
∃−Var (A,c) (cm+1 ∧ ∃−Var (Am+1 ,cm+1 ) d′′ )
∃−Var (A,c) (cm+1 ∧ ∃−Var (Am+1 ,cm+1 ) d′ )
∃−Var (A,c) d′
∃−Var (A,c) d

=
=
=
=

which concludes the proof.
Before proving the total correctness result we need some technical lemmata. Here
and in the following we use the notation wt (with t ∈ {ss, dd, ff}) as a shorthand for
indicating the success weight wss , the deadlock weight wdd and the failure weight
wff .
Lemma 4.10. Let q(r̃) ← H ∈ D0 , t ∈ {ss, dd, ff} and let C[ ] be a context. For
any satisfiable constraint c and for any constraint c′ , such that Var(C[q(t̃)], c) ∩
Var (r̃) = ∅ and wt (C[q(t̃)], c, c′ ) is defined, there exists a constraint d′ such that
wt (C[q(r̃) k tell(t̃ = r̃)], c, d′ ) ≤ wt (C[q(t̃)], c, c′ ) and ∃−Var (C[q(t̃)],c) d′ = ∃−Var (C[q(t̃)],c) c′ .
Proof. Immediate.
Lemma 4.11. Let q(r̃) ← H ∈ D0 and t ∈ {ss, dd, ff}. For any context CI [ ], any
satisfiable constraint c and for any constraint c′ , the following holds.
(1 ) If Var(H) ∩ Var (CI , c) ⊆ Var(r̃) and wt (CI [q(r̃)], c, c′ ) is defined, then there
exists a constraint d′ , such that Var(d′ ) ⊆ Var (CI [H], c), wt (CI [H], c, d′ ) ≤
wt (CI [q(r̃)], c, c′ ) and ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ .
(2 ) If Var (H) ∩ Var (CI , c) ⊆ Var (r̃), Var (c′ ) ∩ Var (r̃) ⊆ Var(CI [H], c) and
wt (CI [H], c, c′ ) is defined, then there exists a constraint d′ , such that
wt (CI [q(r̃)], c, d′ ) ≤ wt (CI [H], c, c′ ) and ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ .
Proof. Immediate.
The following Lemma is crucial in the proof of completeness.
Lemma 4.12. Let 0 ≤ i ≤ n, t ∈ {ss, dd, ff}, cl : q(r̃) ← H ∈ Di , and let
cl′ : q(r̃) ← H′ be the corresponding declaration in Di+1 (in the case i < n). For
any context CI [ ] and any satisfiable constraint c and for any constraint c′ the
following holds:
(1 ) If Var(H) ∩ Var (CI , c) ⊆ Var(r̃) and wt (CI [q(r̃)], c, c′ ) is defined, then there
exists a constraint d′ , such that Var(d′ ) ⊆ Var (CI [H], c), wt (CI [H], c, d′ ) ≤
wt (CI [q(r̃)], c, c′ ) and ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ ;
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

25

(2 ) If Var(H, H′ ) ∩ Var (CI , c) ⊆ Var(r̃), Var(c′ ) ∩ Var (r̃) ⊆ Var (CI [H], c) and
wt (CI [H], c, c′ ) is defined, then there exists a constraint d′ , such that Var(d′ ) ⊆
Var(CI [H′ ], c), wt (CI [H′ ], c, d′ ) ≤ wt (CI [H], c, c′ ) and
∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ .
Proof. (Sketch). Observe that, for i = 0, the proof of 1 follows from the first
part of Lemma 4.11. We prove here that, for each i ≥ 0,
a). If 1 holds for i then 2 holds for i;
b). If 1 and 2 hold for i then 1 holds for i + 1.
The proof of the Lemma then follows from straightforward inductive argument.
a). If cl was not affected by the transformation step from Di to Di+1 then the
result is obvious by choosing d′ = ∃−Var (CI [H],c) c′ . Assume then that cl is affected
when transforming Di to Di+1 . We have various cases according to the operation
used to perform the transformation. Here we show only the proofs for the unfolding
and the folding operations, the other cases being deferred to the Appendix.
Unfolding: Assume cl′ ∈ Di+1 was obtained from Di by unfolding. In this case,
the situation is the following:
- cl : q(r̃) ← C[p(t̃)] ∈ Di
- u : p(s̃) ← B ∈ Di
- cl′ : q(r̃) ← C[B k tell(t̃ = s̃)] ∈ Di+1
where cl and u are assumed to be renamed so that they do not share variables.
Let n = wt (CI [C[p(t̃)]], c, c′ ). By the definition of transformation sequence, there
exists a declaration p(s̃) ← B0 ∈ D0 . Moreover, by the hypothesis on the variables,
Var (C[p(t̃)], C[B k tell(t̃ = s̃)]) ∩ Var (CI , c) ⊆ Var (r̃) and then Var (CI [C[p(t̃)]], c) ∩
Var (s̃) = ∅. Therefore, by Lemma 4.10, there exists a constraint d1 , such that
wt (CI [C[p(s̃) k tell(t̃ = s̃)]], c, d1 ) ≤ wt (CI [C[p(t̃)]], c, c′ ) = n

(9)

∃−Var (CI [C[p(t̃)]],c) d1 = ∃−Var (CI [C[p(t̃)]],c) c′ .

(10)

and
By the hypothesis on the variables and since u is renamed apart from cl, Var (B) ∩
Var (CI , C, t̃, c) = ∅ and therefore Var (B) ∩ Var(CI [C[ ] k tell(t̃ = s̃)], c) ⊆ Var(s̃).
Then, by Point 1, there exists a constraint d′ , such that
Var (d′ ) ⊆ Var (CI [C[B k tell(t̃ = s̃)]], c)
wt (CI [C[B k tell(t̃ = s̃)]], c, d′ ) ≤ wt (CI [C[p(s̃) k tell(t̃ = s̃)]], c, d1 )
∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) d′ = ∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) d1 .
I

I

′

By (9), wt (CI [C[B k tell(t̃ = s̃)]], c, d ) ≤ n. Furthermore, by hypothesis and construction,
Var(c′ , d′ ) ∩ Var (r̃) ⊆ Var (CI [C[p(t̃)]], c)
and, without loss of generality, we can assume that
Var (d1 ) ∩ Var (r̃) ⊆ Var(CI [C[p(t̃)]], c).
Then, by (10) and since Var (CI [C[p(t̃)]], c) ⊆ Var (CI [C[p(s̃) k tell(t̃ = s̃)]], c), we
have that ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ and this completes the proof.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

·

26

Sandro Etalle et al.

Folding: Let
- cl : q(r̃) ← C[B] be the folded declaration (∈ Di ),
- f : p(X̃) ← B be the folding declaration (∈ D0 ),
- cl′ : q(r̃) ← C[p(X̃)] be the result of the folding operation (∈ Di+1 ),
where, by hypothesis, Var (cl) ∩ Var(X̃) ⊆ Var (B), Var (B) ∩ Var(r̃, C) ⊆ Var (X̃),
Var (C[B], C[p(X̃)]) ∩ Var (CI , c) ⊆ Var(r̃), Var (c′ ) ∩ Var (r̃) ⊆ Var (CI [C[B]], c) and
there exists n such that wt (CI [C[B]], c, c′ ) = n. Then,
Var (B) ∩ Var (CI [C[ ]], c) ⊆ Var (B) ∩ Var (r̃, C) ⊆ Var(X̃)

(11)

Var(c′ ) ∩ Var (r̃) ⊆ Var (CI [C[B]], c) ∩ Var (r̃) ⊆ Var(CI [C[p(X̃)]], c)

(12)

and
hold. Moreover, we can assume without loss of generality that Var(c′ ) ∩ Var(X̃) ⊆
Var (CI [C[B]], c).
Since f ∈ D0 , from (11) and Point 2 of Lemma 4.11 it follows that there exists a
constraint d′ such that wt (CI [C[p(X̃)]], c, d′ ) ≤ wt (CI [C[B]], c, c′ ) and
∃−Var (CI [C[p(X̃)]],c) d′ = ∃−Var (CI [C[p(X̃)]],c) c′ .

(13)

We can assume, without loss of generality, that Var (d′ ) ⊆ Var (CI [C[p(X̃)]], c). Then
by using (12) and (13) we obtain that ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ which
concludes the proof of a).
b). Assume that the parts 1 and 2 of this Lemma hold for i ≥ 0. We prove that
1 holds for i + 1 > 0.
Let cl : q(r̃) ← H ∈ Di+1 , and let c̄l : q(r̃) ← H̄ be the corresponding declaration
in Di . Moreover let CI [ ] be a context, c a satisfiable constraint and let c′ be a
constraint, such that Var(H) ∩ Var (CI , c) ⊆ Var (r̃) and wt (CI [q(r̃)], c, c′ ) is defined.
Without loss of generality, we can assume that Var (H̄)∩Var (CI , c) ⊆ Var(r̃). Then,
since by inductive hypothesis, part 1 holds for i, there exists a constraint d1 such
that Var (d1 ) ⊆ Var (CI [H̄], c),
wt (CI [H̄], c, d1 ) ≤ wt (CI [q(r̃)], c, c′ ) and ∃−Var (CI [q(r̃)],c) d1 = ∃−Var (CI [q(r̃)],c) c′ . (14)
Since by inductive hypothesis part 2 holds for i, there exists a constraint d′ , such
that Var(d′ ) ⊆ Var (CI [H], c), wt (CI [H], c, d′ ) ≤ wt (CI [H̄], c, d1 ) and ∃−Var (CI [q(r̃)],c) d′ =
∃−Var (CI [q(r̃)],c) d1 . By (14), wt (CI [H], c, d′ ) ≤ wt (CI [q(r̃)], c, c′ ) and ∃−Var (CI [q(r̃)],c) d′ =
∃−Var (CI [q(r̃)],c) c′ and then the thesis follows.
We finally obtain our first main theorem.
Theorem 4.13 (Total Correctness). Let D0 , . . . , Dn be a transformation sequence. Then, for any agent A, O(D0 .A) = O(Dn .A).
Proof. (Sketch). The proof proceeds by showing simultaneously, by induction
on i, that for i ∈ [0, n]:
(1) for any agent A, O(D0 .A) = O(Di .A);
(2) Di is weight complete.
Base case. We just need to prove that D0 is weight complete. Assume that there
exists a derivation hD0 .A, cI i →∗ hD0 .B, cF i, where cI is a satisfiable constraint and
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

27

m(B, cF ) ∈ {ss, dd, ff}. Then there exists a derivation ξ : hD0 .A, cI i →∗ hD0 .B′ , c′F i,
such that m(B′ , c′F ) = m(B, cF ), whose weight is minimal and where ∃−Var (A,cI ) c′F =
∃−Var (A,cI ) cF . It follows from Definition 4.7 that ξ is a split derivation.
Induction step.
By the inductive hypothesis for any agent A, O(D0 .A) = O(Di−1 .A) and Di−1 is
weight complete. From propositions 4.5 and 4.9 it follows that if Di is weight
complete then for any agent A, O(D0 .A) = O(Di .A). So, in order to prove parts 1
and 2, we only have to show that Di is weight complete.
Assume then that there exists a derivation hD0 .A, cI i →∗ hD0 .B, cF i such that cI
is a satisfiable constraint and m(B, cF ) ∈ {ss, dd, ff}. From the inductive hypothesis
it follows that there exists a split derivation
χ = hDi−1 .A, cI i →∗ hDi−1 .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i
where
∃−Var (A,cI ) c′′F = ∃−Var (A,cI ) cF and m(B′′ , c′′F ) = m(B, cF ).

(15)

Let d ∈ Di−1 \Di be the modified clause in the transformation step from Di−1 to Di .
If in the first m steps of χ there is no procedure call which uses d then clearly
there exists a split derivation ξ in Di ∪ D0 ,
ξ = hDi .A, cI i →∗ hDi .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i
which performs the same steps of χ and then the thesis holds.
Otherwise, assume without loss of generality that R4 is the rule used in the first
step of derivation χ and that d is the clause employed in the first step of χ. We
also assume that the declaration d is used only once in χ, since the extension to
the general case is immediate.
We have to distinguish various cases according to what happens to the clause d
when moving from Di−1 to Di . As before, we consider here only the unfolding and
the folding cases, the others being deferred to the Appendix.
Unfolding: Assume that d is unfolded and let d′ be the corresponding declaration
in Di . The situation is the following:
- d : q(r̃) ← C[p(t̃)] ∈ Di−1 ,
- u : p(s̃) ← H ∈ Di−1 , and
- d′ : q(r̃) ← C[H k tell(t̃ = s̃)] ∈ Di ,
where d and u are assumed to be renamed apart. By the definition of split derivation, χ has the form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Am , cm i →
hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i.
Without loss of generality, we can assume that Var (χ) ∩ Var(u) 6= ∅ if and only if
p(t̃) is evaluated in the first m steps of χ, in which case u is used for evaluating it.
We have to distinguish two cases.
1) There exists k < m such that the k-th derivation step of χ is the procedure
call p(t̃). In this case χ has the form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Ck [p(t̃)], ck i →
hDi−1 .Ck [H k tell(t̃ = s̃)], ck i →∗ hDi−1 .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

·

28

Sandro Etalle et al.

Then there exists a corresponding derivation in Di ∪ D0
ξ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Ck [H k tell(t̃ = s̃)], ck i →∗ hDi .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i,
which performs exactly the same steps of χ except for a procedure call to p(t̃). In
this case the proof follows by observing that, since by the inductive hypothesis χ
is a split derivation, the same holds for ξ.
2) There is no procedure call to p(t̃) in the first m steps. Therefore χ has the
form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Cm [p(t̃)], cm i →
hD0 .Cm+1 [p(t̃)], cm i →∗ hD0 .B′′ , c′′F i.
Then, by the definition of Di , there exists a derivation
ξ0 = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Cm [H k tell(t̃ = s̃)], cm i → hD0 .Cm+1 [H k tell(t̃ = s̃)], cm i.
Observe that from the derivation hD0 .Cm+1 [p(t̃)], cm i →∗ hD0 .B′′ , c′′F i and (15) it
follows that
wt (Cm+1 [p(t̃)], cm , c′′F ) is defined, where t = m(B, cF ).

(16)

The hypothesis on the variables implies that Var (Cm+1 [p(t̃)], cm ) ∩ Var (u) = ∅.
Then, by the definition of transformation sequence and since u ∈ Di−1 , there exists
a declaration p(s̃) ← H0 ∈ D0 . By Lemma 4.10 and part 1 of Lemma 4.12 it follows
that there exists a constraint dF such that
wt (Cm+1 [H k tell(t̃ = s̃)], cm , dF ) ≤ wt (Cm+1 [p(t̃)], cm , c′′F )

(17)

∃−Var (Cm+1 [p(t̃)],cm ) dF = ∃−Var (Cm+1 [p(t̃)],cm ) c′′F .

(18)

and

Therefore, by the definition of wt , by (17) and since
there exists a derivation

wt (Cm+1 [p(t̃)], cm , c′′F )

is defined,

ξ1 = hD0 .Cm+1 [H k tell(t̃ = s̃)], cm i →∗ hD0 .B′ , c′F i,
where ∃−Var (Cm+1 [H k tell(t̃=s̃)],cm ) c′F = ∃−Var (Cm+1 [H k tell(t̃=s̃)],cm ) dF and, by (16),
m(B′ , c′F ) = m(B, cF ).

(19)

∃−Var (Cm+1 ,cm ) c′F = ∃−Var (Cm+1 ,cm ) c′′F

(20)

By (18)

holds and, by definition of weight, we obtain
wt (Cm+1 [H k tell(t̃ = s̃)], cm , c′F ) = wt (Cm+1 [H k tell(t̃ = s̃)], cm , dF ).

(21)

Moreover, we can assume without loss of generality that Var(ξ0 ) ∩ Var (ξ1 ) =
Var (Cm+1 [H k tell(t̃ = s̃)], cm ). Then, by the definition of procedure call
Var (CI [q(ṽ)], cI ) ∩ (Var (c′F ) ∪ Var(c′′F )) ⊆ Var (Cm+1 , cm )
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

(22)

Transformations of CCP programs

·

29

and there exists a derivation
ξ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Cm [H k tell(t̃ = s̃)], cm i → hD0 .Cm+1 [H k tell(t̃ = s̃)], cm i →∗ hD0 .B′ , c′F i
such that the first m−1 derivation steps do not use rule R2 and the m-th derivation
step uses the rule R2. Now, we have the following equalities
∃−Var (CI [q(ṽ)],cI ) c′F
∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm+1 ,cm ) c′F )
∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm+1 ,cm ) c′′F )
∃−Var (CI [q(ṽ)],cI ) c′′F
∃−Var (CI [q(ṽ)],cI ) cF .

=
=
=
=

(by
(by
(by
(by

(22) and by construction)
(20))
(22) and by construction)
the first statement in (15))

By the definition of weight, wt (CI [q(ṽ)], cI , c′F ) = wt (CI [q(ṽ)], cI , c′′F ), by (21) and (17),
wt (Cm+1 [H k tell(t̃ = s̃)], cm , c′F ) ≤ wt (Cm+1 [p(t̃)], cm , c′′F ) and wt (Cm+1 [p(t̃)], cm , c′′F ) <
wt (CI [q(ṽ)], cI , c′′F ), since χ is a split derivation. Therefore wt (Cm+1 [H k tell(t̃ =
s̃)], cm , c′F ) < wt (CI [q(ṽ)], cI , c′F ) and then, by definition, ξ is a split derivation in
Di ∪ D0 . This, together with (19), implies the thesis.
Folding: Assume that d is folded and let
- d : q(r̃) ← C[H] be the folded declaration (∈ Di−1 ),
- f : p(X̃) ← H be the folding declaration (∈ D0 ),
- d′ : q(r̃) ← C[p(X̃)] be the result of the folding operation (∈ Di ),
where, by definition of folding, Var(d) ∩ Var(X̃) ⊆ Var (H) and Var (H) ∩ (Var (r̃) ∪
Var (C)) ⊆ Var (X̃). Since C[ ] is a guarding context, the agent H in C[H] appears
in the scope of an ask guard. By definition of split derivation χ has the form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[H] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Cm [H], cm i →
hD0 .Cm+1 [H], cm i →∗ hD0 .B′′ , c′′F i,
where Cm [ ] is a guarding context. Without loss of generality we can assume that
Var (χ) ∩ Var (X̃) ⊆ Var(H). Then, from the definition of Di it follows that there
exists a derivation
ξ0 = hDi .CI [q(ṽ)], cI i → hDi .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Cm [p(X̃)], cm i → hD0 .Cm+1 [p(X̃)], cm i,
which performs exactly the first m steps as χ. Since hD0 .Cm+1 [H], cm i →∗ hD0 .B′′ , c′′F i,
the definition of weight implies that wt (Cm+1 [H], cm , c′′F ) is defined, where t =
m(B′′ , c′′F ). Then, by (15), we have that
t = m(B, cF ).

(23)

The definitions of derivation and folding imply that Var(H) ∩ Var (Cm+1 , cm ) ⊆
Var (H) ∩ (Var (C,r̃)) ⊆ Var(X̃) holds. Moreover, from the assumptions on the variables, we obtain that Var (c′′F )∩Var (X̃) ⊆ Var (H). Thus, from part 2 of Lemma 4.11
it follows that there exists a constraint d′ such that
wt (Cm+1 [p(X̃)], cm , d′ ) ≤ wt (Cm+1 [H], cm , c′′F ) and
∃−Var (Cm+1 [p(X̃)],cm ) d′ = ∃−Var (Cm+1 [p(X̃)],cm ) c′′F .

(24)
(25)

¿From the definition of weight and the fact that wt (Cm+1 [H], cm , c′′F ) is defined it follows that there exists a derivation ξ1 = hD0 .Cm+1 [p(X̃)], cm i →∗ hD0 .B′ , c′F i, where
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

30

·

Sandro Etalle et al.

m(B′ , c′F ) = t and ∃−Var (Cm+1 [p(X̃)],cm ) c′F = ∃−Var (Cm+1 [p(X̃)],cm ) d′ . Then, by the definition of weight, wt (Cm+1 [p(X̃)], cm , c′F ) = wt (Cm+1 [p(X̃)], cm , d′ ) and therefore, by
(24) and (25),
∃−Var (Cm+1 [p(X̃)],cm ) c′F = ∃−Var (Cm+1 [p(X̃)],cm ) c′′F and
wt (Cm+1 [p(X̃)], cm , c′F ) ≤ wt (Cm+1 [H], cm , c′′F )

(26)
(27)

hold. Moreover, from (23) we obtain
m(B′ , c′F ) = m(B, cF ).

(28)

Without loss of generality, we can now assume that
Var (ξ0 ) ∩ Var (ξ1 ) = Var (Cm+1 [p(X̃)], cm )
. Then, by (26), (27) and (15) it follows that
∃−Var (CI [q(ṽ)],cI ) c′F = ∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm+1 [p(X̃)],cm ) c′F ) =
∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm+1 [p(X̃)],cm ) c′′F ) =
∃−Var (CI [q(ṽ)],cI ) c′′F = ∃−Var (CI [q(ṽ)],cI ) cF .

(29)

¿From the definition of weight wt (CI [q(ṽ)], cI , c′F ) = wt (CI [q(ṽ)], cI , c′′F ) and since χ
is a split derivation we obtain wt (CI [q(ṽ)], cI , c′′F ) > wt (Cm+1 [H], cm , c′′F ). Then, from
(29) it follows that
wt (CI [q(ṽ)], cI , c′F ) > wt (Cm+1 [p(X̃)], cm , c′F )

(30)

and therefore, by construction,
ξ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗ hDi .Cm [p(X̃)], cm i →
hD0 .Cm+1 [p(X̃)], cm i →∗ hD0 .B′ , c′F i
is a derivation in Di ∪ D0 such that: (a) rule R2 is not used in the first m − 1 steps;
(b) rule R2 is used in the m-th step. The thesis then follows from (29), (28) and
(30) thus concluding the proof.
It is important to notice that – given the definition of observables we are adopting (Definition 4.1) – the initial program D0 and the final one Dn have exactly the
same successful derivations, the same deadlocked derivations and the same failed
derivations. The first feature (regarding successful derivations) is to some extent
the one we expect and require from a transformation, because it corresponds to the
intuition that Dn “produces the same results” as D0 . Nevertheless, also the second feature (preservation of deadlock derivations) has an important role. Firstly,
it ensures that the transformation does not introduce deadlock points, which is of
crucial importance when we are using the transformation for optimizing a program.
Secondly, as exemplified in the Section 6, this feature allows us to use the transformation as a tool for proving deadlock freeness (i.e., absence of deadlock). In fact,
if, after the transformation we can prove or see that the process Dn .A does never
deadlock, then we are also sure that D0 .A does not deadlock either.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

31

5. CORRECTNESS FOR NON-TERMINATING COMPUTATIONS
The correctness results obtained so far consider terminating (successful and deadlocked) and failed computations only. This is satisfactory for many applications
of concurrent constraint programming which have a “transformational” behaviour,
i.e. which are supposed to produce a (finite) output for a given (finite) input. In
this respect, it is worth noting that the two main semantic models of CCP consider essentially the same notion of observables we used. In fact, the model based
on linear sequences defined in [de Boer and Palamidessi 1991] characterizes (in a
fully abstract way) the results of terminating computations, together with a termination mode indicating success, deadlock or failure6 . Such a model has been
proved ([de Boer and Palamidessi 1992]) to be isomorphic to the semantics based
on (bounded) closure operators introduced in [Saraswat et al. 1991], provided that
the termination mode and the consistency checks are eliminated.
So, our correctness results are adequate in the sense that they ensure that the
standard semantics of CCP is preserved. On the other hand, as in the case of any
other concurrent programming paradigm, CCP programs may have a “reactive” nature: rather than producing a final result they produce a (possibly non-terminating)
sequence of intermediate results in response to some external stimuli. For these programs the notion of observables employed in Theorem 4.13 and the related results
are not adequate, since they exclude non-terminating computations.
When considering non-terminating computations one is interested in observing
(possibly in terms of traces) the intermediate results, that is the constraints produced also by non-maximal derivations, rather than the final limit of the computation (note however that in CCP such a notion of limit makes sense, as the store
grows monotonically). Therefore, in the remainder of this section we first discuss
the correctness of our system w.r.t. this new class of observables. Then, we show
a modification of our transformation system and we present a stronger correctness
result, which guarantees that (traces of) intermediate results are preserved.
5.1 Partial preservation of intermediate results
It is easy to see that the system we have proposed does not preserve the intermediate
results of computations. More precisely, let us define these observables as follows:
Oi (D.A) = {hc, ∃−Var (A,c) d, ppi | c and d are satisfiable, and there exists
a derivation hD.A, ci →∗ hD.B, di
}
(the symbol pp indicates here that we consider results obtained from “partial”, that
is, possibly not maximal, derivations). Now, it is easy to see that the operations
of ask and tell simplification are neither partially nor totally correct w.r.t. the
semantics Oi (D.A). In fact, the ask simplification allows one to transform the agent
A : tell(c) k ask(true) → tell(d)
6 There

are irrelevant differences between the observables considered in [de Boer and Palamidessi
1991] and the ones we used, due to the treatment of failure and to the existential quantification
on local variables.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

32

·

Sandro Etalle et al.

into the agent
A′ : tell(c) k ask(c) → tell(d).
While the agent A, when evaluated in the empty store, produces the intermediate
result d, this is not the case for the agent A′ (we assume that c∧d 6= d). Analogously,
assuming that D |= d → c and D |= d → c′ , the tell simplification allows one to
transform
B : tell(c) k tell(d)
into the agent
B′ : tell(c′ ) k tell(d)
and the agents B and B′ have different intermediate results. Other operations
which are not correct w.r.t. the above semantics are the distribution and the tell
elimination and introduction.
Nevertheless, the system we have defined does preserve already a form of intermediate results. This is shown by the following theorem.
Theorem 5.1 (Total Correctness 2). Let D0 , . . . , Dn be a transformation
sequence, and A be an agent.
—If there exists a derivation hD0 .A, ci →∗ hD0 .B, di then there exists a derivation
hDn .A, ci →∗ hDn .B′ , d′ i such that D |= ∃−Var(A,c) d′ → ∃−Var(A,c) d.
—Conversely, if there exists a derivation hDn .A, ci →∗ hDn .B, di then there exists a
derivation hD0 .A, ci →∗ hD0 .B′ , d′ i with D |= ∃−Var(A,c) d′ → ∃−Var(A,c) d.
Proof. The proof of this result is essentially the same as that one of the total
correctness Theorem 4.13 provided that in such a proof, as well as in the proofs of
the related preliminary results, we perform the following changes:
(1) Rather than considering terminating derivations, we consider any (possibly
non-maximal) finite derivation.
(2) Whenever in a proof we write that, given a derivation ξ, a derivation ξ ′ is
constructed which performs the same steps ξ does, possibly in a different order,
we now write that a derivation ξ ′′ is constructed which performs the same step
of ξ (possibly in a different order) plus some other additional steps. Since
the store grows monotonically in CCP derivations, clearly if a constraint c is
the result of the derivation ξ, then a constraint c′′ is the result of ξ ′′ such
that D |= c′′ → c holds. For example, for case 2 in the proof of Proposition
4.5, when considering a (non-maximal) derivation ξ which uses the declaration
H ← C[tell(s̃ = t̃)] k B] we can always construct a derivation ξ ′′ which performs
all the steps of ξ (possibly plus others) and such that the tell(s̃ = t̃) agent is
evaluated before B. Differently from the previous proof, now we are not ensured
that the result of ξ is the same as that one of ξ ′′ , since ξ is non-maximal (thus,
ξ could also avoid the evaluation of tell(s̃ = t̃)). However, we are ensured that
the result of ξ ′′ is stronger (i.e. implies) that one of ξ.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

33

This result ensures that the original and the transformed program have the same
intermediate results up to logical implication: If the evaluation of an agent in
the original program produces a constraint d, then a constraint stronger than d is
produced in the transformed program and vice versa. The vice versa is important,
as it ensures that the transformed program will never produce something that could
not be produced by the original program, up to implication. Clearly, this result is
relevant in presence of non-terminating computations (which were not covered by
Theorem 4.13).
In order to maintain a consistent notation throughout the paper, the above result
can be reformulated in terms of the following class of observables
Oic (D.A) = {hc, ∃−Var (A,c) d, ppi | c is satisfiable, there exists a derivation
hD.A, ci →∗ hD.B, d′ i
and D |= ∃−Var (A,c) d′ → ∃−Var (A,c) d
}
where the subscript ic stands for implication closure (of intermediate results). We
then have following Corollary whose proof is immediate.
Corollary 5.2. Let D0 , . . . , Dn be a transformation sequence. Then, for any
agent A, Oic (D0 .A) = Oic (Dn .A).
This result guarantees a degree of correctness which should be sufficient for many
reactive programs employing non-terminating computations. In fact, when transforming a program, probably one should not expect to be able to preserve exactly
each intermediate result the original program was producing.
Nevertheless, it is of interest to check if it is possible to modify the system in
order to obtain stronger correctness results. We do this in the following section.
5.2 Full preservation of intermediate results
In this section we introduce a few restrictions on our transformation system and we
prove that they guarantee the preservation of the whole sequence of intermediate
results of a program.
As previously mentioned, the only operations not preserving the intermediate
results are the ask and tell simplification, the distribution and the tell elimination
and introduction. As it possibly appears from the example above, the problem using
the ask and tell simplification lies in the fact that one can modify the arguments
of ask and tell agents by taking into account (via the “produced constraint”) also
the constraints introduced by tell actions appearing in the parallel context (see
Definitions 3.4 and 3.6). This clearly can affect the intermediate results of the
computations, since no order is imposed on the evaluation of parallel agents. This
reasoning applies to the distribution operation as well.
We have then to modify the ask and tell simplification and the distribution by
considering a weaker notion of “produced constraint”, which includes only those
constraints which have certainly been produced before reaching the ask or tell agent
we are simplifying. Such a notion is defined as follows.
Definition 5.3. Given a context C[ ] the weakest produced constraint wpc(C[ ])
of C[ ] is inductively defined as follows:
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

34

·

Sandro Etalle et al.

wpc([ ]) = true
′
′
wpc(C
P[n ] k B) = wpc(C [ ])
wpc( i=1 ask(ci ) → Ai ) = cj ∧ wpc(C′ [ ]) where j ∈ [1, n] and Aj = C′ [ ].
For example, the weakest produced constraint of [ ] k tell(c) is true, while the
weakest produced constraint of tell(c) k ask(d) → (ask(e) → [ ]) is d ∧ e. We can
then define the weak equivalence of two constraints within a given context C[ ] as
follows.
Definition 5.4. Let c, c′ be constraints, C[ ] be a context, and Z̃ be a set of
variables. We say that c is weakly equivalent to c′ within C[ ] and w.r.t. the
variables in Z̃ iff D |= ∃−Z̃ (wpc(C[ ]) ∧ c) ↔ ∃−Z̃ (wpc(C[ ]) ∧ c′ ).
Using this definition we can modify the operations of ask and tell simplification
and of distribution by simply replacing the context equivalence used in Definition
3.6 with the above notion of weak context equivalence. For the sake of clarity we
state below the resulting definitions.
Definition 5.5 (Restricted Ask and Tell Simplification). Let D be a set
of declarations.
Pn
(1) Let d : H ← C[ i=1 ask(ci ) → Ai ] be a declaration of D. Suppose that c′1 , . . . , c′n
are constraints such that for j ∈ [1, n], c′j is weakly equivalent to cj within
C[ ] and w.r.t.
Pn the variables in Var(C, H, Aj ). Then we can replace d with
d′ : H ← C[ i=1 ask(c′i ) → Ai ] in D. We call this a restricted ask simplification
operation.
(2) Let d : H ← C[tell(c)] be a declaration of D. Suppose that the constraint c′ is
weakly equivalent to c within C[ ] and w.r.t. the variables in Var (C, H). Then
we can replace d with d′ : H ← C[tell(c′ )] in D. We call this a restricted tell
simplification operation.
Definition 5.6 (Restricted Distribution). Let D be a set of declarations and
let
Pn
d : H ← C[A k i=1 ask(ci ) → Bi ]

be a declaration in D. Let also e = wpc(C[ ]). The restricted distribution of A in d
yields the definition
Pn
d′ : H ← C[ i=1 ask(ci ) → (A k Bi )]

provided that for every constraint c such that Var (c) ∩ Var(d) ⊆ Var (H, C), if
hD.A, c ∧ ei is productive then both the following conditions hold:
(a) There exists at least one i ∈ [1, n] such that D |= (c ∧ e) → ci ,
(b) for each i ∈ [1, n], either D |= (c ∧ e) → ci or D |= (c ∧ e) → ¬ci .

Remark 3.12 is also sufficient for guaranteeing that the restricted distribution
operation is applicable. Thus we have the following.
Remark 5.7. Referring to Definition 5.6. If A requires a variables which does not
occur in H, C[ ], then the restricted distribution operation is applicable.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

35

Also the tell elimination and the tell introduction operations do not preserve the
intermediate results of computations. This is not due to the presence of the produced
constraint, but rather to the very nature of the operation which can eliminate or
introduce constraints which, via the local variables, can (temporarily) affect also
the values of global variables. For example, the declaration
d : p(Y) ← tell(Z = a) k tell(Y = f(Z))
can be transformed via a tell elimination into
d′ : p(Y) ← tell(Y = f(a))
The evaluation of p(Y) in the empty store and using d produces the (intermediate)
result Y = f(Z), while this is not the case if one uses the declaration d′ . We can
solve this problem by simply requiring that if we eliminate a tell by applying the
resulting substitution to the parallel context B, then B does not contain any variable
appearing the head or in the outer context. Thus we have the following.
Definition 5.8 (Restricted Tell Elimination and Tell Introduction).
The declaration
d : H ← C[tell(s̃ = t̃) k B]
can be transformed via a restricted tell elimination into
d′ : H ← C[Bσ]
where σ is a relevant most general unifier of s̃ and t̃, provided that the variables in
the domain of σ do not occur neither in C[ ] nor in H, and that Var (B) ∩ Var (H, C) =
∅. Again, this operation is applicable either when the computational domain admits
a most general unifier, or when s̃ and t̃ are sequence of distinct variables, in which
case σ is simply a renaming. On the other hand, the declaration
d : H ← C[Bσ]
can be transformed via a restricted tell introduction into
d′ : H ← C[tell(X̃ = X̃σ) k B]
provided that σ is a substitution such that X̃ = Dom(σ) and Dom(σ) ∩ (Var (C[ ], H)∪
Ran(σ)) = ∅, and that Var (B) ∩ Var (H, C) = ∅.
At this point it is worth recalling that the tell elimination is often used for
making variable bindings explicit after an unfolding operation: In fact we start
from a definition of the form d : H ← C[p(t̃)] and by unfolding p(t̃) we end with
d′ : H ← C[B k tell(t̃ = s̃)] (provided that p is defined by u : p(s̃) ← B). Then we
want to eliminate tell(t̃ = s̃) from d′ in order to perform the “parameter passing”.
Since d and u are always renamed apart, clearly the additional condition of the
restricted tell elimination (Var (B) ∩ Var(H, C) = ∅) is always satisfied here. So, in
general, this operation is applicable every time that t̃ is an instance of s̃.
We can finally define the restricted transformation system as follows.
Definition 5.9. A restricted transformation sequence is a sequence of programs
D0 , . . . , Dn in which D0 is a initial program and each Di+1 is obtained from Di
via one of the following operations: unfolding, backward instantiation, restricted
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

36

·

Sandro Etalle et al.

tell elimination, restricted tell introduction, restricted ask and tell simplification,
branch elimination, conservative ask elimination, restricted distribution and folding.
Clearly, the restricted transformation operations are applicable in fewer situations
than their non-restricted counterparts, yet they are useful in many cases. Example
6.1 shows a case of an unfold-fold transformation sequence using only restricted
operations and the other examples contain several occurrences of them. We now
prove that the restricted system is correct w.r.t. the trace semantics of CCP. Here
and in the following we denote by c1 ; c2 ; . . . ; cn a sequence of constraints, also called
trace.
Definition 5.10 (Traces). Let D.A be a CCP process. We define Ot (D.A) =
{hc1 ; c2 ; . . . ; cn , ssi | there exists a derivation
hD.A, d1 i → hD.A2 , d2 i → . . . → hD.Stop, dn i
di is satisfiable for each i ∈ [1, n],
c1 = d1 and cj = ∃−Var (A,c1 ) dj for each j ∈ [2, n]}
∪
{hc1 ; c2 ; . . . ; cn , ddi | there exists a derivation
hD.A, d1 i → hD.A2 , d2 i → . . . → hD.An , dn i 6→
An 6= Stop, di is satisfiable for each i ∈ [1, n],
c1 = d1 and cj = ∃−Var (A,c1 ) dj for each j ∈ [2, n]}
∪
{hc1 ; c2 ; . . . ; cn , ppi | there exists a derivation
hD.A, d1 i → hD.A2 , d2 i → . . . → hD.An , dn i
di is satisfiable for each i ∈ [1, n],
c1 = d1 and cj = ∃−Var (A,c1 ) dj for each j ∈ [2, n]}
∪
{hc1 ; c2 ; . . . ; cn , ffi | there exists a derivation
hD.A, d1 i → hD.A2 , d2 i → . . . → hD.An , dn i 6→
di is satisfiable for each i ∈ [1, n − 1], dn = false
c1 = d1 and cj = ∃−Var (A,c1 ) dj for each j ∈ [2, n].}
Thus what we observe are the finite traces consisting of the constraints produced by
any (possibly non-terminating) derivation. As before, we abstract from the values
for the local variables in the results, and we make distinction between the successful
traces (termination mode ss), the deadlocked ones (dd), the partial (i.e. possibly
non maximal) traces (pp) and the failed ones (ff). Note that, due to the monotonic
computational model of CCP which does not allow us to retract information from
the global store, the traces we observe are monotonically increasing. That is, given
a trace c1 ; c2 ; . . . ; cn appearing in the observables, we have that D |= ci → cj for
each i, j ∈ [1, n] such that i ≥ j. Before giving the correctness result, we need one
last definition.
Definition 5.11. We say that a trace c1 ; c2 ; . . . ; cn is simulated by a trace
d1 ; d2 ; . . . ; dm , notation c1 ; c2 ; . . . ; cn  d1 ; d2 ; . . . ; dm , iff there exists
{j1 , . . . jn } ⊆ {1, 2, . . . , m} such that
(1) ci = dji for each i ∈ [1, n];
(2) j1 = 1, jn = m and ji ≤ jk iff i < k.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

37

So, a trace s is simulated by a trace s′ iff they have the same first and last element
and, all components appearing in s appear, in the same order, in s′ .
We can now state our strongest correctness result. Its proof, contained in the
Appendix, follows the guidelines of that one of Theorem 4.13. In fact, the definitions of mode, weight, split derivation and weight complete program can readily
be extended to consider traces and weakest produced constraints, rather than input/output pairs and produced constraints. Then it is easy to extend all the technical lemmata needed for Theorem 4.13 in order to obtain the preliminary results
needed in the proof of the following.
Theorem 5.12 (Strong Total Correctness). Let D0 , . . . , Dn be a restricted
transformation sequence, and A be an agent.
—If hs, xi ∈ Ot (D0 .A) (with x ∈ {ss, dd, pp, ff}) then there exists hs′ , xi ∈ Ot (Dn .A)
such that s  s′ .
—Conversely, if hs, xi ∈ Ot (Dn .A) then there exists hs′ , xi ∈ Ot (D0 .A) such that
s  s′ .
As it results from the definition of , we do not have exactly the equality of
traces since in some traces we might introduce some intermediate steps. However,
notice that these additional steps do not introduce new values, rather they can
be seen as different “approximation” to obtain a given constraint, since we consider here monotonically increasing traces. This can best be explained by means
of an example. Consider the following one-line program D0 : p(Y) ← tell(X =
f(a,W)) k tell(X = f(Z,b)) k tell(X = Y). Its trace semantics Ot (D0 .p(Y)) contains
ht, ssi, where t is the trace (true; true; true; Y = f(a, b)). If we apply here a
restricted tell evaluation to tell(X = Y) we obtain the program D1 : p(Y) ← tell(Y
= f(a,W)) k tell(Y = f(Z,b)). Now, Ot (D1 .p(Y)) does not contain t: one cannot
obtain Y = f(a, b) from true in one step. On the other hand, Ot (D1 .p(Y)) contains
h(true; ∃W Y = f(a, W); Y = f(a, b)), ssi and h(true; ∃Z Y = f(Z, b); Y = f(a, b)), ssi
and both the two traces appearing in these pairs simulate t. Notice also that the
intermediate results semantics is now preserved. In fact, the following is an immediate consequence of Theorem 5.12.
Corollary 5.13. Let D0 , . . . , Dn be a restricted transformation sequence, and
A be an agent. Then Oi (D0 .A) = Oi (Dn .A).
5.3 Preservation of infinite traces
It is worth noting that Theorem 5.12 can be extended to consider also infinite
traces, as we show below.
In the following we indicate by |si | the length of a trace si and we say that a
configuration hD.A, c1 i produces the trace c1 ; c2 ; . . . ; cn iff there exists a derivation
hD.A, d1 i → hD.A2 , d2 i → . . . → hD.An , dn i such that c1 = d1 and cj = ∃−Var (A,c1 ) dj
for each j ∈ [2, n]. This notion can be extended to consider infinite computations
(and infinite traces) in the obvious way. We also call an infinite trace c1 ; c2 . . .
“active” iff, for any i ≥ 1, there exists j > i such that D |= ¬(ci → cj ) (on the other
hand, the implication D |= (cj → ci ) holds for any j ≥ i when considering traces
produced by CCP derivations, since they are monotonically increasing). So, an
active trace is that one produced by a computation which continuously updates the
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

38

·

Sandro Etalle et al.

store by adding new constraints. Clearly, when considering infinite computations,
one is interested mainly in those producing active traces, as the others are essentially
pure loops which stop producing new results after a finite number of steps.
The essential result we use for extending Theorem 5.12 to infinite traces is the
following: If a CCP configuration can produce all the finite prefixes of an infinite
trace, then it can produce the infinite trace itself. The following Lemma contains
a slightly stronger version of it. With a minor abuse of notation, in the following
we denote by ; also the operator which concatenates traces. Thus, if si are traces
and ci are constraints, for i ∈ [1, n], then c1 ; s1 ; c2 ; s2 . . . ; sn−1 ; cn denotes the trace
obtained by concatenating the si e ci in the obvious way.
Lemma 5.14. Let D.A be a CCP process and c0 be a constraint. Assume that
hD.A, c0 i produces the (infinitely many) finite traces
c0
c0 ; s1,1 ; c1
c0 ; s2,1 ; c1 ; s2,2 ; c2
c0 ; s3,1 ; c1 ; s3,2 ; c2 ; s3,3 ; c3
..
.
where the c0 , c1 , c2 . . . are different constraints (i.e. for any i, D |= ¬(ci → ci+1 ))
and the si,j are (finite) sub-traces such that, for each j ≥ 1, the (infinite) set containing the lengths {|s1,j |, |s2,j |, |s3,j |, . . .} admits a (finite) maximal element. Then
hD.A, c0 i produces also the infinite trace c0 ; s1 ; c1 ; s2 ; c2 ; s3 ; c3 ; . . . where, for each
j ≥ 1, sj = si,j for some i ≥ 1.
Proof. The proof uses the Koenig Lemma and the fact that the transition
system defining the CCP operational semantics is finitely branching.
Let us denote by mj the maximal element appearing in the set ({|s1,j |, |s2,j |, |s3,j |, . . .},
for each j ≥ 1, that is, mj is the maximal length of the sub-traces si,j for a fixed
j and i = 1, 2, . . .. We now construct a tree T representing the (infinitely many)
finite traces
c0
c0 ; s1,1 ; c1
c0 ; s2,1 ; c1 ; s2,2 ; c2
c0 ; s3,1 ; c1 ; s3,2 ; c2 ; s3,3 ; c3
..
.
produced by hD.A, c0 i. The nodes of the tree T are labeled by configurations of the
form hD.B, ci i, for some i, and the edges are labeled by the sub-traces si,j . More
precisely, the tree T is defined inductively as follows:
(Base step). The root (level 0) of T is labeled by hD.A, c0 i. For each derivation
of the form hD.A, c0 i →∗ hD.Ai,1 , c1 i which performs at most m1 + 1 transition steps
and which produces the trace c0 ; si,1 we add a son N of the root (at level 1) labeled
by hD.Ai,1 , c1 i and an edge, labeled by si,1 , connecting the root and N .
(Inductive step). Assume that T has depth n − 1 and let hD.Ai,n−1 , cn−1 i be a
configuration labeling a node N at level n − 1. For each derivation of the form
hD.Ai,n−1 , cn−1 i →∗ hD.Ai,n , cn i which performs at most mn + 1 transition steps
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

39

we add a son N ′ of N labeled by hD.Ai,n , cn i and we add an edge labeled by si,n ,
connecting N and N ′ .
Note that the number of the configurations hD.Ai,n , cn i obtained in this way is
finite, since we allow at most mn + 1 transition steps. Therefore we construct a
finitely branching tree.
On the other hand, such a tree contains infinitely many nodes, as it contains
all the (different) constraints ci with i ≥ 1. Then, from the Koenig Lemma it
follows that the tree contains an infinite branch and this, by construction of the
tree, implies that hD.A, c0 i produces the infinite trace c0 ; s1 ; c1 ; s2 ; c2 . . . sn ; cn ; . . .
where, for each j ≥ 1, sj = si,j for some i ≥ 1.

We also need the following Lemma.
Lemma 5.15. Let D0 , . . . , Dn be a restricted transformation sequence, and A be
an agent. If hD0 .A, c0 i produces the trace c0 ; s1 ; c1 ; s2 ; c2 . . . sm ; cm , where the ci are
different constraints and the si are sub-traces of constraints all equal to ci−1 , then
hDn .A, c0 i produces the trace c0 ; s′1 ; c1 ; s′2 ; c2 . . . s′m ; cm such that, for any i ∈ [1, m],
there exists ki such that |s′i | ≤ |si | + ki . Furthermore, the vice versa (obtained by
exchanging D0 with Dn in the previous statement) holds as well.
Proof. The first part follows from Theorem 5.12. The part concerning the
length is a direct consequence of the definition of the transformation sequence,
since each transformation operation can at most add or delete a finite number of
computation step.

We then obtain the following extension of Theorem 5.12. Here we consider the
obvious extension of the relation  to the case of infinite traces.
Theorem 5.16. Let D0 , . . . , Dn be a restricted transformation sequence and A
be an agent.
—If hD0 .A, c0 i produces the infinite active trace s, then hDn .A, c0 i produces an infinite trace s′ such that s  s′ .
—Conversely, if hDn .A, c0 i produces the infinite active trace s, then hD0 .A, c0 i produces an infinite trace s′ such that s  s′ .
Proof. Assume that hD0 .A, c0 i produces the infinite active trace
t : c0 ; s 1 ; c1 ; s 2 ; c2 ; s 3 ; c3 . . .
where, in order to simplify the notation, we assume that the ci are different constraints while the si are sequences of constraints all equal to ci−1 (so the si are sequences of stuttering steps). Clearly, by definition of produced sequence, hD0 .A, c0 i
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

40

·

Sandro Etalle et al.

produces also the (infinitely many) finite prefixes of t
c0
c0 ; s 1 ; c1
c0 ; s 1 ; c1 ; s 2 ; c2
c0 ; s 1 ; c1 ; s 2 ; c2 ; s 3 ; c3
..
.
¿From Lemma 5.15 it follows that hDn .A, c0 i produces the traces
c0
c0 ; s′1,1 ; c1
c0 ; s′2,1 ; c1 ; s′2,2 ; c2
c0 ; s′3,1 ; c1 ; s′3,2 ; c2 ; s′3,3 ; c3
..
.
where, for any j ≥ 1, there exists kj such that for any i ∈ [1, j] we have that |s′i,j | ≤
|sj | + kj . Therefore the set {|s1,j |, |s2,j |, |s3,j |, . . .} admits a (finite) maximal element
for each j. Lemma 5.14 then implies that hDn .A, c0 i produces the infinite trace
t′ : c0 ; s′1 ; c1 ; s′2 ; c2 ; s′3 ; c3 . . . and clearly, by construction, t  t′ holds. Analogously
for the vice versa.
5.3.1 Preservation of Termination. The results we have presented guarantee the
correctness of the transformation system w.r.t. various semantics based on produced
constraints. We should mention however that these results do not imply that the
system preserves non-declarative properties such as termination. In fact, in case of
non-active traces (that from a certain point do not generate any new constraint),
the semantics we have considered equate infinite and finite traces.
A full treatment of infinite computations is beyond the scope of this paper and
is left for future work.
Nevertheless, we claim that the transformation system we have proposed here
cannot introduce non-termination. That is, if the initial program, for a given configuration, does not produce any infinite computations then this is the case also for
the transformed program.
We now provide a sketch of a proof of this claim by considering a specific class of
declarations, and by showing the intuitive, informal, argument that indicates the
proof methodology to be used for the general case.
Let us then assume that declarations does not contain mutually recursive definitions (note that mutually recursive definitions can usually be eliminated by means
of unfolding). We also concentrate on the restricted system, which preserves active traces. In the following we say that a configuration hD.A, ci terminates if it
produces only finite computations, while we say that it does not terminate if it
produces also at least one infinite derivation.
Let D0 , . . . , Dn be a transformation sequence, and assume that hDn .A, ci has
an infinite (non active)7 trace. This implies that there exists a derivation ξ =
7 In case of active traces, our result on the preservation of intermediate results guarantees the
preservation of termination.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

41

hDn .A, ci → hDn .A1 , c1 i →∗ . . . →∗ hDn .Aj , cj i →∗ . . ., where for some k, for each
i ≥ k, ∃Var(A,c) ci = ∃Var(A,c) ck holds. Assume also that for each i ∈ [0, n−1], hDi .A, ci
terminates.
It is easy to see that the only operation that might introduce non-termination
is the folding one (all other operations are clearly “safe” in this respect). So the
situation is the following::
d : H ← C[A′ ] ∈ Dn−1
f : B ← A′
∈ D0
d′ : H ← C[B] ∈ Dn
This operation can introduce non-termination only when it introduces recursion,
i.e., when the definition of B depends on the one of H. The typical case is when B
and H have the same predicate and in the following, for the sake of simplicity, we
assume that this is the case, so we assume that:
d:
f:
d′ :

p(X̃) ← C[A′ ]
∈ Dn−1
p(Ỹ) ← A′
∈ D0
p(X̃) ← C[p(Ỹ)] ∈ Dn

¿From the definition of folding we have that C[ ] is a guarding context and
Var(A′ ) ∩ Var(C, X̃) ⊆ Ỹ (f and d are suitably renamed so that the variables they
have in common are only those
in A′ ). Since C is a guarding context
Pn occurring
′
′
let us assume that C[ ] = C [ i=1 ask(ci ) → A′i ], where A′1 = C′′ [ ] and C′ [ ] and
C′′ [ ] are non-guarding contexts. If the infinite computation is due to the folding
operation then the derivation ξ must contain an infinite number of calls of the form
p(Ỹ)σi , where, for each i ≥ 1, σi is a renaming and the current the store di entails
c′1 σi . Moreover, assume that A is of the form C0 [p(ṽ)].
Now, by the definition of transformation sequence, the unfolding is the only
operation which can introduce a new ask action, thus the guard c′1 in the context
C[ ] was certainly introduced during an unfolding operation of an agent in A′ with
a recursive definition (recall that d must be obtained from f, thus, by unfolding A′
we must obtain C[A′ ], and that we are restricting to the case of direct recursion).
Therefore A′ must contain an atom q, whose definition in D0 is
d : q(Z̃) ← D[q(W̃)]

∈ D0

where the weakest produced constraint of D is precisely c′1 ρ, for some appropriate
renaming. Notice also that all tell actions present in D can be skipped (they are
always in parallel with the rest, they don’t form a guard). Because of this, by taking
c as initial store, one can show that there exist an infinite derivation starting from
hD0 .C0 [p(Ṽ)], ci where, from a certain point of the derivation j, the current store d
satisfies ∃Var(C0 [p(ṽ)],c) dj = ∃Var(C0 [p(ṽ)],c) c′1 .
This is in contrast with the hypothesis made on the original program, thus showing that no new infinite computation is generated.
In the rest of the paper we are going to provide some extra examples of transformations and – in the Appendix – the technical proofs of the correctness results.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

42

·

Sandro Etalle et al.

6. MORE EXAMPLES
The following example is inspired by the one in [Etalle et al. 1998]. It shows that the
transformation system can be used to simplify the dynamic behavior of a program
to the point that it can be used to prove deadlock freeness. All the operations used
in it are of the restricted sort; the transformation preserves thus the semantics of
the intermediate results as well as that of terminating derivations.
Here and in the following we say that a variable X is instantiated to a term t
in case the current store entails X = t. Accordingly, we also say that an agent
instantiates a variable X to t in case that the agent adds the constraint X = t to
the store. Finally, we say that X is instantiated if the store entails X = t for some
non variable term t.
Example 6.1. Consider the following simple Collect-Deliver program, which uses
a buffer of length one:
collect deliver ← collect(Xs) k deliver(Xs).
collect(Xs) ← % collects tokens and puts them in the queue Xs
ask(∃X,Xs′ Xs=[X|Xs’]) → tell(Xs=[X|Xs’]) k get token(X) k collect(Xs’)
+ ask(Xs=[ ]) → stop.
deliver([Y|Ys]) ← % delivers the tokens in the queue Xs
ask(Y=eof) → tell(Ys=[ ])
+ ask(Y 6= eof) → deliver token(Y) k deliver(Ys).

The dynamic behavior of this program is not elementary. collect(Xs) behaves as
follows: (a) it waits until more information for the variable Xs is produced, (b1)
if Xs is instantiated to [X|Xs’] (i.e. when the store entails ∃X,Xs′ Xs = [X|Xs’]) then
(by using get token(X)) it instantiates X with the value it collects, (b2) if Xs is
instantiated to [ ] it stops. On the other hand, the actions deliver(Xs) performs are:
(a) it instantiates Xs to [Y|Ys] (this activates collect(Xs)), then (b) it waits until Y
is instantiated. Now there are two possibilities: (c1) if Y is the end of file character
then it instantiates Ys to [ ] (this will also stop the collector), (c2) otherwise it
delivers Y (by using deliver token(Y)) and proceeds with the recursive call (which
will further activate collect).
Thus, collect-deliver actually implements a communication channel with a buffer
of length one, and Xs is a bidirectional communication channel. Note also that
proving that this program is deadlock-free is not trivial.
We now proceed with the transformation. First we unfold deliver(Xs) in the body
of the first definition. The result, after cleaning up the definition via a (restricted)
tell elimination is.
collect deliver ← collect([Y|Ys]) k
( ask(Y=eof) → tell(Ys=[ ])
+ ask(Y 6= eof) → deliver token(Y) k deliver(Ys)).

Then, we unfold collect([Y|Ys]) in the resulting definition; we obtain
collect deliver ←
( ask(∃X,Xs [Y|Ys]=[X|Xs]) → tell([Y|Ys]=[X|Xs]) k get token(X) k collect(Xs)
+ ask([Y|Ys]=[ ]) → stop)
k
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

43

( ask(Y=eof) → tell(Ys=[ ])
+ ask(Y 6= eof) → deliver token(Y) k deliver(Ys))

This definition can be simplified: first, by an ask simplification, we obtain.
collect deliver ←
( ask(true) → tell([Y|Ys]=[X|Xs]) k get token(X) k collect(Xs)
+ ask(false) → stop)
k
( ask(Y=eof) → tell(Ys=[ ])
+ ask(Y 6= eof) → deliver token(Y) k deliver(Ys))

Then we can eliminate the branch ask(false) → stop, eliminate tell([Y|Ys]=[X|Xs])
and eliminate the ask(true); the result is
collect deliver ← get token(Y) k collect(Ys) k
( ask(Y=eof) → tell(Ys=[ ])
+ ask(Y 6= eof) → deliver token(Y) k deliver(Ys))

Now, we apply the restricted distributive operation in order to bring collect(Ys)
inside the scope of the ask construct. Notice that collect(Ys) requires Ys. Remark
5.7 allows us to apply the operation.
collect deliver ← get token(Y) k
( ask(Y=eof) → collect(Ys) k tell(Ys=[ ])
+ ask(Y 6= eof) → deliver token(Y) k collect(Ys) k deliver(Ys))

We can now fold collect(Ys) k deliver(Ys), using the original definition collect deliver
← collect(Xs) k deliver(Xs). We obtain.
collect deliver ← get token(Y) k
( ask(Y=eof) → collect(Ys) k tell(Ys=[ ])
+ ask(Y 6= eof) → deliver token(Y) k collect deliver)

To clean up the result, we can now eliminate tell(Ys=[ ]), unfold the obtained
collect([ ]) agent, and perform the usual clean-up operations on the result. Our
final program is the simple
collect deliver ← get token(Y) k
( ask(Y=eof) → stop
+ ask(Y 6= eof) → deliver token(Y) k collect deliver)

It is important to compare this to the initial program. In particular, three aspects
are worth noticing.
First, that – as opposed to the initial program – the resulting one has a straightforward dynamic behavior. For instance if we consider the agent collect deliver,
one can easily see it to be deadlock-free in the latter program while in the original
program this is not at all immediate. After proving that the transformation does
not introduce nor eliminate any deadlocking branch in the semantics of the program, we are able to state that “since the resulting program is deadlock-free then
also the initial program is deadlock-free”. Thus program’s transformations can be
profitably used as analysis tool: it is in fact often easier to prove deadlock freeness
for a transformed version of a program than for the original one.
Secondly, that the resulting program is more efficient than the initial one: in fact
it does not need to use the global store as heavily as the initial one for passing the
parameters between collect and deliver.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

44

·

Sandro Etalle et al.

Finally, it is straightforward to check that all transformation operations used
here are of the restricted kind, therefore, by the Strong Total Correctness Theorem
5.12 this transformation is correct wrt the sequence of intermediate results.
We show now an application of our methodology with a third example, containing
an extended folding operation (see discussion after Definition 3.15): this is the case
when the replaced agent coincides with an instance of the body of the folding
definition.
Example 6.2. We consider a stream protocol problem where two input streams
are merged into an output stream. An input stream consists of lines of messages,
and each line has to be passed to the output stream without interruption. Input
and output streams are dynamically constructed by a reader and a monitor process,
respectively. A reader communicates with the monitor by means of a buffer of length
one, and is synchronized in such a way that it can read a new message only when
the buffer is empty (i.e., when the previous message has been processed by the
monitor). On the other hand, the monitor can access a buffer only when it is not
empty (i.e., when the corresponding reader has put a message into its buffer). This
protocol is implemented by the following program STREAMER:
streamer ← reader(left,Ls) k reader(right,Rs) k monitor(Ls,Rs,idle)
reader(Channel,Xs) ←
ask(∃X,Xs′ Xs=[X|Xs’]) → tell(Xs=[X|Xs’]) k read(Channel,X) k reader(Channel,Xs’)
+
ask(Xs=[ ]) → stop.
monitor([L|Ls],[R|Rs],State) ←
ask(State=idle) →
% waiting for an input
(
ask(char(L)) → monitor([L|Ls],[R|Rs],left)
+
ask(char(R)) → monitor([L|Ls],[R|Rs],right))
+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → tell(Ls=[ ]) k onestream([R|Rs])
+
ask(L=eol) → monitor(Ls,[R|Rs],idle)
+
ask(L 6= eol AND L 6= eof) → monitor(Ls,[R|Rs],left))
+ ask(State=right) → ask(char(R)) → → . . . )

% analogously for the right stream

onestream([X|Xs]) ←
ask(char(X)) →
( ask(X=eof) → tell(Xs=[ ])
+ ask(X 6= eof) → write(X) k onestream(Xs))

Here, the primitive agent read(Channel,X) is supposed to read an input token from
channel Channel and instantiate X with the read value; similarly, write(X) writes the
value of X to the (unique) output stream. The primitive constraint predicate char is
true if its argument is either a printable (e.g. ASCII) character or if it is equal to eol
or eof, which are constants denoting the end of line and the end of file characters,
respectively. Furthermore, the agent reader(Channel,Xs) waits to process Channel
until Xs is instantiated; monitor(Ls,Rs,State) takes care of merging Ls and Rs and
of writing to the output; the agent onestream(Xs) takes care of handling the single
stream Xs (when one of the streams has finished). Finally, the constants left, right
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

45

and idle describe the state of the monitor, i.e., if it is processing a message from
the left stream, from right stream, or if it is in an idle situation, respectively.
Notice that reader(Channel,Xs) suspends until Xs is instantiated and that Xs will
eventually be instantiated by the monitor process.
We can now transform the STREAMER program in order to improve its efficiency.
First we add the following new declaration to the original program.
handle two(L,R,State) ← reader(left,Ls) k reader(right,Rs) k monitor([L|Ls],[R|Rs],State)

Next, we unfold the agent monitor([L|Ls],[R|Rs],State) in the new declaration and
then we perform the subsequent tell eliminations (these are restricted in virtue of
the argument presented after Definition 5.8). The result of these operations is the
following program.
handle two(L,R,State) ← reader(left,Ls) k reader(right,Rs) k
( ask(State=idle) →
% waiting for an input
(
ask(char(L)) → monitor([L|Ls],[R|Rs],left)
+
ask(char(R)) → monitor([L|Ls],[R|Rs],right))
+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → tell(Ls=[ ]) k onestream([R|Rs])
+
ask(L=eol) → monitor(Ls,[R|Rs],idle)
+
ask(L 6= eol AND L 6= eof) → monitor(Ls,[R|Rs],left))
+ ask(State=right) → ask(char(R)) → . . . )

% analogously for the right stream

According to Definition 3.11, the agent reader(left, Ls) requires the variable Ls
and reader(right, Rs) requires the variable Rs. By Remark 3.12 it is possible for us
to apply twice the distribution operation8 and bring them inside the ask constructs.
The result is the following program.
handle two(L,R,State) ←
( ask(State=idle) →
% waiting for an input
(
ask(char(L)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],left)
+
ask(char(R)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],right))
+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → reader(left,Ls) k reader(right,Rs) k tell(Ls=[ ])
k onestream([R|Rs])
+
ask(L=eol) → reader(left,Ls) k reader(right,Rs) k monitor(Ls,[R|Rs],idle)
+
ask(L6=eol AND L6=eof) → reader(left,Ls) k reader(right,Rs) k
monitor(Ls,[R|Rs],left))
+ ask(State=right) → ask(char(R)) → . . . )

% analogously for the right stream

In this program we can now eliminate tell(Ls = [ ]) in the agent reader(left, Ls) k
reader(right, Rs) k tell(Ls = [ ]) k onestream([R|Rs]) thus obtaining9 :
handle two(L,R,State) ←
8 Remark

5.7, guarantees also in both cases it is a restricted distribution operation.
it is true that the variable Ls here occurs also elsewhere in the definition, but since it
occurs only on choice-branches different than the one on which the considered agent lies, we can
assume it to be renamed.

9 Again,

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

·

46

Sandro Etalle et al.

( ask(State=idle) →
% waiting for an input
(
ask(char(L)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],left)
+
ask(char(R)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],right))
+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → reader(left,[ ]) k reader(right,Rs) k onestream([R|Rs])
+
ask(L=eol) → reader(left,Ls) k reader(right,Rs) k monitor(Ls,[R|Rs],idle)
+
ask(L6=eol AND L6=eof) → reader(left,Ls) k reader(right,Rs) k
monitor(Ls,[R|Rs],left))
+ ask(State=right) → ask(char(R)) → . . . )

% analogously for the right stream

In this program, the unfolding of the agent reader(left, [ ]) yields as result the agent

+

ask(∃X,Xs′ [ ]=[X|Xs’]) → tell([ ]=[X|Xs’]) k read(Channel,X)
k reader(Channel,Xs’)
ask([ ]=[ ]) → stop .

By (trivial) guard simplification, this can become
+

ask(false) → tell([ ]=[X|Xs’]) k read(Channel,X) k reader(Channel,Xs’)
ask(true) → stop.

Now, by using branch elimination we can eliminate the first branch and by applying
the conservative ask elimination we can transform the second branch into stop. The
application of these operations yields:
handle two(L,R,State) ←
( ask(State=idle) →
% waiting for an input
(
ask(char(L)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],left)
+
ask(char(R)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],right))
+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → reader(right,Rs) k onestream([R|Rs])
+
ask(L=eol) → reader(left,Ls) k reader(right,Rs) k monitor(Ls,[R|Rs],idle)
+
ask(L6=eol AND L6=eof) → reader(left,Ls) k reader(right,Rs) k
monitor(Ls,[R|Rs],left))
+ ask(State=right) → ask(char(R)) → . . . )

% analogously for the right stream

We now apply the backward instantiation operation to monitor(Ls,[R|Rs],idle) and
to monitor(Ls,[R|Rs],left). By cleaning up the result with a tell elimination10 , this
amounts to instantiating Ls to [L’|Ls’]. Therefore, we have obtained.
handle two(L,R,State) ←
( ask(State=idle) →
% waiting for an input
(
ask(char(L)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],left)
+
ask(char(R)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],right))
10 This

is the first operation in this example that is not restricted.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

47

+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → reader(right,Rs) k onestream([R|Rs])
+
ask(L=eol) → reader(left,[L’|Ls’]) k reader(right,Rs) k
monitor([L’|Ls’],[R|Rs],idle)
+
ask(L6=eol AND L6=eof) → reader(left,[L’|Ls’]) k reader(right,Rs) k
monitor([L’|Ls’],[R|Rs],left))
+ ask(State=right) → ask(char(R)) → . . . )

% analogously for the right stream

In order to prepare the program for the folding operation we need one more clean
up phase: using the unfolding and some simplification operations, we can replace
each call reader(left, [L′ |Ls′ ]) with read(left, L′ ) k reader(left, Ls′ ). The result of these
operations is the program:
handle two(L,R,State) ←
( ask(State=idle) →
% waiting for an input
(
ask(char(L)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],left)
+
ask(char(R)) → reader(left,Ls) k reader(right,Rs) k
monitor([L|Ls],[R|Rs],right))
+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → reader(right,Rs) k onestream([R|Rs])
+
ask(L=eol) → read(left,L’) k reader(left,Ls’) k reader(right,Rs) k
monitor([L’|Ls’],[R|Rs],idle)
+
ask(L6=eol AND L6=eof) → read(left,L’) k reader(left,Ls’) k reader(right,Rs) k
monitor([L’|Ls’],[R|Rs],left))
+ ask(State=right) → ask(char(R)) → . . . )

% analogously for the right stream

We can now apply twice the extended folding operation. The first folding allows
us to replace reader(left,Ls) k reader(right,Rs) k monitor([L|Ls],[R|Rs],left) with handle two(L,R,left). With the second one we replace reader(left,Ls) k reader(right,Rs)
k monitor([L|Ls],[R|Rs],right) with handle two(L,R,right). Recall that the extended
folding operation, as described in Subsection 3.7, occurs when the replaced agent
coincides with a non-trivial instance of the body of the folding definition; as already explained in the discussion after Definition 3.15 this is only a shorthand for
a sequence of tell introduction, folding and tell elimination, as described in Subsection 3.7. The resulting program after these two operations is:
handle two(L,R,State) ←
( ask(State=idle) →
% waiting for an input
(
ask(char(L)) → handle two(L,R,left)
+
ask(char(R)) → handle two(L,R,right)
+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → reader(right,Rs) k onestream([R|Rs])
+
ask(L=eol) → read(left,L’) k reader(left,Ls’) k reader(right,Rs) k
monitor([L’|Ls’],[R|Rs],idle)
+
ask(L6=eol AND L6=eof) → read(left,L’) k reader(left,Ls’) k reader(right,Rs) k
monitor([L’|Ls’],[R|Rs],left))
+ ask(State=right) → ask(char(R)) → . . . )

% analogously for the right stream

Then, we perform two more extended foldings: with the first one we replace the
agent reader(left,Ls’) k reader(right,Rs) k monitor([L’|Ls’],[R|Rs],idle) with the agent
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

·

48

Sandro Etalle et al.

handle two(L’,R,idle), with the latter we replace reader(left,Ls’) k reader(right,Rs)
k monitor([L’|Ls’],[R|Rs],left) with handle two(L’,R,left). The resulting program is
handle two(L,R,State) ←
ask(State=idle) →
% waiting for an input
(
ask(char(L)) → handle two(L,R,left)
+
ask(char(R)) → handle two(L,R,right)
+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → reader(right,Rs) k onestream([R|Rs])
+
ask(L=eol) → read(left,L’) k handle two(L’,R,idle)
+
ask(L6=eol AND L6=eof) → read(left,L’) k handle two(L’,R,left)
+ ask(State=right) → ask(char(R)) → . . . )

% analogously for the right stream

Notice that now the definition of handle two is recursive. Moreover, the above
program is almost completely independent from the definition of reader. In order
to eliminate the atom reader(right,Rs) as well, we use an unfold/fold transformation
similar to (but simpler than) the previous one. This transformation starts with the
new definition11 :
handle one(X, Channel) ← reader(Channel,Xs) k onestream([X|Xs])

After the transformation, we end up with the definition:
handle one(X, Channel) ← ask(char(X)) →
( ask(X=eof) → stop
+ ask(X6=eof) → write(X) k read(Channel,X’) k handle one(X’,Channel))

Also in this case the folding operation allows us to save computational space. In
fact, the parallel composition of reader and of onestream in the original definition
leads to the construction of a list containing all the data read so far. In a concurrent
setting this list could easily be of unbounded size and monotonically increasing. The
initial definition employs a computational space which is linear in the input. After
the transformation we have a definition which does not build the list any longer, and
which could be optimized to employ only constant space (this could be achieved
by a using a garbage collection mechanism which allows one to re-use the space
allocated for local variables).
We now continue with the last steps of our example. By folding handle one into
the last definition of handle two, we obtain
handle two(L,R,State) ←
( ask(State=idle) →
% waiting for an input
(
ask(char(L)) → handle two(L,R,left)
+
ask(char(R)) → handle two(L,R,right)
+ ask(State=left) → ask(char(L)) → write(L) k
% processing the left stream
(
ask(L=eof) → handle one(R,right)
+
ask(L=eol) → read(left,L’) k handle two(L’,R,idle)
+
ask(L6=eol AND L6=eof) → read(left,L’) k handle two(L’,R,left)
+ ask(State=right) → ask(char(R)) → . . . )

% analogously for the right stream

11 This

definition is presented here for the sake of clarity; however recall that we assume that it is
added to the original program at the beginning of the transformation.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

49

We now want to let streamer benefit from the improvements we have obtained via
this transformation. First, we transform its definition by applying the backward
instantiation to monitor(Ls,Rs,idle), and obtain:
streamer ← reader(left,[L|Ls]) k reader(right,[R|Rs]) k monitor([L|Ls],[R|Rs],idle).

Next, we unfold the two reader atoms, and eliminate the redundant ask and tell
guards.
streamer ← read(left,L) k reader(left,Ls) k
read(right,R) k reader(right,Rs) k monitor([L|Ls],[R|Rs],idle).

We can now fold handle two in it (via an extended folding operation), obtaining:
streamer ← read(left,L) k read(right,R) k handle two(L,R,idle).

Note that this last folding operation is applied to a non-guarding context. As
discussed in Remark 3.16, we can apply the folding also in this case because the
definition of streamer is never modified nor used by the transformation. So we
can simply assume that the original definition of streamer contained a dummy ask
guard as in
streamer ← ask(true) → ( read(left,L) k reader(left,Ls) k read(right,R) k
reader(right,Rs) k monitor([L|Ls],[R|Rs],idle))

Then we assume that the folding operation is applied to this definition, and that
the guard ask(true) will eventually be removed by an ask elimination operation.
In the final program, we only need the definitions of streamer and of handle two
together with the ones of the built-it predicates. Observe that the definition of
streamer is much more efficient than the original one. Firstly, it now benefits from
a straightforward left-to-right dataflow. In the initial program the variables Ls and
Rs are employed as bidirectional communication channels, in fact there exist two
agents (reader and monitor) which alternate in “instantiating” them further. This
is not the case in the final program, where for each variable it is clear which is the
agent that is supposed to “instantiate” it (i.e. to progressively add information to
the store about it). This fact implies that on the final program are possible a number
of powerful compile-time (low-level) optimizations which in the first program are
not possible.
Secondly, the number of suspension points is dramatically reduced: in the original
program reader had to suspend and awaken itself at each input token. In the final
one streamer is independent from reader and has to suspend less often.
Last but certainly not least, as previously mentioned streamer now does not
construct the list and could be optimized to employ a constant computational
space, while in its initial version it employed a space linear in the input, that is,
possibly unbounded. It is worth remarking that in a concurrent setting processes
are often not meant to end their computation, in which case it is of vital importance
that the computational space remains bounded in size; thus in this context a space
gain like the one obtained in the above example makes the difference between a
viable and a non-viable definition.
Example 6.3. This is a variation on a standard example for unfold/fold transformations: a program computing the sum and the length of the elements in a list.
The variation consists in the fact that we consider only the elements of the list
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

50

·

Sandro Etalle et al.

which are larger than the given parameter Limit. We assume here that the constraint system being used incorporates some arithmetic domain. Therefore, in the
following program we use also arithmetic constraints, with the obvious intended
meaning.
sumlen(Xs,Limit,S,L) ← sum(Xs,Limit,S) k len(Xs,Limit,L)
sum(Xs,Limit,S) ←
(
ask(Xs=[ ]) → tell(S=0)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y ≤ Limit)) → tell(Xs=[Y|Ys]) k
sum(Ys,Limit,S)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y > Limit)) → tell (Xs= [Y|Ys]) k
sum(Ys,Limit,S’) k
tell(S=S’+ Y))
len(Xs,Limit,L) ←
(
ask(Xs=[ ]) → tell(L=0)
+
ask(∃Y,Ys ( Xs=[Y|Ys] ∧ Y ≤ Limit)) → tell (Xs=[Y|Ys]) k
len(Ys,Limit,L)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y > Limit)) → tell (Xs=[Y|Ys]) k
len(Ys,Limit,L’) k
tell(L=L’+ 1))

With two unfoldings we obtain:
sumlen(Xs,Limit,S,L) ←
(
ask(Xs=[ ]) → tell(S=0)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y ≤ Limit)) → tell (Xs=[Y|Ys]) k
sum(Ys,Limit,S)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y > Limit)) → tell (Xs=[Y|Ys]) k
sum(Ys,Limit,S’) k
tell(S=S’+ Y))
k
(
ask(Xs=[ ]) → tell(L=0)
+
ask(∃Y′ ,Ys′ (Xs=[Y’|Ys’] ∧ Y’ ≤ Limit)) → tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L)
+
ask(∃Y′ ,Ys′ (Xs=[Y’|Ys’] ∧ Y’ > Limit)) → tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L’) k
tell(L=L’+ 1))

We now apply the (restricted) distribution operation; in practice, we now bring one
choice inside the other one.
sumlen(Xs,Limit,S,L) ←
(
ask(Xs=[ ]) → tell(S=0) k
(
ask(Xs=[ ]) → tell(L=0)
+
ask(∃Y′ ,Ys′ (Xs=[Y’|Ys’] ∧ Y’ ≤ Limit)) → tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L)
+
ask(∃Y′ ,Ys′ ( Xs=[Y’|Ys’] and Y’ > Limit)) → tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L’) k
tell(L=L’+ 1))
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y ≤ Limit)) → tell (Xs=[Y|Ys]) k
sum(Ys,Limit,S) k
(
ask(Xs=[ ]) → tell(L=0)
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

51

ask(∃Y′ ,Ys′ (Xs=[Y’|Ys’] and Y’ ≤ Limit)) → tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L)
+
ask(∃Y′ ,Ys′ (Xs=[Y’|Ys’] and Y’ > Limit)) → tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L’) k
tell(L=L’+ 1))
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y > Limit) ) → tell (Xs=[Y|Ys]) k
sum(Ys,Limit,S’) k
tell(S=S’+ Y) k
(
ask(Xs=[ ]) → tell(L=0)
+
ask(∃Y′ ,Ys′ (Xs=[Y’|Ys’] ∧ Y’ ≤ Limit)) → tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L)
+
ask(∃Y′ ,Ys′ ( Xs=[Y’|Ys’] ∧ Y’ > Limit)) → tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L’) k
tell(L=L’+ 1)))
+

+

It is worth noticing that the applicability conditions of Definition 3.10 are trivially
satisfied thanks to the fact that both choices depend on the same variable Xs. Notice
also that in this case we cannot apply Remark 3.12, in fact this is an example of a
distribution operation which is not possible with the tools of [Etalle et al. 1998].
By using the ask simplification followed by a branch elimination and by a conservative ask elimination we obtain the following program. Notice that the ask
simplification is possible here because we can take arithmetic constraints into account.
sumlen(Xs,Limit,S,L) ←
(
ask(Xs=[ ]) → tell(S=0) k tell(L=0)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y ≤ Limit)) → tell (Xs=[Y|Ys]) k
sum(Ys,Limit,S) k
tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y > Limit)) → tell (Xs=[Y|Ys]) k
sum(Ys,Limit,S’) k
tell(S=S’+ Y) k
tell (Xs=[Y’|Ys’]) k
len(Ys’,Limit,L’) k
tell(L=L’+ 1))

Via a tell simplification (first and last non-restricted operation of this example),
we can transform tell(Xs = [Y′ |Ys′ ]) into tell([Y|Ys] = [Y′ |Ys′ ]), and subsequently
apply a tell elimination we obtain:
sumlen(Xs,Limit,S,L) ←
(
ask(Xs=[ ]) → tell(S=0) k tell(L=0)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y ≤ Limit)) → tell (Xs=[Y|Ys]) k
sum(Ys,Limit,S) k
len(Ys,Limit,L)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y > Limit)) → tell (Xs=[Y|Ys]) k
sum(Ys,Limit,S’) k
tell(S=S’+ Y) k
len(Ys,Limit,L’) k
tell(L=L’+ 1))

We can now apply the folding operation.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

52

·

Sandro Etalle et al.

sumlen(Xs,Limit,S,L) ←
(
ask(Xs=[ ]) → tell(S=0) k tell(L=0)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y ≤ Limit)) → tell (Xs=[Y|Ys]) k
sumlen(Ys,Limit,S,L)
+
ask(∃Y,Ys (Xs=[Y|Ys] ∧ Y > Limit)) → tell (Xs=[Y|Ys]) k
sumlen(Ys,Limit,S’,L’) k
tell(S=S’+ Y) k
tell(L=L’+ 1))

Again, we have reached a point in which the main definition is directly recursive.
Moreover, the number of choice-points encountered while traversing a list is now
half of what it was initially.
7. RELATED WORK
As mentioned in the introduction, this is one of the few attempts to apply fold/unfold
techniques in the field of concurrent languages. In fact, in the literature we find
only three papers which are relatively closely related to the present one: Ueda
and Furukawa [1988] defined transformation systems for the concurrent logic language GHC [Ueda 1986], Sahlin [1995] defined a partial evaluator for AKL, while
de Francesco and Santone in [1996] presented a transformation system for CCS
[Milner 1989].
The transformation system we are proposing builds on the systems defined in
the papers above and can be considered an extension of them. Differently from the
previous cases, our system is defined for a generic (concurrent) constraint language.
Thus, together with some new transformations such as the distribution, the backward instantiation and the branch elimination, we introduce also specific operations
which allow constraint simplification and elimination (though, some constraint simplification is done in [Sahlin 1995] as well).
It is interesting and not straightforward to compare our system with the one
of Ueda and Furukawa [1988]. This is specific for the GHC language, which has a
different syntactic structure from CCP and uses the Herbrand universe as computational domain. Also because of this, [Ueda and Furukawa 1988] employs operations
which are completely different from ours. In particular, our operation of unfolding is replaced by immediate execution and case splitting in [Ueda and Furukawa
1988]. Our unfolding is a weaker operation which has a broader applicability than
case splitting, since the latter operation involves the moving of synchronization
points and therefore requires suitable applicability conditions. Furthermore, the
distribution operation is not present in [Ueda and Furukawa 1988], as it would not
be possible in the syntactic structure of GHC. However, in many cases the effect
of distribution can be achieved in [Ueda and Furukawa 1988] by introduction of
a new clause followed by case splitting. In order to clarify this, below we report
how the transformations of the Example 6.1 could be mimicked in GHC by using
the operations of [Ueda and Furukawa 1988]. The transformation in the following
example was provided by a reviewer of this paper.
Example 7.1. The initial program collect deliver considered in Example 6.1, in
terms of the GHC syntax is
1: collect_deliver :- | collect(Xs), deliver(Xs).
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

53

2: collect([X|Xs]) :- | get_token(X), collect(Xs).
3: collect([])
:- | true.
4: deliver(Ys0) :- | Ys0=[Y|Ys], deliver_2(Y,Ys).
5: deliver_2(eof,Ys) :- | Ys=[].
6: deliver_2(Y,Ys) :- Y\=eof | deliver_token(Y), deliver(Ys).
The presence of deliver_2 is due to the fact that GHC does not allow nested
guards. The first operation to be used is an immediate execution, applied to clause
(1). The result is
7: collect_deliver :- | collect(Xs), Xs=[Y|Ys], deliver_2(Y,Ys).
By normalizing this, we obtain
8: collect_deliver :- | collect([Y|Ys]), deliver_2(Y,Ys).
Another immediate execution operation yields
9: collect_deliver :- | get_token(Y), collect(Ys), deliver_2(Y,Ys).
Now, we need to introduce a new definition.
10: collect_deliver_2(Y) :- | collect(Ys), deliver_2(Y,Ys).
By applying to this the case splitting operation, we obtain
11: collect_deliver_2(eof) :- | collect(Ys), Ys=[].
12: collect_deliver_2(Y) :- Y\=eof | collect(Ys), deliver_token(Y),
deliver(Ys).
By normalizing clause 11, and subsequently applying an immediate execution operation, we obtain
13: collect_deliver_2(eof) :- | true.
To (12) and (9) we can apply the folding operation, and the resulting program is
thus
collect_deliver :- | get_token(Y), collect_deliver_2(Y).
collect_deliver_2(eof) :- | true.
collect_deliver_2(Y) :- Y\=eof | deliver_token(Y), collect_deliver.
It is worth noting how it is possible to achieve a resulting program which is basically
identical to the one of Example 6.1, despite the completely different nature of the
operation used.
Compared to [Ueda and Furukawa 1988] we also provide a more flexible definition
for the folding operation which allows the folding clause to be recursive (which is
really a step forward in the context of folding operations which are themselves
capable of introducing recursion) and frees the initial program from having to be
partitioned in Pnew and Pold . In fact, as opposed to virtually all fold operations
which enable to introduce recursion presented so far (the only exception being
[Francesco and Santone 1996]), the applicability of the folding operation does not
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

54

·

Sandro Etalle et al.

depend on the transformation history, (which has always been one of the “obscure
sides” of it) but it relies on plain syntactic criteria. The idea of using a guarded
folding in order to obtain applicability conditions independent of the transformation
history was first introduced by de Francesco and Santone [1996] in the CCS setting.
However, their technical development is rather different from ours, in particular
our correctness results and proofs are completely different from those sketched in
[Francesco and Santone 1996].
As previously mentioned, differently from our case in [Sahlin 1995] it is considered a definition of ask elimination which allows us to remove potentially selectable
branches; the consequence is that the resulting transformation system is only partially (thus not totally) correct. We should mention that in [Sahlin 1995] two
preliminary assumptions on the “scheduling” are made in such a way that this
limitation is actually less constraining than it might appear.
8. CONCLUSIONS
We have introduced an unfold/fold transformation system for CCP and we have
proved its total correctness w.r.t. the input/output semantics defined by the observables O, which takes into account also the termination modes. This semantics
corresponds (modulo irrelevant differences due to the treatment of failure and of
local variables) to that one proposed in [de Boer and Palamidessi 1991]. This is
one of the two fully abstract “standard” semantics for CCP, the other being that
one defined in [Saraswat et al. 1991]. (Actually, these two semantic models have
been proved to be isomorphic ([de Boer and Palamidessi 1992]), provided that the
termination mode and the consistency checks are eliminated.)
We have also shown that the proposed transformation system preserves another,
stronger semantics which takes into account the intermediate results of computations up to logical implication (Theorem 5.1). We argued that this result should
be strong enough for transforming also programs which might not terminate, in
particular for transforming reactive programs. Nevertheless, in addition to this
we have presented a restricted transformation system, obtained from the initial
one by adding some (relatively mild) restrictions on some operations. We have
shown that this second system preserves the trace semantics of programs (up to
simulation, Theorem 5.12) and therefore it is totally correct w.r.t. the semantics
Oi which takes into account all the intermediate results (Corollary 5.13). We have
also proved that this system preserves active infinite computations and we claim
that, more generally, this system does not introduce in the transformed program
any new infinite computation which was not present in the original one.
As shown by the examples, this system can be used for the optimization of concurrent constraint programs both in terms of time and of space. In fact, it allows us
to eliminate unnecessary suspension points (and therefore to reduce sequentiality),
to reduce the number of communication channels and to avoid the construction of
some global data structures. The system can also be used to simplify the dynamic
behavior of a program, thus allowing us to prove directly absence of deadlock.
Concerning future work, there exist other techniques for proving deadlock freeness
for CCP programs, notably in [Codish et al. 1994] a methodology based on abstract
interpretation has been defined. It could be interesting to investigate an integration
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

55

of our methodology with abstract interpretation tools. We are also considering
a formal comparison of some different transformation systems (in particular our
system and that one of [Ueda and Furukawa 1988]) to assess their relative strength.
This task is not immediate, since the target languages are different.
A. DETAILED PROOFS
Appendix A is available only online. You should be able to get the online-only
toplas from the citation page for this article:
2039

Alternative instructions on how to obtain online-only appendices are given on
the back inside cover of current issues of ACM TOPLAS or on the ACM TOPLAS
web page:
http://www.acm.org/toplas
ACKNOWLEDGMENTS

We would like to thank the reviewers for their precise and helpful comments.
REFERENCES
Bensaou, N. and Guessarian, I. 1998. Transforming constraint logic programs. Theoretical
Computer Science 206, 1–2, 81–125.
Boer, F. S. D., Gabbrielli, M., Marchiori, E., and Palamidessi, C. 1997. Proving concurrent constraint programs correct. ACM Transactions on Programming Languages and Systems 19, 5, 685–725.
Burstall, R. and Darlington, J. 1977. A transformation system for developing recursive programs. Journal of the ACM 24, 1 (January), 44–67.
Clark, K. and Sickel, S. 1977. Predicate logic: a calculus for deriving programs. In Proceedings
of IJCAI’77. 419–120.
Codish, M., Falaschi, M., and Marriott, K. 1994. Suspension Analyses for Concurrent Logic
Programs. ACM Transactions on Programming Languages and Systems 16, 3, 649–686.
de Boer, F. and Palamidessi, C. 1991. A fully abstract model for concurrent constraint programming. In TAPSOFT/CAAP, S. Abramsky and T. Maibaum, Eds. Number 493 in LNCS.
Springer-Verlag.
de Boer, F. and Palamidessi, C. 1992. On the semantics of concurrent constraint programming.
In ALPUK 92, Workshops in Computing, Springer-Verlag, Ed. 145–173.
Etalle, S. and Gabbrieli, M. 1998. Partial evaluation of concurrent constraint languages. ACM
Computing Surveys 30, 3es (September). Article 11.
Etalle, S. and Gabbrielli, M. 1996. Transformations of CLP modules. Theoretical Computer
Science 166, 1, 101–146.
Etalle, S., Gabbrielli, M., and Meo, M. C. 1998. Unfold/Fold Transformations of CCP Programs. In CONCUR98 – 1998 International Conference on Concurrency Theory, D. Sangiorgi
and R. de Simone, Eds. LNCS 1466. Springer-Verlag, 348–363.
Francesco, N. D. and Santone, A. 1996. Unfold/fold transformation of concurrent processes.
In Proc. 8th Int’l Symp. on Programming Languages: Implementations, Logics and Programs,
H. Kuchen and S. Swierstra, Eds. Vol. 1140. Springer-Verlag, 167–181.
Gengler, M. and Martel, M. 1997. Self-applicable partial evaluation for pi-calculus. In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program
Manipulation (PEPM-97). ACM SIGPLAN Notices, vol. 32, 12. ACM Press, New York, 36–46.
Hogger, C. 1981. Derivation of logic programs. Journal of the ACM 28, 2 (April), 372–392.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

56

·

Sandro Etalle et al.

Hosoya, H., Kobayashi, N., and Yonezawa, A. 1996. Partial evaluation scheme for concurrent
languages and its correctness. In Euro-Par’96, L. B. et al., Ed. Number 1123 in LNCS. SpringerVerlag, 625–632.
Jaffar, J. and Maher, M. J. 1994. Constraint logic programming: A survey. Journal of Logic
Programming 19/20, 503–581.
Jørgensen, N., Marriott, K., and Michaylov, S. 1991. Some global compile-time optimizations
for CLP(R). In International Logic Programming Symposium, V. Saraswat and K. Ueda, Eds.
MIT Press, San Diego, 420–434.
Kawamura, T. and Kanamori, T. 1988. Preservation of Stronger Equivalence in Unfold/Fold
Logic Programming Transformation. In Proc. Int’l Conf. on Fifth Generation Computer Systems. Institute for New Generation Computer Technology, Tokyo, 413–422.
Komorowski, H. 1982. Partial evaluation as a means for inferencing data structures in an applicative language: A theory and implementation in the case of Prolog. In Ninth ACM Symposium
on Principles of Programming Languages, Albuquerque, New Mexico. ACM, 255–267.
Lloyd, J. W. 1987. Foundations of Logic Programming. Symbolic Computation – Artificial
Intelligence. Springer-Verlag, Berlin. Second edition.
Maher, M. 1993. A transformation system for deductive databases with perfect model semantics.
Theoretical Computer Science 110, 2 (March), 377–403.
Marinescu, M. and Goldberg, B. 1997. Partial-evaluation techniques for concurrent programs.
In Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based
Program Manipulation (PEPM-97). ACM SIGPLAN Notices, vol. 32, 12. ACM Press, New
York, 47–62.
Milner, R. 1989. Communication and Concurrency. Prentice-Hall.
Mogensen, T. and Sestoft, P. 1997. Partial evaluation. In Encyclopedia of Computer Science
and Technology, A. Kent and J. Williams, Eds. Vol. 37. M. Dekker, 247–279.
Pettorossi, A. and Proietti, M. 1994. Transformation of logic programs: Foundations and
techniques. Journal of Logic Programming 19,20, 261–320.
Sahlin, D. 1995. Partial Evaluation of AKL. In Proceedings of the First International Conference
on Concurrent Constraint Programming.
Saraswat, V. and Rinard, M. 1990. Concurrent constraint programming. In Proc. of the
Seventeenth ACM Symposium on Principles of Programming Languages. ACM, New York,
232–245.
Saraswat, V., Rinard, M., and Panangaden, P. 1991. Semantics foundations of concurrent constraint programming. In Proc. Eighteenth Annual ACM Symp. on Principles of Programming
Languages. ACM Press.
Saraswat, V. A. 1989. Concurrent constraint programming languages. Ph.D. thesis, CarnegieMellon University.
Smolka, G. 1995. The Oz programming model. In Computer Science Today, J. van Leeuwen,
Ed. Number 1000 in LNCS. Springer-Verlag. see www.ps.uni-sb.de/oz/.
Tamaki, H. and Sato, T. 1984. Unfold/Fold Transformations of Logic Programs. In Proc. Second
Int’l Conf. on Logic Programming, S.-A. ke Tärnlund, Ed. 127–139.
Ueda, K. 1986. Guarded Horn Clauses. In Logic Programming ‘85, E. Wada, Ed. Lecture Notes
in Computer Science, vol. 221. Springer-Verlag, Berlin, 168–179.
Ueda, K. and Furukawa, K. 1988. Transformation rules for GHC Programs. In Proc. Int’l Conf.
on Fifth Generation Computer Systems. Institute for New Generation Computer Technology,
Tokyo, 582–591.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

57

Received 1/4/99; Revised 12/14/00; Accepted 4/5/01.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–1

This document is the online-only appendix to:

Transformations of CCP programs
SANDRO ETALLE
University of Twente and CWI
MAURIZIO GABBRIELLI
Università di Udine
and
MARIA CHIARA MEO
Università di L’Aquila

In this Appendix we provide the detailed proofs for the results which ensure
that the transformation system we have defined is totally correct. In particular,
we provide the detailed proofs for Theorems 4.13 and 5.12. In order to obtain a
self contained Appendix some technical Lemmata contained also in the paper are
repeated here. In what follows, we are going to refer to a fixed transformation
sequence D0 , . . . , Dn .
Lemma A.1. Assume that there exists a derivation hD.C[A], ci →∗ hD.C′ [A], c′ i
where c is a satisfiable constraint and the context C′ [ ] has the form
A1 k . . . k C̄[ ] k . . . k An
and, for each j ∈ [1, n], Aj is either a choice agent, or a procedure call or the agent
Stop. Then D |= (pc(C̄[ ]) ∧ c′ ) → pc(C[ ]) holds and in case C̄[ ] is the empty
context also D |= c′ → pc(C[ ]) holds.
Proof. By a straightforward inductive argument it follows that if there exists
a derivation hD.C[A], ci →∗ hD.C′ [A], c′ i, then D |= (pc(C′ [ ]) ∧ c′ ) → pc(C[ ]).
Now, if C′ [ ] has the form A1 k . . . k C̄[ ] k . . . k An , where each Aj is either a
choice agent or a procedure call or Stop, then pc(C′ [ ]) = pc(C̄[ ]) which implies
D |= (pc(C̄[ ]) ∧ c′ ) → pc(C[ ]). Obviously if C̄[ ] is the empty context then
pc(C̄[ ]) = true, from which the second part of the Lemma follows.
We prove now Proposition 4.5.
Proposition 4.5 (Partial Correctness). If, for each agent A, O(D0 .A) =
O(Di .A) then, for each agent A, O(Di .A) ⊇ O(Di+1 .A).
Proof. We now show that given an agent A and a satisfiable constraint cI ,
if there exists a derivation ξ = hDi+1 .A, cI i →∗ hDi+1 .B, cF i, with m(B, cF ) ∈
{ss, dd, ff}, then there exists also a derivation ξ ′ = hDi .A, cI i →∗ hDi .B′ , c′F i with
Permission to make digital/hard copy of all or part of this material without fee for personal
or classroom use provided that the copies are not made or distributed for profit or commercial
advantage, the ACM copyright/server notice, the title of the publication, and its date appear, and
notice is given that copying is by permission of the ACM, Inc. To copy otherwise, to republish,
to post on servers, or to redistribute to lists requires prior specific permission and/or a fee.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–2

·

Sandro Etalle et al.

∃−Var (A,cI ) c′F = ∃−Var (A,cI ) cF and m(B′ , c′F ) = m(B, cF ). By Definition 4.1, this will
imply the thesis. The proof is by induction on the length l of the derivation.
(l = 0). In this case ξ = hDi+1 .A, cI i. By the definition hDi .A, cI i is also a
derivation of length 0 and then the thesis holds.
(l > 0). If the first step of derivation ξ does not use rule R4, then the proof
follows from the inductive hypothesis: In fact, if ξ = hDi+1 .A, cI i → hDi+1 .A1 , c1 i →∗
hDi+1 .B, cF i then by the inductive hypothesis, there exists a derivation
ξ ′′ = hDi .A1 , c1 i →∗ hDi .B′ , c′F i
with ∃−Var (A1 ,c1 ) c′F = ∃−Var (A1 ,c1 ) cF and m(B′ , c′F ) = m(B, cF ). We can assume,
without loss of generality, that Var(A, cI ) ∩ Var (ξ ′′ ) ⊆ Var (A1 , c1 ). Therefore,
there exists a derivation ξ ′ = hDi .A, cI i →∗ hDi .B′ , c′F i. Now, to prove the thesis
it is sufficient to observe that, by the hypothesis on the variables, ∃−Var (A,cI ) c′F =
∃−Var (A,cI ) (c1 ∧ ∃−Var (A1 ,c1 ) c′F ) = ∃−Var (A,cI ) (c1 ∧ ∃−Var (A1 ,c1 ) cF ) = ∃−Var (A,cI ) cF .
Now, assume that the first step of derivation ξ uses rule R4 and let d′ ∈ Di+1
be the declaration used in the first step of ξ. If d′ was not modified in the transformation step from Di to Di+1 (that is, d′ ∈ Di ), then the result follows from the
inductive hypothesis. We assume then that d′ 6∈ Di , d′ is then the result of the
transformation operation applied to obtain Di+1 , and we now distinguish various
cases according to the operation itself.
Case 1: d′ is the result of an unfolding operation.
In this case the proof is straightforward.
Case 2: d′ is the result of a tell elimination or of a tell introduction.
In this case the thesis follows from a straightforward analysis of the possible derivations which use d or d’. First, observe that for any derivation which uses a declaration H ← C[tell(s̃ = t̃) k B], we can construct another derivation such that the
agent tell(s̃ = t̃) is evaluated before B. Moreover for any constraint c such that
∃dom(σ) c = ∃dom(σ) cσ, (where σ is a relevant most general unifier of s̃ and t̃), there
exists a derivation step hDi .B1 σ, cσi → hDi .B2 σ, c′ i if and only if there exists a
derivation step hDi .B1 , c ∧ (s̃ = t̃)i → hDi .B2 , c′′ i, where, for some constraint e,
c′ = eσ, c′′ = e ∧ (s̃ = t̃) and therefore c′ = ∃dom(σ) c′′ . Finally, since by definition σ
is idempotent and the variables in the domain of σ do not occur neither in C[ ] nor
in H, for any constraint e we have that ∃−Var (A,cI ) eσ = ∃−Var (A,cI ) (e ∧ (s̃ = t̃)).
Case 3: d′ is the result of a backward instantiation.
Let d be the corresponding declaration in Di . The situation is the following:
- d : q(r̃) ← C[p(t̃)]
- d′ : q(r̃) ← C[p(t̃) k tell(b) k tell(t̃ = s̃)]
where f : p(s̃) ← tell(b) k H ∈ Di has no variable in common with d (the case
d′ : q(r̃) ← C[p(t̃) k tell(t̃ = s̃)] is analogous and hence omitted). In this case
ξ = hDi+1 .CI [q(ṽ)], cI i → hDi+1 .CI [C[p(t̃) k tell(b) k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i
→∗ hDi+1 .B, cF i.
By the inductive hypothesis, there exists a derivation
χ = hDi .CI [C[p(t̃) k tell(b) k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i →∗ hDi .B′′ , c′′F i,
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–3

with
∃−Var (C [C[p(t̃) k tell(b) k tell(t̃=s̃)] k tell(ṽ=r̃)],c ) c′′F =
I

I

∃−Var (C [C[p(t̃) k tell(b) k tell(t̃=s̃)] k tell(ṽ=r̃)],c ) cF
I

I

and
m(B′′ , c′′F ) = m(B, cF ).

(31)

Moreover, since Var(CI [q(ṽ)], cI ) ⊆ Var (CI [C[p(t̃) k tell(b) k tell(t̃ = s̃)] k tell(ṽ =
r̃)], cI ), we have that
∃−Var (CI [q(ṽ)],cI ) c′′F = ∃−Var (CI [q(ṽ)],cI ) cF .

(32)

If p(t̃) is not evaluated in χ, then the proof is immediate. Otherwise, by the
definition of χ and since f ∈ Di , there exists also a derivation
χ′ = hDi .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi .B′ , c′F i
such that ∃−Var (C [C[p(t̃)] k tell(ṽ=r̃)],c ) c′F = ∃−Var (C [C[p(t̃)] k tell(ṽ=r̃)],c ) c′′F and m(B′ , c′F )
I

I

I

I

= m(B′′ , c′′F ). Therefore, by (32) and (31)
∃−Var (CI [q(ṽ)],cI ) c′F = ∃−Var (CI [q(ṽ)],cI ) cF and m(B′ , c′F ) = m(B, cF ).

(33)

By the definition of χ′ , Var (CI [q(ṽ)], cI )∩Var(χ′ ) ⊆ Var (CI [C[p(t̃)] k tell(ṽ = r̃)], cI ).
Then, by the definition of derivation and since d ∈ Di ,
hDi .CI [q(ṽ)], cI i → hDi .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi .B′ , c′F i
and then the thesis follows from (33).
Case 4: d′ is obtained from d by either an ask simplification or a tell simplification.
We consider only the first case (the proof of the other one is analogous and hence
it is omitted). LetP
n
- d′ : q(r̃) ← C[ j=1 ask(c′j ) → Aj ], and
Pn
- d : q(r̃) ← C[ j=1 ask(cj ) → Aj ],
where for j ∈ [1, n], D |= ∃−Var (q(r̃),C,Aj ) (pc(C[ ]) ∧ cj ) ↔ (pc(C[ ]) ∧ c′j ). According
to the definition of pc and by Lemma A.1, for any derivation χ for
hDi .CI [C[

n
X

ask(c′j ) → Aj ] k tell(ṽ = r̃)], cI i

j=1

′

there exists a derivation χ for
hDi .CI [C[

n
X

ask(cj ) → Aj ] k tell(ṽ = r̃)], cI i

j=1

which performs the same steps of χ (possibly in a different order) and such that
whenever the choice agent inside C[ ] is evaluated the current store implies pc(C[ ]).
Therefore the thesis follows from the above equivalence.
Case 5: d′ is the result of a branch elimination or of a conservative ask elimination.
The proof is straightforward by noting that: (a) according to Definition 4.1 we
consider also inconsistent stores resulting from non-terminated computations; (b)
an ask action of the form ask(true) always succeeds.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–4

·

Sandro Etalle et al.

Case 6: d′ is the result
Pnof a distribution operation. Let
- d : q(r̃) ← C[H k j=1 ask(cj ) → Bj ] ∈ Di
Pn
- d′ : q(r̃) ← C[ j=1 ask(cj ) → (H k Bj )] ∈ Di+1
where e = pc(C[ ]) and for every constraint c such that Var (c) ∩ Var (d) ⊆
Var (q(r̃), C), if hDi .H, c ∧ ei is productive then both the following conditions hold:
—there exists at least one j ∈ [1, n] such that D |= (c ∧ e) → cj
—for each j ∈ [1, n], either D |= (c ∧ e) → cj or D |= (c ∧ e) → ¬cj .
Pn
In this case ξ = hDi+1 .CI [q(ṽ)], cI i → hDi+1 .CI [C[ j=1 ask(cj ) → (H k Bj )] k tell(ṽ =
r̃)], cI i →∗ hDi+1 .B, cF i. By the inductive hypothesis, there exists a derivation
n
X
χ = hDi .CI [C[
ask(cj ) → (H k Bj )] k tell(ṽ = r̃)], cI i →∗ hDi .B′′ , c′′F i
j=1

with

and

∃−Var (C [C[Pn ask(cj )→(H k Bj )] k tell(ṽ=r̃)],c ) c′′F =
I
I
j=1
∃−Var (C [C[Pn ask(c )→(H k B )] k tell(ṽ=r̃)],c ) cF
j
j
I
I
j=1

m(B′′ , c′′F ) = m(B, cF ).
(34)
Pn
Moreover, since Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[ j=1 ask(cj ) → (H k Bj )] k tell(ṽ =
r̃)], cI ), we have that
∃−Var (CI [q(ṽ)],cI ) c′′F = ∃−Var (CI [q(ṽ)],cI ) cF .

(35)

Now, P
we distinguish two cases:
n
1)
ask(cj ) → (H k Bj ) is not evaluated in χ. In this case the proof is obvious.
Pj=1
n
2)
j=1 ask(cj ) → (H k Bj ) is evaluated in χ. We have two more possibilities:
2a) There exists h ∈ [1, n], such that
Pn
χ = hDi .CI [C[ j=1 ask(cj ) → (H k Bj )] k tell(ṽ = r̃)], cI i →∗
Pn
hDi .Cm [ j=1 ask(cj ) → (H k Bj )], cm i → hDi .Cm [H k Bh ], cm i →∗ hDi .B′′ , c′′F i
where D |= cm → ch . In this case the thesis follows immediately, since using d one
can obtain the agent Cm [H k Bh ] after having evaluated the choice agent in C[ ].
2b) There is no h ∈ [1, n], such that D |= c′′F → ch . In this case
c′′F is satisfiable, m(B′′ , c′′F ) = dd,
′′

(36)

Pn

ask(cj ) → (H k Bj )] and
P
χ = hDi .CI [C[ nj=1 ask(cj ) → (H k Bj )] k tell(ṽ = r̃)], cI i →∗
P
hDi .CF [ nj=1 ask(cj ) → (H k Bj )], c′′F i 6→ .

B is the agent CF [

j=1

the definition of derivation, the definition of B′′ and
P¿From
Pn the hypothesis that
n
ask(c
)
→
(H
k
B
)
is
evaluated
in
χ,
it
follows
that
C
[
j
j
F
j=1
j=1 ask(cj ) → (H k Bj )]
P
is of the form A1 k . . . k nj=1 ask(cj ) → (H k Bj ) k . . . k Al , where either Ak is
a choice agent or Ak = Stop. By Lemma A.1, D |= c′′F → pc(C[ ]) and by
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–5

definition of derivation Var (c′′F ) ∩ Var (d) ⊆ Var(q(r̃), C). Then, since there is
no j ∈ [1, n] such that D |= c′′F → cj , by definition of distribution, hDi .H, c′′F i
is not productive. Then, by definition, hDi .H, c′′F i has at least one finite derivation χ1 = hDi .H, c′′F i →∗ hDi .H′ , c′F i 6→ such that D |= ∃−Z̃ c′′F ↔ ∃−Z̃ c′F , where
Z̃ = Var (H). Moreover, since in a derivation we can add to the store only constraints
on the variables occurring in the agents, c′′F = ∃−Var (H,c′′F ) c′′F = ∃−Var (H,c′′F ) c′F holds.
Without loss of generality, we can assume that Var (χ1 ) ∩ Var (χ) ⊆ Var (H, c′′F ).
Therefore, by the previous observation,
∃−Var (C [Pn
F

and since hDi .CF [
derivation

Pn

j=1

j=1

′
′′
k Bj )],c′′F ) cF = cF

ask(cj )→(H

(37)

ask(cj ) → (H k Bj )], c′′F i 6→ and hDi .H′ , c′F i 6→, there exists a

Pn
χ′ = hDi .CI [C[H k j=1 ask(cj ) → Bj ] k tell(ṽ = r̃)], cI i →∗
Pn
Pn
hDi .CF [H k j=1 ask(cj ) → Bj ], c′′F i →∗ hDi .CF [H′ k j=1 ask(cj ) → Bj ], c′F i 6→ .

Moreover, since d ∈ Di , there exists a derivation
Pn
ξ ′ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H k j=1 ask(cj ) → Bj ] k tell(ṽ = r̃)], cI i →∗
Pn
Pn
hDi .CF [H k j=1 ask(cj ) → Bj ], c′′F i →∗ hDi .CF [H′ k j=1 ask(cj ) → Bj ], c′F i 6→ .
Finally, to prove the thesis it is sufficient
Pn to observe that from (34), (36), (37) and
from the definition of B′ = CF [H′ k j=1 ask(cj ) → Bj ] it follows that m(B′ , c′F ) =
m(B, cF ) = dd. Moreover
∃−Var (CI [q(ṽ)],cI ) c′F
∃−Var (CI [q(ṽ)],cI ) (c′′F ∧ ∃−Var (C

F [H

∃−Var (CI [q(ṽ)],cI ) c′′F

k

Pn

j=1

= (by construction)
′
)
= (by (37))
c
ask(c )→B ],c′ ) F
j

j

F

= (by (35))

∃−Var (CI [q(ṽ)],cI ) cF

which concludes the proof of this case.
Case 7: d′ is the result of a folding.
Let
- d : q(r̃) ← C[H] be the folded declaration (∈ Di ),
- f : p(X̃) ← H be the folding declaration (∈ D0 ),
- d′ : q(r̃) ← C[p(X̃)] be the result of the folding operation (∈ Di+1 )
where, by hypothesis, Var (d)∩Var (X̃) ⊆ Var (H) and Var(H)∩(Var (r̃)∪Var (C)) ⊆
Var (X̃). In this case ξ = hDi+1 .CI [q(ṽ)], cI i → hDi+1 .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗
hDi+1 .B, cF i and we can assume, without loss of generality, that Var (CI [q(ṽ)], cI ) ∩
Var (H) = ∅.
By the inductive hypothesis, there exists a derivation
χ = hDi .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗ hDi .B′′ , c′′F i,
with ∃−Var (C [C[p(X̃)] k tell(ṽ=r̃)],c ) c′′F = ∃−Var (C [C[p(X̃)] k tell(ṽ=r̃)],c ) cF and
I

I

I

I

m(B′′ , c′′F ) = m(B, cF ).

(38)

Since Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[p(X̃)] k tell(ṽ = r̃)], cI ), we have that
∃−Var (CI [q(ṽ)],cI ) c′′F = ∃−Var (CI [q(ṽ)],cI ) cF .

(39)

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

·

App–6

Sandro Etalle et al.

Since by hypothesis for any agent A′ , O(D0 .A′ ) = O(Di .A′ ), there exists a derivation
ξ0 = hD0 .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗ hD0 .B0 , c0 i
such that ∃−Var (C [C[p(X̃)] k tell(ṽ=r̃)],c ) c0 = ∃−Var (C [C[p(X̃)] k tell(ṽ=r̃)],c ) c′′F and m(B0 , c0 ) =
I

I

I

I

m(B′′ , c′′F ). By (38), (39) and since Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[p(X̃)] k tell(ṽ =
r̃)], cI ), we have that
∃−Var (CI [q(ṽ)],cI ) c0 = ∃−Var (CI [q(ṽ)],cI ) cF and m(B0 , c0 ) = m(B, cF ).

(40)

Let f ′ : p(X̃′ ) ← H′ be an appropriate renaming of f, which renames only the variables in X̃, such that Var (d)∩Var (f ′ ) = ∅ (note that this is possible, since Var (H)∩
(Var (r̃) ∪ Var (C)) ⊆ Var (X̃)). Moreover by hypothesis, Var (CI [q(ṽ)], cI ) ∩ Var (H) =
∅. Then, without loss of generality we can assume that Var(ξ0 ) ∩ Var (f ′ ) 6= ∅ if and
only if the procedure call p(X̃) is evaluated, in which case declaration f ′ is used.
Thus there exists a derivation
hD0 .CI [C[H′ k tell(X̃ = X̃′ )] k tell(ṽ = r̃)], cI i →∗ hD0 .B′0 , c0 i,
where m(B′0 , c0 ) = m(B0 , c0 ). By (40) we have
m(B′0 , c0 ) = m(B, cF ).
′

(41)
′

We show now that we can substitute H for H k tell(X̃ = X̃ ) in the previous derivation. Since f ′ : p(X̃′ ) ← H′ is a renaming of f : p(X̃) ← H, the equality X̃ = X̃′
is a conjunction of equations involving only distinct variables. Then, by replacing X̃ with X̃′ and vice versa in the previous derivation we obtain the derivation
χ0 = hD0 .CI [C[H k tell(X̃′ = X̃)] k tell(ṽ = r̃)], cI i →∗ hD0 .B′′0 , c′0 i where
∃−Var (C [C[H k tell(X̃′ =X̃)] k tell(ṽ=r̃)],c ) c′0 = ∃−Var (C [C[H k tell(X̃′ =X̃)] k tell(ṽ=r̃)],c ) c0
I
I
I
I
and m(B′′0 , c′0 ) = m(B′0 , c0 ).
¿From (41) it follows that
m(B′′0 , c′0 ) = m(B, cF ).

(42)
′

Then, from (40) and since Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[H k tell(X̃ = X̃)] k tell(ṽ =
r̃)], cI ) we obtain
∃−Var (CI [q(ṽ)],cI ) c′0 = ∃−Var (CI [q(ṽ)],cI ) cF .

(43)

Moreover, we can drop the constraint tell(X̃′ = X̃), since the declarations used
in the derivation are renamed apart and, by construction, Var (CI [C[H] k tell(r̃ =
ṽ)], cI ) ∩ Var(X̃′ ) = ∅. Therefore there exists a derivation hD0 .CI [C[H] k tell(ṽ =
r̃)], cI i →∗ hD0 .B̄0 , c̄0 i which performs exactly the same steps of χ0 , (possibly) except for the evaluation of tell(X̃′ = X̃), and such that ∃−Var (C [C[H] k tell(ṽ=r̃)],c ) c̄0 =
I

I

∃−Var (C [C[H] k tell(ṽ=r̃)],c ) c′0 and m(B̄0 , c̄0 ) = m(B′′0 , c′0 ). ¿From (42), (43) and since
I

I

Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[H] k tell(ṽ = r̃)], cI ), it follows that
m(B̄0 , c̄0 ) = m(B, cF ) and ∃−Var (CI [q(ṽ)],cI ) c̄0 = ∃−Var (CI [q(ṽ)],cI ) cF .
′

′

′

(44)

Since O(D0 .A ) = O(Di .A ) holds by hypothesis for any agent A , there exists a
derivation
hDi .CI [C[H] k tell(ṽ = r̃)], cI i →∗ hDi .B′ , c′F i
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–7

where
∃−Var (C [C[H] k tell(ṽ=r̃)],c ) c′F = ∃−Var (C [C[H] k tell(ṽ=r̃)],c ) c̄0
I

I

I

I

and m(B′ , c′F ) = m(B̄0 , c̄0 ). From (44) and since Var (CI [q(ṽ)], cI ) ⊆ Var (CI [C[H] k tell(ṽ =
r̃)], cI ), we obtain
m(B′ , c′F ) = m(B, cF ) and ∃−Var (CI [q(ṽ)],cI ) c′F = ∃−Var (CI [q(ṽ)],cI ) cF .

(45)

Finally, since d : q(r̃) ← C[H] ∈ Di , there exists a derivation
ξ ′ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H] k tell(ṽ = r̃)], cI i →∗ hDi .B′ , c′F i
and then the thesis follows from (45).
Before proving the total correctness result we need some technical lemmata. Here
and in the following we use the notation wt (with t ∈ {ss, dd, ff}) as a shorthand for
indicating the success weight wss , the deadlock weight wdd and the failure weight
wff .
Lemma A.3. Let q(r̃) ← H ∈ D0 , t ∈ {ss, dd, ff} and let C[ ] be context. For
any satisfiable constraint c and for any constraint c′ , such that Var(C[q(t̃)], c) ∩
Var (r̃) = ∅ and wt (C[q(t̃)], c, c′ ) is defined, there exists a constraint d′ such that
wt (C[q(r̃) k tell(t̃ = r̃)], c, d′ ) ≤ wt (C[q(t̃)], c, c′ ) and ∃−Var (C[q(t̃)],c) d′ = ∃−Var (C[q(t̃)],c) c′ .
Proof. Immediate.
Lemma A.4. Let q(r̃) ← H ∈ D0 and t ∈ {ss, dd, ff}. For any context CI [ ], any
satisfiable constraint c and for any constraint c′ , the following holds.
(1 ) If Var(H) ∩ Var (CI , c) ⊆ Var(r̃) and wt (CI [q(r̃)], c, c′ ) is defined, then there
exists a constraint d′ , such that Var(d′ ) ⊆ Var (CI [H], c), wt (CI [H], c, d′ ) ≤
wt (CI [q(r̃)], c, c′ ) and ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ .
(2 ) If Var (H)∩Var (CI , c) ⊆ Var (r̃), Var (c′ )∩Var (r̃) ⊆ Var(CI [H], c) and wt (CI [H], c, c′ )
is defined, then there exists a constraint d′ , such that
wt (CI [q(r̃)], c, d′ ) ≤ wt (CI [H], c, c′ ) and ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ .
Proof. Immediate.
The following Lemma is crucial in the proof of completeness.
Lemma A.5. Let 0 ≤ i ≤ n, t ∈ {ss, dd, ff}, cl : q(r̃) ← H ∈ Di , and let cl′ :
q(r̃) ← H′ be the corresponding declaration in Di+1 (in the case i < n). For any
context CI [ ] and any satisfiable constraint c and for any constraint c′ the following
holds:
(1 ) If Var(H) ∩ Var (CI , c) ⊆ Var(r̃) and wt (CI [q(r̃)], c, c′ ) is defined, then there
exists a constraint d′ , such that Var(d′ ) ⊆ Var (CI [H], c), wt (CI [H], c, d′ ) ≤
wt (CI [q(r̃)], c, c′ ) and ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ ;
(2 ) If Var(H, H′ ) ∩ Var (CI , c) ⊆ Var(r̃), Var(c′ ) ∩ Var (r̃) ⊆ Var (CI [H], c) and
wt (CI [H], c, c′ ) is defined, then there exists a constraint d′ , such that Var(d′ ) ⊆
Var(CI [H′ ], c), wt (CI [H′ ], c, d′ ) ≤ wt (CI [H], c, c′ ) and
∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ .
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

·

App–8

Sandro Etalle et al.

Proof. Observe that, for i = 0, the proof of 1 follows from the first part of
Lemma A.4. We prove here that, for each i ≥ 0,
a) if 1 holds for i then 2 holds for i;
b) if 1 and 2 hold for i then 1 holds for i + 1.
The proof of the Lemma then follows from straightforward inductive argument.
a) If cl was not affected by the transformation step from Di to Di+1 then the
result is obvious by choosing d′ = ∃−Var (CI [H],c) c′ . Assume then that cl is affected
when transforming Di to Di+1 and let us distinguish various cases.
Case 1: cl′ ∈ Di+1 was obtained from Di by unfolding.
In this case, the situation is the following:
- cl : q(r̃) ← C[p(t̃)] ∈ Di
- u : p(s̃) ← B ∈ Di
- cl′ : q(r̃) ← C[B k tell(t̃ = s̃)] ∈ Di+1
where cl and u are assumed to be renamed so that they do not share variables.
Let n = wt (CI [C[p(t̃)]], c, c′ ). By the definition of transformation sequence, there
exists a declaration p(s̃) ← B0 ∈ D0 . Moreover, by the hypothesis on the variables,
Var (C[p(t̃)], C[B k tell(t̃ = s̃)]) ∩ Var (CI , c) ⊆ Var (r̃) and then Var (CI [C[p(t̃)]], c) ∩
Var (s̃) = ∅. Therefore, by Lemma A.3, there exists a constraint d1 , such that
wt (CI [C[p(s̃) k tell(t̃ = s̃)]], c, d1 ) ≤ wt (CI [C[p(t̃)]], c, c′ ) = n

(46)

∃−Var (CI [C[p(t̃)]],c) d1 = ∃−Var (CI [C[p(t̃)]],c) c′ .

(47)

and
By the hypothesis on the variables and since u is renamed apart from cl, Var (B) ∩
Var (CI , C, t̃, c) = ∅ and therefore Var (B) ∩ Var(CI [C[ ] k tell(t̃ = s̃)], c) ⊆ Var(s̃).
Then, by Point 1, there exists a constraint d′ , such that Var (d′ ) ⊆ Var(CI [C[B k tell(t̃ =
s̃)]], c), wt (CI [C[B k tell(t̃ = s̃)]], c, d′ ) ≤ wt (CI [C[p(s̃) k tell(t̃ = s̃)]], c, d1 ) and
∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) d′ = ∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) d1 .
I

I

By (46), wt (CI [C[B k tell(t̃ = s̃)]], c, d′ ) ≤ n.
Furthermore, by hypothesis and construction, Var (c′ , d′ )∩Var (r̃) ⊆ Var (CI [C[p(t̃)]], c)
and, without loss of generality, we can assume that Var (d1 )∩Var (r̃) ⊆ Var (CI [C[p(t̃)]], c).
Then, by (47) and since Var (CI [C[p(t̃)]], c) ⊆ Var (CI [C[p(s̃) k tell(t̃ = s̃)]], c), we
have that ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ and this completes the proof.
Case 2: cl′ is the result of a tell elimination or introduction.
The proof is analogous to that one given for Case 2 of Proposition 4.5 and it is
omitted.
Case 3: cl′ is the result of a backward instantiation.
Let cl be the corresponding declaration in Di . The situation is then the following:
- cl : q(r̃) ← C[p(t̃)]
- cl′ : q(r̃) ← C[p(t̃) k tell(b) k tell(t̃ = s̃)]
where f : p(s̃) ← tell(b) k H ∈ Di has no variable in common with cl (the case
cl′ : q(r̃) ← C[p(t̃) k tell(t̃ = s̃)] is analogous and hence omitted). By the hypothesis,
Var (C[p(t̃)], C[p(t̃) k tell(b) k tell(t̃ = s̃)]) ∩ Var(CI , c) ⊆ Var (r̃), Var (c′ ) ∩ Var(r̃) ⊆
Var (CI [C[p(t̃)]], c) and there exists n such that wt (CI [C[p(t̃)]], c, c′ ) = n. Then
Var (CI [C[p(t̃)]], c) ∩ Var (s̃) = ∅ and, without loss of generality, we can assume
that Var (H) ∩ Var (CI , c) = ∅.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–9

Moreover, by the definition of transformation sequence, there exists a declaration
p(s̃) ← B0 ∈ D0 and then, by Lemma A.3, there exists a constraint d1 such that
wt (CI [C[p(s̃) k tell(t̃ = s̃)]], c, d1 ) ≤ wt (CI [C[p(t̃)]], c, c′ ) = n

(48)

∃−Var (CI [C[p(t̃)]],c) d1 = ∃−Var (CI [C[p(t̃)]],c) c′ .

(49)

and

Using the hypothesis on the variables and since f is renamed apart from Var (r̃),
we have that
Var(tell(b) k H) ∩ Var(CI [C[ k tell(t̃ = s̃)]], c) ⊆ Var (s̃).
Then, from Point 1 of the Lemma (assumed as hypothesis) and (48) it follows that
there exists a constraint d2 such that
wt (CI [C[tell(b) k H k tell(t̃ = s̃)]], c, d2 ) ≤ wt (CI [C[p(s̃) k tell(t̃ = s̃)]], c, d1 ) ≤ n (50)
and
∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) d2 = ∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) d1
I

I

(51)

hold. By definition of weight, we can assume that Var (d1 ) ⊆ Var (CI [C[p(s̃) k tell(t̃ =
s̃)]], c) and therefore, we have that Var (b) ∩ Var(CI [C[p(s̃) k tell(t̃ = s̃)]], c, d1 ) ⊆
Var (s̃).
We have now two cases:
1) D |= ∃−Var (s̃) d1 → ∃−Var (s̃) b. In this case, by (48), there exists a derivation
ξ = hD0 .CI [C[p(s̃) k tell(t̃ = s̃)]], ci →∗ hD0 .BF , cF i,
such that m(BF , cF ) = t, wh(ξ) ≤ n and
∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) cF = ∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) d1 .
I

I

By the hypothesis on the variables, we can build a derivation
χ = hD0 .CI [C[p(t̃) k tell(b) k tell(t̃ = s̃)]], ci →∗ hD0 .B′F , d3 i
which performs exactly the same steps of ξ, plus possibly a tell action, such that
wh(χ) ≤ n, m(B′F , d3 ) = m(BF , cF ) and
∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) d3 = ∃−Var (C [C[p(s̃) k tell(t̃=s̃)]],c) d1 .
I

I

(52)

Let d′ = ∃−Var (C [C[p(t̃) k tell(b) k tell(t̃=s̃)]],c) d3 . By the previous result and by definiI

tion of weight wt (CI [C[p(t̃) k tell(b) k tell(t̃ = s̃)]], c, d′ ) ≤ n.
Moreover, by hypothesis, Var (c′ , d′ ) ∩ Var(r̃) ⊆ Var (CI [C[p(t̃)]], c) and we can
assume, without loss of generality, that Var (d1 , d2 ) ∩ Var (r̃) ⊆ Var(CI [C[p(t̃)]], c).
Then, by (49), (52) and by definition of d′ , it follows that ∃−Var (CI [q(r̃)],c) d′ =
∃−Var (CI [q(r̃)],c) c′ and then the thesis holds.
2) D 6|= ∃−Var (s̃) d1 → ∃−Var (s̃) b. In this case, by (51), D 6|= ∃−Var (s̃) d2 → ∃−Var (s̃) b.
By (50) this means that there exists a derivation
ξ = hD0 .CI [C[tell(b) k H k tell(t̃ = s̃)]], ci →∗ hD0 .BF , cF i 6→
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

·

App–10

Sandro Etalle et al.

such that tell(b) k H k tell(t̃ = s̃) is not evaluated in ξ, m(BF , cF ) = t, wh(ξ) ≤ n and
∃−Var (C [C[tell(b) k H k tell(t̃=s̃)]],c) cF = ∃−Var (C [C[tell(b) k H k tell(t̃=s̃)]],c) d2 . By definiI
I
tion, we can construct another derivation
χ = hD0 .CI [C[p(t̃) k tell(b) k tell(t̃ = s̃)]], ci →∗ hD0 .B′F , cF i 6→
which performs exactly the same steps of ξ (and therefore wh(χ) ≤ n) and such that
m(BF , cF ) = m(B′F , cF ). Let d′ = ∃−Var (C [C[p(t̃) k tell(b) k tell(t̃=s̃)]],c) cF . By definition
I
of derivation
Var(cF ) ∩ Var(CI [C[tell(b) k H k tell(t̃ = s̃)]], c) ⊆ Var(CI , C, c)
and therefore ∃−Var (C [C[tell(b) k H k tell(t̃=s̃)]],c) d′ = ∃−Var (C [C[tell(b) k H k tell(t̃=s̃)]],c) d2 .
I
I
The remainder of the proof is now analogous to that one of the previous case.
Case 4: Either cl′ is the result of an ask simplification or cl′′ is the result of a tell
simplification. The proof is analogous to that one given for Case 4 of Proposition 4.5
and hence it is omitted.
Case 5: cl′ is the result of a branch elimination or of a conservative ask elimination.
The proof is straightforward by noting that: (a) according to Definition 4.1 we
consider also inconsistent stores resulting from non-terminated computations; (b)
an ask action of the form ask(true) always succeeds; (c) if we delete an ask(true)
action we obtain a derivation whose weight is smaller.
Case 6: cl′ is the result of a distribution.
Let
Pn
- cl : q(r̃) ← C[H k j=1 ask(cj ) → Bj ] ∈ Di
P
n
- cl′ : q(r̃) ← C[ j=1 ask(cj ) → (H k Bj )] ∈ Di+1
where e = pc(C[ ]) and for every constraint e′ such that Var (e′ ) ∩ Var (cl) ⊆
Var (q(r̃), C), if hDi .H, e′ ∧ ei is productive then both the following conditions hold:
—there exists at least one j ∈ [1, n] such that D |= (e′ ∧ e) → cj
—for each j ∈ [1, n], either D |= (e′ ∧ e) → cj or D |= (e′ ∧ e) → ¬cj
We prove that, for any derivation
ξ = hD0 .CI [C[H k

n
X

ask(cj ) → Bj ]], ci →∗ hD0 .B, di

j=1

with m(B, d) ∈ {ss, dd, ff}, there exists a derivation
ξ ′ = hD0 .CI [C[

n
X

ask(cj ) → (H k Bj )]], ci →∗ hD0 .B′ , d′ i

j=1

such that
∃−Var (C [C[H k Pn
I

j=1

ask(cj )→Bj ]],c)

d′ = ∃−Var (C [C[H k Pn
I

j=1

ask(cj )→Bj ]],c)

d

where also wh(ξ ′ ) ≤ wh(ξ), and m(B′ , d′ ) = m(B, d). This together with the definition of weight implies the thesis.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–11

P
If H k nj=1 ask(cj ) → Bj is not evaluated in ξ, then the proof is immediate.
Otherwise we have to distinguish two cases:
1) There exists an h ∈ [1, n], such that
P
P
ξ = hD0 .CI [C[H k nj=1 ask(cj ) → Bj ]], ci →∗ hD0 .Cm [H k nj=1 ask(cj ) → Bj ], dm i
→ hD0 .Cm [H k Bh ], dm i →∗ hD0 .B, di
and D |= dm → ch . In this case we can construct the derivation
Pn
χ = hD0 .CI [C[ j=1 ask(cj ) → (H k Bj )]], ci
Pn
→∗ hD0 .Cm [ j=1 ask(cj ) → (H k Bj )], dm i
→ hD0 .Cm [H k Bh ], dm i →∗ hD0 .B, di
which performs exactly the same steps of ξ and then the thesis holds.
2) ξ is of the form
P
P
ξ = hD0 .CI [C[H k nj=1 ask(cj ) → Bj ]], ci →∗ hD0 .Cm [H k nj=1 ask(cj ) → Bj ], dm i
P
n
→ hD0 .Cm [H′ k j=1 ask(cj ) → Bj ], dm+1 i →∗ hD0 .B, di.
By Lemma A.1 and by definition of pc, we can construct another derivation
Pn
Pn
χ = hD0 .CI [C[H k j=1 ask(cj ) → Bj ]], ci →∗ hD0 .Cm [H k j=1 ask(cj ) → Bj ], dm i
P
n
→∗ hD0 .Ck [H k j=1 ask(cj ) → Bj ], dk i →∗ hD0 .B, di
which performs the same steps of ξ (possibly in a different order) and such that
the the agent H is not evaluated in the first k steps, where Var(dP
k ) ∩ Var (cl) ⊆
Var (q(r̃), C) and D |= dk → e(= pc(C[ ])). Let χ1 = hD0 .Ck [H k nj=1 ask(cj ) →
Bj ], dk i →∗ hD0 .B, di. Now, if hD0 .H, dk i is not productive, the proof is analogous
to that one of Case 6 of Proposition 4.5 and hence it is omitted. Then assume
that hD0 .H, dk i is productive. By definition of distribution there exists at least one
j ∈ [1, n] such that D |= dk → cj and for each j ∈ [1, n], either D |= dP
k → cj or D |=
n
dk → ¬cj . Then, by definition, there exists a derivation ξ1 = hD0 .Ck [ j=1 ask(cj ) →
∗
(H k Bj )], dk i → hD0 .B, di, which performs the same steps of χ1 (possibly in a
different order).
Therefore there exists a derivation
Pn
Pn
′
ξ = hD0 .CI [C[ j=1 ask(cj ) → (H k Bj )]], ci →∗ hD0 .Cm [ j=1 ask(cj ) → (H k Bj )], dm i
Pn
→∗ hD0 .Ck [ j=1 ask(cj ) → (H k Bj )], dk i →∗ hD0 .B, di
which performs the same steps of χ (in a different order). By construction wh(ξ ′ ) =
wh(χ) = wh(ξ) and then the thesis holds.
Case 7: cl′ is the result of a folding.
Let
- cl : q(r̃) ← C[B] be the folded declaration (∈ Di ),
- f : p(X̃) ← B be the folding declaration (∈ D0 ),
- cl′ : q(r̃) ← C[p(X̃)] be the result of the folding operation (∈ Di+1 ),
where, by hypothesis, Var (cl) ∩ Var(X̃) ⊆ Var (B), Var (B) ∩ Var(r̃, C) ⊆ Var (X̃),
Var (C[B], C[p(X̃)]) ∩ Var (CI , c) ⊆ Var(r̃), Var (c′ ) ∩ Var (r̃) ⊆ Var (CI [C[B]], c) and
there exists n such that wt (CI [C[B]], c, c′ ) = n. Then,
Var (B) ∩ Var (CI [C[ ]], c) ⊆ Var (B) ∩ Var (r̃, C) ⊆ Var(X̃)

(53)

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–12

·

Sandro Etalle et al.

and
Var(c′ ) ∩ Var (r̃) ⊆ Var (CI [C[B]], c) ∩ Var (r̃) ⊆ Var(CI [C[p(X̃)]], c)

(54)

hold. Moreover, we can assume without loss of generality that Var(c′ ) ∩ Var(X̃) ⊆
Var (CI [C[B]], c).
Since f ∈ D0 , from (53) and Point 2 of Lemma A.4 it follows that there exists a
constraint d′ such that wt (CI [C[p(X̃)]], c, d′ ) ≤ wt (CI [C[B]], c, c′ ) and
∃−Var (CI [C[p(X̃)]],c) d′ = ∃−Var (CI [C[p(X̃)]],c) c′ .

(55)

We can assume, without loss of generality, that Var (d′ ) ⊆ Var (CI [C[p(X̃)]], c). Then
by using (54) and (55) we obtain that ∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′ which
concludes the proof of a).
b) Assume that the parts 1 and 2 of this Lemma hold for i ≥ 0. We prove that
1 holds for i + 1 > 0.
Let cl : q(r̃) ← H ∈ Di+1 , and let c̄l : q(r̃) ← H̄ be the corresponding declaration
in Di . Moreover let CI [ ] be a context, c a satisfiable constraint and let c′ be a
constraint, such that Var(H) ∩ Var (CI , c) ⊆ Var (r̃) and wt (CI [q(r̃)], c, c′ ) is defined.
Without loss of generality, we can assume that Var (H̄)∩Var (CI , c) ⊆ Var(r̃). Then,
since by inductive hypothesis, part 1 holds for i, there exists a constraint d1 such
that Var (d1 ) ⊆ Var (CI [H̄], c),
wt (CI [H̄], c, d1 ) ≤ wt (CI [q(r̃)], c, c′ ) and ∃−Var (CI [q(r̃)],c) d1 = ∃−Var (CI [q(r̃)],c) c′ . (56)
Since by inductive hypothesis part 2 holds for i, there exists a constraint d′ , such
that Var(d′ ) ⊆ Var (CI [H], c), wt (CI [H], c, d′ ) ≤ wt (CI [H̄], c, d1 ) and ∃−Var (CI [q(r̃)],c) d′ =
∃−Var (CI [q(r̃)],c) d1 .
By (56) we obtain wt (CI [H], c, d′ ) ≤ wt (CI [q(r̃)], c, c′ ) and
∃−Var (CI [q(r̃)],c) d′ = ∃−Var (CI [q(r̃)],c) c′
and then the thesis holds.
Lemma A.6. Let 0 ≤ i ≤ n, c1 , cm satisfiable constraints, ck a constraint and
assume that there exists a derivation ξ : hDi .A1 , c1 i →∗ hDi .Am , cm i →∗ hDi .Ak , ck i,
such that
i). in the first m − 1 steps of ξ rule R2 is used only for evaluating agents of the
form ask(c) → B,
ii). wt (A1 , c1 , ck ) is defined (for t = m(Ak , ck ) ∈ {ss, dd, ff}).
Then there exists a constraint c′ such that Var(c′ ) ⊆ Var(Am , cm ), ∃−Var (A1 ,c1 ) ck =
∃−Var (A1 ,c1 ) c′ and wt (Am , cm , c′ ) ≤ wt (A1 , c1 , ck ).
Proof. We prove the thesis for one derivation step. Then the proof of the
Lemma follows by using a straightforward inductive argument. Assume that c1 , c2
are satisfiable constraints, ck is a constraint and that there exists a derivation
hDi .A1 , c1 i → hDi .A2 , c2 i →∗ hDi .Ak , ck i
such that m(Ak , ck ) ∈ {ss, dd, ff} and the first step can use rule R2 only for evaluating agents of the form ask(c) → B. By the definition of derivation we have
A1 = C1 [A], where C1 [ ] is not a guarding context. We have now three cases:
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–13

1) A = tell(c). In this case
hDi .C1 [tell(c)], c1 i → hDi .C1 [Stop], c1 ∧ ci →∗ hDi .Ak , ck i.
Since C1 [ ] is not a guarding context the definition of weight implies that
wt (C1 [Stop], c1 ∧ c, ∃−Var (C1 [Stop],c1 ∧c) ck ) = wt (C1 [tell(c)], c1 , ck )
where t = m(Ak , ck ). Then the thesis holds
2) A = q(ṽ) and there exists a declaration cl : q(r̃) ← B ∈ Di . In this case
hDi .C1 [q(ṽ)], c1 i → hDi .C1 [B k tell(ṽ = r̃)], c1 i →∗ hDi .Ak , ck i.
¿From the definition of derivation it follows that Var(C1 [q(ṽ)], c1 ) ∩ Var(q(r̃)) =
∅. Furthermore, by definition of transformation sequence, there exists a declaration q(r̃) ← H ∈ D0 . Since wt (C1 [q(ṽ)], c1 , ck ) is defined by hypothesis (where
t = m(Ak , ck )), from Lemma A.3 it follows that there exists a constraint d′ such
that wt (C1 [q(r̃) k tell(ṽ = r̃)], c1 , d′ ) ≤ wt (C1 [q(ṽ)], c1 , ck ) and ∃−Var (C1 [q(ṽ)],c1 ) d′ =
∃−Var (C1 [q(ṽ)],c1 ) ck .
¿From the definition of derivation it follows that Var (B) ∩ Var (C1 [ k tell(ṽ =
r̃)], c1 ) ⊆ Var (r̃). Part 1 of Lemma A.5 implies that there exists a constraint
c′ such that Var (c′ ) ⊆ Var(C1 [B k tell(ṽ = r̃)], c1 ), wt (C1 [B k tell(ṽ = r̃)], c1 , c′ ) ≤
wt (C1 [q(r̃) k tell(ṽ = r̃)], c1 , d′ ) and
∃−Var (C

1 [q(r̃)

′
′
k tell(ṽ=r̃)],c1 ) c = ∃−Var (C1 [q(r̃) k tell(ṽ=r̃)],c1 ) d .

These results together with the inclusion Var (C1 [q(ṽ)], c1 ) ⊆ Var (C1 [q(r̃) k tell(ṽ =
r̃)], c1 ) imply that wt (C1 [B k tell(ṽ = r̃)], c1 , c′ ) ≤ wt (C1 [q(ṽ)], c1 , ck ) and
∃−Var (C1 [q(ṽ)],c1 ) c′ = ∃−Var (C1 [q(ṽ)],c1 ) ck ,
thus concluding the proof for this case.
3) A = ask(c) → B and D |= c1 → c. In this case
hDi .C1 [ask(c) → B], c1 i → hDi .C1 [B], c1 i →∗ hDi .Ak , ck i.
Since C1 [ ] is not a guarding context and D |= c1 → c we obtain
wt (C1 [B], c1 , ∃−Var (C1 [B],c1 ) ck ) ≤ wt (C1 [ask(c) → B], c1 , ck )
where t = m(Ak , ck ), which concludes the proof.
We need one last lemma.
Lemma A.7. Let c be a satisfiable constraint, A be the agent A1 k . . . k Al , where
for any j ∈ [1, l] either Aj is a choice agent or Aj = Stop and assume there exists a
split derivation ν in D0 ,
ν = hD0 .A, ci → hD0 .A′ , c′ i →∗ hD0 .B, di,
where m(B, d) ∈ {ss, dd, ff}. Then hDi .A, ci → hD0 .A′ , c′ i →∗ hD0 .B, di is a split
derivation in Di ∪ D0 .
Proof. The proof is straightforward, by observing that by the hypothesis on A
the first step of ν uses the rule R2 (in case such a step exists) and therefore, by
definition of split derivation, wt (A, c, d) > wt (A′ , c′ , d), where t = m(B, d). Then by
definition, hDi .A, ci → hD0 .A′ , c′ i →∗ hD0 .B, di is a split derivation in Di ∪ D0 .
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–14

·

Sandro Etalle et al.

We can now prove our main theorem.
Theorem 4.13 (Total Correctness). Let D0 , . . . , Dn be a transformation sequence. Then, for any agent A,
—O(D0 .A) = O(Dn .A).
Proof. The proof proceeds by showing simultaneously, by induction on i, that
for i ∈ [0, n]:
(1) for any agent A, O(D0 .A) = O(Di .A);
(2) Di is weight complete.
Base case. We just need to prove that D0 is weight complete. Assume that there
exists a derivation hD0 .A, cI i →∗ hD0 .B, cF i, where cI is a satisfiable constraint and
m(B, cF ) ∈ {ss, dd, ff}. Then there exists a derivation ξ : hD0 .A, cI i →∗ hD0 .B′ , c′F i,
such that m(B′ , c′F ) = m(B, cF ), whose weight is minimal and where ∃−Var (A,cI ) c′F =
∃−Var (A,cI ) cF . It follows from Definition 4.7 that ξ is a split derivation.
Induction step.
By the inductive hypothesis for any agent A, O(D0 .A) = O(Di−1 .A) and Di−1 is
weight complete. From propositions 4.5 and 4.9 it follows that if Di is weight
complete then for any agent A, O(D0 .A) = O(Di .A). So, in order to prove parts 1
and 2, we only have to show that Di is weight complete.
Assume then that there exists a derivation hD0 .A, cI i →∗ hD0 .B, cF i such that cI is
a satisfiable constraint and m(B, cF ) ∈ {ss, dd, ff}. ¿From the inductive hypothesis
it follows that there exists a split derivation
χ = hDi−1 .A, cI i →∗ hDi−1 .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i
where
∃−Var (A,cI ) c′′F = ∃−Var (A,cI ) cF and m(B′′ , c′′F ) = m(B, cF ).

(57)

Let d ∈ Di−1 \Di be the modified clause in the transformation step from Di−1 to Di .
If in the first m steps of χ there is no procedure call which uses d then clearly
there exists a split derivation ξ in Di ∪ D0 ,
ξ = hDi .A, cI i →∗ hDi .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i which performs
the same steps of χ and then the thesis holds.
Otherwise, assume without loss of generality that R4 is the rule used in the first
step of derivation χ and that d is the clause employed in the first step of χ. We
also assume that the declaration d is used only once in χ, since the extension to
the general case is immediate.
We have to distinguish various cases according to what happens to the clause d
when moving from Di−1 to Di .
Case 1: d is unfolded.
Let d′ be the corresponding declaration in Di . The situation is the following:
- d : q(r̃) ← C[p(t̃)] ∈ Di−1 ,
- u : p(s̃) ← H ∈ Di−1 , and
- d′ : q(r̃) ← C[H k tell(t̃ = s̃)] ∈ Di ,
where d and u are assumed to be renamed apart. By the definition of split derivaACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–15

tion, χ has the form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Am , cm i →
hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i.
Without loss of generality, we can assume that Var (χ) ∩ Var(u) 6= ∅ if and only if
p(t̃) is evaluated in the first m steps of χ, in which case u is used for evaluating it.
We have to distinguish two cases.
1) There exists k < m such that the k-th derivation step of χ is the procedure
call p(t̃). In this case χ has the form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Ck [p(t̃)], ck i →
hDi−1 .Ck [H k tell(t̃ = s̃)], ck i →∗ hDi−1 .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i.
Then there exists a corresponding derivation in Di ∪ D0
ξ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Ck [H k tell(t̃ = s̃)], ck i →∗
hDi .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .B′′ , c′′F i,
which performs exactly the same steps of χ except for a procedure call to p(t̃). In
this case the proof follows by observing that, since by the inductive hypothesis χ
is a split derivation, the same holds for ξ.
2) There is no procedure call to p(t̃) in the first m steps. Therefore χ has the
form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Cm [p(t̃)], cm i →
hD0 .Cm+1 [p(t̃)], cm i →∗ hD0 .B′′ , c′′F i.
Then, by the definition of Di , there exists a derivation
ξ0 = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Cm [H k tell(t̃ = s̃)], cm i → hD0 .Cm+1 [H k tell(t̃ = s̃)], cm i.
Observe that from the derivation hD0 .Cm+1 [p(t̃)], cm i →∗ hD0 .B′′ , c′′F i and (57) it
follows that
wt (Cm+1 [p(t̃)], cm , c′′F ) is defined, where t = m(B, cF ).

(58)

The hypothesis on the variables implies that Var (Cm+1 [p(t̃)], cm ) ∩ Var (u) = ∅.
Then, by the definition of transformation sequence and since u ∈ Di−1 , there exists
a declaration p(s̃) ← H0 ∈ D0 . By Lemma A.3 and part 1 of Lemma A.5 it follows
that there exists a constraint dF such that
wt (Cm+1 [H k tell(t̃ = s̃)], cm , dF ) ≤ wt (Cm+1 [p(t̃)], cm , c′′F )

(59)

∃−Var (Cm+1 [p(t̃)],cm ) dF = ∃−Var (Cm+1 [p(t̃)],cm ) c′′F .

(60)

and
Therefore, by the definition of wt , by (59) and since wt (Cm+1 [p(t̃)], cm , c′′F ) is defined,
there exists a derivation
ξ1 = hD0 .Cm+1 [H k tell(t̃ = s̃)], cm i →∗ hD0 .B′ , c′F i,
where ∃−Var (Cm+1 [H k tell(t̃=s̃)],cm ) c′F = ∃−Var (Cm+1 [H k tell(t̃=s̃)],cm ) dF and, by (58),
m(B′ , c′F ) = m(B, cF ).

(61)

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–16

·

Sandro Etalle et al.

By (60)
∃−Var (Cm+1 ,cm ) c′F = ∃−Var (Cm+1 ,cm ) c′′F

(62)

holds and, by definition of weight, we obtain
wt (Cm+1 [H k tell(t̃ = s̃)], cm , c′F ) = wt (Cm+1 [H k tell(t̃ = s̃)], cm , dF ).

(63)

Moreover, we can assume without loss of generality that Var(ξ0 ) ∩ Var (ξ1 ) =
Var (Cm+1 [H k tell(t̃ = s̃)], cm ). Then, by the definition of procedure call
Var (CI [q(ṽ)], cI ) ∩ (Var (c′F ) ∪ Var(c′′F )) ⊆ Var (Cm+1 , cm )

(64)

and there exists a derivation
ξ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Cm [H k tell(t̃ = s̃)], cm i → hD0 .Cm+1 [H k tell(t̃ = s̃)], cm i →∗ hD0 .B′ , c′F i
such that the first m−1 derivation steps do not use rule R2 and the m-th derivation
step uses the rule R2. Now, we have the following equalities
∃−Var (CI [q(ṽ)],cI ) c′F
∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm+1 ,cm ) c′F )
∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm+1 ,cm ) c′′F )
∃−Var (CI [q(ṽ)],cI ) c′′F
∃−Var (CI [q(ṽ)],cI ) cF .

=
=
=
=

(by
(by
(by
(by

(64) and by construction)
(62))
(64) and by construction)
the first statement in (57))

By the definition of weight, wt (CI [q(ṽ)], cI , c′F ) = wt (CI [q(ṽ)], cI , c′′F ), by (63) and (59),
wt (Cm+1 [H k tell(t̃ = s̃)], cm , c′F ) ≤ wt (Cm+1 [p(t̃)], cm , c′′F ) and wt (Cm+1 [p(t̃)], cm , c′′F ) <
wt (CI [q(ṽ)], cI , c′′F ), since χ is a split derivation. Therefore wt (Cm+1 [H k tell(t̃ =
s̃)], cm , c′F ) < wt (CI [q(ṽ)], cI , c′F ) and then, by definition, ξ is a split derivation in
Di ∪ D0 . This, together with (61), implies the thesis.
Case 2: A tell constraint in d is eliminated or introduced.
In the first case, let d′ be the corresponding declaration in Di . Therefore the situation is the following:
- d : q(r̃) ← C[tell(s̃ = t̃) k H]
- d′ : q(r̃) ← C[Hσ]
where σ is a relevant most general unifier of s and t and the variables in the domain
of σ do not occur neither in C[ ] nor in q(r̃). Observe that for any derivation which
uses the declaration d, we can construct another derivation such that the agent
tell(s̃ = t̃) is evaluated before H. Then the thesis follows from Lemma A.5 and from
the argument used in the proof of Case 2 of Proposition 4.5. The proof for the tell
introduction is analogous and hence it is omitted.
Case 3: d is backward instantiated.
Let d′ be the corresponding declaration in Di . The situation is the following:
- d : q(r̃) ← C[p(t̃)] ∈ Di−1 ,
- d′ : q(r̃) ← C[p(t̃) k tell(b) k tell(t̃ = s̃)] ∈ Di ,
where c : p(s̃) ← tell(b) k B ∈ Di−1 has no variable in common with d (the case
d′ : q(r̃) ← C[p(t̃) k tell(t̃ = s̃)] is analogous and hence omitted). We distinguish
two cases:
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–17

1) There is no procedure call to p(t̃) in the first m steps. Therefore χ has the
form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Cm [p(t̃)], cm i →
hD0 .Cm+1 [p(t̃)], cm i →∗ hD0 .B′′ , c′′F i.
Without loss of generality, we can assume that Var(χ) ∩ Var (p(t̃) k tell(b) k tell(t̃ =
s̃)) = Var (t̃). Then, by the definition of Di , there exists a derivation corresponding
to χ,
ξ0 = hDi .CI [q(ṽ)], cI i → hDi .CI [C[p(t̃) k tell(b) k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Cm [p(t̃) k tell(b) k tell(t̃ = s̃)], cm i →
hD0 .Cm+1 [p(t̃) k tell(b) k tell(t̃ = s̃)], cm i.
Following the same reasoning as in Case 3 of Lemma A.5, we can prove that there
exists a constraint dF such that
wt (Cm+1 [p(t̃) k tell(b) k tell(t̃ = s̃)], cm , dF ) ≤ wt (Cm+1 [p(t̃)], cm , c′′F )
where ∃−Var (Cm+1 [p(t̃)],cm ) dF = ∃−Var (Cm+1 [p(t̃)],cm ) c′′F and t = m(B′′ , c′′F ). The rest of
the proof is analogous to Case 1 (unfolding) and hence it is omitted.
2) There is exists k < m such that the k-th derivation step of χ is the procedure
call p(t̃). We distinguish two more cases:
2a) p 6= q. In this case we can assume, without loss of generality, that χ has the
form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[p(t̃)] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Ck [p(t̃)], ck i →
hDi−1 .Ck [tell(b̄) k B̄ k tell(t̃ = s̃′ )], ck i →∗ hDi−1 .Am , cm i →
hD0 .Am+1 , cm i →∗ hD0 .B′′ , c′′F i
where c′ = p(s̃′ ) ← tell(b̄) k B̄ is a renaming of c such that Var(c′ ) ∩ Var (d′ ) = ∅.
In this case there exists a derivation
hDi .CI [q(ṽ)], cI i → hDi .CI [C[p(t̃) k tell(b) k tell(t̃ = s̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Ck [tell(b̄) k B̄ k tell(t̃ = s̃′ ) k tell(b) k tell(t̃ = s̃)], ck i.
Observe now that, given any set of declarations, if there exists a derivation χ′
for the configuration hC′ [tell(b̄) k B̄ k tell(t̃ = s̃′ )], c′ i where c′ is satisfiable and
Var (C′ , c′ )∩Var (b, s̃) = ∅, then there exists a derivation for hC′ [tell(b̄) k B̄ k tell(t̃ =
s̃′ ) k tell(b) k tell(t̃ = s̃)], c′ i which performs the same steps of χ′ plus (possibly) two
steps corresponding to the evaluation of tell(b) and tell(t̃ = s̃). Since (t̃ = s̃′ )∧(t̃ = s̃)
is logically equivalent to (t̃ = s̃′ ) ∧ (s̃′ = s̃), we can substitute tell(t̃ = s̃′ ) k tell(t̃ = s̃)
for tell(t̃ = s̃′ ) k tell(s̃′ = s̃). Moreover, since p(s̃′ ) ← tell(b̄) k B̄ is a renaming of c
and therefore D |= (b̄ ∧ (s̃′ = s̃)) → b holds, we can drop the agent tell(b).
Finally, observe that s̃′ = s̃ can be reduced to a conjunction of equations of the
form X̃ = Ỹ, where X̃ ⊆ Var(s̃) and Ỹ ⊆ Var (s̃′ ) are distinct variables. Therefore,
we can drop the constraint tell(s̃′ = s̃), since the declarations used in the derivation
are renamed apart and Var (C′ [tell(b̄) k B̄ k tell(t̃ = s̃′ )], c′ ) ∩ Var (s̃) = ∅. Then the
thesis holds for this case.
2b) p = q. In this case, the situation is the following:
- d : p(r̃) ← tell(b′ ) k C′′ [p(t̃)] ∈ Di−1 ,
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–18

·

Sandro Etalle et al.

- d′ : p(r̃) ← tell(b′ ) k C′′ [p(t̃) k tell(b) k tell(t̃ = s̃)] ∈ Di ,
where c : p(s̃) ← tell(b) k C′ [p(ũ)] is a renaming of d which has no variables in common with d. Let c′ = p(s̃′ ) ← tell(b̄) k C̄[p(ũ′ )] be a renaming of c such that Var (c′ )∩
Var (d′ ) = ∅. Now the proof is analogous to the previous one by observing that, for
any set of declarations, if there exists a derivation χ′ for hC̄′ [tell(b̄) k C̄[p(ũ′ )] k tell(t̃ =
s̃′ )], c′ i where c′ is satisfiable and Var (C̄′ , c′ ) ∩ Var (b, s̃) = ∅, then there exists a
derivation for hC̄′ [tell(b̄) k C̄[p(ũ′ )] k tell(t̃ = s̃′ ) k tell(b) k tell(t̃ = s̃)], c′ i which performs the same steps of χ′ , plus some tell actions (analogously to the previous case,
we can drop the tell agents tell(b) and tell(t̃ = s̃)). This concludes the proof of this
case.
Case 4: An ask P
guard in d is simplified. Let
- d : q(r̃) ← C[ nj=1 ask(cj ) → Bj ],
Pn
- d′ : q(r̃) ← C[ j=1 ask(c′j ) → Bj ] ∈ Di ,
where for j ∈ [1, n], D |= ∃−Var (q(r̃),C,Bj ) (pc(C[ ]) ∧ cj ) ↔ (pc(C[ ]) ∧ c′j ) and
d ∈ Di−1 is the declaration to which the guard simplification was applied.
By the definition of split derivation χ has the form
Pn
χ = hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[ j=1 ask(cj ) → Bj ] k tell(ṽ = r̃)], cI i →∗
Pn
hDi−1 .Cm [ j=1 ask(cj ) → Bj ], cm i → hD0 .Am+1 , cm i →∗ hD0 .B′′ , c′′F i.
Since by the inductive hypothesis for any agent A, O(D0 .A) = O(Di−1 .A), it is easy
to check that there exists a derivation
Pn
χ′ = hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[ j=1 ask(cj ) → Bj ] k tell(ṽ = r̃)], cI i →∗
Pn
Pn
hDi−1 .Cm [ j=1 ask(cj ) → Bj ], cm i →∗ hDi−1 .Cm+h [ j=1 ask(cj ) → Bj ], cm+h i
→∗ hDi−1 .B̄, c̄F i
such that ∃−Var (CI [q(ṽ)],cI ) c̄F = ∃−Var (CI [q(ṽ)],cI ) c′′F and m(B̄, c̄F ) = m(B′′ , c′′F ). ¿From
(57) it follows that
∃−Var (CI [q(ṽ)],cI ) c̄F = ∃−Var (CI [q(ṽ)],cI ) cF and m(B̄, c̄F ) = m(B, cF ).

(65)

Without loss of generality, we can assume that χ′ is chosen in such a way that
the first m + h steps of χ′ do not use rule R2 and that h is maximal, in the sense
that either cm+h is not satisfiable or in the m + h + 1-th step we can only use rule
R2.
In the first case, let C′m+h be thePcontext obtained from Cm+h as follows: any
(renamed) occurrence of the agent nj=1 ask(cj ) → Bj in Cm+h [ ], introduced in χ0
by a procedure
Pncall of the form q(s̃), is replaced by a (suitably renamed) occurrence
of the agent j=1 ask(c′j ) → Bj . Then, by definition of Di , we have that
Pn
ξ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[ j=1 ask(c′j ) → Bj ] k tell(ṽ = r̃)], cI i →∗
P
n
hDi .C′m+h [ j=1 ask(c′j ) → Bj ], cm+h i
is a derivation in Di which does not use rule R2 and such that
m(C′m+h [

n
X

ask(c′j ) → Bj ], cm+h ) = m(B, cF ) = ff.

j=1

Then the thesis follows by definition of split derivation.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–19

Now assume that cm+h is satisfiable. ByPLemma A.6 and (65), there exists a
n
constraint d̄, such that Var (d̄) ⊆ Var (Cm+h [ j=1 ask(cj ) → Bj ], cm+h ) and
wt (Cm+h [

n
X

ask(cj ) → Bj ], cm+h , d̄) ≤ wt (CI [q(ṽ)], cI , cF )

(66)

j=1

where
∃−Var (CI [q(ṽ)],cI ) d̄ = ∃−Var (CI [q(ṽ)],cI ) cF and t = m(B, cF ).
(67)
Pn
By definition of weight, by (66) and since Var (d̄) ⊆ Var(Cm+h [ j=1 ask(cj ) →
Bj ], cm+h ), there exists a derivation
hD0 .Cm+h [

n
X

ask(cj ) → Bj ], cm+h i →∗ hD0 .B̄′ , d̄′ i

j=1

such that ∃−Var (Cm+h [

Pn

j=1

ask(cj )→Bj ],cm+h ) d̄

′

= d̄ and m(B̄′ , d̄′ ) = t. Then, by the

definition of weight and by (66),
wt (Cm+h [

n
X

ask(cj ) → Bj ], cm+h , d̄′ ) ≤ wt (CI [q(ṽ)], cI , cF )

(68)

j=1

holds. Without loss of generality, we can assume that Var(d̄′ ) ∩ Var (CI [q(ṽ)], cI ) ⊆
Var (Cm+h , cm+h ). Therefore, from (67) it follows that
∃−Var (CI [q(ṽ)],cI ) d̄′ = ∃−Var (CI [q(ṽ)],cI ) cF and m(B̄′ , d̄′ ) = m(B, cF ).
Pn
Let B̃′ = C′m+h [ j=1 ask(c′j ) → Bj ] be the agent obtained from
B̃ = Cm+h [

n
X

(69)

ask(cj ) → Bj ]

j=1

P
as follows: any (renamed) occurrence of the agent nj=1 ask(cj ) → Bj in Cm+h [ ],
introduced in χ0 by a procedure call
Pn of the form q(s̃), is replaced by a (suitably
renamed) occurrence of the agent j=1 ask(c′j ) → Bj . By the definition of Di and
Pn
since hDi−1 .CI [q(ṽ)], cI i →∗ hDi−1 .Cm+h [ j=1 ask(cj ) → Bj ], cm+h i, there exists a
derivation
n
X
ask(c′j ) → Bj ], cm+h i,
ξ0 = hDi .CI [q(ṽ)], cI i →∗ hDi .C′m+h [
j=1

which does not use rule R2. Observe that, by construction, B̃ has the form
A1 k . . . k Al , where Aj is either a choice agent or Stop for each j ∈ [1, l]. Moreover,
since the first m + h steps of χ0 do not use rule R2 (and therefore, it is not possible
evaluate a procedure call of the form q(s̃) inside a guarding context), B̃′ has the
form A′1 k . . . k A′l , where either A′j = Aj or Aj is a (renamed) occurrence of the
Pn
agent j=1 ask(cj ) → Bj while A′j is a (suitably renamed) occurrence of the agent
Pn
′
′
′
j=1 ask(cj ) → Bj . By Lemma A.1, D |= cm+h → pc(C [ ]), where C [ ] is a renamed
version of the context C[ ] in B̃, which was introduced in χ0 by a procedure call of
the form q(s̃).
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–20

·

Sandro Etalle et al.

Now from the definition of derivation and of ask simplification it follows that, if
ask(c̃j ) → B̃j is a choice branch in B̃ and ask(c̃′j ) → B̃j is the corresponding choice
branch in B̃′ , then
D |= ∃−Var (B̃j ,cm+h ) (cm+h ∧ c̃j ) ↔ (cm+h ∧ c̃′j )
holds. Therefore, by using the same arguments as in Case 4 of Proposition
4.5,
Pn
since (by inductive hypothesis) D0 is weight complete and hD0 .Cm+h [ j=1 ask(cj ) →
Bj ], cm+h i →∗ hD0 .B̄′ , d̄′ i, we obtain that there exists a split derivation in D0 of the
form
ν = hD0 .C′m+h [

n
X

ask(c′j ) → Bj ], cm+h i → hD0 .Bm+h+1 , cm+h i →∗ hD0 .B′ , c′F i

j=1

such that ∃−Var (C′

m+h

[

Pn

j=1

′
ask(c′j )→Bj ],cm+h ) cF

= ∃−Var (C′

m+h

[

Pn

j=1

ask(c′j )→Bj ],cm+h ) d̄

′

and

m(B′ , c′F ) = m(B̄′ , d̄′ ).
Then, by using the same arguments as in Case 4 of Proposition 4.5, from the
definition of weight and from (68) it follows that
Pn
=
wt (C′m+h [ j=1 ask(c′j ) → Bj ], cm+h , c′F )
P
n
′
′
′
wt (Cm+h [ j=1 ask(cj ) → Bj ], cm+h , d̄ )
=
(70)
Pn
wt (Cm+h [ j=1 ask(cj ) → Bj ], cm+h , d̄′ ) ≤ wt (CI [q(ṽ)], cI , cF ),
where t = m(B′ , c′F ). Moreover, we can assume without loss of generality that
Var(ξ0 ) ∩ Var(ν) = Var (C′m+h [

n
X

ask(c′j ) → Bj ], cm+h ).

j=1

Then by (69) we obtain
∃−Var (CI [q(ṽ)],cI ) c′F = ∃−Var (CI [q(ṽ)],cI ) cF and m(B′ , c′F ) = m(B, cF )

(71)

and therefore, by definition of weight,
wt (CI [q(ṽ)], cI , c′F ) = wt (CI [q(ṽ)], cI , cF )
Pn
holds. By Lemma A.7 and by construction of C′m+h [ j=1 ask(c′j ) → Bj ]
ξ1 = hDi .C′m+h [

n
X

(72)

ask(c′j ) → Bj ], cm+h i → hD0 .Bm+h+1 , cm+h i →∗ hD0 .B′ , c′F i

j=1

is a split derivation
in Di ∪D0 . By the definition of split derivation wt (Bm+h+1 , cm+h , c′F ) <
Pn
′
wt (Cm+h [ j=1 ask(c′j ) → Bj ], cm+h , c′F ), where t = m(B′ , c′F ). Then, by (72) and (70),
we have that
wt (Bm+h+1 , cm+h , c′F ) < wt (CI [q(ṽ)], cI , c′F ).
Finally,
P
ξ = hDi .CI [q(ṽ)], cI i →∗ hDi .C′m+h [ nj=1 ask(c′j ) → Bj ], cm+h i →
hD0 .Bm+h+1 , cm+h i →∗ hD0 .B′ , c′F i
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

(73)

Transformations of CCP programs

·

App–21

is a derivation in Di ∪ D0 . By construction the first m + h steps of ξ do not use
rule R2, the m + h + 1-th step uses rule R2. Thus the thesis follows from (73) and
(71).
Case 5: d is the declaration to which either a branch elimination or an ask elimination was applied. In the case of branch elimination the proof follows immediately
from the fact that we consider also the inconsistent results of non-terminated computations. As for the ask elimination case, let us assume that
- d : q(r̃) ← C[ask(true) → H] ∈ Di−1 and
- d′ : q(r̃) ← C[H] ∈ Di .
We show, by induction on the weight wt (CI [q(ṽ)], cI , c′′F ), where t = m(B, cF ), that
there exists a split derivation ξ = hDi .CI [q(ṽ)], cI i →∗ hD0 .B′ , c′F i in Di ∪ D0 , such
that ∃−Var (CI [q(ṽ)],cI ) c′F = ∃−Var (CI [q(ṽ)],cI ) c′′F and m(B′ , c′F ) = m(B′′ , c′′F ). Then the
proof follows by (57).
Base case. In this case wt (CI [q(ṽ)], cI , c′′F ) = 0 and by definition of split derivation,
B′′ = Ck [ask(true) → H], χ has the form
χ = hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[ask(true) → H] k tell(ṽ = r̃)], cI i →∗
hDi−1 .Ck [ask(true) → H], c′′F i,
rule R2 is not used and therefore each derivation step is done in Di−1 . Moreover,
observe that since t ∈ {ss, dd, ff}, if c′′F is satisfiable, then Ck is a guarding context.
Then, it is easy to check that
ξ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H] k tell(ṽ = r̃)], cI i →∗ hDi .Ck [H], c′′F i
is a split derivation in Di ∪ D0 , such that m(Ck [H], c′′F ) = m(Ck [ask(true) → H], c′′F ) ∈
{dd, ff} and then the thesis follows by the previous observation.
Induction step. Assume that wt (CI [q(ṽ)], cI , c′′F ) = n > 0 and that χ has the form
χ = hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[ask(true) → H] k tell(ṽ = r̃)], cI i →∗
hDi−1 .Cm [ask(true) → H], cm i → hD0 .Cm [H], cm i →∗ hD0 .B′′ , c′′F i,
since the other case is immediate. By the definition of Di and since χ is a split
derivation, there exists a derivation
ξ0 = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H] k tell(ṽ = r̃)], cI i →∗ hDi .Cm [H], cm i,
which does not use rule R2. Moreover, by definition of split derivation
wt (Cm [H], cm , c′′F ) < wt (CI [q(ṽ)], cI , c′′F )
and therefore, by inductive hypothesis there exists a split derivation in Di ∪ D0 ,
ξ1 = hDi .Cm [H], cm i →∗ hD0 .B′ , c′F i,
such that
m(B′ , c′F ) = m(B′′ , c′′F ) = t and ∃−Var (Cm [H],cm ) c′F = ∃−Var (Cm [H],cm ) c′′F .

(74)

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–22

·

Sandro Etalle et al.

Without loss of generality, we can assume that Var(ξ0 )∩Var (ξ1 ) ⊆ Var (Cm [H], cm ).
Therefore, by (74) and by definition of c′F and c′′F ,
∃−Var (CI [q(ṽ)],cI ) c′F
=
∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm [H],cm ) c′F ) =
∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm [H],cm ) c′′F ) =
∃−Var (CI [q(ṽ)],cI ) c′′F .

(75)

Then by definition of weight, since wt (Cm [H], cm , c′′F ) < wt (CI [q(ṽ)], cI , c′′F ) and by
(74)
wt (Cm [H], cm , c′F ) < wt (CI [q(ṽ)], cI , c′F ).

(76)

Moreover, by our hypothesis on the variables of ξ0 and of ξ1 , there exists a derivation
Di ∪ D0 ,
ξ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[H] k tell(ṽ = r̃)], cI i →∗
hDi .Cm [H], cm i →∗ hD0 .B′ , c′F i.
By (74), (76), since ξ0 do not use Rule R2 and ξ1 is a split derivation in Di ∪ D0 , we
have that ξ is a split derivation in Di ∪ D0 , such that m(B′ , c′F ) = m(B′′ , c′′F ). Now,
the thesis follows by (75).
Case 6: An ask guard
d is distributed. Let
Pin
n
- d : q(r̃) ← C[H k j=1 ask(cj ) → Bj ] ∈ Di−1
Pn
- d′ : q(r̃) ← C[ j=1 ask(cj ) → (H k Bj )] ∈ Di ,
where, for every constraint e′ such that Var (e′ ) ∩ Var (d) ⊆ Var (q(r̃), C), if
hDi−1 .H, e′ ∧ pc(C[ ])i is productive then there exists at least one j ∈ [1, n] such
that D |= (e′ ∧ pc(C[ ])) → cj and for each j ∈ [1, n], either D |= (e′ ∧ pc(C[ ])) → cj
or D |= (e′ ∧ pc(C[ ])) → ¬cj .
By the definition of split derivation, χ has the form
Pn
χ = hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[H k j=1 ask(cj ) → Bj ] k tell(ṽ = r̃)], cI i →∗
Pn
hDi−1 .Cm [ j=1 ask(cj ) → Bj ], cm i → hD0 .Am+1 , cm i →∗ hD0 .B′′ , c′′F i.
If the first m − 1 steps of χ do not evaluate the agent H then the proof is analogous
to that one of Case 6 of Lemma A.5. Otherwise, let us assume that
P
χ = hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[H k nj=1 ask(cj ) → Bj ] k tell(ṽ = r̃)], cI i →∗
P
hDi−1 .Cm [H′ k nj=1 ask(cj ) → Bj ], cm i → hD0 .Am+1 , cm i →∗ hD0 .B′′ , c′′F i.
Since by the inductive hypothesis for any agent A, O(D0 .A) = O(Di−1 .A) there
exists a derivation
Pn
χ′ = hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[H k j=1 ask(cj ) → Bj ] k tell(ṽ = r̃)], cI i →∗
Pn
hDi−1 .Ck [H k j=1 ask(cj ) → Bj ], ck i →∗ hDi−1 .B̄, c̄F i,
where ∃−Var (CI [q(ṽ)],cI ) c̄F = ∃−Var (CI [q(ṽ)],cI ) c′′F and m(B̄, c̄F ) = m(B′′ , c′′F ). By (57),
∃−Var (CI [q(ṽ)],cI ) c̄F = ∃−Var (CI [q(ṽ)],cI ) cF and m(B̄, c̄F ) = m(B, cF ).
′

(77)

Without loss of generality we can assume that the first k steps of χ neither use
rule R2 nor contain the
Pn evaluation of any (renamed) occurrence H̄ of the agent H,
where q(r̃′ ) ← C̄[H̄ k j=1 ask(c̄j ) → B̄j ] is a renamed version of the declaration d
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–23

P
and C̄[H̄ k nj=1 ask(c̄j ) → B̄j ] has been introduced by the evaluation of a procedure
call of the form q(s̃). Moreover, we can assume that k is maximal, in the sense
that either ck is not satisfiable or the k + 1-th step can only either use rule R2 or
evaluate a (renamed) occurrence of H introduced by a procedure call of the form
q(s̃). If ck is not satisfiable, then the proof is analogous to that one of the previous
Case 4.
Assume then that ck is satisfiable. By Lemma
A.6 and (77), there exists a
Pn
constraint d̄, such that Var (d̄) ⊆ Var (Ck [H k j=1 ask(cj ) → Bj ], ck ) and
wt (Ck [H k

n
X

ask(cj ) → Bj ], ck , d̄) ≤ wt (CI [q(ṽ)], cI , cF ),

(78)

j=1

where
∃−Var (CI [q(ṽ)],cI ) d̄ = ∃−Var (CI [q(ṽ)],cI ) cF and t = m(B, cF ).
(79)
Pn
By definition of weight, by (78) and since Var (d̄) ⊆ Var(Ck [H k j=1 ask(cj ) →
Bj ], ck ), there exists a derivation
hD0 .Ck [H k

n
X

ask(cj ) → Bj ], ck i →∗ hD0 .B̄′ , d̄′ i

j=1

′
′ ′
P
k nj=1 ask(cj )→Bj ],ck ) d̄ = d̄ and m(B̄ , d̄ ) = t. Then, by the
definition of weight and by (78),

such that ∃−Var (C

k [H

wt (Ck [H k

n
X

ask(cj ) → Bj ], ck , d̄′ ) ≤ wt (CI [q(ṽ)], cI , cF ).

(80)

j=1

Without loss of generality, we can assume that Var(d̄′ ) ∩ Var (CI [q(ṽ)], cI ) ⊆
Var (Ck , ck ). Therefore from (79) it follows that
∃−Var (CI [q(ṽ)],cI ) d̄′ = ∃−Var (CI [q(ṽ)],cI ) cF and m(B̄′ , d̄′ ) = m(B, cF ).
(81)
P
Pn
n
′
Let Ck [ j=1 ask(cj ) → (H k Bj )] be the agent obtained from Ck [H k j=1 ask(cj ) →
Pn
Bj ] as follows: any (renamed) occurrence of the agent H k j=1 ask(cj ) → Bj in Ck [ ]
which has been introduced by a procedure P
call of the form q(s̃) is replaced by a
(suitably) renamed occurrence of the agent nj=1 ask(cj ) → (H k Bj ).
Pn
By the definition of Di and since hDi−1 .CI [q(ṽ)], cI i →∗ hDi−1 .Ck [H k j=1 ask(cj ) →
Bj ], ck i, there exists a derivation
ξ0 = hDi .CI [q(ṽ)], cI i →∗ hDi .C′k [

n
X

ask(cj ) → (H k Bj )], ck i

j=1

which does not use rule R2. P
n
Now, by construction, C′k [ j=1 ask(cj ) → (H k Bj )] has the form A1 k . . . k Al ,
where Aj is either a choice agent or Stop.
Pn
Moreover, since D0 is weight complete, hD0 .Ck [H k j=1 ask(cj ) → Bj ], ck i →∗
hD0 .B̄′ , d̄′ i and analogously to the Case 6 of Lemma A.5, there exists a split derivation
Pn
ξ1 = hD0 .C′k [ j=1 ask(cj ) → (H k Bj )], ck i →∗ hD0 .B′ , c′F i,

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–24

·

Sandro Etalle et al.

such that ∃−Var (C′ [Pn
k

j=1

ask(cj )→(H

′
′
P
k Bj )],ck ) cF ) = ∃−Var (C′k [ nj=1 ask(cj )→(H k Bj )],ck ) d̄ )

and m(B′ , c′F ) = m(B̄′ , d̄′ ).
Then, by using the same arguments as in Case 6 of Lemma A.5, from the definition of weight and (80) it follows that
wt (C′k [

n
X

ask(cj ) → (H k Bj )], ck , c′F ) =

n
X

ask(cj ) → (H k Bj )], ck , d̄′ ) ≤

j=1

wt (C′k [

j=1

wt (Ck [H k

n
X

ask(cj ) → Bj ], ck , d̄′ ) ≤ wt (CI [q(ṽ)], cI , cF ),

j=1

where t = m(B′ , c′F ).
¿From this point the proof proceeds exactly as in Case 4 by using Lemma A.7
and therefore it is omitted.
Case 7: Finally assume that d is folded.
Let
- d : q(r̃) ← C[H] be the folded declaration (∈ Di−1 )
- f : p(X̃) ← H be the folding declaration (∈ D0 ),
- d′ : q(r̃) ← C[p(X̃)] be the result of the folding operation (∈ Di ),
where, by definition of folding, Var(d) ∩ Var(X̃) ⊆ Var (H) and Var (H) ∩ (Var (r̃) ∪
Var (C)) ⊆ Var (X̃). Since C[ ] is a guarding context, the agent H in C[H] appears
in the scope of an ask guard. By definition of split derivation χ has the form
hDi−1 .CI [q(ṽ)], cI i → hDi−1 .CI [C[H] k tell(ṽ = r̃)], cI i →∗ hDi−1 .Cm [H], cm i →
hD0 .Cm+1 [H], cm i →∗ hD0 .B′′ , c′′F i,
where Cm [ ] is a guarding context. Without loss of generality we can assume that
Var (χ) ∩ Var (X̃) ⊆ Var(H). Then, from the definition of Di it follows that there
exists a derivation
ξ0 = hDi .CI [q(ṽ)], cI i → hDi .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗
hDi .Cm [p(X̃)], cm i → hD0 .Cm+1 [p(X̃)], cm i,
which performs exactly the first m steps as χ. Since hD0 .Cm+1 [H], cm i →∗ hD0 .B′′ , c′′F i,
the definition of weight implies that wt (Cm+1 [H], cm , c′′F ) is defined, where t =
m(B′′ , c′′F ). Then, by (57), we have that
t = m(B, cF ).

(82)

The definitions of derivation and folding imply that Var(H) ∩ Var (Cm+1 , cm ) ⊆
Var (H) ∩ (Var (C,r̃)) ⊆ Var(X̃) holds. Moreover, from the assumptions on the variables, we obtain that Var (c′′F )∩Var (X̃) ⊆ Var (H). Thus, from part 2 of Lemma A.4
it follows that there exists a constraint d′ such that
wt (Cm+1 [p(X̃)], cm , d′ ) ≤ wt (Cm+1 [H], cm , c′′F ) and
∃−Var (Cm+1 [p(X̃)],cm ) d′ = ∃−Var (Cm+1 [p(X̃)],cm ) c′′F .
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

(83)

Transformations of CCP programs

·

App–25

¿From the definition of weight and the fact that wt (Cm+1 [H], cm , c′′F ) is defined it follows that there exists a derivation ξ1 = hD0 .Cm+1 [p(X̃)], cm i →∗ hD0 .B′ , c′F i, where
m(B′ , c′F ) = t and ∃−Var (Cm+1 [p(X̃)],cm ) c′F = ∃−Var (Cm+1 [p(X̃)],cm ) d′ . Then, by the definition of weight, wt (Cm+1 [p(X̃)], cm , c′F ) = wt (Cm+1 [p(X̃)], cm , d′ ) and therefore, by
(83),
∃−Var (Cm+1 [p(X̃)],cm ) c′F = ∃−Var (Cm+1 [p(X̃)],cm ) c′′F and
wt (Cm+1 [p(X̃)], cm , c′F ) ≤ wt (Cm+1 [H], cm , c′′F )

(84)

holds. Moreover, from (82) we obtain
m(B′ , c′F ) = m(B, cF ).

(85)

Without loss of generality, we can now assume that
Var(ξ0 ) ∩ Var (ξ1 ) = Var (Cm+1 [p(X̃)], cm ).
Then, by (84) and (57) it follows that
∃−Var (CI [q(ṽ)],cI ) c′F = ∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm+1 [p(X̃)],cm ) c′F ) =
∃−Var (CI [q(ṽ)],cI ) (cm ∧ ∃−Var (Cm+1 [p(X̃)],cm ) c′′F ) = ∃−Var (CI [q(ṽ)],cI ) c′′F =
∃−Var (CI [q(ṽ)],cI ) cF .

(86)

¿From the definition of weight wt (CI [q(ṽ)], cI , c′F ) = wt (CI [q(ṽ)], cI , c′′F ) and since χ
is a split derivation we obtain wt (CI [q(ṽ)], cI , c′′F ) > wt (Cm+1 [H], cm , c′′F ). Then, from
(84) and (86) it follows that
wt (CI [q(ṽ)], cI , c′F ) > wt (Cm+1 [p(X̃)], cm , c′F )

(87)

and therefore, by construction,
ξ = hDi .CI [q(ṽ)], cI i → hDi .CI [C[p(X̃)] k tell(ṽ = r̃)], cI i →∗ hDi .Cm [p(X̃)], cm i →
hD0 .Cm+1 [p(X̃)], cm i →∗ hD0 .B′ , c′F i
is a derivation in Di ∪ D0 such that: (a) rule R2 is not used in the first m − 1 steps;
(b) rule R2 is used in the m-th step. The thesis then follows from (86), (85) and
(87) thus concluding the proof.
A.1

Proof of correctness for intermediate results and traces

In this subsection we show how the previous proofs can be adapted when considering
intermediate results and traces as observables. We first consider Theorem 5.1. Since
its proof is essentially the same of that one already given for the total correctness
theorem, here we provide only the intuition illustrating the (minor) modifications
needed.
Theorem 5.1 (Total Correctness 2). Let D0 , . . . , Dn be a transformation
sequence, and A be an agent.
—If there exists a derivation hD0 .A, ci →∗ hD0 .B, di then there exists a derivation
hDn .A, ci →∗ hDn .B′ , d′ i such that D |= ∃−Var(A,c) d′ → ∃−Var(A,c) d.
—Conversely, if there exists a derivation hDn .A, ci →∗ hDn .B, di then there exists a
derivation hD0 .A, ci →∗ hD0 .B′ , d′ i with D |= ∃−Var(A,c) d′ → ∃−Var(A,c) d.
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–26

·

Sandro Etalle et al.

Proof. The proof of this result is essentially the same as that one of the total
correctness Theorem 4.13 provided that in such a proof, as well as in the proofs of
the related preliminary results, we perform the following changes:
(1) Rather than considering terminating derivations, we consider any (possibly
non-maximal) finite derivation.
(2) Whenever in a proof we write that, given a derivation ξ, a derivation ξ ′ is
constructed which performs the same steps of ξ, possibly in a different order,
we now write that a derivation ξ ′′ is constructed which performs the same steps
as ξ (possibly in a different order) plus some other additional steps. Since the
store grows monotonically in ccp derivations, clearly if a constraint c is the
result of the derivation ξ, then a constraint c′′ is the result of ξ ′′ such that
D |= c′′ → c holds. For example, for case 2 in the proof of Proposition 4.5
(in the Appendix), when considering a (non-maximal) derivation ξ which uses
the declaration H ← C[tell(s̃ = t̃)] k B] we can always construct a derivation
ξ ′′ which performs all the steps of ξ (possibly plus others) and such that the
tell(s̃ = t̃) agent is evaluated before B. Differently from the previous proof, now
we are not ensured that the result of ξ is the same as that one of ξ ′′ , since ξ is
non-maximal (thus, ξ could also avoid the evaluation of tell(s̃ = t̃)). However,
we are ensured that the result of ξ ′′ is stronger (i.e. implies) that one of ξ.

We now consider the correctness results given for the restricted transformation
system with respect to the traces. Also in this case, the proofs follow the guidelines
of that one already presented in Section 4 and in the previous part of this Appendix.
We then sketch the proofs by showing which are the relevant new notions and
differences with respect to the previous ones.
In the remainder of this section we will always refer to the restricted transformation system and to a given restricted transformation sequence D0 , . . . , Dn .
We start with the following definition.
Definition A.10. Let D be a set of declarations and let ξ be the derivation
hD.A1 , c1 i →∗ hD.Am , cm i →∗ hD.An , cn i.
We define tr(ξ) =
∃−Var (A1 ,c1 ) (c1 ; c2 ; . . . ; cn ) = (c1 ; (∃−Var (A1 ,c1 ) c2 ); . . . ; (∃−Var (A1 ,c1 ) cn )).
The function mode (m(A, d)) is extended to consider also non-terminated derivations in the obvious way. We then extend the notion of weight, split derivation
and weight complete programs to the case of traces. Here and in the following the subscript t will denote a generic termination mode, that is, we assume
t ∈ {ss, dd, pp, ff}. We also say that a trace starts with c in case c is the first
constraint appearing in that trace.
Definition A.11 (Weight for traces). Given an agent A, a satisfiable constraint c and a trace s starting with c, we define the weight of the agent A w.r.t.
the trace s, notation wt (A, s), as follows:
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–27

wt (A, s) = min{n | n = wh(ξ) and ξ is a derivation hD0 .A, ci →∗ hD0 .B, di
such that ∃−Var (A,c) s  tr(ξ) and t = m(B, d)}.
Definition A.12 (Split derivation for traces). Let D0 , . . . , Di be a transformation sequence. We call a derivation in Di ∪ D0 a split derivation for traces if
it has the form
hDi .A1 , c1 i →∗ hDi .Am , cm i → hD0 .Am+1 , cm+1 i →∗ hD0 .An , cn i
where m ∈ [1, n] and the following conditions hold:
(a) the first m − 1 derivation steps do not use rule R2;
(b) the m-th derivation step hDi .Am , cm i → hD0 .Am+1 , cm+1 i uses rule R2;
(c) wt (A1 , (c1 ; c2 ; . . . ; cn )) > wt (Am+1 , (cm+1 ; . . . ; cn )), where t = m(An , cn ).
Definition A.13. We call the program Di weight complete for traces iff, for any
agent A and any satisfiable constraint c the following hold: If there exists a derivation
χ = hD0 .A, ci →∗ hD0 .B, di
such that m(B, d) ∈ {ss, dd, pp, ff} then there exists a split derivation in Di ∪ D0
ξ = hDi .A, ci →∗ hD0 .B′ , d′ i
where tr(χ)  tr(ξ) and m(B′ , d′ ) = m(B, d).
Proposition 4.9 holds also when considering as observables Ot rather than O and
its proof is essentially the same, thus we omit it.
The following Lemma is obtained from Lemma A.1 by considering the weakest produced constraint wpc rather than the produced constraint. The proof is
analogous to that one given for Lemma A.1 and hence it is omitted.
Lemma A.14. Assume that there exists a derivation hD.C[A], ci →∗ hD.C′ [A], c′ i
where c is a satisfiable constraint and the context C′ [ ] has the form
A1 k . . . k C̄[ ] k . . . k An .
′

Then D |= (wpc(C̄[ ]) ∧ c ) → wpc(C[ ]) holds and in case C̄[ ] is the empty context
also D |= c′ → wpc(C[ ]) holds.
In the following we extend to set of observables the (pre-order) relation  in the
expected way: Given two sets of observables Ot (Di .A) and Ot (Dj .A), we say that
Ot (Di .A)  Ot (Dj .A) iff, for any hs, xi ∈ Ot (Di .A), (with x ∈ {ss, dd, pp, ff}), there
exists hs′ , xi ∈ Ot (Dj .A) such that s  s′ . We denote by ≡ the equivalence relation
induced by  on sets of observables, that is, Ot (Di .A) ≡ Ot (Dj .A) iff Ot (Di .A) 
Ot (Dj .A) and Ot (Dj .A)  Ot (Di .A).
The following is analogous of Proposition 4.5 for traces.
Proposition A.15 (Partial Correctness for traces). If, for each agent
A, Ot (D0 .A) ≡ Ot (Di .A) then, for each agent A, Ot (Di+1 .A)  Ot (Di .A).
Proof. We have to show that, given an agent A and a satisfiable constraint cI ,
if there exists a derivation ξ = hDi+1 .A, cI i →∗ hDi+1 .B, cF i, then there exists also
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–28

·

Sandro Etalle et al.

a derivation ξ ′ = hDi .A, cI i →∗ hDi .B′ , c′F i such that tr(ξ)  tr(ξ ′ ) and m(B′ , c′F ) =
m(B, cF ).
The proof is analogous to that one given for Proposition 4.5, therefore we illustrate only the modifications needed to adapt such a proof.
Assume that the first step of derivation ξ uses rule R4 and let d′ ∈ Di+1 be the
declaration used in the first step of ξ. Assume also that d′ 6∈ Di and that d′ is
the result of the transformation operation applied to obtain Di+1 . As usual, we
distinguish various cases according to the kind of operation performed. Here we
consider only those cases whose proof is different from that one of Proposition 4.5,
due to the fact that here we consider traces (consisting of intermediate results)
rather than the final constraints.
Case 2. In this case d : H ← C[tell(s̃ = t̃) k B] ∈ Di , d′ : H ← C[Bσ] ∈ Di+1 , where
σ is a relevant most general unifier of s̃ and t̃ (or a renaming, in case of s̃ and t̃
consist of distinct variables). From the definition of the operation we know that the
variables in the domain of σ do not occur neither in C[ ] nor in H and, differently
from the case of Proposition 4.5, that Var(B) ∩ Var(H, C) = ∅.
For any derivation which uses a declaration H ← C[tell(s̃ = t̃) k B], if the agent
tell(s̃ = t̃) is evaluated before B then the proof is analogous to that one given for
Case 2 of Proposition 4.5. Otherwise, if the agent tell(s̃ = t̃) is not evaluated before
B, then by using the condition Var(B) ∩ Var(H, C) = ∅ we obtain that the evaluation
of the agent B can add to the store only constraints on variables which do not occur
neither in the global store (before the evaluation of B) nor in Var (A, cI ). Therefore
the contribution to the global store of the agent B (before the evaluation of the
agent tell(s̃ = t̃)) when restricted to Var (A, cI ) is equivalent either to the constraint
true or to the constraint false.
In the first case the global store is the same as that one existing before the
evaluation of B. In the second case we can obtain the constraint false by evaluating
the same agents evaluated in B also in Bσ.
Case 3. In this case the proof is analogous to that one given for Case 3 of Proposition 4.5 by observing the following: If in the derivation χ in Di either the agent
tell(b) or the agent tell(t̃ = s̃) are evaluated, then in the derivation χ′ the agent p(t̃)
can be evaluated and then one performs exactly the same steps of χ, except for the
evaluation of a renamed version of the agents tell(b) and tell(t̃ = s̃).
Cases 4. For the ask simplification the proof of Case 4 of Proposition 4.5 is
simplified by using Lemma A.14 and by observing that, for any derivation, when
the choice agent inside C[ ] is evaluated the current store certainly implies wpc(C[ ]).
Therefore we do not need to construct the new derivation χ′ . The same holds for
the tell simplification.
Case 7. In this case the proof is analogous to that given for the previous Case 2,
by observing that in the derivation
β = hD0 .CI [C[H′ k tell(X̃ = X̃′ )] k tell(ṽ = r̃)], cI i →∗ hD0 .B′0 , c0 i,
Var (H′ ) ∩ Var(CI , C, cI , X̃, ṽ,r̃) = ∅. Therefore we can construct a derivation
χ0 = hD0 .CI [C[H k tell(X̃′ = X̃)] k tell(ṽ = r̃)], cI i →∗ hD0 .B′′0 , c′0 i
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–29

where tr(β)  tr(χ0 ) and m(B′′0 , c′0 ) = m(B′0 , c0 ). Moreover, we can drop the constraint tell(X̃′ = X̃), since the declarations used in the derivation are renamed apart
and, by construction, Var (CI [C[H] k tell(r̃ = ṽ)], cI ) ∩ Var (X̃′ ) = ∅. We then obtain
that there exists a derivation β ′ = hD0 .CI [C[H] k tell(ṽ = r̃)], cI i →∗ hD0 .B̄0 , c̄0 i
which performs exactly the same steps of χ0 except for (possibly) the evaluation of tell(X̃′ = X̃) and such that ∃−Var (C [C[H] k tell(ṽ=r̃)],c ) tr(χ0 )  tr(β ′ ) and
I

I

m(B̄0 , c̄0 ) = m(B′′0 , c′0 ). Now, the proof is the same to that given for Case 7 of
Proposition 4.5, since the evaluation of tell(X̃′ = X̃) does not modify the current
store with respect to the variables not in Var (X̃′ ).

The following Lemmata are the counterpart of previous Lemma A.3 and Lemma A.4,
when considering the observable Ot (Di .A).
Lemma A.16. Let q(r̃) ← H ∈ D0 and let C[ ] be context. For any satisfiable
constraint c and for any trace s starting with c, such that Var (C[q(t̃)], c)∩Var (r̃) = ∅
and wt (C[q(t̃)], s) is defined, there exists a trace s′ such that wt (C[q(r̃) k tell(t̃ =
r̃)], s′ ) ≤ wt (C[q(t̃)], s) and ∃−Var (C[q(t̃)],c) s  ∃−Var (C[q(t̃)],c) s′ .
Proof. Immediate.
Lemma A.17. Let q(r̃) ← H ∈ D0 . For any context CI [ ], any satisfiable constraint c and for any sequence s starting in c, the following holds:
(1 ) If Var (H) ∩ Var (CI , c) ⊆ Var (r̃) and wt (CI [q(r̃)], s) is defined, then there exists
a sequence s′ , such that Var(s′ ) ⊆ Var (CI [H], c), wt (CI [H], s′ ) ≤ wt (CI [q(r̃)], s)
and ∃−Var (CI [q(r̃)],c) s  ∃−Var (CI [q(r̃)],c) s′ .
(2 ) If Var (H)∩Var (CI , c) ⊆ Var (r̃), Var (s)∩Var (r̃) ⊆ Var (CI [H], c) and wt (CI [H], s)
is defined, then there exists a sequence s′ , such that wt (CI [q(r̃)], s′ ) ≤ wt (CI [H], s)
and ∃−Var (CI [q(r̃)],c) s  ∃−Var (CI [q(r̃)],c) s′ .
Proof. Immediate.
Analogously to the case of the previous results, the following Lemma is crucial
in the proof of completeness for traces.
Lemma A.18. Let 0 ≤ i ≤ n, cl : q(r̃) ← H be a declaration in Di and let
cl′ : q(r̃) ← H′ be the corresponding declaration in Di+1 (in case i < n). For any
context CI [ ], any satisfiable constraint c and for any sequence s starting in c the
following holds:
(1 ) If Var (H) ∩ Var (CI , c) ⊆ Var (r̃) and wt (CI [q(r̃)], s) is defined, then there exists
a sequence s′ , such that Var(s′ ) ⊆ Var (CI [H], c), wt (CI [H], s′ ) ≤ wt (CI [q(r̃)], s)
and ∃−Var (CI [q(r̃)],c) s  ∃−Var (CI [q(r̃)],c) s′ ;
(2 ) If Var(H, H′ ) ∩ Var (CI , c) ⊆ Var(r̃), Var(c′ ) ∩ Var (r̃) ⊆ Var (CI [H], c) and
wt (CI [H], s) is defined, then there exists a sequence s′ , such that Var (s′ ) ⊆
Var(CI [H′ ], c), wt (CI [H′ ], s′ ) ≤ wt (CI [H], s) and ∃−Var (CI [q(r̃)],c) s  ∃−Var (CI [q(r̃)],c) s′ .
Proof. The proof is analogous to that given for Lemma A.5, by using Lemma A.17
and A.16 instead of Lemma A.4 and A.3, respectively. We have only to observe the
following facts:
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

App–30

·

Sandro Etalle et al.

For Case 3, Point (1) we can evaluate the agent tell(b) after the global store
implies ∃−Var (s̃) b. In this way the new derivation has the same sequence of intermediate results.
For Case 6, Point (2), by using Lemma A.14, if there exists a derivation
Pn
Pn
ξ = hD0 .CI [C[H k j=1 ask(cj ) → Bj ]], ci →∗ hD0 .Cm [H k j=1 ask(cj ) → Bj ], dm i →
P
n
hD0 .Cm [H′ k j=1 ask(cj ) → Bj ], dm+1 i →∗ hD0 .B, di,
then D |= dm → e(= wpc(C[ ])). If hD0 .H, dm i is not productive then the proof is
straightforward. Otherwise, assume that hD0 .H, dm i is productive. By definition of
distribution there exists at least one j ∈ [1, n] such that D |= dm → cj and, for each
j ∈ [1, n], either D |= dmP
→ cj or D |= dm → ¬cj . Then, by definition, there exists a
derivation ξ1 = hD0 .Cm [ nj=1 ask(cj ) → (H k Bj )], dm i →∗ hD0 .B, di which performs
the same
Pn steps of χ1 in the same order, except for one step of evaluation of the
agent j=1 ask(cj ) → Bj which is performed before evaluating the agent H. Then
the thesis follows by definition of the relation .
Also the proof of the following Lemma is analogous to that of its previous counterpart (Lemma A.6) and hence it is omitted.
Lemma A.19. Let 0 ≤ i ≤ n, c1 be a satisfiable constraint and assume that there
exists a derivation ξ : hDi .A1 , c1 i →∗ hDi .Am , cm i →∗ hDi .Ak , ck i, such that cm is
satisfiable. If
. i) in the first m − 1 steps of ξ rule R2 is used only for evaluating agents of the
form ask(c) → B,
. ii) wt (A1 , tr(ξ)) is defined (for t = m(Ak , ck ) ∈ {ss, dd, pp, ff}).
then there exists a sequence s′ starting in cm , such that Var (s′ ) ⊆ Var(Am , cm ),
∃−Var (A1 ,c1 ) (cm ; . . . ; ck )  ∃−Var (A1 ,c1 ) s′ and wt (Am , s′ ) ≤ wt (A1 , tr(ξ)).
Finally we have the following.
Theorem 5.12 (Strong Total Correctness). Let D0 , . . . , Dn be a restricted
transformation sequence, and A be an agent.
—If hs, xi ∈ Ot (D0 .A) (with x ∈ {ss, dd, pp, ff}) then there exists hs′ , xi ∈ Ot (Dn .A)
such that s  s′ .
—Conversely, if hs, xi ∈ Ot (Dn .A) then there exists hs′ , xi ∈ Ot (D0 .A) such that
s  s′ .
Proof. The proof is analogous to that given for Theorem 4.13 and proceeds by
showing simultaneously, by induction on i, that for i ∈ [0, n] and for any agent A:
(1) Ot (D0 .A) ≡ Ot (Di .A);
(2) Di is weight complete for the traces.
The proof of the base case is analogous to that given for the base case of Theorem 4.13 and hence it is omitted. For the induction step we have that, by induction hypothesis, for any agent A, Ot (D0 .A) ≡ Ot (Di−1 .A) and Di−1 is weight
complete for the traces. Proposition 4.9 holds also when considering Ot rather
than O. From Proposition A.15 and (the counterpart for traces of) Proposition 4.9
ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

Transformations of CCP programs

·

App–31

then it follows that if Di is weight complete for traces then, for any agent A,
Ot (D0 .A) = Ot (Di .A). So, in order to prove parts 1 and 2, we have only to show
that, for any derivation β = hD0 .A, cI i →∗ hD0 .B, cF i such that cI is a satisfiable
constraint and m(B, cF ) ∈ {ss, dd, pp, ff}, there exists a split derivation in Di ∪ D0 ,
ξ = hDi .A, cI i →∗ hD0 .B′ , c′F i, such that tr(β)  tr(ξ) and m(B′ , c′F ) = m(B, cF ).
¿From the inductive hypothesis it follows that there exists a split derivation
χ = hDi−1 .A, cI i →∗ hD0 .B′′ , c′′F i
where tr(β)  tr(χ) and m(B′′ , c′′F ) = m(B, cF ). Now, let d ∈ Di−1 \Di be the modified
clause in the transformation step from Di−1 to Di . The rest of the proof is essentially
analogous to that given for Theorem 4.13. The only points which require some case
are the following:
Case 2. In this case, the proof is analogous to that given for Case 2 of Proposition A.15.
Case 3. In this case the proof is analogous to that given for Case 3 of Proposition A.15, provided we observe the following fact for case 2a) in such a proof:
Given any set of declarations, if there exists a derivation χ′ for the configuration
hC′ [tell(b̄) k B̄ k tell(t̃ = s̃′ )], c′ i where c′ is satisfiable and Var(C′ [tell(b̄) k B̄ k tell(t̃ =
s̃′ )], c′ ) ∩ Var(b, s̃) = ∅, then there exists a derivation for hC′ [tell(b̄) k B̄ k tell(t̃ =
s̃′ ) k tell(b) k tell(t̃ = s̃)], c′ i which performs the same steps of χ′ plus (possibly) two
steps corresponding to the evaluation of tell(t̃ = s̃) and tell(b), after the evaluation
of tell(b̄) and tell(t̃ = s̃′ ).
Case 4. Analogously to the proof of Case 4 of Proposition A.15, it is sufficient to
observe the following. From Lemma A.14 it follows that, for any derivation, when
the choice agent inside a context C[ ] is evaluated the current store implies wpc(C[ ]).
Then, by definition of ask simplification, the constraint cj and c′j are equivalent with
respect to the current store (and therefore we do not need to construct the new
derivation χ′ ). The same reasoning applies to the case of tell simplification.
Case 6. The proof is analogous to that of Case 6 of Lemma A.18.

ACM Transactions on Programming Languages and Systems, Vol. TBD, No. TDB, Month Year.

