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[1][rediger | rediger kilde]
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[rediger | rediger kilde]
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.[2] Det har vært mye videre utvikling innen unifikasjons teori siden det.[3]
Høyere ordens unifikasjon[rediger | rediger kilde]
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]
Eksempler på unifikasjon[rediger | rediger kilde]
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[rediger | rediger kilde]
- ^ Russell, Norvig: Artificial Intelligence, A Modern Approach, p. 277
- ^ "A Unification Algorithm for Typed Lambda-Calculus", Gerard P. Huet, Theoretical Computer Science 1 1975), 27-57[død lenke]
- ^ "30 Years of Higher-Order Unification", Gérard Huet, TPHOL 2002, INRIA
- ^ Claire Gardent, Michael Kohlhase, Karsten Konrad, A multi-level, Higher-Order Unification approach to ellipsis (1997). Link[død lenke]
Litteratur[rediger | rediger kilde]
- 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.