{'fraction_non_alphanumeric': 0.05083662342545591, 'fraction_numerical': 0.009956758789246099, 'mean_word_length': 4.105036855036855, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 8, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 51, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Transformations of CCP programs

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 wrt a class of queries. To this aim it is sometimes sufficient to apply our transformations and to specialize the resulting program wrt the given queries in such a way that the obtained program is trivially deadlock free.


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

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.
In the sequel, constraints will be considered up to equivalence in the domain D, i.e. we write c 1 = c 2 in case D |= c 1 ↔ c 2 . Terms will be denoted by t, s, . . ., variables with X, Y, Z, . . ., further, as a notational convention,t andX 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 inX 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(σ), is the finite set of variables {X | Xσ = 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 operator allows one to express parallel composition of two agents and it is usually described in terms of interleaving, while non-determinism arises by introducing a (global) choice operator n i=1 ask(c i ) → A i : the agent n i=1 ask(c i ) → A i nondeterministically selects one ask(c i ) which is enabled in the current store, and then behaves like A i . Thus, the syntax of CCP declarations and agents is given by the following grammar: Proc ::= D.A where c and c i '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) tell(X =t), while the declaration p(t) ← A is equivalent to p(X) ← A 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 is a set of declarations. In the following examples we assume that the operator binds tighter than (so, ask(a) → A ask(b) → B + ask(d) → C means (ask(c) → A) (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 int, 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  of declarations and we denote by defn D (p) the set of variants 2 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 considered 3 . 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 constructs. A finite derivation (or computation) containing only satisfiable constraints is called successful if it is of the form D.A, c → * D.Stop, d → while it is called deadlocked if it is of the form D.A, c → * D.B, d → 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.

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) bidder b(LeftBids,RightBids) 2 A variant of a declaration d is obtained by replacing the tupleX of all the variables appearing in d for another tupleỸ. 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. 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 = 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.

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, whereX 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 D 0 the program obtained after the introduction of new definitions.
In the case of program AUCTION, we assume that the following new declarations are added to the original program.
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.

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.  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).
Notice that, in particular, we can always exchange C[tell(true) 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.

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 be two definitions of D. The backward instantiation of p(t) in d consists in replacing d by d ′ , which is either (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) 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 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).

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.
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: = 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: 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, andZ be a set of variables. We say that c is equivalent to This definition is employed in the following operation, which allows us to simplify the constraints in the ask and tell guards.

Transformations of CCP programs · 11
Definition 3.6 (Ask and Tell Simplification). Let D be a set of declarations.
(1) Let d : We call this an ask simplification operation.

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 be a declaration of D. Assume that n > 1 and that for some j ∈ [1, n], we have that c j = false, then we can replace d with 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) 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 = quit) bidder a(Bs, As) We can transform d into the declaration 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) , 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:

Distribution
A crucial operation in our transformation system is the distribution, which consists of bringing an agent inside a choice as follows: from the agent A i ask(c i ) → B i , we want to obtain the agent i ask(c i ) → (A B i ). 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.
In this program, the process D.p(Y) originates the derivation D.p(Y), true → * D.Stop, Y = 0 . Now, if we blindly apply the distribution operation to the first definition we would change D into: and now we have that D.p(Y), true 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 D.
Definition 3.9 (Productive). Given a process D.A and a satisfiable constraint c, we say that D.A, c is productive iff either it has no (finite) maximal derivations or there exists a derivation D.
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 provided that for every constraint c such that Var (c) ∩ Var(d) ⊆ Var (H, C), if D.A, c ∧ e is productive then both the following conditions hold: Intuitively, the constraint c models the possible ways of "calling" A n i=1 ask(c i ) → B i . Condition (b) basically requires that if the store c is such that A might produce some output (that is, the configuration D.A, c ∧ e 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) ask(false) → stop, which would clearly be wrong. If D.A, c ∧ e is not productive then we do not impose any condition, since the evaluation of D.A, c ∧ e 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 ], 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 ].
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, D.A, c 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 D.A, c ∧ e 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 = quit) make new bid b(LastBid,MyBid) ask(MyBid = quit) → tell(Bs = [quit|Bs']) broadcast("b quits") bidder a(Bs, As) + ask(MyBid = quit) → (tell(Bs = [MyBid|Bs']) tell(MyBid = quit) bidder a(Bs, As) 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:

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 D 0 , . . . , D n , in which D 0 is an initial program and each D i+1 is obtained from D i 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 D 0 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 So, for example, ask(c) → (A [ ]) is a guarding context, while (ask(c) → A) [ ] is not. We can finally give the definition of folding: (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 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 = quit) make new bid b(LastBid,MyBid) ask(MyBid = quit) → broadcast("b quits") + ask(MyBid = quit) → auction left (MyBid) Now, by performing an identical optimization on auction left, we can also obtain: auction left(LastBid) ← tell(LastBid = quit) make new bid a(LastBid,MyBid) ask(MyBid = quit) → broadcast("a quits") + ask(MyBid = 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 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 by using the definition In the first place, via a tell introduction, we can modify definition d as follows Clearly, we assume here thatX and σ fulfill the applicability conditions given in Definition 3.2. Then, via a normal folding operation we obtain (provided that the applicability conditions for the folding are satisfied) which is equivalent to the definition 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.

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. 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 D 0 , . . . , D n is partially correct iff, for each agent A, we have that holds, that is, nothing is added to the semantics of the initial program. Dually, we say that D 0 , . . . , D n is complete iff, for each agent A, we have that 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 the transformation history (while allowing the introduction of recursion), and that the folding definitions are allowed to be recursive (the distinction between P new and P old of [Tamaki and Sato 1984] is now superfluous).
We start with the following proposition allows us to eliminate stop agents in programs. The following notion of mode will be useful to shorten the notation.
Note that the notion of mode does not depend on the set of declarations D i we are considering, that is, in the above definition we could equivalently use D i rather than D 0 . This is the content of the following. Proof. Immediate by observing that a procedure call can be evaluated in D 0 iff it can be evaluated in D i , for any i ∈ [1, n].
In what follows, we are going to refer to a fixed transformation sequence D 0 , . . . , D n . We start with the following result, concerning partial correctness. Proof. (Sketch). We show that given an agent A and a satisfiable constraint 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 ξ = D i+1 .A, c I . By the definition D i .A, c 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 ′ ∈ D i+1 be the declaration used in the first step of ξ. If d ′ was not modified in the transformation step from D i to D i+1 (that is, d ′ ∈ D i ), then the result follows from the inductive hypothesis. We assume then that d ′ ∈ D i , d ′ is then the result of the transformation operation applied to obtain D i+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) 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 ofs andt), there exists a derivation step  By the inductive hypothesis, there exists a derivation Since Since by hypothesis for any agent (3) Let f ′ : p(X ′ ) ← H ′ be an appropriate renaming of f, which renames only the variables inX, such that Var(d) ∩ Var(f ′ ) = ∅ (note that this is possible, since · 21 Var (H) ∩ (Var (r) ∪ Var (C)) ⊆ Var (X)). By hypothesis, Var (C I [q(ṽ)], c I ) ∩ Var (H) = ∅. Then, without loss of generality we can assume that Var(ξ 0 ) ∩ Var (f ′ ) = ∅ if and only if the procedure call p(X) is evaluated, in which case declaration f ′ is used. Thus there exists a derivation We now show that we can substitute H for H ′ tell(X =X ′ ) in the previous derivation. Since f ′ : p(X ′ ) ← H ′ is a renaming of f : p(X) ← H, the equalityX =X ′ is conjunction of equations involving only distinct variables. Then, by replacing the variablesX withX ′ and vice versa in the previous derivation we obtain the derivation Then, from (3) and since Var ( Since O(D 0 .A ′ ) = O(D i .A ′ ) holds by hypothesis for any agent A ′ , there exists a derivation Finally, since d : and then the thesis follows from (8).
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 w ss (A, c, d) of the agent A w.r.t. the constraints c and d as follows Analogously, we define the deadlock weight w dd (A, c, d) of the agent A w.r.t. the constraints c and d is undefined in case there is no successful derivation corresponding to the given constraints (and analogously for w dd and w ff ). Also, both w ss (A, c, false) and w dd (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 D i while the second one is carried out in D 0 .
Definition 4.7 (Split derivation). Let D 0 , . . . , D i be a transformation sequence. We call a derivation in D i ∪ D 0 a successful split derivation if it has the form where c n 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; A deadlocked split derivation is defined analogously, by replacing w ss for w dd and Stop for a generic agent B = Stop in the last configuration of the derivation above.
Finally a failed split derivation is defined by replacing w ss for w ff and Stop for a generic agent (which is not necessarily terminated) and by assuming that c n = 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 D i 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 So D i is weight complete if we can reconstruct the semantics of D 0 by using only (successful, deadlocked and failed) split derivations in D i ∪ D 0 . We now show that if D i is weight complete then no observables are lost during the transformation (i.e., the transformation is complete). This is the content of the following.
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 D 0 .A, c → * D 0 .Stop, d . We show, by induction on the success weight of (A, c, d), that there exists a derivation Base Case. If w ss (A, c, d) = 0 then, since D i is weight complete, from Definition 4.7 and Definition 4.8 it follows that there exists a (successful) split derivation in is not used in ξ then the proof is the same as in the previous case. Otherwise ξ has the form By the inductive hypothesis, there exists a derivation Without loss of generality, we can assume that Var (ξ ′ ) ∩ Var (ξ ′′ ) = Var (A m+1 , c m+1 ) and hence there exists a derivation Finally, by our hypothesis on the variables and by construction, Before proving the total correctness result we need some technical lemmata. Here and in the following we use the notation w t (with t ∈ {ss, dd, ff}) as a shorthand for indicating the success weight w ss , the deadlock weight w dd and the failure weight w ff .

ff} and let C[ ] be a context. For any satisfiable constraint c and for any constraint
Proof. Immediate.
Lemma 4.11. Let q(r) ← H ∈ D 0 and t ∈ {ss, dd, ff}. For any context C I [ ], any satisfiable constraint c and for any constraint c ′ , the following holds.
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 ∈ D i , and let cl ′ : q(r) ← H ′ be the corresponding declaration in D i+1 (in the case i < n). For any context C I [ ] and any satisfiable constraint c and for any constraint c ′ the following holds: 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 D i to D i+1 then the result is obvious by choosing d ′ = ∃ −Var (C I [H],c) c ′ . Assume then that cl is affected when transforming D i to D i+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 ′ ∈ D i+1 was obtained from D i by unfolding. In this case, the situation is the following: where cl and u are assumed to be renamed so that they do not share variables. and By the hypothesis on the variables and since u is renamed apart from cl, Then, by Point 1, there exists a constraint d ′ , such that Furthermore, by hypothesis and construction, and, without loss of generality, we can assume that Then, by (10) and since Var ( ,c) c ′ and this completes the proof. and hold. Moreover, we can assume without loss of generality that (11) and Point 2 of Lemma 4.11 it follows that there exists a We can assume, without loss of generality, that , c). Then by using (12) and (13) we obtain that 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 ∈ D i+1 , and letcl : q(r) ←H be the corresponding declaration in D i . Moreover let C I [ ] be a context, c a satisfiable constraint and let c ′ be a constraint, such that Var(H) ∩ Var (C I , c) ⊆ Var (r) and w t (C I [q(r)], c, c ′ ) is defined. Without loss of generality, we can assume that Var (H)∩Var (C I , c) ⊆ Var(r). Then, since by inductive hypothesis, part 1 holds for i, there exists a constraint d 1 such that Since by inductive hypothesis part 2 holds for i, there exists a constraint d ′ , such that ,c) c ′ and then the thesis follows.
We finally obtain our first main theorem. Proof. (Sketch). The proof proceeds by showing simultaneously, by induction on i, that for i ∈ [0, n]: Base case. We just need to prove that D 0 is weight complete. Assume that there exists a derivation D 0 .A, c I → * D 0 .B, c F , where c I is a satisfiable constraint and

Transformations of CCP programs
It follows from Definition 4.7 that ξ is a split derivation.

Induction step.
By the inductive hypothesis for any agent A, O(D 0 .A) = O(D i−1 .A) and D i−1 is weight complete. From propositions 4.5 and 4.9 it follows that if D i is weight complete then for any agent . So, in order to prove parts 1 and 2, we only have to show that D i is weight complete.
Assume then that there exists a derivation D 0 .A, c I → * D 0 .B, c F such that c I is a satisfiable constraint and m(B, c F ) ∈ {ss, dd, ff}. From the inductive hypothesis it follows that there exists a split derivation Let d ∈ D i−1 \D i be the modified clause in the transformation step from D i−1 to D i . If in the first m steps of χ there is no procedure call which uses d then clearly there exists a split derivation ξ in 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 D i−1 to D i . 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 D i . The situation is the following: where d and u are assumed to be renamed apart. By the definition of split derivation, χ has the form F . Without loss of generality, we can assume that Var (χ) ∩ Var(u) = ∅ 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

Then there exists a corresponding derivation in
, 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 The hypothesis on the variables implies that Then, by the definition of transformation sequence and since u ∈ D i−1 , there exists a declaration p(s) ← H 0 ∈ D 0 . By Lemma 4.10 and part 1 of Lemma 4.12 it follows that there exists a constraint d F such that and Therefore, by the definition of w t , by (17) and (16), By (18) holds and, by definition of weight, we obtain Moreover, we can assume without loss of generality that Then, by the definition of procedure call and there exists a derivation 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 (22) and by construction) (22) and by construction) (21) and (17), (19), implies the thesis.

Folding: Assume that d is folded and let
appears in the scope of an ask guard. By definition of split derivation χ has the form is a guarding context. Without loss of generality we can assume that Var (χ) ∩ Var (X) ⊆ Var(H). Then, from the definition of D i it follows that there exists a derivation which performs exactly the first m steps as χ.
The definitions of derivation and folding imply that 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 ¿From the definition of weight and the fact that , c m , d ′ ) and therefore, by (24) and (25), hold. Moreover, from (23) we obtain Without loss of generality, we can now assume that . Then, by (26), (27) and (15) it follows that ¿From the definition of weight and therefore, by construction, 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 D 0 and the final one D n 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 D n "produces the same results" as D 0 . 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 D n .A does never deadlock, then we are also sure that D 0 .A does not deadlock either.

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 failure 6 . 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.

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: (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 O i (D.A). In fact, the ask simplification allows one to transform the agent 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.
into the agent 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 = d). Analogously, assuming that D |= d → c and D |= d → c ′ , the tell simplification allows one to transform into the agent 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 D 0 , . . . , D n be a transformation sequence, and A be an agent.
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 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 ξ.

· 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 where the subscript ic stands for implication closure (of intermediate results). We then have following Corollary whose proof is immediate.
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.

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: 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, andZ be a set of variables. We say that c is weakly equivalent to 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. ( 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 A, c ∧ e is productive then both the following conditions hold: 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.

· 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 can be transformed via a tell elimination into 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 can be transformed via a restricted tell elimination into where σ is a relevant most general unifier ofs andt, 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 whens andt are sequence of distinct variables, in which case σ is simply a renaming. On the other hand, the declaration can be transformed via a restricted tell introduction into provided that σ is a substitution such thatX = 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 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 thatt is an instance ofs.
We can finally define the restricted transformation system as follows.
Definition 5.9. A restricted transformation sequence is a sequence of programs D 0 , . . . , D n in which D 0 is a initial program and each D i+1 is obtained from D i via one of the following operations: unfolding, backward instantiation, restricted 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 c 1 ; c 2 ; . . . ; c n a sequence of constraints, also called trace.
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 c 1 ; c 2 ; . . . ; c n appearing in the observables, we have that D |= c i → c j 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 c 1 ; c 2 ; . . . ; c n is simulated by a trace d 1 ; d 2 ; . . . ; d m , notation c 1 ; c 2 ; . . . ; c n d 1 ; d 2 ; . . . ; d m , iff there exists {j 1 , . . . j n } ⊆ {1, 2, . . . , m} such that (1) c i = d ji for each i ∈ [1, n]; (2) j 1 = 1, j n = m and j i ≤ j k iff i < k. 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 D 0 , . . . , D n be a restricted transformation sequence, and A be an agent.
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 D 0 : p(Y) ← tell(X = f(a,W)) tell(X = f(Z,b)) tell(X = Y). Its trace semantics O t (D 0 .p(Y)) contains t, ss , 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 D 1 : p(Y) ← tell(Y = f(a,W)) tell(Y = f(Z,b)). Now, O t (D 1 .p(Y)) does not contain t: one cannot obtain Y = f(a, b) from true in one step. On the other hand, O t (D 1 .p(Y)) contains (true; ∃ W Y = f(a, W); Y = f(a, b)), ss and (true; ∃ Z Y = f(Z, b); Y = f(a, b)), ss 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 D 0 , . . . , D n be a restricted transformation sequence, and A be an agent.

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 |s i | the length of a trace s i and we say that a configuration D.A, c 1 produces the trace c 1 ; c 2 ; . . . ; c n iff there exists a derivation D.A, d 1 → D.A 2 , d 2 → . . . → D.A n , d n such that c 1 = d 1 and c j = ∃ −Var (A,c1) d j 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 c 1 ; c 2 . . . "active" iff, for any i ≥ 1, there exists j > i such that D |= ¬(c i → c j ) (on the other hand, the implication D |= (c j → c i ) 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 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 s i are traces and c i are constraints, for i ∈ [1, n], then c 1 ; s 1 ; c 2 ; s 2 . . . ; s n−1 ; c n denotes the trace obtained by concatenating the s i e c i in the obvious way.
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 m j the maximal element appearing in the set ({|s 1,j |, |s 2,j |, |s 3,j |, . . .}, for each j ≥ 1, that is, m j is the maximal length of the sub-traces s i,j for a fixed j and i = 1, 2, . . .. We now construct a tree T representing the (infinitely many) finite traces c 0 c 0 ; s 1,1 ; c 1 c 0 ; s 2,1 ; c 1 ; s 2,2 ; c 2 c 0 ; s 3,1 ; c 1 ; s 3,2 ; c 2 ; s 3,3 ; c 3 . . . produced by D.A, c 0 . The nodes of the tree T are labeled by configurations of the form D.B, c i , for some i, and the edges are labeled by the sub-traces s i,j . More precisely, the tree T is defined inductively as follows: (Base step). The root (level 0) of T is labeled by D.A, c 0 . For each derivation of the form D.A, c 0 → * D.A i,1 , c 1 which performs at most m 1 + 1 transition steps and which produces the trace c 0 ; s i,1 we add a son N of the root (at level 1) labeled by D.A i,1 , c 1 and an edge, labeled by s i,1 , connecting the root and N .
(Inductive step). Assume that T has depth n − 1 and let D.A i,n−1 , c n−1 be a configuration labeling a node N at level n − 1. For each derivation of the form D.A i,n−1 , c n−1 → * D.A i,n , c n which performs at most m n + 1 transition steps · 39 we add a son N ′ of N labeled by D.A i,n , c n and we add an edge labeled by s i,n , connecting N and N ′ .
Note that the number of the configurations D.A i,n , c n obtained in this way is finite, since we allow at most m n + 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 c i 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 D.A, c 0 produces the infinite trace c 0 ; s 1 ; c 1 ; s 2 ; c 2 . . . s n ; c n ; . . . where, for each j ≥ 1, s j = s i,j for some i ≥ 1.
We also need the following Lemma. 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. where, in order to simplify the notation, we assume that the c i are different constraints while the s i are sequences of constraints all equal to c i−1 (so the s i are sequences of stuttering steps). Clearly, by definition of produced sequence, D 0 .A, c 0 produces also the (infinitely many) finite prefixes of t c 0 c 0 ; s 1 ; c 1 c 0 ; s 1 ; c 1 ; s 2 ; c 2 c 0 ; s 1 ; c 1 ; s 2 ; c 2 ; s 3 ; c 3 . . .

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 D.A, c 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 D 0 , . . . , D n be a transformation sequence, and assume that D n .A, c has an infinite (non active) 7 trace. This implies that there exists a derivation ξ = 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:: 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: ¿From the definition of folding we have that C[ ] is a guarding context and Var(A ′ ) ∩ Var(C,X) ⊆Ỹ (f and d are suitably renamed so that the variables they have in common are only those occurring in A ′ ). Since C is a guarding context let us assume that 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(Ỹ)σ i , where, for each i ≥ 1, σ i is a renaming and the current the store d i entails c ′ 1 σ i . Moreover, assume that A is of the form C 0 [p(ṽ)]. 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 D 0 is 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 D 0 .C 0 [p(Ṽ)], c where, from a certain point of the derivation j, the current store d 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.

MORE EXAMPLES
The following example is inspired by the one in ]. 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: 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. We can now fold collect(Ys) deliver(Ys), using the original definition collect deliver ← collect(Xs) deliver(Xs). We obtain. 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.
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:  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 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. 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 operation 8 and bring them inside the ask constructs. The result is the following program.  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: 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 definition 11 :

handle one(X, Channel) ← reader(Channel,Xs) onestream([X|Xs])
After the transformation, we end up with the definition: handle one(X, Channel) ← ask(char(X)) → ( ask(X=eof) → stop + ask(X =eof) → write(X) read(Channel,X') 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 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: We can now fold handle two in it (via an extended folding operation), obtaining: streamer ← read(left,L) read(right,R) 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 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 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. We now apply the (restricted) distribution operation; in practice, we now bring one choice inside the other one.
len(Ys',Limit,L') 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 ]. 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. We can now apply the folding operation.

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). 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).
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 P new and P old . 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 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.

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 O i 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 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 D 0 , . . . , D n . We prove now Proposition 4.5.

Proposition 4.5 (Partial Correctness). If, for each agent
Proof. We now show that given an agent A and a satisfiable constraint 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.
. 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 ξ = D i+1 .A, c I . By the definition D i .A, c 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 ξ = D i+1 .A, c I → D i+1 .A 1 , c 1 → * D i+1 .B, c F then by the inductive hypothesis, there exists a derivation We can assume, without loss of generality, that Var(A, c I ) ∩ Var (ξ ′′ ) ⊆ Var (A 1 , c 1 ). Therefore, there exists a derivation ξ ′ = D i .A, c I → * D i .B ′ , c ′ F . Now, to prove the thesis it is sufficient to observe that, by the hypothesis on the variables, . Now, assume that the first step of derivation ξ uses rule R4 and let d ′ ∈ D i+1 be the declaration used in the first step of ξ. If d ′ was not modified in the transformation step from D i to D i+1 (that is, d ′ ∈ D i ), then the result follows from the inductive hypothesis. We assume then that d ′ ∈ D i , d ′ is then the result of the transformation operation applied to obtain D i+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) 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 ofs andt), there exists a derivation step D i .B 1 σ, cσ → D i .B 2 σ, c ′ if and only if there exists a derivation step D i .B 1 , c ∧ (s =t) → D i .B 2 , c ′′ , 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,c I ) eσ = ∃ −Var (A,c I ) (e ∧ (s =t)).
Case 3: d ′ is the result of a backward instantiation. Let d be the corresponding declaration in D i . The situation is the following:

Transformations of CCP programs
If p(t) is not evaluated in χ, then the proof is immediate. Otherwise, by the definition of χ and since f ∈ D i , there exists also a derivation . Therefore, by (32) and (31) By the definition of Then, by the definition of derivation and since d ∈ D 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). Let According to the definition of pc and by Lemma A.1, for any derivation χ for ask(c j ) → A j ] tell(ṽ =r)], c I 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.
where e = pc(C[ ]) and for every constraint c such that Var (c) ∩ Var (d) ⊆ Var (q(r), C), if D i .H, c ∧ e is productive then both the following conditions hold: -there exists at least one j ∈ [1, n] such that D |= (c ∧ e) → c j -for each j ∈ [1, n], either D |= (c ∧ e) → c j or D |= (c ∧ e) → ¬c j .
.B, c F . By the inductive hypothesis, there exists a derivation Now, we distinguish two cases: 1) n j=1 ask(c j ) → (H B j ) is not evaluated in χ. In this case the proof is obvious.

2)
n j=1 ask(c j ) → (H B j ) is evaluated in χ. We have two more possibilities: 2a) There exists h ∈ [1, n], such that where D |= c m → c h . In this case the thesis follows immediately, since using d one can obtain the agent C m [H B h ] after having evaluated the choice agent in

Transformations of CCP programs
is not productive. Then, by definition, D i .H, c ′′ F has at least one finite derivation (H). Moreover, since in a derivation we can add to the store only constraints on the variables occurring in the agents, c ′′ Without loss of generality, we can assume that Var (χ 1 ) ∩ Var (χ) ⊆ Var (H, c ′′ F ). Therefore, by the previous observation, and Finally, to prove the thesis it is sufficient to observe that from (34), (36), (37) and from the definition of By the inductive hypothesis, there exists a derivation Since Var (C I [q(ṽ)], c I ) ⊆ Var (C I [C[p(X)] tell(ṽ =r)], c I ), we have that App-6 · Sandro Etalle et al.

Since by hypothesis for any agent
We show now that we can substitute H for H ′ tell(X =X ′ ) in the previous derivation. Since f ′ : p(X ′ ) ← H ′ is a renaming of f : p(X) ← H, the equalityX =X ′ is a conjunction of equations involving only distinct variables. Then, by replac-ingX withX ′ and vice versa in the previous derivation we obtain the derivation Then, from (40) Finally, since d : 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 w t (with t ∈ {ss, dd, ff}) as a shorthand for indicating the success weight w ss , the deadlock weight w dd and the failure weight w ff . Lemma A.3. Let q(r) ← H ∈ D 0 , 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) Proof. Immediate.  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 ∈ D i , and let cl ′ : q(r) ← H ′ be the corresponding declaration in D i+1 (in the case i < n). For any context C I [ ] and any satisfiable constraint c and for any constraint c ′ the following holds: 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 D i to D i+1 then the result is obvious by choosing d ′ = ∃ −Var (C I [H],c) c ′ . Assume then that cl is affected when transforming D i to D i+1 and let us distinguish various cases.
Case 1: cl ′ ∈ D i+1 was obtained from D i by unfolding. In this case, the situation is the following: where cl and u are assumed to be renamed so that they do not share variables.
and 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 D i . The situation is then the following: has no variable in common with cl (the case cl ′ : q(r) ← C[p(t) tell(t =s)] is analogous and hence omitted). By the hypothesis, Var Moreover, by the definition of transformation sequence, there exists a declaration p(s) ← B 0 ∈ D 0 and then, by Lemma A.3, there exists a constraint d 1 such that and Using the hypothesis on the variables and since f is renamed apart from Var (r), we have that Then, from Point 1 of the Lemma (assumed as hypothesis) and (48) it follows that there exists a constraint d 2 such that hold. By definition of weight, we can assume that , c) and therefore, we have that We have now two cases: In this case, by (48) By the hypothesis on the variables, we can build a derivation , c → * D 0 .B ′ F , d 3 which performs exactly the same steps of ξ, plus possibly a tell action, such that By the previous result and by defini- , c) and we can assume, without loss of generality, that Var F , c F → which performs exactly the same steps of ξ (and therefore wh(χ) ≤ n) and such that 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.
where e = pc(C[ ]) and for every constraint e ′ such that Var (e ′ ) ∩ Var (cl) ⊆ Var (q(r), C), if D i .H, e ′ ∧ e is productive then both the following conditions hold: -there exists at least one j ∈ [1, n] such that D |= (e ′ ∧ e) → c j -for each j ∈ [1, n], either D |= (e ′ ∧ e) → c j or D |= (e ′ ∧ e) → ¬c j We prove that, for any derivation If H n j=1 ask(c j ) → B j 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 and D |= d m → c h . In this case we can construct the derivation which performs exactly the same steps of ξ and then the thesis holds.
2) ξ is of the form By Lemma A.1 and by definition of pc, we can construct another derivation Therefore there exists a derivation which performs the same steps of χ (in a different order). By construction wh(ξ ′ ) = wh(χ) = wh(ξ) and then the thesis holds. and hold. Moreover, we can assume without loss of generality that Var(c ′ ) ∩ Var(X) ⊆ Var (C I [C [B]], c).
Since f ∈ D 0 , from (53) and Point 2 of Lemma A.4 it follows that there exists a constraint d ′ such that ], c, c ′ ) and We can assume, without loss of generality, that Var (d ′ ) ⊆ Var (C I [C[p(X)]], c). Then by using (54) and (55)  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 ∈ D i+1 , and letcl : q(r) ←H be the corresponding declaration in D i . Moreover let C I [ ] be a context, c a satisfiable constraint and let c ′ be a constraint, such that Var(H) ∩ Var (C I , c) ⊆ Var (r) and w t (C I [q(r)], c, c ′ ) is defined. Without loss of generality, we can assume that Var (H)∩Var (C I , c) ⊆ Var(r). Then, since by inductive hypothesis, part 1 holds for i, there exists a constraint d 1 such that Lemma A.6. Let 0 ≤ i ≤ n, c 1 , c m satisfiable constraints, c k a constraint and assume that there exists a derivation ξ : Then there exists a constraint c ′ such that Proof. We prove the thesis for one derivation step. Then the proof of the Lemma follows by using a straightforward inductive argument. Assume that c 1 , c 2 are satisfiable constraints, c k is a constraint and that there exists a derivation such that m(A k , c k ) ∈ {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 A 1 = C 1 [A], where C 1 [ ] is not a guarding context. We have now three cases: Since C 1 [ ] is not a guarding context the definition of weight implies that where t = m(A k , c k ). Then the thesis holds 2) A = q(ṽ) and there exists a declaration cl : q(r) ← B ∈ D i . In this case ¿From the definition of derivation it follows that Var(C 1 [q(ṽ)], c 1 ) ∩ Var(q(r)) = ∅. Furthermore, by definition of transformation sequence, there exists a decla- These results together with the inclusion thus concluding the proof for this case.
3) A = ask(c) → B and D |= c 1 → c. In this case Since C 1 [ ] is not a guarding context and D |= c 1 → c we obtain where t = m(A k , c k ), which concludes the proof.
We need one last lemma.
Lemma A.7. Let c be a satisfiable constraint, A be the agent A 1 . . . A l , where for any j ∈ [1, l] either A j is a choice agent or A j = Stop and assume there exists a split derivation ν in D 0 , 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, w t (A, c, d) We can now prove our main theorem. Assume then that there exists a derivation D 0 .A, c I → * D 0 .B, c F such that c I is a satisfiable constraint and m(B, c F ) ∈ {ss, dd, ff}. ¿From the inductive hypothesis it follows that there exists a split derivation Let d ∈ D i−1 \D i be the modified clause in the transformation step from D i−1 to D i . If in the first m steps of χ there is no procedure call which uses d then clearly there exists a split derivation ξ in F 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 D i−1 to D i .
F . Without loss of generality, we can assume that Var (χ) ∩ Var(u) = ∅ 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 , 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 Observe that from the derivation D 0 .C m+1 [p(t)], c m → * D 0 .B ′′ , c ′′ F and (57) it follows that The hypothesis on the variables implies that Var (C m+1 [p(t)], c m ) ∩ Var (u) = ∅. Then, by the definition of transformation sequence and since u ∈ D i−1 , there exists a declaration p(s) ← H 0 ∈ D 0 . By Lemma A.3 and part 1 of Lemma A.5 it follows that there exists a constraint d F such that and Therefore, by the definition of w t , by (59) and since w t (C m+1 [p(t)], c m , c ′′ F ) is defined, there exists a derivation holds and, by definition of weight, we obtain Moreover, we can assume without loss of generality that Var(ξ 0 ) ∩ Var (ξ 1 ) = Var (C m+1 [H tell(t =s)], c m ). Then, by the definition of procedure call and there exists a derivation 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 (64) and by construction) (64) and by construction) By the definition of weight, w t (C I [q(ṽ)], c I , c ′ F ) = w t (C I [q(ṽ)], c I , c ′′ F ), by (63) and (59), , c I , c ′ F ) and then, by definition, ξ is a split derivation in D i ∪ D 0 . 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 D i . Therefore the situation is the following: 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 D i . The situation is the following: 1 has no variable in common with d (the case d ′ : q(r) ← C[p(t) tell(t =s)] is analogous and hence omitted). We distinguish two cases: · App-17 1) There is no procedure call to p(t) in the first m steps. Therefore χ has the form Without loss of generality, we can assume that Var(χ) ∩ Var (p(t) tell(b) tell(t = s)) = Var (t). Then, by the definition of D i , there exists a derivation corresponding to χ, Following the same reasoning as in Case 3 of Lemma A.5, we can prove that there exists a constraint d F such that 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 = q. In this case we can assume, without loss of generality, that χ has the form In this case there exists a derivation Observe now that, given any set of declarations, if there exists a derivation χ ′ for the configuration C ′ [tell(b) B tell(t =s ′ )], c ′ where c ′ is satisfiable and Var (C ′ , c ′ )∩Var (b,s) = ∅, then there exists a derivation for C ′ [tell(b) B tell(t = s ′ ) tell(b) tell(t =s)], c ′ 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 ′ ) tell(t =s) for tell(t =s ′ ) tell(s ′ =s). Moreover, since p(s ′ ) ← tell(b) B is a renaming of c and therefore D |= (b ∧ (s ′ =s)) → b holds, we can drop the agent tell(b).
Finally, observe thats ′ =s can be reduced to a conjunction of equations of the formX =Ỹ, whereX ⊆ Var(s) andỸ ⊆ 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) B tell(t =s ′ )], c ′ ) ∩ Var (s) = ∅. Then the thesis holds for this case.
2b) p = q. In this case, the situation is the following: ] is a renaming of d which has no variables in common with d. Let c ′ = p(s ′ ) ← tell(b) C [p(ũ ′ )] 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 , c ′ 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 guard in d is simplified. Let and d ∈ D i−1 is the declaration to which the guard simplification was applied.
By the definition of split derivation χ has the form

Since by the inductive hypothesis for any agent
it is easy to check that there exists a derivation 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 c m+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 the context obtained from C m+h as follows: any (renamed) occurrence of the agent n j=1 ask(c j ) → B j in C m+h [ ], introduced in χ 0 by a procedure call of the form q(s), is replaced by a (suitably renamed) occurrence of the agent n j=1 ask(c ′ j ) → B j . Then, by definition of D i , we have that , c m+h is a derivation in D i which does not use rule R2 and such that Then the thesis follows by definition of split derivation. Now assume that c m+h is satisfiable. By Lemma A.6 and (65), there exists a constraintd, such that Var (d) ⊆ Var (C m+h [ n j=1 ask(c j ) → B j ], c m+h ) and where By definition of weight, by (66) and since  (66), holds. Without loss of generality, we can assume that Var(d ′ ) ∩ Var (C I [q(ṽ)], c I ) ⊆ Var (C m+h , c m+h ). Therefore, from (67) it follows that as follows: any (renamed) occurrence of the agent n j=1 ask(c j ) → B j in C m+h [ ], introduced in χ 0 by a procedure call of the form q(s), is replaced by a (suitably renamed) occurrence of the agent n j=1 ask(c ′ j ) → B j . By the definition of D i and since D i−1 .C I [q(ṽ)], c I → * D i−1 .C m+h [ n j=1 ask(c j ) → B j ], c m+h , there exists a derivation Now from the definition of derivation and of ask simplification it follows that, if ask(c j ) →B j is a choice branch inB and ask(c ′ j ) →B j is the corresponding choice branch inB ′ , then D |= ∃ −Var (Bj,c m+h ) (c m+h ∧c j ) ↔ (c m+h ∧c ′ j ) holds. Therefore, by using the same arguments as in Case 4 of Proposition 4.5, since (by inductive hypothesis) D 0 is weight complete and D 0 .C m+h [ n j=1 ask(c j ) → B j ], c m+h → * D 0 .B ′ ,d ′ , we obtain that there exists a split derivation in D 0 of the form . 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 where t = m(B ′ , c ′ F ). Moreover, we can assume without loss of generality that Then by (69) we obtain and therefore, by definition of weight, holds. By Lemma A.7 and by construction of Then, by (72) and (70), we have that Finally,

Transformations of CCP programs
· App-21 is a derivation in D i ∪ D 0 . 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 . Then the proof follows by (57). Base case. In this case w t (C I [q(ṽ)], c I , c ′′ F ) = 0 and by definition of split derivation, rule R2 is not used and therefore each derivation step is done in D i−1 . Moreover, observe that since t ∈ {ss, dd, ff}, if c ′′ F is satisfiable, then C k is a guarding context. Then, it is easy to check that since the other case is immediate. By the definition of D i and since χ is a split derivation, there exists a derivation which does not use rule R2. Moreover, by definition of split derivation and therefore, by inductive hypothesis there exists a split derivation in D i ∪ D 0 , Then by definition of weight, Moreover, by our hypothesis on the variables of ξ 0 and of ξ 1 , there exists a derivation (74), (76), since ξ 0 do not use Rule R2 and ξ 1 is a split derivation in D i ∪ D 0 , we have that ξ is a split derivation in D i ∪ D 0 , such that m(B ′ , c ′ F ) = m(B ′′ , c ′′ F ). Now, the thesis follows by (75).
By the definition of split derivation, χ has the form F . 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

Transformations of CCP programs
· App-23 andC[H n j=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 c k 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 c k is not satisfiable, then the proof is analogous to that one of the previous Case 4.
Assume then that c k is satisfiable. By Lemma A.6 and (77), there exists a constraintd, such that where By definition of weight, by (78) and since Then, by the definition of weight and by (78), Without loss of generality, we can assume that Var(d ′ ) ∩ Var (C I [q(ṽ)], c I ) ⊆ Var (C k , c k ). Therefore from (79) it follows that Let C ′ k [ n j=1 ask(c j ) → (H B j )] be the agent obtained from C k [H n j=1 ask(c j ) → B j ] as follows: any (renamed) occurrence of the agent H n j=1 ask(c j ) → B j in C k [ ] which has been introduced by a procedure call of the form q(s) is replaced by a (suitably) renamed occurrence of the agent n j=1 ask(c j ) → (H B j ). By the definition of D i and since Moreover, since D 0 is weight complete, D 0 .C k [H n j=1 ask(c j ) → B j ], c k → * D 0 .B ′ ,d ′ and analogously to the Case 6 of Lemma A.5, there exists a split derivation 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 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.
which performs exactly the first m steps as χ.
The definitions of derivation and folding imply that Var(H) ∩ Var (C m+1 , c m ) ⊆ 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 , c m , d ′ ) and therefore, by (83), holds. Moreover, from (82) we obtain Without loss of generality, we can now assume that Then, by (84) and (57) it follows that ¿From the definition of weight w t (C I [q(ṽ)], c I , c ′ F ) = w t (C I [q(ṽ)], c I , c ′′ F ) and since χ is a split derivation we obtain w t (C I [q(ṽ)], c I , c ′′ F ) > w t (C m+1 [H], c m , c ′′ F ). Then, from (84) and (86) (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 D 0 , . . . , D n be a transformation sequence, and A be an agent. 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)] 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 D 0 , . . . , D n .
We start with the following definition.
Definition A.10. Let D be a set of declarations and let ξ be the derivation D.A 1 , c 1 → * D.A m , c m → * D.A n , c n .
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 w t (A, s), as follows: w t (A, s) = min{n | n = wh(ξ) and ξ is a derivation D 0 .A, c → * D 0 .B, d such that ∃ −Var (A,c) s tr(ξ) and t = m(B, d)}.
Definition A.12 (Split derivation for traces). Let D 0 , . . . , D i be a transformation sequence. We call a derivation in D i ∪ D 0 a split derivation for traces if it has the form Proposition 4.9 holds also when considering as observables O t 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. In the following we extend to set of observables the (pre-order) relation in the expected way: Given two sets of observables O t (D i .A) and O t (D j .A), we say that O t (D i .A) O t (D j .A) iff, for any s, x ∈ O t (D i .A), (with x ∈ {ss, dd, pp, ff}), there exists s ′ , x ∈ O t (D j .A) such that s s ′ . We denote by ≡ the equivalence relation induced by on sets of observables, that is, The following is analogous of Proposition 4.5 for traces. 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 ′ ∈ D i+1 be the declaration used in the first step of ξ. Assume also that d ′ ∈ D i and that d ′ is the result of the transformation operation applied to obtain D i+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. For any derivation which uses a declaration H ← C[tell(s =t) 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, c I ). 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, c I ) 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 D i 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

Transformations of CCP programs
·  where tr(β) tr(χ 0 ) and m(B ′′ 0 , c ′ 0 ) = m(B ′ 0 , c 0 ). Moreover, we can drop the constraint tell(X ′ =X), since the declarations used in the derivation are renamed apart and, by construction, Var (C I [C[H] tell(r =ṽ)], c I ) ∩ Var (X ′ ) = ∅. We then obtain that there exists a derivation β ′ = D 0 .C I [C[H] tell(ṽ =r)], c I → * D 0 .B 0 ,c 0 which performs exactly the same steps of χ 0 except for (possibly) the evaluation of tell(X ′ =X) and such that ∃ −Var (C I [C[H] tell(ṽ=r)],c I ) tr(χ 0 ) tr(β ′ ) and 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 ′ ). 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 D i and let cl ′ : q(r) ← H ′ be the corresponding declaration in D i+1 (in case i < n). For any context C I [ ], any satisfiable constraint c and for any sequence s starting in c the following holds: 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: 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, c 1 be a satisfiable constraint and assume that there exists a derivation ξ : Finally we have the following.
Theorem 5.12 (Strong Total Correctness). Let D 0 , . . . , D n be a restricted transformation sequence, and A be an agent.
-If s, x ∈ O t (D 0 .A) (with x ∈ {ss, dd, pp, ff}) then there exists s ′ , x ∈ O t (D n .A) such that s s ′ . -Conversely, if s, x ∈ O t (D n .A) then there exists s ′ , x ∈ O t (D 0 .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: (2) D i 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, O t (D 0 .A) ≡ O t (D i−1 .A) and D i−1 is weight complete for the traces. Proposition 4.9 holds also when considering O t rather than O. From Proposition A.15 and (the counterpart for traces of) Proposition 4.9 then it follows that if D i is weight complete for traces then, for any agent A, O t (D 0 .A) = O t (D i .A). So, in order to prove parts 1 and 2, we have only to show that, for any derivation β = D 0 .A, c I → * D 0 .B, c F such that c I is a satisfiable constraint and m(B, c F ) ∈ {ss, dd, pp, ff}, there exists a split derivation in D i ∪ D 0 , ξ = D i .A, c I → * D 0 .B ′ , c ′ F , such that tr(β) tr(ξ) and m(B ′ , c ′ F ) = m(B, c F ). ¿From the inductive hypothesis it follows that there exists a split derivation where tr(β) tr(χ) and m(B ′′ , c ′′ F ) = m(B, c F ). Now, let d ∈ D i−1 \D i be the modified clause in the transformation step from D i−1 to D i . 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 C ′ [tell(b) B tell(t =s ′ )], c ′ where c ′ is satisfiable and Var(C ′ [tell(b) B tell(t = s ′ )], c ′ ) ∩ Var(b,s) = ∅, then there exists a derivation for C ′ [tell(b) B tell(t = s ′ ) tell(b) tell(t =s)], c ′ 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 c j 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.