Francois Fages

The "Logic Languages and Constraints'' (LLC) group

at ENS Paris conducts research on various aspects of constraint programming. From a foundational point of view, the leading programming paradigm investigated is the one of logic programming in a broad sense, which identifies:

Specifications = Programs = Theories

Execution = Proof search

In this paradigm, programs are defined with operators having a logical reading, and constraints are distinguished formulas interpreted in a fixed structure presented by a logical theory. Execution as proof search then combines specific constraint solving algorithms dedicated to the constraint fragment, with the logical resolution process. The close connection between constraint languages and logic provides constraint programs with unique features for their specification and design, for reasoning about them and for proving their properties.

While this is very well understood for the class of constraint logic programs CLP built on the pure Horn fragment of predicate calculus, practical constraint languages include extra-logical operators for meta-programming, imperative assignment, concurrency, which make sometimes questionable the depth of the link between theory and practice. One of our aims is to reconcile the programming idioms of constraint languages within the Logic Programming paradigm, possibly by changing the logic for a more refined one such as Linear Logic which allows for both powerful programming constructs and powerful proof methods.

Our approach is, on the one hand, to contribute to the success of constraint programming in combinatorial optimization especially, by working on new constraint algorithms for classical problems and by developing the multi-paradigm constraint language CLAIRE , and on the other hand, to work on the logical foundations of constraint programming and on the development of mathematical tools for analyzing constraint software.

Constraints over Finite Domains

From basic constraint propagation...

Constraint propagation algorithms over finite domains have been shown very useful for solving combinatorial problems. These algorithms can be easily encoded with the co-routining mechanism of logic programming languages, and one of the success story of Concurrent Constraint (CC) programming is the rationale reconstruction of the Chip constraint system over finite domains as a set of CC agents. In essence, the correctness of constraint propagation is a corollary of an approximation theorem by chaotic iteration of closure operators. This fact has been used in to develop a fully incremental constraint propagation algorithm with both dynamic addition and deletion of constraints, for a reactive extension of CLP with query manipulation commands. The system developed in collaboration with Thomson Corporate Research has been evaluated on a dynamic scheduling problem for aircraft sequencing, and on an interactive multi-criteria optimization problem for frequency bands allocation, where the incremental strategy was shown to pay-off.

... to global constraints

Basic constraint propagation algorithms are however not sufficient to compete with more traditional Operations Research (OR) approaches to combinatorial optimization problems. More powerful algorithms for handling global constraints have to be designed or imported from OR to this purpose. Following this route, constraint programming has been shown to be as efficient as OR and yet more flexible in various domains: job-shop and cumulative scheduling, traveling salesman problem with constraints, weighted matching.

Global constraints involve the management of imperative structures which evolve non-monotonically during constraint propagation. This makes their analysis in the CC paradigm difficult and motivates the study of a version of CC in linear logic presented in the next section. The approach used for the experiments was to get back to a lower abstraction level, with the development of the Claire programming language which uses imperative variables and production rules. Claire is currently used to experiment complex search methods and hybrid approaches to combinatorial optimization problems, in collaboration with Bouygues and the CHIC-2 Esprit project.

Concurrent Constraint Programming and Linear Logic

CC languages extend the class of CLP languages with a new operator ask for expressing a form of synchronization between agents based on constraint entailment, generalizing the co-routining facilities of CLP with delay. This extension obviously destroys the completeness results of the operational semantics w.r.t. the logical semantics of CLP. A natural question is then to what extend can CC recover a logical semantics, and in what logic?

A disjunctive agent such as (x > 0 * y + 1) + (x = 0 * y = 1) cannot have as specification (x >= 0 * y = 1) as it suspends with the store x >= 0. Intuitionistic logic (IL) provides a first solution to this problem, so that the operational transitions of CC agents can be interpreted as deductions in IL (soundness), and if a constraint can be deduced from (the translation of) an agent, then that constraint is entailed by the store at some point in the derivation from the agent (completeness on stores).

Terminating stores, in particular successes, cannot be characterized however because of the contraction and weakening rules of IL. These considerations lead naturally to a translation of agents in (intuitionistic) Linear Logic (LL). Along this way it is natural also to consider an extension LCC of CC languages with linear constraint systems, providing an account for resource consumption and imperative variables in addition to classical constraint systems. We have shown that LCC programs have a simple logical semantics in linear logic, and that completeness results hold for the observation of both stores and successes. The usefulness of these results is illustrated in by showing with examples how the phase semantics of linear logic can then be used to give simple "semantical'' proofs of safety properties of LCC programs.

The characterization of terminating stores with suspended agents is not possible in LL, mainly because of the deduction A*(cB)(integral)c(A*B) which would be interpreted as creating arbitrary suspensions. This difficulty leads to the investigation of a new non-commutative version of LL, where the implication which is the adjoint of the non-commutative conjunction is used to interpret the ask operator, providing completeness results for stores, successes and suspensions. These topics are currently developed in the group with support from the Esprit TMR "Linear Logic'' project.

Negation and Multi-Valued Logic

Negation is a very natural and powerful extension to constraint programs, allowing the full expressiveness of first order logic. However, numerous problems coming from the possible inconsistency of normal logic programs, from the undecidability of standard models when they exist, and from algorithmical difficulties for infering negative information, have stimulated numerous research during the past twenty years.

Turning to constraint logic programs made particularly appealing the fact that both finite failure for definite programs and constructive negation for normal programs were provided with soundness and completeness results w.r.t.the 3-valued logical consequences of the program and of the theory of the structure. We pushed forward these results by studying a version of constructive negation by pruning, in which computation involves the development of standard derivation trees augmented with a concurrent pruning mechanism (that reduces to a branch and bound like procedure in the case of optimization formula), and for which we give a simple fixpoint definition of the set of computed answer constraints, thereby generalizing the S-semantics of definite programs to normal programs.

These results are used in to define a hierarchy of semantics related by abtract interpretation, that can be used for the bottom-up data-flow analysis of normal CLP programs.

Previous results on the existence of stable models for normal programs have been generalized also to extended programs combining two forms of negation: an explicit negation operator and a default negation operator. We have show in that the canonical models of extended programs correspond to standard models in 4-valued Belnap's logic, and we define a computable semantics for extended programs, analogous to Kunen's 3-valued semantics for normal programs.

Typing and Higher-Order

Another topic of interest in our group is the typing issues for constraint languages. The constraint domain is generally a quite complex combination of basic structures, and many sorted logic is not adequate for representing such a combination. We are currently developing a static type system for CLP/CC languages in which the combination of parametric polymorphism with subtyping on constructor types is flexible enough to allow metapredicates. This type system is used also as the basis for a visual constraint programming environment.

In a different direction, we study the definition of higher-order functions in a logic language by rewriting rules. Suitable type systems have been defined so that confluence and termination properties are preserved, and the basis of a parallel implementation by interaction nets is currently under investigation. This research is supported bu the NATO exchange program "Extended rewriting and types''.