*The LLC group at
ENS Paris* 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''. |