Unifikasjon

Innen matematisk logikk, spesielt anvendt innen informatikk, er en
unifikasjon av to termer en sammenslåing (av typen en finner for delvis ordnede
set) med hensyn til en spesialiserings orden. Det vil si, vi antar en preorden
på et sett av termer, der t* ≤ t betyr at t* er utledet fra t ved
å substituere en eller flere termer for en eller flere frie variabler i t. Unifikasjonen av
u for s og t, om den eksisterer, er en term som er en substitusjons instans
av både s og t. Om en felles substitusjons instans for s og t også er en
instans for u, u så kalles den for en minimal unifikasjon.

For eksempel, kan polynomene, X 2 og Y 3 unifiseres
til Z6 ved å gjøre substitusjonene X = Z3 og Y =
Z2.

Definisjon av unifikasjon for første ordens logikk

La p og q være setninger i første ordens logikk.

UNIFISER(p,q) = U der subst(U,p) = subst(U,q)

Her vil subst(U,p) si resultatet av å utføre substitusjonen U på setningen p. Da kalles U en
unifiserer for p og q. Unifikasjonen av p og q er resultatet av å anvende
U på begge setningene.

La L være et sett av setninger, for eksempel, L = {p,q}. En unifiserer U kalles mest generell unifiserer for L om, for alle unifiserere U' for L, så eksisterer det en substitusjon s slik at å anvende s på resultatet av å anvende U på L gir samme resultat som å anvende U' på L:
subst(U',L) = subst(s,subst(U,L)).

Unifikasjon i logikk programmering og type teori

Unifikasjon er en av hovedideene bak  logikk programmering, kanskje best kjent
gjennom språket Prolog. Det representerer mekanismen for binding av innholdet av variabler
og kan sees på som en slags en gangs tilordning. I Prolog, er denne operasjonen angitt av
likhets symbolet =, men blir også utført ved instansiering av variabler
(se under). Det blir også brukt i andre språk ved bruk av likhets symbolet
=, men også i sammen med andre operasjoner som
+, -, *, /. Type slutnings algoritmer er
typisk basert på unifikasjon.

I Prolog:
 En variabel som ikke er instansiert—dvs. ikke har noen tidligere unifikasjoner utført på den—kan unifiseres med et atom, en term, eller en annen ikke instansiert variabel og blir dermed et alias for det. I mange moderne Prolog dialekter og i første ordens logikk, kan ikke en variabel unifiseres med en term som inneholder det den unifiseres med; Dette er den såkalte forekomst-sjekken.
 To atomer kan kun unifiseres om de er identiske.
 liknende, en term kan unifiseres med en annen term om de på topp nivå har funksjons symboler og ariteter for termene som er identiske og om parametrene kan unifisereres simultant. Legg merke til den rekursive atferden.

I type teori, er de analoge uttalelsene:
 Hvilken som helst type variabel unifiseres med hvilken som helst type uttrykk, og er instansiert til det uttrykket. En spesifikk teori vil kanskje innskrenke denne regelen med en forekomst sjekk.
 To type konstanter unifisres bare om de er av samme type.
 To type konstruksjoner unifiserer bare om de er resultatet av anvendelser av samme type konstruktør og alle deres komponenters typer unifiserer rekursivt.

På grunn av unifikasjonens deklarative natur, spiller rekkefølgen av sekvensen av unifikasjoner(vanligvis)
ingen rolle.

Merk at unifikasjon av termer i første ordens logikk, unifiseres på lignende måte som for Prolog termer.

Den franske informatikeren Gérard Huet publiserte en algoritme for unifikasjon i simply typed lambda calculus i 1973.  Det har vært mye videre utvikling innen unifikasjons teori siden det.

Høyere ordens unifikasjon

En av de mest innflytelsesrike teoriene for ellipser(i lingvistisk sammenheng) er at
ellipser kan representeres av frie variabler der verdiene så avgjøres ved å bruke
Høyere ordens unifikasjon (HOU). For eksempel, den semantiske representasjonen av "Jan liker
Mari og Peter gjør det også" er liker(j,m)&R(p) og verdien av R (den semantiske representasjonen
av ellipsen) avgjøres av likningen liker(p,m) = R(p). Prosessen for å løse slike likninger
kalles Høyere ordens unifikasjon.

Eksempler på unifikasjon

I Prolog, av konvensjon, begynner atomer med små bokstaver.

 A, A : Unifikasjon lykkes (tautologi)
 A, B, abc : Både A og B unifiseres med atomet abc
 abc, B, A : Som over (unifikasjon er symmetrisk)
 abc, abc : Unifikasjon lykkes, like atomer
 abc, xyz : Unifikasjon feiler, kan ikke unifisere ulike atomer
 f(A), f(B) : A unifiseres med B
 f(A), g(B) : Unifikasjon feiler, ulike funksjoner så termer er ulike
 f(A), f(B, C) : Unifikasjon feiler, termer har ulik aritet
 f(g(A)), f(B) : Unifiserer B med termen g(A)
 f(g(A), A), f(B, xyz) : Unifiserer A med atomet xyz og B med termen g(xyz)
 A, f(A) : Uendelig unifikasjon, A unifiseres med f(f(f(f(...)))). I første ordens logikk og i mange moderne Prolog dialekter er dette ulovlig (og hindres av forekomst sjekken)
 A, abc, xyz, X: Unifikasjon feiler, finnes ingen unifikasjon som gjør A = abc =X = xyz

Referanser

Litteratur
 F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.
 F. Baader and W. Snyder, Unification Theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447?533. Elsevier Science Publishers, 2001.
 Joseph Goguen, What is Unification?.
 

Logikk