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 $E ={l 1 ≐ r 1, ..., l n ≐ r n}$ jednačina koje treba rešiti, gde su $l i, r i$ u skupu $T$ č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

^ Dowek, Gilles (1. 1. 2001). „Higher-order unification and matching”. Handbook of automated reasoning. Elsevier Science Publishers B. V. стр. 1009—1062. ISBN 978-0-444-50812-6. Архивирано из оригинала 15. 5. 2019. г. Приступљено 15. 5. 2019.

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" Архивирано 2019-05-15 на сајту Wayback Machine. In Handbook of Automated Reasoning.
Franz Baader and Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press.
Franz Baader and de (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 . "Unification Theory". In Claude Kirchner (editor) Unification. Academic Press. 1990. .
Kevin Knight (март 1989). „Unification: A Multidisciplinary Survey” (PDF). ACM Computing Surveys. 21 (1): 93—124. CiteSeerX 10.1.1.64.8967 . S2CID 14619034. doi:10.1145/62029.62030.
Gérard Huet and Derek C. Oppen (1980). "Equations and Rewrite Rules: A Survey". Technical report. Stanford University.
Raulefs, Peter; Siekmann, Jörg; Szabó, P.; Unvericht, E. (1979). „A short survey on the state of the art in matching and unification problems”. ACM SIGSAM Bulletin. 13 (2): 14—20. S2CID 17033087. doi:10.1145/1089208.1089210.
Claude Kirchner and Hélène Kirchner. Rewriting, Solving, Proving. In preparation.

[1] Dowek, Gilles (1. 1. 2001). „Higher-order unification and matching”. Handbook of automated reasoning. Elsevier Science Publishers B. V. стр. 1009—1062. ISBN 978-0-444-50812-6. Архивирано из оригинала 15. 5. 2019. г. Приступљено 15. 5. 2019.

[1]