Изворни код странице Unifikacija (informatika)


U [[logic|logici]] i [[computer science|računarstvu]], posebno [[automated reasoning|automatizovanom zaključivanju]], '''unifikacija''' je algoritamski proces [[solving equations|rešavanja jednačina]] između simboličkih [[expression (mathematics)|izraza]], svaki u obliku ''Leva strana = Desna strana''. Na primer, koristeći ''x'',''y'',''z'' kao promenljive i uzimajući ''f'' kao [[uninterpreted function|neinterpretiranu funkciju]], skup [[Singleton (mathematics)|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 [[first-order terms|članova prvog reda]], a ekvivalentnost je sintaksička. Ova verzija objedinjavanja ima jedinstveni „najbolji“ odgovor i koristi se u [[logic programming|logičkom programiranju]] i implementaciji [[type system|tipskih sistema]] programskog jezika, posebno u [[Hindley–Milner|Hindli–Milnerovim]] algoritmima za [[type inference|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 (theorem prover)|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 solver|SMT rešavačima]], algoritmima za [[term rewriting|zamenu članova]] i analizi [[cryptographic protocol|kriptografskih protokola]].

== Formalna definicija ==

''Problem ujedinjenja'' je konačan skup {{math|1=''E''={{mset| ''l''<sub>1</sub> ≐ ''r''<sub>1</sub>, ..., ''l''<sub>''n''</sub> ≐ ''r''<sub>''n''</sub> }}}} jednačina koje treba rešiti, gde su {{math|''l''<sub>''i''</sub>, ''r''<sub>''i''</sub>}} u skupu <math>T</math> ''č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 [[function (mathematics)|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.<ref>{{cite book |last1=Dowek |first1=Gilles |title=Handbook of automated reasoning |date=1 January 2001 |publisher=Elsevier Science Publishers B. V. |isbn=978-0-444-50812-6 |pages=1009–1062 |url=http://www.lsv.fr/~dowek/Publi/unification.ps |chapter=Higher-order unification and matching |access-date=15 May 2019 |archive-date=15 May 2019 |archive-url=https://web.archive.org/web/20190515113555/http://www.lsv.fr/~dowek/Publi/unification.ps |url-status=dead }}</ref>

== Reference ==
{{reflist|}}

== Literatura ==
{{refbegin|30em}}
* [[Franz Baader]] and [[Wayne Snyder]] (2001). [https://web.archive.org/web/20150608053650/http://www.cs.bu.edu/~snyder/publications/UnifChapter.pdf "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). [http://www.lsv.fr/~dowek/Publi/unification.ps "Higher-order Unification and Matching"] {{Webarchive|url=https://web.archive.org/web/20190515113555/http://www.lsv.fr/~dowek/Publi/unification.ps |date=2019-05-15 }}. In ''Handbook of Automated Reasoning''.
* Franz Baader and [[Tobias Nipkow]] (1998). [http://www.in.tum.de/~nipkow/TRaAT/ ''Term Rewriting and All That'']. Cambridge University Press.
* Franz Baader and {{ill|Jörg H. Siekmann|de}} (1993). "Unification Theory". In ''Handbook of Logic in Artificial Intelligence and Logic Programming''.
* Jean-Pierre Jouannaud and [[Claude Kirchner (computer scientist)|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.&nbsp;243–320
* Jörg H. Siekmann . {{cite book|author= |chapter=Unification Theory |editor=[[Claude Kirchner (computer scientist)|Claude Kirchner]] (editor) |title=Unification|location= |publisher=Academic Press |year=1990 |isbn=}}.
* {{cite journal| author=Kevin Knight| title=Unification: A Multidisciplinary Survey| journal=ACM Computing Surveys|date= March 1989| volume=21| number=1| pages=93–124| url=http://www.isi.edu/natural-language/people/unification-knight.pdf| doi=10.1145/62029.62030| citeseerx=10.1.1.64.8967| s2cid=14619034}}
* [[Gérard Huet]] and [[Derek C. Oppen]] (1980). [http://infolab.stanford.edu/pub/cstr/reports/cs/tr/80/785/CS-TR-80-785.pdf "Equations and Rewrite Rules: A Survey"]. Technical report. Stanford University.
* {{cite journal | last1 = Raulefs | first1 = Peter | last2 = Siekmann | first2 = Jörg | last3 = Szabó | first3 = P. | last4 = Unvericht | first4 = E. | title = A short survey on the state of the art in matching and unification problems | journal = ACM SIGSAM Bulletin |date= 1979 |volume = 13 | issue = 2 | pages = 14–20 | doi = 10.1145/1089208.1089210 | s2cid = 17033087 }}
* Claude Kirchner and Hélène Kirchner. ''Rewriting, Solving, Proving''. In preparation.
{{refend}}

[[Категорија:Једначине]]
[[Категорија:Математичка логика]]
[[Категорија:Теоријско рачунарство]]
[[Категорија:Математичке структуре]]