Concurrent Constraint Programming and Linear Logic

François Fages

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000

Abstract

The class of Concurrent Constraint programming languages (CC) was introduced a decade ago by Vijay Saraswat as a unifying framework for constraint logic programming and concurrent logic programming. The CC paradigm constitutes a representative abstraction of constraint programming languages that are used nowadays in a wide variety of application domains, most notably for solving combinatorial search problems.

The search for a logical semantics for CC led to interesting developments that benefited from recent advances in logic. A series of results has been obtained in the general Logic Programming paradigm that identifies programs with theories and computations with deductions. While it is possible to characterize the set of accessible stores of a deterministic CC computation as the set of constraints which are deducible in intuitionistic logic from the program formulas, the characterization of the success stores, i.e. the constraints of terminal configurations with no suspended agent, requires restricting the deductions that can be carried-out in order to forbid the logical deletions of agents by weakening. Jean-Yves Girard's Linear Logic (LL) is a refinement of classical logic obtained by dropping the structural rules of weakening and contraction, and by introducing a connective ``!'' with these properties in order to recover classical logic. One can give a simple translation of CC programs in intuitionistic linear logic that is sound and complete or observing the set of successes and accessible stores. This approach makes it possible to analyze both ``may'' properties, i.e. those properties which are true on some branch of the computation, and ``must'' properties, which are true on all branches of the computation. These results have been used to prove safety properties of CC programs simply by exhibiting special phase models of programs. The logical characterization of other observable properties of CC computations, such as the set of terminal stores, i.e. constraints of terminal configurations with or without suspended agents, is more delicate. Preliminary results have been obtained in the non-commutative logic NL of Paul Ruet that allows limiting the reductions that can be done with the guard constraints inside agents.

All the previous completeness results remain valid when generalized constraint systems based on linear logic are considered instead of classical logic. Linear constraint systems greatly enhance the expressive power of CC by allowing resource consumptions in the store, and thus non-monotonic evolutions of the store along a derivation. Several levels of linear constraint systems can be considered according to the different kinds of axioms that are allowed. The simplest level combines classical constraint systems with linear tokens that have no other axiom than a general equality axiom. This level adds a simple multiset processing machinery to the classical part of the constraint system. This extension is sufficient to fundamentally extend the expressive power of CC with the capability of encoding imperative variables and control structures in the LCC framework. This is illustrated by simple LCC programs for solving constraints over finite domains and for protocol specification.