Уніфікація (інформатика)

Уніфікація в логіці та інформатиці — це алгоритмічний процес розв'язання рівнянь між символічними виразами.

Залежно від того, яким виразам (термам) дозволено з'являтись в наборі рівнянь (також називається проблемою уніфікації), і які вирази вважаються рівними, виділяють кілька структур уніфікації. Якщо у виразі допускаються змінні вищого порядку, тобто змінні, що представляють функції, процес називається уніфікація вищого порядку, інакше, уніфікація першого порядку. Якщо потрібно, щоб обидві сторони кожного рівняння були буквально рівними, цей процес називається синтаксичним або вільним уніфікація, в іншому випадку — семантичне або рівноправна уніфікація, або Е-уніфікація або теорія модулів уніфікації.

Рішення проблеми уніфікації позначається як заміна, тобто відображення, що присвоює символічне значення кожній змінній виразів задачі. Алгоритм уніфікації повинен обчислити для заданої задачі повний і мінімальний набір підстановок, тобто набір, що охоплює всі його рішення, і не містить зайвих членів. Залежно від структури, повний та мінімальний набір заміни може мати не більше одного, не більше ніж кінцевого числа або, можливо, нескінченно багато членів або може не існувати зовсім.[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], який застосував синтаксичне уніфікація першого порядку як базовий будівельний блок його рішення процедури логіки першого порядку, великий крок вперед в автоматизоване обґрунтування технології, оскільки вона усуває одне джерело комбінаторного вибуху: пошук об'єктів термінів. Сьогодні автоматизовані міркування залишаються головною областю застосування уніфікації.

Синтаксичне уніфікація першого порядку використовується для здійснення логічного програмування та реалізації мови програмування типа даних, особливо в Хіндлі-Мілнер на основі алгоритму виведення типу. Семантичне об'єднання використовується в алгоритмах Satisfiability Modulo Theories, алгоритмах рерайтинг та аналізі криптографічного протоколу. Об'єднання більш високого порядку використовується в асистентах-доказах, наприклад Isabelle, а також обмежені форми уніфікації більш високого порядку (уніфікація шаблонів вищого порядку) використовуються в деяких реалізаціях мов програмування, таких як λProlog, оскільки шаблони вищих порядків є експресивними, проте їх пов'язана процедура уніфікації зберігає теоретичні властивості ближче до уніфікації першого порядку.

Загальні формальні визначення

Необхідні умови

Формально припускає уніфікаційний підхід

  • Безліч встановлених V змінних. Для уніфікації вищого порядку зручно вибрати V , непересічну з набору лямбда-термінів.
  • Набір T термінів такий, що V ⊆ T. Для уніфікації першого порядку та уніфікації вищого порядку T — це зазвичай набір виразів першого порядку (вирази побудовані з символів змінної та функцій) і лямбда-числення (вираз, що містять деякі змінні вищестоящих порядків), відповідно.
  • Позначення vars : T → ℙ ( V ), присвоюючи кожному терміну t встановлений vars ( т ) ⊊ V з вільних змінних, що відбуваються у t .
  • Відношення еквівалентності ≡ T , вказуючи, які терміни вважаються рівними. Для уніфікації більш високого порядку, як правило, t ≡ u якщо t і u є еквівалент альфа. Для Е-уніфікації першого порядку ≡ відображає фонові знання про певні символьні функції; наприклад, якщо ⊕ вважається комутативним, t ≡ u , якщо u виходить з t , обмінюючи аргументи ⊕ на деяких (можливо, всіх) випадках.[note 2] Якщо взагалі не існує фонового знання, то в буквальному чи синтаксичному відношенні однакові терміни вважаються рівними; в цьому випадку ≡ називається вільна теорія (тому що це вільний об'єкт), або теорія конструкторів (оскільки всі символьні функції просто створюють терміни даних, а не працюють на них).

Термін першого порядку

Враховуючи набір символів V змінних, набір символів C постійних символів і встановлює Fn функції n — ary Символи, також називаються символами оператора, для кожного натурального числа n ≥ 1, сукупність (несортованих першого порядку) термінів T є рекурсивно визначено як найменший набір з наступних властивостей:[5]

  • кожен змінний символ позначається виразом: V ⊆ T ,
  • кожен постійний символ — це вираз: C ⊆ T ,
  • з кожним n виразом t 1 , …, t n, можна побудувати кожен n  — функціональний символ f ∈ F n , більший за цей вираз f ( t 1 , …, t n ).

Наприклад, якщо x ∈ V є символом змінної, 1 ∈ C є постійним символом і add ∈ F 2 — це символ двійкової функції, потім x ∈ T , 1 ∈ T і (отже) add ( x , 1) ∈ T відповідно до правил будівництва першого, другого та третього виразів відповідно. Останній термін зазвичай записується як x + 1, використовуючи інфіксну нотацію та більш загальний символ оператора + для зручності. <! — перейти до основної статті: Часто математики фіксують аріус (кількість аргументів) символу функції (див. Підпис), як правило, в задачах синтаксичного уніфікації символ функції може мати будь-яку (кінцеву) кількість аргументів і, можливо, може мати різні числа аргументів у різних контекстах. наприклад, f (f (a), f (x, y, z)) — добре сформований термін для задач уніфікації.

Термін вищого порядку

Замещение

Замещение — це відображення σ: V → T від змінних до виразів; позначення {x1 ↦ t1, ..., xk ↦ tk } означає підстановку, що заміняє кожну змінну xi to the term ti, for i=1,…,k, та кожної іншої змінної для себе. Застосування, що заміняє до виразаt записується як постфіксний запис, оскільки t {x1 ↦ t1, ..., xk ↦ tk}; це означає (одночасно) замінити кожну змінну xi на вираз t іti. Результат tσ застосування заміни σ на вираз t називається екземпляр цього вираза t. Як приклад першого порядку застосуємо заміщення {x ↦ h(a,y), z ↦ b } до вираза

f( x , a, g( z ), y)
перетворимо  
f( h(a,y) , a, g( b ), y).

Узагальнення, спеціалізація

Якщо вираз t має екземпляр, еквівалентний виразу u, тобто якщо, tσ ≡ u для деякої заміни σ, то t називається більш загальним, ніж u,і u називається більш спеціальним, або підкоряється t. Наприклад, x ⊕ a загальніший, ніж a ⊕ b, якщо ⊕ — , комутативне, з того часу (x ⊕ a) x↦b = b ⊕ a ≡ a ⊕ b.


Якщо ≡ синтаксичний ідентичність термінів, вираз, можливо, є як загальніший, так і більше спеціальний, ніж інший, тільки якщо обидва виирази відрізняються тільки їх іменами змінної, не в їх синтаксичній структурі; такі вирази — звані перейменування один одного. Наприклад f(x1,a,g(z1),y1)  —варіант f(x2,a,g(z2),y2), , оскільки f(x1,a,g(z1),y1) {{x1 ↦ x2, y1 ↦ y2, z1 ↦ z2}} = f(x2,a,g(z2),y2) і f(x2,a,g(z2),y2) {{x2 ↦ x1, y2 ↦ y1, z2 ↦ z1}} = f(x1,a,g(z1),y1). Проте, f(x1,a,g(z1),y1) не є варіантом f(x2,a,g(x2),x2), , оскільки жодна заміна не може перетворити останній член на перший. Отже, останній вираз є набагато більш спеціальним, ніж перший.

Для довільного ≡, вираз може бути як загальним, так і більш спеціальним, ніж структурно інший вираз. Наприклад, якщо ⊕ є ідемпотентним, тобто, якщо завжди x ⊕ x ≡ x, тоді вираз x ⊕ y є більш загальним, ніж (x ⊕ y) x ↦ z, y ↦ z = z ⊕ z ≡ z, і навпаки z є більш загальним, ніж z z ↦ x ⊕ y = x ⊕ y, хоча x⊕y and z мають різну структуру.

Заміна σ є більш спеціальною чи підпорядкований ніж, заміна τ у tσ є більш спеціальним, ніж tτ для кожного вираза t.Ми також говоримо, що τ є більш загальним, ніж σ. Наприклад, x ↦ a, y ↦ a є більш спеціальним, ніж τ = x ↦ y , але σ = x ↦ a ні, оскільки f(x,y)σ = f(a,y) не більш особливий, ніж f(x,y)τ = f(y,y).[6]

Примітки
  1. в цьому випадку, все ще існує повні набори заміщення (наприклад, набір усіх рішень взагалі); однак, кожен такий набір містить резервні члени.
  2. Наприклад, a ⊕ (b ⊕ f(x)) ≡ a ⊕ (f(x) ⊕ b) ≡ (b ⊕ f(x)) ⊕ a ≡ (f(x) ⊕ b) ⊕ a

Список літератури
  1. Fages, François; Huet, Gérard (1986). Complete Sets of Unifiers and Matchers in Equational Theories. Theoretical Computer Science 43: 189–200. doi:10.1016/0304-3975(86)90175-1.
  2. Martelli, Alberto; Montanari, Ugo (Apr 1982). An Efficient Unification Algorithm. ACM Trans. Program. Lang. Syst. 4 (2): 258–282. doi:10.1145/357162.357169.
  3. J.A. Robinson (Jan 1965). A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM 12 (1): 23–41. doi:10.1145/321250.321253.; Here: sect.5.8, p.32
  4. J.A. Robinson (1971). Computational logic: The unification computation. Machine Intelligence 6: 63–72.
  5. C.C. Chang; H. Jerome Keisler (1977). Model Theory. Studies in Logic and the Foundation of Mathematics 73. North Holland.; here: Sect.1.3
  6. K.R. Apt. «From Logic Programming to Prolog», p. 24. Prentice Hall, 1997.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.