În informatică și logică , unificarea este un proces algoritmic care, având în vedere doi termeni, găsește o substituție care aplicată celor doi termeni îi face identici. De exemplu, și poate fi făcut identic prin substituție și , care dă atunci când este aplicat fiecăruia dintre acești termeni termenul . Cu alte cuvinte, unificarea este rezoluția unei ecuații în algebra de termeni (unificare sintactică) sau într-o algebră coeficientă printr-un set de identități (unification modulo une theory); soluția ecuației este înlocuirea care face ca cei doi termeni să fie identici și care se numește unificator. Unificarea are aplicații în inferența de tip , programarea logică , dovada automată a teoremelor , sisteme de rescriere , procesarea limbajului natural .
Adesea, suntem interesați de unificarea sintactică unde este necesar ca termenii obținuți prin aplicarea unificatorului să fie sintactici egali, ca în exemplul de mai sus. De exemplu, problema de unificare sintactică cu datele și nu are nicio soluție. Model de potrivire (sau model de potrivire ) este o restricție de unificare unde unificator este aplicată numai unul dintre cei doi termeni. De exemplu, și sunt făcute egale prin substituție .
Sfârșitul articolului prezintă, de asemenea, modulul de unificare o teorie , care este cazul în care cineva are cunoștințe suplimentare despre funcții (de exemplu, este comutativ).
Primul cercetător care a evocat un algoritm de unificare este Jacques Herbrand în teza sa din 1930. Este vorba despre un algoritm nedeterminist pentru a unifica doi termeni. Herbrand era interesat să rezolve ecuații. În 1960, Prawitz și Voghera au generalizat calculul propozițional la formule neinstanțiate de prim ordin sau cel puțin prin instanțierea lor minimă. Unificarea a fost redescoperită în 1963, dar articolul care o descrie a fost publicat abia în 1965, de John Alan Robinson ca parte a metodei sale de rezolvare în demonstrație automată . Potrivit lui Baader și Snyder, Knuth și Bendix în 1970 au introdus conceptul de „cea mai generală substituție” în lucrarea lor privind confluența locală a unui sistem de rescriere. Cu un an înainte de publicarea articolului lui Robinson, în 1964, Guard a studiat independent problema unificării sub numele de potrivire .
Algoritmul original al lui Robinson este ineficient deoarece rulează în timp exponențial și necesită o cantitate exponențială de memorie . Robinson a scris apoi o notă în 1971 în care a prezentat o reprezentare mai concisă a termenilor. Algoritmul folosește apoi un spațiu de memorie polinomială. Boyer și Moore oferă, de asemenea, un algoritm care utilizează un spațiu de memorie polinomială în timp exponențial în cel mai rău caz. Venturini-Zilli introduce un sistem de marcare astfel încât algoritmul Robinson să ruleze în timp pătratic, în cel mai rău caz, în dimensiunea termenilor. Huet lucrează la unificarea ordinii superioare și îmbunătățește timpul de execuție al algoritmului sintactic de ordinul întâi: algoritmul său este cvasiliniar. Alți cercetători au prezentat algoritmi cvasi-liniari.
Un pas important este descoperirea algoritmilor liniari în 1976 de către Martelli și Montanari, Paterson și Wegman și Huet . Deoarece articolele lui Paterson și Wegman sunt scurte, Dennis de Champeaux a explicat din nou ideea algoritmului în 1986.
În 1982, Martelli și Montanari au prezentat un algoritm aproape liniar, dar mai eficient în practică.
În 1984, Dwork și colab. arată că unificarea este P-completă , ceea ce înseamnă că a priori unirea este dificil de paralelizat. În schimb, problema potrivirii modelelor este în NC , adică ușor de paralel.
Prolog a contribuit mult și la popularizarea sa . Au fost propuși algoritmi specifici pentru termenii anumitor teorii, numite și unificare ecuațională (în special asociativă și comutativă de către Stickel) (a se vedea mai sus).
O problemă de unificare poate fi prezentată ca referință a doi termeni, sau apoi ca o ecuație, sau ca un set de termeni care urmează să fie unificați, sau ca un set de perechi de termeni sau ca un set de ecuații. Problema unificării are o soluție deoarece înlocuirea (adică înlocuirea) termenului pentru variabilă și a termenului pentru variabilă , în ambii termeni și dă același termen . Pe de altă parte, problema unificării nu are nicio soluție și nici problema unificării .
O problemă de unificare poate avea un număr infinit de soluții. De exemplu, un număr infinit de soluții: , , etc. Dintre toate aceste soluții, expunem așa-numitele soluții principale, deoarece permit construirea tuturor celorlalte soluții: este conceptul de soluție principală sau cel mai general unificator (cel mai general unificator, mgu).
În primul rând, se spune că o soluție a unei probleme de unificare este mai generală decât o soluție , dacă se obține prin substituirea termenilor cu variabile în . De exemplu, dacă luăm în considerare problema unificării , atunci soluția este mai generală decât soluția care se obține prin înlocuirea termenului cu variabila în . La fel, soluția este mai generală decât soluția , care se obține prin înlocuirea termenului cu variabila din soluție .
Se spune că o soluție a unei probleme de unificare este principală dacă este mai generală decât toate soluțiile acestei probleme, adică dacă se obține orice soluție prin înlocuirea termenilor cu variabile în . În acest exemplu, soluția este o soluție primară la problemă .
Principal Soluția Teorema exprimă că , dacă o problemă de unificare are o soluție, atunci acesta are o soluție principală. Un algoritm de unificare calculează o soluție principală sau eșuează dacă termenii nu sunt unifiabili.
Tabelul următor oferă exemple de probleme de unificare. În plus, oferim, de asemenea, în coloana din stânga, exemple cu sintaxa Prolog: o variabilă începe cu o majusculă, constantele și simbolurile funcției încep cu o literă mică. Pentru notațiile matematice, x, y, z sunt variabile , f, g sunt simboluri funcționale și a, b sunt constante.
Evaluare prolog | Notatie matematica | Soluție (principală) | Explicaţie |
---|---|---|---|
a = a | { a = a } | {} | Reușește |
a = b | { a = b } | a eșuat | a și b sunt simboluri ale constantelor diferite. |
X = X | { x = x } | {} | Reușește |
a = X | { a = x } | { x ↦ a } | x este unificat cu constanta a |
X = Y | { x = y } | { x ↦ y } | x este unificat cu y |
f(a,X) = f(a,b) | { f ( a , x ) = f ( a , b )} | { x ↦ b } | Simbolurile funcției sunt aceleași. x este unificat cu constanta b |
f(a) = g(a) | { f ( a ) = g ( a )} | a eșuat | f și g sunt simboluri funcționale diferite |
f(X) = f(Y) | { f ( x ) = f ( y )} | { x ↦ y } | x este unificat cu y |
f(X) = g(Y) | { f ( x ) = g ( y )} | a eșuat | f și g sunt simboluri funcționale diferite |
f(X) = f(Y,Z) | { f ( x ) = f ( y , z )} | a eșuat | Simbolul funcției f are arity 1 în partea stângă și arity 2 în partea dreaptă. |
f(g(X)) = f(Y) | { f ( g ( x )) = f ( y )} | { y ↦ g ( x )} | y este unificat cu g (x) |
f(g(X),X) = f(Y,a) | { f ( g ( x ), x ) = f ( y , a )} | { x ↦ a , y ↦ g ( a )} | x este unificat cu constanta a , iar y este unificat cu g (a) |
X = f(X) | { x = f ( x )} | a eșuat | eșuează deoarece x apare în f (x). Testul de membru al lui x în termenul corect f (x) se numește check verificare . Există implementări ale Prolog în care nu există nici o verificare a evenimentelor . Pentru acesta din urmă, unificăm x cu termenul infinit x=f(f(f(f(...)))). |
X = Y, Y = a | { x = y , y = a } | { x ↦ a , y ↦ a } | x și y sunt unificate cu constanta a |
a = Y, X = Y | { a = y , x = y } | { x ↦ a , y ↦ a } | x și y sunt unificate cu constanta a |
X = a, b = X | { x = a , b = x } | a eșuat | a sunt b sunt simboluri ale constantelor diferite. x nu se poate uni cu ambele în același timp. |
Modelul de potrivire este restricția de unificare în care, în fiecare ecuație, variabile apar numai pe termen stânga. De exemplu, problema este o problemă de filtrare, deoarece termenul nu conține variabile. Filtrarea este utilizată în limbaje funcționale precum Haskell, Caml, LISP.
În cazul filtrării, algoritmul Martelli și Montanari este simplificat.
Alegem o ecuație în sistem.
Dacă această ecuație are forma
îl înlocuim cu ecuațiile , ... și rezolvăm sistemul obținut.
Dacă această ecuație are forma
unde și sunt diferite simboluri, eșuăm.
Dacă această ecuație are forma
înlocuim termenul cu variabila din restul sistemului, rezolvăm sistemul obținut, care oferă o soluție și returnăm soluția .
Unificarea este ceea ce distinge cel mai mult limbajul de programare Prolog de alte limbaje de programare .
În Prolog , unificarea este asociată cu simbolul „=” și regulile sale sunt după cum urmează:
Datorită naturii sale declarative, ordinea într-o secvență de unificare nu joacă un rol.
Algoritmul Robinson din 1965 a fost reformulat de Corbin și Bidoit în 1983, apoi îmbunătățit de Ruzicka și Prívara în 1989, apoi preluat de Melvin Fitting în 1990 ca algoritm nedeterminist, prezentare preluată și de Apt în 1996. prezentați și această versiune. Algoritmul ia ca intrare doi termeni t1 și t2 pentru a se uni, dat sub forma a doi copaci. Se bazează pe noțiunea de dezacord chiar, care este datele unui subterm de t1 și al unui subterm de t2, ale cărui noduri din copacii t1 și t2 sunt în aceeași poziție față de rădăcini, dar cu etichete diferite. Un astfel de dezacord uniform este simplu dacă unul dintre sub-termeni este o variabilă care nu apare în celălalt sub-termen. Algoritmul calculează o substituție, inițial goală. Algoritmul continuă atâta timp cât substituția nu face ca cei doi termeni să fie egali. El alege într-un mod nedeterminist un dezacord uniform . Dacă nu este simplu, algoritmul eșuează. În caz contrar, îmbogățește substituția.
Algoritmul lui Robinson pseudo-cod entrée : deux termes t1, t2 sortie : vrai si les termes sont unifiables, non sinon fonction unifier(t1, t2) σ := id tant que σ(t1) différent de σ(t2) choisir une disagreement pair (w, u) si (w, u) est simple soit γ la substitution donnée par (w, u) σ := σγ sinon retourner faux; retourner vraiÎn 1982, Martelli și Montanari au descris un algoritm sub forma unui set de reguli care transformă un set de ecuații. Algoritmul este prezentat în cărți educaționale. Este similar cu algoritmul propus de Herbrand în teza sa. Potrivit lui Baader și Snyder, un algoritm sub forma unui set de reguli eliberează conceptele esențiale și permite să demonstreze corectitudinea mai multor algoritmi practici în același timp.
Ne oferim un set finit de ecuații G = { s 1 ≐ t 1 , ..., s n ≐ t n } unde s i și t i sunt termeni de ordinul întâi. Obiectivul este de a calcula cea mai generală substituție. Apoi, aplicăm următoarele reguli setului G până la epuizare:
G ∪ { t ≐ t } | ⇒ | G | elimina | |
G ∪ { f ( s 1 , ..., s k ) ≐ f ( t 1 , ..., t k )} | ⇒ | G ∪ { s 1 ≐ t 1 , ..., s k ≐ t k } | pană | |
G ∪ { f (t⃗) ≐ x} | ⇒ | G ∪ { x ≐ f (t⃗)} | a schimba | |
G ∪ { x ≐ t } | ⇒ | G { x ↦ t } ∪ { x ≐ t } | dacă x ∉ vars ( t ) și x ∈ vars ( G ) | înlătura |
Regula de șters elimină o ecuație t ≐ t , adică unde termenii părții stângi și ai părții drepte sunt aceiași. Regula de descompunere elimină o ecuație de forma f ( s 1 , ..., s k ) ≐ f ( t 1 , ..., t k ) și o înlocuiește cu ecuațiile s 1 ≐ t 1 , ..., s k ≐ t k . Regula de schimb orientează ecuațiile astfel încât variabila x să fie în stânga. În prezența unei ecuații x ≐ t în care variabila x nu apare în termenul t, regula elimină înlocuiește aparițiile lui x cu t în celelalte ecuații.
Următoarele reguli sunt, de asemenea, adăugate ca optimizare:
G ∪ { f (s⃗) ≐ g (t⃗)} | ⇒ | ⊥ | dacă f ≠ g sau k ≠ m | conflict |
G ∪ { x ≐ f (s⃗)} | ⇒ | ⊥ | dacă x ∈ vars ( f (s⃗)) | verifica (apare-verifica) |
Dacă setul conține o ecuație de forma f (s⃗) ≐ g (t⃗) unde f și g nu sunt aceleași simboluri funcționale sau dacă numărul argumentelor nu este același ( k ≠ m ) atunci regula conflictului determină procesul de unificare a esua. Regula apare-verificare , pe de altă parte, face ca unificarea să eșueze dacă setul conține o ecuație x ≐ f (s⃗) unde x apare în f (s⃗).
Algoritmul este în timp exponențial și necesită cel mult un spațiu de memorie exponențial dacă termenii sunt reprezentați prin arborii lor de sintaxă. Cu toate acestea, se poate utiliza un spațiu de memorie liniar numai dacă se reprezintă termenii prin grafice.
Prin implementarea algoritmului cu grafice, spațiul de memorie este liniar în mărimea intrării, chiar dacă timpul rămâne exponențial în cel mai rău caz. Algoritmul ia ca intrare doi termeni sub formă de grafice, adică un grafic aciclic în care nodurile sunt sub-termeni. În special, există un singur nod pentru fiecare variabilă (vezi figura din dreapta). Algoritmul returnează ca ieșire o substituție cea mai generală: este scris în loc în graficul reprezentând termenii folosind pointeri (în albastru în figura din dreapta). adică, pe lângă graficul care descrie structura termenilor (care sunt și indicii), avem indicatori particulari pentru a reprezenta substituția. Dacă x: = h (1) este înlocuirea curentă, x indică nodul corespunzător termenului h (1).
unde unifyLists unifică termenii a două liste:
entrée : deux listes de termes L, M sortie : vrai si les termes des listes sont deux à deux sont unifiables, non sinon fonction unifierlistes(L, M) etude de cas sur (L, M) ([], []): retourner vrai; ([], t::t') ou (t::t', []): retourner faux; (s::L', t::M'): si unifier(s, t) retourner unifierlistes(L', M') sinon retourner fauxunde find găsește sfârșitul unui șir:
entrée : un terme t sortie : le terme en bout de chaîne de t fonction find(t) si t n'est pas une variable retourner t sinon si t est déjà assigné à un terme u retourner find(u) sinon retourner tși unde o implementare naivă a "x apare în t" este dată de:
entrée : une variable x et un terme t sortie : vrai si la variable x apparaît dans le terme t, non sinon fonction apparaîtdans(x, t) etude de cas sur t y: retourner x = y f(L): retourner apparaîtdansliste(x, L) entrée : une variable x et une liste de termes L sortie : vrai si la variable x apparaît dans l'un des termes de L, non sinon fonction apparaîtdansliste(x, L) etude de cas sur L []: retourner faux t::L': si apparaîtdans(x, find(t)) retourner vrai sinon retourner apparaîtdansliste(x, L') Algoritm quadraticAlgoritmul prezentat în această subsecțiune se datorează lui Corbin și Bidoit (1983). Pentru a avea o complexitate pătratică, există două îmbunătățiri ale algoritmului anterior.
Testați dacă o variabilă apare într-un sub-termenImplementarea pentru a testa dacă o variabilă x apare într-un subterm t este a priori în timp exponențial. Ideea este de a evita traversarea acelorași noduri de mai multe ori. Marcăm nodurile vizitate ca într-o traversare a adâncimii graficului. Odată ce a fost efectuat un test de apartenență, nodurile trebuie să fie delimitate a priori. În schimb, acestea sunt marcate cu „ora curentă”. Apoi se adaugă un câmp la nodurile graficului pe care îl numim punch care conține „ora curentă”. Avem o variabilă globală „ora curentă” care este incrementată la fiecare test de membru.
Pentru a evita apelurile inutile la procedura care urmărește unificarea a doi termeni, sunt folosite indicii pentru toate nodurile și nu doar pentru variabile. Putem arăta că numărul de apeluri la procedura de unificare este O (| A |) unde | A | este numărul de arce din grafic. Procesarea internă folosește o cale de indicatori „găsiți” în O (| S |) unde | S | este numărul de vârfuri și un test de apartenență al unei variabile într-un termen care este O (| S | + | A |) = O (| A |) deoarece graficul este conectat. Deci algoritmul este destul de pătratic.
și
entrée : deux termes t1, t2 sortie : vrai si les termes sont unifiables, non sinon fonction unifier(t1, t2) t1 = find(t1); t2 = find(t2); si t1 = t2 retourner vrai; sinon etude de cas sur (t1, t2) (x, y): faire pointer x vers y retourner vrai; (x, t) ou (t, x): si x apparaît dans t retourner faux sinon faire pointer x vers t retourner vrai; (f(L), g(M)): si f = g faire pointer f(L) vers g(M) retourner unifierlistes(L, M) sinon retourner faux Algoritm cvasi-liniarAlgoritmul este inspirat din algoritmul pătratic din secțiunea anterioară. Testul dacă x apare în t nu mai este efectuat în timpul algoritmului, ci doar la sfârșit: la final, verificăm dacă graficul este aciclic. În cele din urmă, indicatoarele de substituție și „găsire” sunt implementate folosind o structură de date de găsire a Uniunii . Mai exact, păstrăm indicii în structură, dar avem și o structură anexă Union-find. În structura de date pentru găsirea Uniunii, clasele de echivalență conțin fie numai variabile, fie numai termeni complecși. Pentru a trece de la o variabilă la un termen complex, folosim orice indicatori care se află în grafic.
Pentru a construi un grafic dintr-un copac, parcurgem arborele și folosim un tabel de simboluri (implementat cu un tabel hash sau un arbore de căutare binar) pentru variabile, deoarece trebuie să garantăm unicitatea nodului x pentru o variabilă x.
Teoria unificării modulo a , numită și (unificare ecuațională E-unificare, unificare în teorie) este extensia unificării sintactice în cazurile în care operatorii sunt supuși axiomelor, formând o teorie generală. Teoria E. este descrisă de un set de egalități universale. De exemplu, o teorie E poate conține identitatea în care variabilele și sunt implicit cuantificate universal și care spune că operatorul este comutativ. Prin urmare, deși termenii și nu sunt unifiabili din punct de vedere sintactic, aceștia sunt unifiabili E:
{ x ↦ b , y ↦ a } | |||
= | prin aplicarea substituției | ||
= | deoarece este comutativ. | ||
= | { x ↦ b , y ↦ a } | prin aplicarea substituției |
∀ u , v , w | u * (v * w) | = | (u * v) * w | LA | Asociativitatea * |
∀ u , v | u * v | = | v * u | VS | Comutativitatea lui * |
∀ u , v , w | u * (v + w) | = | u * v + u * w | D l | Distributivitate la stânga * peste + |
∀ u , v , w : | (v + w) * u | = | v * u + w * u | D r | Distributivitate corectă a * pe + |
∀ u : | u * u | = | tu | Eu | Idempotența * |
∀ u : | gol | = | tu | N l | n este lăsat element neutru al lui * |
tu : | A | = | tu | N r | n este un element neutru drept al lui * |
E-unificarea este decisă pentru o teorie E dacă există un algoritm pentru această teorie care se termină la fiecare intrare și rezolvă problema unificării E. Este semi-hotărâtor dacă există un algoritm care se termină pentru intrări care au o soluție și care pot face loop pentru ecuații fără o soluție.
E-unificarea este decisă pentru următoarele teorii:
E-unificarea este semi-decisivă pentru următoarele teorii:
Dacă ne plasăm într -o logică de ordin superior , adică dacă ne permitem să folosim variabile ca simboluri funcționale sau ca predicate, pierdem caracterul decisiv și unicitatea unificatorului atunci când acesta există. În cel mai rău caz, doi termeni pot avea chiar un infinit de unire diferit, în următorul sens: fie t și t ' două cuvinte care doresc să unifice, poate exista un set infinit U de unificare a lui t și t' astfel încât dacă σ și ρ sunt în U , atunci σ nu este mai general decât ρ și ρ nu este mai general decât σ.