Il existe plusieurs connexions fondamentales entre logique et calcul, qui permettent de concevoir des langages de programmation dans lesquels les problèmes de spécification et certification prennent un sens précis à l'intérieur du formalisme logique. La programmation logique repose sur les identifications Spécifications=Programmes=Théories
Exécution = Recherche de preuves
Dans ce paradigme la programmation est d'abord une tâche de modélisation.
La classe des Programmes Logiques avec Contraintes, CLP( 
), telle
qu'introduite par Joxan Jaffar et Jean-Louis Lassez en 1987, distingue
le ``domaine du discours'', c'est-à-dire
les structures manipulées,
de la modélisation du problème proprement dite, à l'aide de formules
logiques.
La recherche de preuves combine alors des techniques hybrides de résolution
logique et de résolution de contraintes sur des structures spécifiques,
par exemple l'arithmétique réelle, entière,
les domaines finis, les termes, les structures à traits, etc.
En se limitant à des théories clausales de Horn,
on définit ainsi une classe CLP( 
) de langages de programmation
logique avec contraintes, paramétrée par la structure considérée.
La classe des langages concurrents avec contraintes, CC( ) , définie par Vijay Saraswat en 1989,
introduit de plus des primitives
de concurrence (communication, synchronisation)
basées sur la satisfaction de contraintes.
Les langages CC autorisent un contrôle dynamique
des calculs dirigé par les données qui permet
de représenter les résolveurs de contraintes par un ensemble
d'agents concurrents,
programmer des stratégies de résolution,
et ouvrent la voie à un nouveau champ d'applications
nécessitant des systèmes réactifs et non plus seulement
transformationnels.
Le succès de langages de programmation par contraintes
comme CHIP (Cosytec), Prolog III, IV (PrologIA), CLP(R), ILOG-Solver,
OZ (Saarbrück),
CLAIRE (LIENS), Meta( 
) (Thomson),
à résoudre de façon déclarative
des problèmes
réels d'optimisation combinatoire ou de modélisation de systèmes
complexes,
a été démontré par plusieurs applications industrielles.
Cependant ces premiers succès montrent aussi que l'état de l'art actuel ne pourra pas être dépassé sans certaines extensions fondamentales à la fois
Ces thèmes sont étudiés tant du point de vue théorique (sémantique - algorithmique), que du point de vue de l'implémentation (développement de nouveaux langages) et de celui des applications, abordées en collaboration avec plusieurs partenaires extérieurs.
Les langages CC( ) peuvent ainsi être présentés
dans le style des algèbres de processus (CCS, 
-calcul, ...)
par un ensemble d'opérateurs pour la composition parallèle
, le choix non-déterministe +, la localisation de
variable 
, la synchronisation 
,
et par un système de transitions entre agents.
Toutefois l'opérateur de synchronisation donne naissance
à un mécanisme de suspension qui change la nature des succès
et fait perdre leur caractérisation logique.
Dès lors il est naturel de chercher à comprendre dans quelle mesure
le paradigme de la programmation logique s'applique encore aux
langages CC( ) , et dans quelle logique [384] [347].
Il s'agit donc d'interpréter les
opérateurs de composition d'agents comme des connecteurs logiques
et les règles de transitions comme des inférences de formules.
Après de nombreuses recherches infructueuses c'est finalement
dans une nouvelle version non-commutative de la logique linéaire
[367] [380]
qu'une solution sera trouvée.
Cette logique linéaire mixte qui combine des connecteurs commutatifs
et non-commutatifs,
permet de rendre compte finement
de la concurrence dans les langages CC( ) : ainsi
les suspensions peuvent être caractérisées dans la logique,
et de plus, dans certains cas intéressants, les déductions correspondent
exactement aux traces d'exécution.
Dans sa thèse, Paul Ruet présente la logique mixte par un calcul des séquents (dont le fragment multiplicatif - qui est la partie vraiment originale - étend d'une part la LLM commutative et d'autre part la LLM non-commutative circulaire de Girard et Yetter), et par les éléments de base d'une théorie de la démonstration (réseaux de preuve, séquentialisation, élimination des coupures, sémantique des phases).
Ces résultats ouvrent un vaste champ de recherche pour l'analyse des programmes concurrents avec contraintes.
)Nous proposons d'étendre aux CC les techniques d'interprétation abstraite proposés par Codognet et Filé (abstraction entre systèmes de contraintes), en utilisant cependant la sémantique dénotationnelle des CC plutôt qu'une sémantique opérationnelle [296]. Ceci permettra une généralisation de l'approche de Codognet et Corsini aux langages logiques concurrents. Une autre approche consiste à considérer une forme intermédiaire de non-déterminisme angélique / démoniaque [322].
Parmi les applications d'une telle analyse statique on peut citer : l'optimisation du contrôle (éviter les suspensions inutiles de processus), diverses optimisations du code compilé (reconnaissance de cas particuliers de contraintes par exemple), et vérification de propriétés des programmes, telle la détection de l'interblocage (deadlock) possible.
Réciproquement, les CC offrent un cadre naturel
pour implanter des interprètes abstraits. C'est-à-dire
étant donné un programme P à analyser, il s'agit de construire
un programme 
correspondant dont l'exécution fournit le
résultat de l'analyse sémantique de P.
Les réseaux d'interaction de Yves Lafont sont à la fois un langage
de programmation et un modèle de calcul inspiré des réseaux de
preuve de la logique linéaire. Une propriété fondamentale de ces
réseaux est la localité et asynchronicité des étapes
d'évaluation, ce qui donne lieu de manière très naturelle à des
implémentations parallèles. Vus comme modèle de calcul, les
réseaux d'interaction se
sont avérés très utiles pour l'étude de la dynamique d'autres
systèmes (par exemple, la réduction optimale dans le
-calcul). Nous avons continué cette ligne de recherche, en
étudiant les correspondances entre les systèmes de réécriture et
les réseaux d'interaction [333, 305]. Ces résultats nous
permettent d'une part l'application aux langages fondés sur les
réseaux d'interaction des techniques bien connues pour la
réécriture, par exemple pour montrer la propriété de
terminaison, ou définir des conditions suffisantes de
modularité. D'autre part, le codage des systèmes de réécriture
dans les réseaux [332] nous permet d'obtenir des
implémentations des langages fondés sur la réécriture, en
utilisant les implémentations des réseaux (par exemple,
l'implémentation parallèle de Gay et Mackie). Nous comptons aussi
pouvoir adapter au cadre de la réécriture des résultats
sémantiques développés pour les réseaux, ainsi qu'étendre les
codages précédants pour modéliser l'unification, ce qui nous
donnera des extensions de ces résultats pour la
programmation logique.
L'ajout du connecteur de négation aux programmes logiques est une extension très naturelle et utile, qui fournit toute la puissance d'expression de la logique du premier ordre. Cette extension a toutefois suscité de nombreuses recherches pendant ces vingt dernières années à cause d'une part des problèmes sémantiques, d'incohérence possible des programmes ou d'indécidabilité des modèles standards quand on peut les définir, et d'autre part à cause des difficultés algorithmiques qu'il y a à inférer des informations négatives.
Dans [304] [298] nous avons introduit un nouveau principe de négation constructive qui repose sur un mécanisme d'élagage (coupure par propagation de contraintes) entre arbres de dérivation SLD standards. La négation est entièrement traitée par le mécanisme concurrent d'élagage sans ajout d'autre principe d'inférence.
Le principal résultat théorique est un théorème de complète adéquation qui a permis de généraliser aux programmes avec négation la S-sémantique développée à l'université de Pise pour les programmes sans négation. Nous montrons en effet que le comportement opérationnel des programmes avec négation constructive par élagage, est complètement caractérisé par une sémantique de point fixe simple basée sur une version finitaire de l'opérateur de Fitting.
Ces résultats ont été utilisés pour définir, dans le cadre de l'interprétation abstraite, une hiérarchie de sémantiques pour les programmes logiques avec contraintes et négation [325], et pour donner des méthodes d'analyse de propriétés des programmes logiques avec contraintes et négation [364].
Nous souhaiterions aussi mieux comprendre le sens algorithmique des principes de négation constructive, en particulier pour la représentation intentionnelle des ensembles. Ceci permettrait de généraliser les constructions de programmation par contraintes et par ensembles finis. Plusieurs collaborations sont envisageables sur ce thème dont une dans le cadre d'un projet de spécification formelle proposé au GDR Programmation.
Il est possible de dériver des résultats de complétude précédents pour les programmes logiques avec négation des schémas opérationnels complets pour les programmes logiques avec prédicats d'ordre supérieur d'optimisation. Ces prédicats sont d'une grande importance pratique mais étaient vus comme des constructions ad hoc qui sortaient du cadre logique. De fait la procédure d'optimisation de type séparation-évaluation (``branch & bound'') qui est actuellement utilisée dans les systèmes CLP n'est pas correcte lorsqu'on l'applique à d'autres buts que la requête principale.
Nous avons montré qu'il était possible de doter les prédicats d'optimisation d'une sémantique déclarative fidèle en terme de négation constructive. Dans [329] [298] [304] nous montrons que l'on peut dériver du principe de négation constructive par élagage une version concurrente complète de la procédure d'optimisation par séparation-évaluation, autorisant la composition arbitraire de buts d'optimisation dans le programme ainsi que la récursion à travers les prédicats d'optimisation.
Par ailleurs dans [323] nous introduisons le
concept d'optimisation relationnelle,
qui permet de
représenter les contraintes de préférence sur les solutions,
par un programme CLP.
Nous étudions les aspects sémantiques et algorithmiques de ce concept,
et illustrons sa mise en 
uvre dans un problème d'optimisation
multi-critère d'allocation de fréquences.
Les modèles stables, introduits par Gelfond et Lifschitz, constituent la notion la plus générale de modèle standard bi-valué d'un programme logique (incluant les modèles bien fondés et stratifiés par exemple).
Les critères d'existence de modèles stables donnés dans [303] fournissent des conditions syntaxiques très générales de cohérence bi-valuée des programmes logiques, ainsi qu'une conjecture toujours ouverte.
La théorie des modèles stables est équivalente à la théorie des défauts de Reiter, mais présentée dans le cadre de la logique classique. Cette théorie est donc importante, elle resurgit par exemple dans les travaux récents de Vijay Saraswat sur les langages TCC (langages temporels concurrents avec contraintes).
Ces résultats ont été généralisés également aux programmes étendus qui combinent deux formes de négation : un opérateur de négation explicite et un opérateur de négation par défaut. Nous avons montré dans [346] [307] que les answer sets de Gelfond et Lifshitz pour les programmes étendus correspondent des modèles standards en logique de Belnap à 4 valeurs, et nous développons dans une logique à 9 valeurs une sémantique calculable des programmes étendus, analogue à la sémantique tri-valuée de Kunen pour les programmes normaux.
Nous étudions des langages logiques permettant la définition de fonctions du premier ordre et d'ordre supérieur, par des règles de réécriture. Ces règles sont utilisées pour évaluer les expressions fonctionnelles par réduction, et pour résoudre des contraintes sur les algèbres de termes par surréduction. Les deux propriétés principales qu'il faut alors assurer sont la confluence et la terminaison : la terminaison (appelée aussi normalisation forte) nous garantie que toutes les séquences de réduction sont finies, tandis que la confluence implique le déterminisme du calcul. Montrer ces propriétés n'est pas en général facile, il est naturel dans ce cas de s'appuyer sur la technique classique de décomposition d'un problème en sous-problèmes : c'est l'approche modulaire. Une propriété est dite modulaire si elle est vraie pour un système quand elle est vraie pour chacun de ses constituants.
Ni la confluence ni la terminaison ne sont modulaires
quand on combine des systèmes de réécriture arbitraires, même
du premier ordre.
Nous avons commencé par étudier les conditions
pour lesquelles la confluence et la terminaison sont modulaires quand
on combine des systèmes de réécriture du premier ordre [331].
Nous avons développé tout d'abord une méthode d'approche uniforme des
problèmes de modularité, basée sur une technique de preuve
originale dans ce contexte, inspirée de la preuve de normalisation
forte du -calcul typé due à Tait et Girard.
Outre une généralisation de plusieurs
résultats connus, nous avons obtenu par cette méthode un nouveau résultat de modularité pour les unions hiérarchiques.
Ensuite, nous avons étudiés les unions de systèmes de réécriture
du premier ordre et d'ordre supérieur avec le -calcul, et
généralisé les
résultats précédents dans ce cadre, [310, 301].
Dans la même ligne, nous étudions actuellement [363]
des mélanges de
réécriture et des calculs orientés objet, comme le
-calcul de Abadi et Cardelli.
Nous avons considéré un autre aspect des langages d'ordre supérieur qui est très important du point de vue pratique : les systèmes de typage. En général, on utilise deux catégories de systèmes de types : les systèmes explicites, où les types décorent les termes du langage, et les systèmes à assignation de types, où il n'y a pas d'information de type dans les termes. Dans le dernier cas un mécanisme d'inférence de types permet de transformer les programmes non-typés ou partiellement typés en des programmes bien typés. Une raison pragmatique essentielle pour préférer les systèmes d'inférence aux langages explicitement typés, est qu'ils permettent des définitions beaucoup plus concises.
Nous avons défini un système d'assignation de types pour les systèmes de réécriture d'ordre supérieur, qui utilise des types intersection, et nous avons étudié ensuite sous quelles conditions les systèmes de réécriture typés sont fortement normalisants, normalisants, ou ``head''-normalisants [353, 351]. Nous avons étendu ces résultats aux mélanges de systèmes de réécriture d'ordre supérieur et lambda-calcul [350], qui donnent plus de pouvoir d'expression pour la définition des fonctions. Actuellement nous travaillons sur l'extension polymorphe de ces systèmes, ainsi que sur la définition d'une restriction où l'inférence de types est décidable (fondée sur les types de rank 2).
) et méta-programmationNous étudions des systèmes de types adaptés à la programmation par contraintes. L'idée est d'extraire des types sous-jacents aux contraintes, que l'on peut voir comme des types dynamiques, une discipline de typage statique permettant de détecter des erreurs de type à la compilation.
Le système de types statiques de Mycroft-O'Keefe et Reddy
adapté de ML aux programmes logiques, ne permet pas de typer les
prédicats de méta-programmation, ni les programmes
logiques avec contraintes sur une structure , qui est le
plus souvent une combinaison de plusieurs structures de base :
arithmétique entière, réelle, listes, termes, structures à traits,
etc.
L'introduction d'une relation de sous-typage permet de résoudre ces problèmes. Les difficultés que cela soulève dans les langages fonctionnels (à cause de la contra-variance de la flèche) ne se présentent pas de la même manière dans les langages (premier ordre) de programmation logique par contraintes, ce qui permet d'espérer développer des systèmes de typage simples mais puissants, permettant de fonder également les extensions orientées objet de la programmation par contraintes.
Dans [365] nous
présentons un système de types pour les langages CLP et CC( ),
dans lequel les types sont des termes du premier ordre partiellement
ordonnés, appelés potermes.
Ce langage de types combine sans restriction polymorphisme paramétrique
et sous-typage. Il permet de typer les prédicats de méta-programmation
(qui en programmation logique remplacent l'ordre supérieur),
les extensions orientée-objet, et
les hiérarchies de domaines de contraintes.
Le problème de la vérification statique des types
d'un programme se ramène à la résolution d'un système linéaire
à gauche d'inéquations entre potermes, que l'on montre
facilement décidable avec existence de solution principale.
L'inférence de type pour les prédicats se ramène à la résolution
de systèmes généraux d'inéquations pour lesquels
nous étudions les algorithmes de résolution.
Ce système de types statiques est par ailleurs à la base d'un système de programmation visuelle [340] [339] [341] [342] pour la programmation par contraintes.
L'étude du problème de satisfiabilité des formules équationnelles dans les algèbres de termes commence avec les travaux de J. Herbrand en 1930 sur l'unification. Plusieurs extensions de ce problème ont été étudiées, par exemple, pour résoudre aussi des diséquations, ou pour la résolution d'équations modulo une théorie équationnelle (problème appelé E-unification). Par analogie, on appelle disunification la résolution de diséquations dans l'univers de Herbrand, et E-disunification la résolution de diséquations dans le quotient de l'univers de Herbrand par une théorie équationnelle E.
Pour résoudre le problème de E-unification, une recherche naïve des E-unificateurs basée sur la paramodulation
est très inefficace. Heureusement, il y a un très grand nombre
de stratégies efficaces et complètes. La plus utilisée est
une stratégie ordonnée, appelée surréduction.
Nous avons montré que la surréduction permet aussi de résoudre le
problème de E-disunification. Notre procédure de
E-disunification trouve des solutions explicites au problème donné.
Mais en ce qui concerne la représentation des solutions des problèmes
de disunification, les approches que l'on trouve dans la bibliographie
sont très différentes : les solutions peuvent être représentées
par des ``formes résolues'' qui peuvent encore
contenir diséquations, ou par des ensembles de substitutions, comme
dans notre procédure.
La représentation des solutions par des substitutions est très liée
à l'élimination de la négation : si toutes les
solutions de la diséquation 
peuvent être engendrées
par un ensemble fini de substitutions, alors on peut éliminer la
négation de .
L'élimination de la négation des
systèmes d'équations et diséquations, et même des formules
équationnelles du premier ordre arbitraires est décidable, mais
quand on interprète les formules équationnelles
dans un quotient de l'univers de Herbrand, elle devient indécidable :
l'élimination de la négation est indécidable
modulo une théorie AC, et nous avons montré qu'elle est aussi
indécidable
dans le quotient de l'univers de Herbrand par une théorie
présentée par un système de réécriture convergent.
Mais, nous avons aussi montré que l'élimination de la négation
des formules équationnelles arbitraires est décidable modulo une
théorie permutative de Mal'cev, cas qui inclut et
généralise les théories commutatives [366]. Dans le
cas des théories AC,
nous avons montré que l'élimination de la négation est décidable quand
les formules sont des problèmes de complément
linéaires [306]. Les problèmes de complément
permettent de résoudre les problèmes causés par l'ambiguïté
des définitions de fonctions, et ont des nombreuses applications dans
d'autres domaines de l'informatique, comme l'apprentissage inductif, les
spécifications algébriques, et l'implémentation de la négation
constructive dans les langages de programmation logique.
Les contraintes sur les domaines finis
ou discrets (ex. nombres entiers, flottants, etc.)
sont d'une grande importance pratique.
En plus des contraintes numériques (linéaires ou non-linéaires),
rentrent dans ce cadre
les contraintes symboliques, ensemblistes (ex. de cardinalité),
d'indice (ex. 
où I et V sont des inconnues), etc.
Les techniques de résolution
par propagation des réductions des domaines des variables
sont d'une efficacité étonnante dans le
contexte de la programmation logique par contraintes.
Nous avions défini depuis 91 une méthode simple mais efficace
d'implémentation de ces techniques au dessus de Prolog avec co-routines
qui permet de construire des bibliothèques extensibles de contraintes
[295].
Une méthode alternative utilisant une primitive originale
d'implémentation appelée sleeper et non le co-routinage
est proposée en [319] [318].
De telles bibliothèques sont en cours d'implémentation
dans le système CC( 
) [343].
Les algorithmes de propagation de contraintes
sur les domaines finis ne rentrent pas bien dans le cadre
logique de CLP( ) car ces algorithmes sont
souvent incomplets.
Suivant les travaux de Saraswat sur les langages CC( ) ,
il est possible de modéliser fidèlement ce type de contraintes
par des opérateurs de fermeture dans un treillis d'informations
partielles formé du domaine des variables
(dual du treillis des contraintes).
Nous avons poussé cette vue dans [324] [302]
pour la réalisation d'un modèle d'exécution réactif
de la programmation par contraintes,
et la conception d'algorithmes incrémentaux de satisfaction
de contraintes avec ajout et retrait de contraintes.
Nous montrons dans ces articles (de façon annexe)
que les algorithmes de
propagation de contraintes découlent en fait du théorème
d'itération chaotique de Cousot pour l'approximation du point fixe
d'un ensemble de fonctions monotones dans un treillis complet.
Nous utilisons cette approche pour donner une preuve simple de correction
des algorithmes incrémentaux pour l'ajout et le retrait de contraintes.
La propagation de contraintes plus complexes nécessite de développer des nouveaux algorithmes de propagation, spécifiques à des contraintes globales rencontrées en optimisation combinatoire. Ces algorithmes considèrent généralement des structures plus riches qu'un simple réseau de contraintes n-aires, en introduisant par exemple des tableaux avec des compteurs par lignes et colonnes (par exemple pour des problèmes d'emplois du temps) ou des histogrammes (pour représenter le niveau consommation d'une ressource [315]) ou même des structures non monotones (comme les intervalles de tâches pour les problèmes d'ordonnancement [313]). Ces structures évoluent, comme les variables logiques, suivant un mécanisme de pose et de levée d'hypothèses (backtrack). Un des points clés dans la mise au point de telles structures est la définition d'algorithmes qui maintiennent leur consistance de manière incrémentale [314].
L'approche utilisée est de revenir à un niveau d'abstraction plus bas, en utilisant le formalisme des règles de production. Une règle associe une expression à une condition logique. Dès que la condition est vérifiée, l'expression est évaluée [373]. La liberté de déclencher une action quelconque permet de décrire précisément les mécanismes de propagation sur des structures redondantes arbitrairement complexes. On peut ainsi définir une matrice de variables logiques où l'on stocke explicitement des min et des max sur les colonnes et les lignes. Les règles logiques permettent de décrire la mise à jour de ces informations redondantes en fonction des variations des variables logiques. Ces mécanismes ont permis l'écriture d'algorithmes compétitifs avec des algorithmes traditionnels de Recherche Opérationnelle. Un mécanisme de différenciation formelle sur les conditions logiques [354] (pouvant inclure des quantificateurs et des manipulations sur les ensembles) permet de prévoir quelles modifications des variables pourront entraîner la validité de la condition et par suite le déclenchement de la règle.
Une voie importante pour augmenter l'impact de la programmation logique par contraintes est de l'étendre de façon à réaliser des systèmes réactifs et non plus seulement transformationnels, c'est-à-dire des systèmes qui au lieu de calculer une seule relation d'entrée/sortie, sont en perpétuelle interaction avec leur environnement.
Nous avons donc cherché à définir un modèle d'exécution réactif pour la CLP. Ces travaux se sont concrétisés par la réalisation d'une implantation prototype et de plusieurs applications en collaboration avec le LCR de Thomson, puis récemment par la publication dans [324] [302] d'un schéma complet de programmation logique réactive. Ce schéma repose d'une part sur les algorithmes de relaxation de contraintes de la section précédente, et d'autre part sur un système de transformation de dérivations SLD. Une procédure de recherche réactive est définie pour explorer un arbre de dérivation SLD à partir de la dérivation transformée, et prendre en compte les interactions extérieures. Le système de transformation des dérivations est très général, il peut être utilisé par ailleurs pour définir des procédures de recherche stochastiques en CLP, il peut être généralisé également pour doter les langages TCC (``temporal concurrent constraint programming'') d'un modèle d'exécution incrémental.
La perspective de ces travaux est le développement d'une théorie unifiée pour la programmation réactive et la programmation logique. L'enjeu est la conception de systèmes réactifs déclaratifs, pour lesquels les travaux sur la programmation logique parallèle, la concurrence et les contraintes n'offrent aujourd'hui que des solutions partielles.
Par ailleurs, si les CC fournissent un cadre puissant et élégant d'expression de la concurrence, ils ne sont pas adaptées à la modélisation de phénomènes (ou à la spécification de calculs...) distribués. On souhaiterait pousser plus avant l'idée d'interactions comme contraintes pour autoriser les contraintes locales (distribution du store) et la résolution locale, dépendante de la structure du réseau d'interactions. Le domaine de contraintes devient alors une structure spatialement étendue, munie de règles de propagation (l'exemple typique est celui d'un réseau d'automates cellulaires) qui remplissent en quelque sorte le rôle de procédures de résolution. Le programme peut alors être vu comme la spécification d'un ensemble de conditions initiales-les contraintes à propager pour chaque agent- sur un système dynamique discret. La réactivité trouve tout naturellement sa place dans un tel cadre : un agent peut se trouver en contact permanent avec un ``point'' de l'univers extérieur. Nous travaillons en particulier sur l'utilisation des propriétés dynamiques et algorithmiques connues des automates cellulaires pour la construction d'un langage permettant de spécifier simplement des calculs distribués quelconques sur des réseaux à connectivité bornée. Puis de prouver des propriétés globales d'évolution du système dynamique à partir d'un ensemble de configurations primitives.
Un des champs d'application des contraintes sur les variables de domaines finis est l'optimisation combinatoire. Les problèmes d'optimisation combinatoire peuvent en effet être naturellement décrits par des entiers. Pour faire le point sur les possibilités et les limites de la programmation par contraintes en optimisation combinatoire, nous avons procédé à une évaluation systématique des techniques de propagation de contraintes :
Sur un ensemble de problèmes représentatifs des grands problèmes combinatoires usuels, l'approche par contraintes a été mise en concurrence avec d'autres approches algorithmiques (théorie des graphes, programmation linéaire, optimisation locale et marches aléatoires). Pour chacun des problèmes, nous avons essayé d'identifier les conditions dans lesquelles l'approche par contraintes était pertinente ainsi que les idées importantes des autres techniques algorithmiques qui pourraient être intégrées à un solveur de contraintes pour le rendre plus performant. Ce travail nous a permis, non seulement d'ébaucher une cartographie de l'utilisation de la programmation par contraintes en optimisation combinatoire, mais encore de définir tout un ensemble de techniques pour améliorer les solveurs sur les domaines finis (structures redondantes, schémas de branchement, heuristiques, optimisation locale avec propagation de contraintes, etc...) Sur certains problèmes, l'implémentation de tels algorithmes de propagation renforcée dans le langage Claire nous a permis d'améliorer l'état de l'art et même de résoudre certains problèmes ouverts [372].
Un des apports du travail de cartographie des contraintes en
optimisation combinatoire a été de montrer la richesse de
l'utilisation des grands principes de la programmation par contraintes
(modélisation d'un système par des variables à valeur dans un
domaines et par des formules logiques, propagation de valeurs,
réduction de domaines, utilisation de l'interprétation abstraites
pour raisonner sur des approximation de solutions, recherche
arborescente, etc.) dans le cadre d'algorithmes hybrides. Les
algorithmes hybrides, comme leur nom l'indique, ne sont pas à
proprement parler des programmes CLP( ) , mais sont des programmes qui
spécialisent et combinent des composants algorithmiques issus de la
CLP, de l'optimisation locale, de la programmation linéaire, etc.
(le développement d'algorithmes hybrides est un des buts du projet
européen CHIC-2). Le développement d'algorithmes hybrides nous a
notamment amenés à définir un calcul pour la formalisation
d'algorithmes de recherche arborescente paramétrés (pour décrire
des arbres construits par des modes de construction hétérogènes,
ou limités par des conditions topologiques). Un de nos buts est la
définition d'un cadre intégrateur permettant de faire coopérer
des modes algorithmiques complètement différents comme
l'optimisation locale et la recherche arborescente.
Les problèmes de planification distribuée, dans lesquels plusieurs utilisateurs interagissent en émettant des requêtes sur l'utilisation de ressources partagées, sont de bons exemples pour valider les concepts de concurrence basée sur les contraintes, et illustrer le caractère déclaratif des programmes CC . Une étude a eu lieu sur le problème posé par l'exécution distribuée des programmes CC dans ce type d'application, dans le cadre d'un contrat d'étude du MESR, avec le LCR de Thomson et SYSECA [385].
D'autres problèmes applicatifs d'ordonnancement d'allocation de fréquences et de placement ont été étudiés en collaboration avec le LCR de Thomson avec le souci de dégager des algèbres de contraintes et des méthodes générales [302] [337] [323].
Enfin, les travaux sur le diagnostic ont montré l'importance du raisonnement hypothétique et en particulier de l'inférence abductive. [321] montre comment l'abduction peut s'exprimer naturellement et efficacement dans les langages logiques concurrents.
(http://www.ens.fr/laburthe/claire.html)
CLAIRE est un langage avec des objets, des règles logiques propagées en chaînage avant et un système de versions pour l'exploration successive d'hypothèses différentes [373]. Le langage se veut simple (reposant sur un nombre minimal de concepts) et élégant (sa syntaxe est issue d'un langage de spécifications formelles). Les règles logiques et la gestion du backtrack permettent d'écrire des programmes avec des contraintes où les domaines, les solveurs (propagation et stratégies de résolution) ainsi que les éventuelles structures redondantes peuvent être arbitrairement compliqués, tout ceci avec une perte en élégance et en concision relativement faible par rapport au formalisme CLP . A la puissance d'expression et au contrôle offerts par le langage s'ajoute la possibilité de compiler en générant du code C++ particulièrement efficace.
Notre travail sur les algorithmes hybrides nous a aussi amené à rajouter des extensions au langage [357]. On a ainsi défini une notion d'itérateurs qui permet de définir de nouvelles structures pour représenter des conteneurs (par exemple pour implémenter des domaines de valeurs) et de les itérer par une simple boucle for. Une autre addition au langage venue de cette expérience algorithmique est l'utilisation d'une forme particulière de polymorphisme, le polymorphisme de composition, qui sert pour l'utilisation de règles de simplification lors manipulations sur des structures complexes. Une troisième exemple d'extensions envisagées dans le langage, motivées par des besoins algorithmiques est la notion de foncteurs de classes (mécanisme permettant d'enrichir des objets par certaines structures algorithmiques, sans polluer la modélisation du problème).
En plus de ces additions du langage, une bibliothèque de générateurs de code a été constituée pour l'écriture d'algorithmes de recherche paramétrés. Celle-ci facilite en particulier l'intégration de composants de recherche arborescente dans un algorithme hybride.
CLAIRE est aujourd'hui distribué avec deux bibliothèques pour l'écriture d'algorithmes d'optimisation combinatoire :
) au dessus de Prolog(http://www.ens.fr/fages/Book/clpFD.html)
Nous avons réalisé et diffusons une implantation de clpFD au dessus de Prolog avec co-routines. Ce système est principalement dédié à des fins d'enseignement, il accompagne le livre [295].
Ce système est utilisé également pour le développement expérimental
d'une extension orientée-objet et
d'un environnement de programmation visuelle pour la
programmation par contraintes.
A cause du nombre potentiellement très grand de contraintes
et de variables d'une application en grandeur nature,
il devient important de développer des techniques de représentation
compacte des programmes, dans le but de faciliter
la gestion de bibliothèques
de modèles réutilisables et composables.
L'idée a été de baser sur le système de types polymorphe défini pour
CLP( ) [365], les notions
de programmation objet pour la définition de classes,
et l'héritage de traits et de contraintes [342] [341] [340] [339].
Un système graphique interactif supportant la méthodologie
de programmation visuelle sur les types
a été développé en Prolog pour être interfacé avec des outils standards
de programmation par contraintes.
)
Nous avons réalisé
une implantation prototype parallèle de
cc(FD). Cette implantation est une application d'un projet plus large
d'implantation générique et parallèle de CC(X). Cette implantation est
basée sur un langage noyau CC( ) qui est une instantiation
particulière de la classe des langages CC basée sur une algèbre de
messages .
le langage CC( ) est le produit de quatre influences
distinctes : la programmation logique par contraintes (PLC), les implantations
parallèles des langages logiques (PARLOG, GHC, FGHC, Muse), le calcul des
CC, et les travaux sur les langages orientés-objets tels Claire ou Objective-CAML.
La Programmation Logique et par Contraintes ont influencé la conception du
langage, en particulier l'intégration des résolveurs de contraintes dans le
langage. L'implantation de ce langage repose sur deux paradigmes de
programmation : les langages objets et les langages logiques parallèles. C'est
grâce aux techniques de ces deux mondes que le langage CC( ) a
pu être efficacement implanté. Enfin, le cadre des langages CC a été
développé et utilisé pour donner une sémantique algébrique au langage
CC( ).
Le résultat est un langage parallèle efficace CC( ). Ce
langage, qui utilise des techniques d'implantation très
pointues[345], offre un environnement objet parallèle muni du
non-déterminisme. Cet environnement se révèle adapté à la recherche en
algorithmique parallèle de contraintes.
Dans les années à venir, le souci de maintenir une liaison forte entre recherche théorique et expérimentation au travers de collaborations industrielles devrait rester l'orientation majeure du thème.
Nous avons indiqué dans les sections précédentes des perspectives pour chaque axe. L'objectif sur le plan théorique est de contribuer aux développements sémantiques et algorithmiques de la programmation par contraintes dans plusieurs directions : concurrence, négation, ordre supérieur, algèbres de contraintes, optimisation combinatoire. L'objectif sur le plan pratique est d'étudier des problèmes difficiles de grande importance pratique, permettant de valider les concepts nouveaux et de motiver de nouvelles extensions.
L'objectif à plus long terme pourrait être d'étudier, au delà des interactions qui se manifestent entre sémantique et algorithmique dans notre domaine, les correspondances profondes entre ces disciplines. Celles-ci se manifestent de multiples façons :
Nous envisageons de poursuivre ces recherches fondamentales et expérimentales dans le cadre de projets européens et nationaux (réseau TMR "Logique Linéaire", réseau Compulog, projet Esprit CHIC-2, actions PRC et inter-PRC des GDR Programmation et AMI du CNRS, etc.). Nous souhaiterions également maintenir notre effort de développement et de diffusion de logiciels. C'est le cas par exemple depuis 3 ans pour le projet CLAIRE, qui fournit une base expérimentale puissante pour nos besoins propres et pour de nombreuses équipes extérieures (une forme contractuelle de collaboration nationale et internationale sur ce projet est à l'étude).