Уніфікація (інформатика)
З Вікіпедії, безкоштовно encyclopedia
Уніфікація в логіці та інформатиці — це алгоритмічний процес розв'язання рівнянь між символічними виразами.
Залежно від того, яким виразам (термам) дозволено з'являтись в наборі рівнянь (також називається проблемою уніфікації), і які вирази вважаються рівними, виділяють кілька структур уніфікації. Якщо у виразі допускаються змінні вищого порядку, тобто змінні, що представляють функції, процес називається уніфікація вищого порядку, інакше, уніфікація першого порядку. Якщо потрібно, щоб обидві сторони кожного рівняння були буквально рівними, цей процес називається синтаксичним або вільним уніфікація, в іншому випадку — семантичне або рівноправна уніфікація, або Е-уніфікація або теорія модулів уніфікації.
Рішення проблеми уніфікації позначається як заміна[en], тобто відображення, що присвоює символічне значення кожній змінній виразів задачі. Алгоритм уніфікації повинен обчислити для заданої задачі повний і мінімальний набір підстановок, тобто набір, що охоплює всі його рішення, і не містить зайвих членів. Залежно від структури, повний та мінімальний набір заміни може мати не більше одного, не більше ніж кінцевого числа або, можливо, нескінченно багато членів або може не існувати зовсім.[note 1][1] В деяких рамках взагалі неможливо вирішити, чи існує якесь рішення. Для синтаксичної уніфікації першого порядку Мартеллі та Монтанарі[2] подали алгоритм, який повідомляє про нерозв'язність, або обчислює повний і мінімальний синтаксичний набір, який містить так званий найбільш загальний уніфікатор.
Наприклад, використовуючи x,y,z як змінні, встановлюється рівняння: { cons(x,cons(x, nil)) = cons (2, y) } — це синтаксична проблема уніфікації першого порядку що має єдине рішення для заміни { x ↦ 2, y ↦ cons(2, nil)}.
Синтаксична проблема уніфікації першого порядку ( y = cons (2, y)} не має вирішення над набором кінцевих виразів; однак у нього є єдине рішення { y ⟩ cons (2, cons (2, cons (2, …)))} над набором нескінченних дерев.
Семантична проблема уніфікації першого порядку {a⋅x = x⋅a} має кожну підстановку форми { x ↦ "'a' ' ⋅ … ⋅a } як рішення в напівгрупи, тобто якщо (⋅) вважається асоціативна; та ж проблема, розглянута в абелевій групі, де (⋅) також вважається комутативна, має взагалі будь-яку заміну як рішення. Синтаксична задача уніфікації другого порядку, оскільки y — функціональна змінна, є синтаксичною задачею { a = y ( x ) }. Одним із рішень є {x ↦ a, y ↦ (тотожність функції)}; інший є {y ↦ (стала функція, що відслідковує кожне значення до a), x ↦ (будь-яке значення)}.
Перше формальне дослідження уніфікації можна віднести до Джон Алан Робінсон,[3][4], який застосував синтаксичне уніфікація першого порядку як базовий будівельний блок його рішення процедури логіки першого порядку, великий крок вперед в автоматизоване обґрунтування технології, оскільки вона усуває одне джерело комбінаторного вибуху: пошук об'єктів термінів. Сьогодні автоматизовані міркування залишаються головною областю застосування уніфікації.
Синтаксичне уніфікація першого порядку використовується для здійснення логічного програмування та реалізації мови програмування типа даних, особливо в Хіндлі-Мілнер[en] на основі алгоритму виведення типу. Семантичне об'єднання використовується в алгоритмах Satisfiability Modulo Theories, алгоритмах рерайтинг та аналізі криптографічного протоколу. Об'єднання більш високого порядку використовується в асистентах-доказах, наприклад Isabelle[en], а також обмежені форми уніфікації більш високого порядку (уніфікація шаблонів вищого порядку) використовуються в деяких реалізаціях мов програмування, таких як λProlog[en], оскільки шаблони вищих порядків є експресивними, проте їх пов'язана процедура уніфікації зберігає теоретичні властивості ближче до уніфікації першого порядку.