Redigerer Unifikasjon (avsnitt)

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