Unifikace nám dnes připadá samozřejmá, byla však v rámci logiky objevena teprve v roce 1965 Johnem Alanem Robinsonem a původně sloužila pouze ke strojovému dokazování tvrzení. J.A.Robinson popsal první (nepříliš efektivní) algoritmus syntaktické unifikace, jejž sám používal pro vytváření instancí termů v predikátové logice (viz předchozí příspěvek o rezoluci).
V informatice byla pravděpodobně poprvé použita v roce 1969 Alainem Colmerauerem v jeho slavném (aspoň pro lidi zabývající se umělou inteligencí) programovacím jazyce Q-systémy (Systèmes Q, doporučuji k přečtení Les systèmes Q ou un formalisme pour analyser et synthétiser des phrases sur ordinateur; pokud studujete či pracujete na MFF UK, někde se tam povaluje český překlad). Opravdu známou se stala ale až použitím v Prologu (jejž má „na svědomí“ také Alain Colmerauer).
V algebře termů je unifikátor s a t taková substituce σ, že platí sσ=tσ. Pokud nějaká taková existuje, je unifikátorů nekonečně mnoho. Proto se zavádí pojem nejobecnějšího unifikátoru: σ je nejobecnější unifikátor s a t, pokud pro každý unifikátor τ termů s a t platí, že τ=σθ pro nějaké θ. Je-li t term, nazývá se tσ instancí t. Je-li t instancí s, píšeme s≼t. (Je snadné nahlédnout, že z algebraického pohledu unifikátory dvou termů tvoří polosvaz a tedy komutativní idempotentní pologrupu.)
Výše popsaná tzv. syntaktická unifikace je dobře známá např. z Prologu. Termy s=f(x,b) a t=f(a,y) jsou unifikovatelné, protože substituce σ={x↦a, y↦b} splňuje sσ=tσ. Unifikace je rozhodnutelná a dokonce existuje lineární algoritmus pro výpočet nejobecnějšího unifikátoru. Pokud dovolíme proměnné i na místě funkčních symbolů, jedná se o unifikaci vyššího řádu.
Speciálním případem je v umělé inteligenci unifikace rámců (v pojetí Minského). Rámce se většinou formalizují jako AVM (attribute-value matrix) nebo jako funkce a slouží k reprezentaci znalostí. Například [a:1] a [b:2] jsou unifikovatelné a výsledkem je [a:1,b:2] (neboli funkce f(a)=1, f(b)=2), tedy v tomto případě sjednocení. Naopak [a:1] a [a:2] unifikovatelné nejsou, protože pokud f(a)=1 a f(a)=2, relace f není funkcí. Výhodou práce s rámci je, že si vystačíme bez proměnných. V rámci algebry tvoří rámce komutativní idempotentní monoid s absorbujícím prvkem (jenž reprezentuje kontradikci). Je snadné dokázat, že polosvaz tvořený rámci je distributivní, a proto podle známého tvrzení existuje pro každý rámec jeho jednoznačná dekompozice na ireducibilní prvky (x je ireducibilní, pokud pro každé y platí y≼x→y∈{1,x}).
Celé to zní poněkud abstraktně, ale kromě umělé inteligence se rámce úspěšně uplatňují například ve formální a aplikované lingvistice ve spojení s Chomského bezkontextovými gramatikami (viz např. na Wikipedii podrobně popsané formalismy LFG a HPSG).
Relativně nedávno začala být zkoumána tzv. E-unifikace, což je unifikace vzhledem k nějaké rovnostní teorii. Speciálním případem je např. AC-unifikace, tedy taková, jež připouští asociativitu a komutativitu (některých) funkčních symbolů. Jednoduchým příkladem je elementární aritmetika. Například (axiomaticky) x+y=y+x, a tedy oba výrazy mají různé konkrétní syntaktické stromy, ale pouze jeden abstraktní. E-unifikace je obecně nerozhodnutelná (pokud je množina rovnostních axiomů konečná, je semirozhodnutelná). Pro některé (například konfluentní) rovnostní teorie je možné zkonstruovat orientovaný přepisovací systém a získat tak relativně efektivní unifikační algoritmus. Je zajímavé, že narozdíl od syntaktické unifikace mohou mít dva termy více (někdy i nekonečně mnoho) navzájem nezávislých unifikátorů. Uvažujeme-li například AC-unifikaci, mají f(x,y) a f(a,b) dva unifikátory: {x↦a, y↦b} a {x↦b, y↦a}.
Unifikaci lze poměrně snadno implementovat třeba v Javě či C# a využít pro nedeterministické výpočty. V C++ pro tyto účely existuje např. knihovna Castor.
ČLÁNKY DO MAILU