Unificació (informàtica)

En lògica i informàtica, específicament en el raonament automatitzat, la unificació és un procés algorítmic de resolució d'equacions entre expressions simbòliques, cadascuna de la forma Left-hand side = Right-hand side. Per exemple, utilitzant x, y, z com a variables i prenent f com una funció no interpretada, el conjunt d'equacions singletó { f (1, y ) = f ( x ,2) } és un problema d'unificació sintàctic de primer ordre que té la substitució { x ↦ 1, y ↦ 2 } com a única solució.

Les convencions difereixen sobre quins valors poden assumir les variables i quines expressions es consideren equivalents. En la unificació sintàctica de primer ordre, les variables van sobre termes de primer ordre i l'equivalència és sintàctica. Aquesta versió d'unificació té una "millor" resposta única i s'utilitza en la programació lògica i la implementació de sistemes de tipus de llenguatge de programació, especialment en algorismes d'inferència de tipus basats en Hindley-Milner. En la unificació d'ordre superior, possiblement restringida a la unificació de patrons d'ordre superior, els termes poden incloure expressions lambda i l'equivalència és fins a la reducció beta. Aquesta versió s'utilitza en assistents de prova i programació lògica d'ordre superior, per exemple Isabelle, Twelf i lambdaProlog. Finalment, en la unificació semàntica o e-unificació, la igualtat està subjecta a coneixements de fons i les variables varien en una varietat de dominis. Aquesta versió s'utilitza en solucionadors SMT, algorismes de reescriptura de termes i anàlisi de protocols criptogràfics.

Definició formal

Un problema d'unificació és un conjunt finit E={I1=r1....In=rn} d'equacions a resoldre, on l_i, r_i es troben en el conjunt $T$ de termes o expressions. Depenent de quines expressions o termes es permeten que es produeixin en un conjunt d'equacions o problema d'unificació, i quines expressions es consideren iguals, es distingeixen diversos marcs d'unificació. Si en una expressió es permeten variables d'ordre superior, és a dir, variables que representen funcions, el procés s'anomena unificació d'ordre superior, en cas contrari, unificació de primer ordre. Si cal una solució per fer els dos costats de cada equació literalment iguals, el procés s'anomena unificació sintàctica o lliure, en cas contrari unificació semàntica o equacional, o unificació E, o unificació mòdul teoria.

Si el costat dret de cada equació està tancat (no hi ha variables lliures), el problema s'anomena coincidència (patró). El costat esquerre (amb variables) de cada equació s'anomena patró.

Aplicacions

Aplicació: unificació en programació lògica

El concepte d'unificació és una de les idees principals darrere de la programació lògica. Concretament, la unificació és un element bàsic de resolució, una regla d'inferència per determinar la satisfacció de la fórmula. A Prolog, el símbol d'igualtat = implica una unificació sintàctica de primer ordre. Representa el mecanisme d'enllaç del contingut de les variables i es pot veure com una mena d'assignació única.

Aplicació: inferència de tipus

Els algorismes d'inferència de tipus es basen normalment en la unificació, particularment en la inferència de tipus Hindley-Milner que s'utilitza pels llenguatges funcionals Haskell i ML. Per exemple, quan intenteu inferir el tipus de l'expressió Haskell True : ['x'], el compilador utilitzarà el tipus a -> [a] -> [a] de la funció de construcció de llista (:), el tipus Bool del primer argument True i el tipus [Char] de la segon argument ['x']. La variable de tipus polimòrfic a s'unificarà amb Bool i el segon argument [a] s'unificarà amb [Char]. a no pot ser Bool i Char al mateix temps, per tant, aquesta expressió no s'escriu correctament.

Aplicació: unificació d'estructura de característiques

La unificació s'ha utilitzat en diferents àrees de recerca de la lingüística computacional.