Korisnik:DaniloMilisic

Unifikacija

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={ l1 ≐ r1, ..., ln ≐ rn } jednačina koje treba rešiti, gde su li, ri u skupu T {\displaystyle 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

1. Dovek, Giles (1. 1. 2001). „Higher-order unification and matching”. Handbook of automated reasoning. Elsevier Science Publishers B. V. str. 1009—1062. ISBN 978-0-444-50812-6. Arhivirano iz originala 15. 5. 2019. g. Pristupljeno 15. 5. 2019.

Literatura

• Franz Bader i Vejn Snyder (2001). "Teorija unifikacije".
• Gilles Dovek (2001). "Higher-order Unification and Matching"