U logici i računarstvu, posebno automatizovanom zaključivanju, unifikacija je algoritamski proces rešavanja jednačina između simboličkih izraza, svaki u obliku Leva strana = Desna strana. Na primer, koristeći x,y,z kao promenljive i uzimajući f kao neinterpretiranu funkciju, skup jednostrukih jednačina { f(1,y) = f(x,2) } je sintaksički problem objedinjavanja prvog reda koji ima zamenu { x ↦ 1, y ↦ 2 } kao njeno jedino rešenje.
Konvencije se razlikuju po tome koje vrednosti mogu da imaju promenljive i koji izrazi se smatraju ekvivalentnim. U sintaksičkom objedinjavanju prvog reda, promenljive su u opsegu članova prvog reda, a ekvivalentnost je sintaksička. Ova verzija objedinjavanja ima jedinstveni „najbolji“ odgovor i koristi se u logičkom programiranju i implementaciji tipskih sistema programskog jezika, posebno u Hindli–Milnerovim algoritmima za tipsko zaključivanje. U objedinjavanju višeg reda, moguće ograničenom na objedinjavanje paterna višeg reda, termini mogu uključivati lambda izraze, a ekvivalentnost je do nivoa beta redukcije. Ova verzija se koristi u pomoćnicima za proveru i logičkom programiranju višeg reda, na primer Isabelle, Twelf, i lambdaProlog. Konačno, u semantičkom objedinjavanju ili E-unifikaciji, jednakost je podložna osnovnom znanju i promenljive se kreću u različitim domenima. Ova verzija se koristi u SMT rešavačima, algoritmima za zamenu članova i analizi kriptografskih protokola.
Formalna definicija
Problem ujedinjenja je konačan skup jednačina koje treba rešiti, gde su u skupu članova ili izraza. U zavisnosti od toga koji izrazi ili članovi su dozvoljeni u skupu jednačina ili problemu objedinjavanja, i koji se izrazi smatraju jednakim, razlikuje se nekoliko okvira unifikacije. Ako su promenljive višeg reda, odnosno promenljive koje predstavljaju funkcije, dozvoljene u izrazu, proces se naziva objedinjavanje višeg reda, inače se radi o objedinjavanju prvog reda. Ako je potrebno rešenje da obe strane svake jednačine budu doslovno jednake, proces se naziva sintaksičko ili slobodno ujedinjenje, inače semantičko ili jednačinsko ujedinjenje, ili E-unifikacija, ili teorija unifikacije po modulu.
Ako je desna strana svake jednačine zatvorena (nema slobodnih promenljivih), problem se naziva podudaranje (paterna). Leva strana (sa promenljivima) svake jednačine se naziva patern.
Reference
Literatura
Franz Baader and Wayne Snyder (2001). "Unification Theory". In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers. Gilles Dowek (2001). . In Handbook of Automated Reasoning. Franz Baader and Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press. Franz Baader and (1993). "Unification Theory". In Handbook of Logic in Artificial Intelligence and Logic Programming. Jean-Pierre Jouannaud and Claude Kirchner (1991). "Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification". In Computational Logic: Essays in Honor of Alan Robinson. Nachum Dershowitz and Jean-Pierre Jouannaud, Rewrite Systems, in: Jan van Leeuwen (ed.), Handbook of Theoretical Computer Science, volume B Formal Models and Semantics, Elsevier, 1990, pp. 243–320 Jörg H. Siekmann . .
Gérard Huet and Derek C. Oppen (1980). "Equations and Rewrite Rules: A Survey". Technical report. Stanford University.
Claude Kirchner and Hélène Kirchner. Rewriting, Solving, Proving. In preparation.
Категорија:Једначине Категорија:Математичка логика Категорија:Теоријско рачунарство Категорија:Математичке структуре