Redigerer Unifikasjon

{{Opprydning}}
{{Språkvask}}
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'' <sup>2</sup> og ''Y'' <sup>3</sup> unifiseres
til ''Z''<sup>6</sup> ved å gjøre substitusjonene ''X'' = ''Z''<sup>3</sup> og ''Y'' =
''Z''<sup>2</sup>.

==Definisjon av unifikasjon for første ordens logikk<ref>Russell, Norvig: Artificial
Intelligence, A Modern Approach, p. 277</ref>==

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 <code>=</code>, men blir også utført ved instansiering av variabler
(se under). Det blir også brukt i andre språk ved bruk av likhets symbolet
<code>=</code>, men også i sammen med andre operasjoner som
<code>+</code>, <code>-</code>, <code>*</code>, <code>/</code>. [[Type slutnings]] algoritmer er
typisk basert på unifikasjon.

I Prolog:
# En [[variabel (programmering)|variabel]] som ikke er instansiert&mdash;dvs. ikke har noen tidligere unifikasjoner utført på den&mdash;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 [[aritet]]er 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.<ref>[http://mathgate.infocebrown/notes/huet75.php "A Unification Algorithm for Typed Lambda-Calculus", Gerard P. Huet, Theoretical Computer Science 1 1975), 27-57]{{død lenke|dato=august 2017 |bot=InternetArchiveBot }}</ref>  Det har vært mye videre utvikling innen unifikasjons teori siden det.<ref>[http://pauillac.inria.fr/~huet/PUBLIC/Hampton.pdf "30 Years of Higher-Order Unification"], Gérard Huet, TPHOL 2002, [[INRIA]]</ref>

==Høyere ordens unifikasjon==

En av de mest innflytelsesrike teoriene for [[Elliptisk konstruksjon|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.<ref>Claire Gardent, Michael Kohlhase,
Karsten Konrad, A multi-level, Higher-Order Unification approach to ellipsis (1997).
[http://en.scientificcommons.org/48410 Link]{{Død lenke|dato=april 2021 |bot=InternetArchiveBot }}</ref>

==Eksempler på unifikasjon==

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

* ''A'', ''A'' : Unifikasjon lykkes ([[Tautologi (logikk)|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==
<references/>

==Litteratur==
* F. Baader and T. Nipkow, ''[https://web.archive.org/web/20051120123456/http://www4.informatik.tu-muenchen.de/~nipkow/TRaAT/ ''Term Rewriting and All That''].'' Cambridge University Press, 1998.
* F. Baader and W. Snyder, ''[http://lat.inf.tu-dresden.de/research/papers/2001/BaaderSnyderHandbook.ps.gz ''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]], ''[http://www-cse.ucsd.edu/~goguen/projs/sem.html ''What is Unification?''].''
* {{MathWorld| urlname=Unification | title=Unification | author=Alex Sakharov}}
{{Autoritetsdata}}

[[Kategori:Logikk]]