cours-ded-contrainte

Description

Deduction contrainte1?Jean-Pierre Jouannaud´LIX, Ecole Polytechnique91400 Palaiseau, Franceemail: [e-mail] http://www.lix.polytechnique.fr/Labo/jean-pierre.jouannaud1 Historique et Motivations1.1 Historique de la programmation contrainte– Programmation logique contrainte en PROLOG [A. Colmerauer]– Pration logique contrainte en PR II [A. Colmerauer, 82]– Programmation contrainte en CHIP [M. Dincbas, 87]– Pration contrainte param`etr´ee CLP(X) [J.-L. Lassez, M. Maher, 88]– Programmation concurrente contrainte [V. Sarasvat, 90]– Contraintes de typage surˆ [F. Pottier, 95]1.2 Historique de la d´eduction contrainte– R´ecriture ordo-sort´ee [Goguen, Jouannaud, Meseguer, 85]– D´eduction contrainte [A. Degtyarev, A. Voronkov, 86 ; C.&H. Kirchner,M. Rusinowitch, 90]– Compl´etion ordo-sort´ee [H. Comon, 91]– Compl´etion basique [R. Nieuwenhuis, A. Rubio, 92]– Strat´egies basiques ordonn´ees de r´esolution [H. Ganzinger et al., 94]– Model-checking modulo [A. Podelski, 95]– SAT modulo theories [R. Nieuwenhuis et al.]1.3 PROLOGProgrammation logique pure contrainte :0 0 0A←−Ck φ ←−A,C k φ.0 0 0←−C,C k φ∧φ ∧A =A´Eliminer ←−Ck φ si φ est insatisfiable←−k φRetourner Sol(φ) si φ est satisfiable?Project LogiCal, Pˆole Commun de Recherche en Informatique du plateau de Saclay,´CNRS, Ecole Polytechnique, INRIA, Universit´e Paris-Sud.6661.4 Ing´edients– lescontraintessontdesconjonctionsd’´egalit´esappell´eescontraintesd’unification– les ...

Informations

• Publié par: Irda
• Nombre de lectures: 18
• Langue: Français

Extrait

Deduction contrainte

Jean-Pierre Jouannaud 1? ´ LIX, Ecole Polytechnique 91400 Palaiseau, France email: [e-mail] http: //www.lix.polytechnique.fr/Labo/jean-pierre.jouannaud

1 Historique et Motivations 1.1 Historique de la programmation contrainte –Programmation logique contrainte en PROLOG [A. Colmerauer] –Programmation logique contrainte en PROLOG II [A. Colmerauer, 82] –Programmation contrainte en CHIP [M. Dincbas, 87] –ioatonncogPrmmra)[J.-L.L´eeCLP(Xramae`rtrtiatnpe]88,rehaM.M,zessa –Programmation concurrente contrainte [V. Sarasvat, 90] –95r,iett]Conttesdraingasetepy.FoPuˆ[r 1.2Historiquedelade´ductioncontrainte –58]ertGoe[enguou,JannaM,dugese,reuRe´rctiruoedr-oos ´ –,voknoroV.A,veraerhnrcKiH..&;C86nooccuit´Ddeegty[A.Dintentra, M. Rusinowitch, 90] –H[eemoC.s-od´tro,9on1]´etionorCompl –plom9t2i]´eC,siuhnew,oibuR.AqusibaoneuNiR.e[ –euossaqi´needrnoStraiesbt´eg94]naG.gniztere,.laersdso´etilu[Hon –Model-checking modulo [A. Podelski, 95] –SAT modulo theories [R. Nieuwenhuis et al.] 1.3 PROLOG Programmation logique pure contrainte :

A←−Ckφ←−A 0 , C 0 kφ 0 ←−C, C 0 kφ∧φ 0 ∧ A . =A 0 ´ Eliminer←−Ckφsiφest insatisfiable ←−kφ RetournerSol(φ) siφest satisfiable ? ,PˆoiCaltLogojechcreedeRmmnueloCqutimaornfnIeechlcaSeduaetalpudeya,rP ´ CNRS,EcolePolytechnique,INRIA,Universit´eParis-Sud.

1.4Ing´edients –ificationntesd’unsa´eitaleg’´sdoniartnocsee´lleppntestraisconlecnitnoojedcsostn –les substitutions ne sont pasapiqplee´usccaslumuiamapcre´secnitnoojon logique : on les diraire´hsee´t. –umucitaledno-nocogirhtemed´dcesiionduvided’uneacnitssce´ealund’´e traintes ´it´ed’unalgorithmedere´solutiond’uneaccumulationdecontraite –necess n s –oStecontraindemrenu’osseofsuouet´erntilusron 1.5 PROLOG II –naegemtnhCnis.edasiaenisfinbrertita´epromed,lonniamodudretni’de –Danomaiscedl,enqe´’itaunof(f(x)) =f . (x) a pour unificateur principal l’arbreinfinipointfixedel’´equation x . =f(x). –Cahocedartnetnievasemngtdenanulgegacita´rderoducintndupctio6 . = et duquantificateurexistentielpourl’e´liminer. –Avec une signature ou 0 etsuccsont les deux seuls symboles, la contrainte ` x6 . = 0 a pour solution la contrainte∃y x=S . (y). –La contrainte6 . zest en forme normale : l’ensemble des solutions ne peut x= plusˆetred´ecritparunensemblefinidesubstitutions. 1.6 CHIP –Nouveau changement du domaine d’interpretation : les domaines finis comme ´ {bleu, blanc, rouge}. –Nouvealudtnemegnahcuantaitronecedagngdocunirtce’lsevacats´edideprtion utilesenpratiquepourl’expressiondeprobl`emesdansdesdomainesd’application vari´es,commelepr´edicatAlldif f erent(x). –,ntmecenannodro’d,noitanificeplaon,dcatilaolse’d`lmerpboppAacilnoitxuas etc. –peOnsle,conmeome´rpitati’dsretnsdomaineed’autrerurpnerdtuibneˆs r´eelspourlescalculsfinanciers. 1.7De´ductioncontrainte R´esolutionetFactorisationcontraintespourdesclausesquelconques: +A∨Ckφ−A 0 ∨C 0 kφ 0 C∨C 0 kφ∧φ 0 ∧A=A . 0 +A∨+A 0 ∨Ckφ +A∨Ckφ∧ A . =A 0 ´ EliminerCkφsiφest insatisfiable ✷kφ RetournercuSesc`siφest satisfiable

2

1.8D´eductioncontrainte,suite Re´solutionetFactorisationordonne´escontraintes:

+A∨Ckφ−A 0 ∨C 0 kφ 0 C∨C 0 kφ∧φ 0 ∧ A . =A 0 ∧A > C∧A 0 > C 0 +A∨+A 0 ∨Ckφ +A∨Ckφ∧A= . A 0 ∧A > C ´ EliminerCkφsiφest insatisfiable ✷kφ Retourners`eccSusiφest satisfiable 1.9D´eductioncontrainte,suite –`leeg’isd´enfCnced´ere’infemedeueenbttoonesncre`tsysudritrapa`s es r re´solutionetfactorisationordonne´esentransformantlesconditionsd’application en contraintes. –dellsysume`tetbneeloso’tbeuss`apaientdecertirocaLudetl´mpegr`esed d’origineparsimulationdesd´erivationsdelaclausevidedansl’anciencalcul par le nouveau. –´h’Ltiredegaocserantteinucsarsoufne´edissetuercneunilistestde satisfia- bilite´qui´economiselecalculdesunificateurs. –ppsaxiroonrdeen´rapmosiatnemocalnreneecosLseni´f∀γ Aγ > Cγavec la conditionC6≥Aqui est plus prolifique.

1.10De´ductioncontrainte,suite –les contraintes sontsymboliques-dinterpr´et´ees,-ca`-erodnusnadHedeniam brand. –arrI.reuopld´moisel`ebl`amed´eprimeuproenddriqeubalespxiuelcavoLe ˆetreform´edecontraintesd’´egalite´s,d’ordre,d’appartenancea`deslangages rationnels d’arbres, ou d’une combinaison d’icelles. –elanLdecogageetniartndnepe´dsmelega´eall’dentogirhtemed´rseloution de contraintes. Il sera clos par conjonction, et par renommage des variables lie´ess’ilyena.Ilserasouventclosparquantificationexistentielle,etparfois parne´gation.Ilpourracomprendretoutlepremierordre.

1.11 R´ iture contrainte ecr ´ –Equation contrainte :l=rkφ ou`φteinrtpotsanleurtseocalartnquationvsraailbseed’le´l=r, lesymbole=e´tantconside´re´commutatif.

3

–Recriture contrainte : ´  s s l= − p r → kφ s[rσ] p s   l φ | σ σ p  es = r t lσ σ vraie i –`Rgeelinrantco:te l→rkφsilφrφ l→rkφ∧lr en internalisant le testlσrσ. 1.12Strate´giesdesuperposition –:euqisabnoitempl´Co g=dkφ l=rkψ g[r] p =lkφ∧ψ∧g| p =l . Pouruner`egle,lasuperpositionpeuteˆtrerestreintea`sonmembregauche. –ubstitutionsissuseLessopispureostnitnonsdaeuligl`esrlesapte,sesselsnad d’inf´erencesant´erieures. –omCe´lpnoitis´aboedurq onnee : g=dkφ l=rkψ g[r] p . =dkφ∧ψ∧g| p =l . ∧gd∧lr –ete`?scsellpmot-elssonegleesr`C 1.13R´ecritureordo-sort´ee[OBJ] sort s, t subsorts s<t op a : s op b, c : t op f : t→t var x : s rule f(x)→b rule a→c Les deux expressionsbetf(ctnemilavesedffidtso)syntaxntueiq´erentes, maisb←−f(a)−→f(c). Unepairecritiquecache´etuelaconfluence. Quelleestlanotiondere`glecontrainte? 2 Logique et Contraintes 2.1 Logique et Contraintes 2.2Syst`emedecontraintes –VocabulaireL C ro´mdeu’fensneblemF C de symboles de fonction,Xde symboles de variables, etR C de symboles de relations. 4