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.
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 @cite_9 as well).
@cite_9
1521956339
One of the main aims of this paper is to show that the nature of the communication mechanism of concurrent constraint languages is essentially different from the classical paradigms of CCS, CSP and ACP. We define indeed a compositional semantics based on linear sequences, while more complicated structures, like trees and failure sets, are needed to model composition ally CCS, CSP and ACP. From this model we are able to derive a fully abstract semantics by imposing some saturation conditions, that model the monotonic nature of communication in concurrent constraint languages. Finally, we show that if we eliminate the consistency check, and drop the distinction between success and deadlock, then our model is isomorphic to the semantics based on Scott’s closure operators proposed in [SRP91].