Unifikasjon

Opprydning: Denne artikkelen trenger en opprydning for å oppfylle Wikipedias kvalitetskrav. Du kan hjelpe Wikipedia ved å forbedre den.

Språkvask: Teksten i denne artikkelen kan ha behov for språkvask for å oppnå en høyere standard. Om du leser gjennom og korrigerer der nødvendig, kan du gjerne deretter fjerne denne malen.

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 ² og Y ³ unifiseres til Z⁶ ved å gjøre substitusjonene X = Z³ og Y = Z².

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 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:

1. 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.
2. To atomer kan kun unifiseres om de er identiske.
3. 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:

1. 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.
2. To type konstanter unifisres bare om de er av samme type.
3. 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.^[2] Det har vært mye videre utvikling innen unifikasjons teori siden det.^[3]

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.^[4]

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

• 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?.
• (en) Alex Sakharov, Unification i MathWorld.