Корисник:ДанилоМилисиц

Унификација

У логици и рачунарству, посебно аутоматизованом закључивању, унификација је алгоритамски процес решавања једначина између симболичких израза, сваки у облику Лева страна = Десна страна. На пример, користећи x,y,з као променљиве и узимајући ф као неинтерпретирану функцију, скуп једноструких једначина { ф(1,y) = ф(x,2) } је синтаксички проблем обједињавања првог реда који има замену { x ↦ 1, y ↦ 2 } као њено једино решење.

Конвенције се разликују по томе које вредности могу да имају променљиве и који изрази се сматрају еквивалентним. У синтаксичком обједињавању првог реда, променљиве су у опсегу чланова првог реда, а еквивалентност је синтаксичка. Ова верзија обједињавања има јединствени „најбољи“ одговор и користи се у логичком програмирању и имплементацији типских система програмског језика, посебно у Хиндли–Милнеровим алгоритмима за типско закључивање. У обједињавању вишег реда, могуће ограниченом на обједињавање патерна вишег реда, термини могу укључивати ламбда изразе, а еквивалентност је до нивоа бета редукције. Ова верзија се користи у помоћницима за проверу и логичком програмирању вишег реда, на пример Исабелле, Тwелф, и ламбдаПролог. Коначно, у семантичком обједињавању или Е-унификацији, једнакост је подложна основном знању и променљиве се крећу у различитим доменима. Ова верзија се користи у СМТ решавачима, алгоритмима за замену чланова и анализи криптографских протокола.

Формална дефиниција

Проблем уједињења је коначан скуп Е={ л1 ≐ р1, ..., лн ≐ рн } једначина које треба решити, где су ли, ри у скупу T {\displaystyle T} чланова или израза. У зависности од тога који изрази или чланови су дозвољени у скупу једначина или проблему обједињавања, и који се изрази сматрају једнаким, разликује се неколико оквира унификације. Ако су променљиве вишег реда, односно променљиве које представљају функције, дозвољене у изразу, процес се назива обједињавање вишег реда, иначе се ради о обједињавању првог реда. Ако је потребно решење да обе стране сваке једначине буду дословно једнаке, процес се назива синтаксичко или слободно уједињење, иначе семантичко или једначинско уједињење, или Е-унификација, или теорија унификације по модулу.

Ако је десна страна сваке једначине затворена (нема слободних променљивих), проблем се назива подударање (патерна). Лева страна (са променљивима) сваке једначине се назива патерн.[1]

Референце

1. Довек, Гилес (1. 1. 2001). „Хигхер-ордер унифицатион анд матцхинг”. Хандбоок оф аутоматед реасонинг. Елсевиер Сциенце Публисхерс Б. В. стр. 1009—1062. ИСБН 978-0-444-50812-6. Архивирано из оригинала 15. 5. 2019. г. Приступљено 15. 5. 2019.

Литература

• Франз Бадер и Вејн Снyдер (2001). "Теорија унификације".
• Гиллес Довек (2001). "Хигхер-ордер Унифицатион анд Матцхинг"