Unifikáció

Unifikáció, vagy unification, a logika és a számítástechnika területén a két kifejezés összeegyeztethetőségének keresését jelenti. A kifejezések általában változókból, konstansokból és függvényjelekből álló fastruktúrák. Egy helyettesítés (substitution) megadja, hogy a változókat milyen kifejezésekkel kell felváltani. Két kifejezés akkor egyeztethető össze, ha létezik olyan helyettesítés, amely alkalmazva mindkét oldalon egyenlő kifejezést ad.

Az unifikáció célja egy olyan legáltalánosabb helyettesítés megtalálása, amely az egyik oldalon és a másikon alkalmazva is azonos eredményt ad. Ezt nevezik legáltalánosabb egyezésnek vagy legfőbb unifiernek (MGU, most General Unifier). Ha létezik MGU, minden más egyező helyettesítés ebből kiindulva áll elő.

Robinson elsőrendű unifikációs algoritmusa meghatározza, hogy két elsőrendű kifejezésre létezik-e MGU, és ha igen, azt megadja. Az algoritmus kifejezések bontásával, változók hozzárendelésével és az occurs-check nevű vizsgálattal dolgozik. Az occurs-check megakadályozza, hogy egy változó saját magába illessze, például x = f(x). Gyakorlatban egyes nyelvek vagy implementációk ezt a kontrollt mellőzik a hatékonyság érdekében, ami bizonyos problémákhoz vezethet.

Alkalmazások: logikai programozás (például Prolog), automatikus bizonyítás, típusinferencia a funkcionális nyelvekben (Hindley–Milner), szimbolikus számítás és természetes nyelv feldolgozás formális elemezése.

Variánsok közé tartozik az AC-unifikáció (asszociatív- és kommutatív elvek figyelembe vétele) és a higher-order unifikáció (lambda-kifejezésekre). A hagyományos elsőrendű unifikáció polinomiális időben megoldható és általában lineáris a bemenet nagyságától függően.