Unifikacija (informatika)
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 Шаблон:Math jednačina koje treba rešiti, gde su Шаблон:Math 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.[1]
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). "Higher-order Unification and Matching" Шаблон:Webarchive. In Handbook of Automated Reasoning.
- Franz Baader and Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press.
- Franz Baader and Шаблон:Ill (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 . Шаблон:Cite book.
- Шаблон:Cite journal
- Gérard Huet and Derek C. Oppen (1980). "Equations and Rewrite Rules: A Survey". Technical report. Stanford University.
- Шаблон:Cite journal
- Claude Kirchner and Hélène Kirchner. Rewriting, Solving, Proving. In preparation.