Алгоритмическое решение уравнений: унификация в логике и информатике

Введение

Алгоритмический процесс решения уравнений
В логике и информатике, в частности в автоматическом доказательстве, унификация — это алгоритмический процесс решения уравнений между символическими выражениями, каждое из которых имеет вид «левая часть = правая часть». Например, используя x, y, z в качестве переменных и принимая f за неинтерпретируемую функцию, множество уравнений, состоящее из одного элемента { f(1, y) = f(x, 2) }, является задачей синтаксической унификации первого порядка, единственным решением которой является подстановка { x ↦ 1, y ↦ 2 }. Соглашения могут различаться в отношении допустимых значений переменных и критериев эквивалентности выражений. В синтаксической унификации первого порядка переменные принимают значения из множества термов первого порядка, а эквивалентность определяется синтаксически. Эта версия унификации имеет единственное «наилучшее» решение и используется в логическом программировании и при реализации систем типов языков программирования, особенно в алгоритмах вывода типов, основанных на алгоритме Хиндли — Милнера. В унификации высшего порядка, возможно, ограниченной унификацией по образцу высшего порядка, термы могут включать лямбда-выражения, а эквивалентность определяется с учётом бета-редукции. Эта версия используется в системах доказательства теорем и логическом программировании высшего порядка, например, в Isabelle, Twelf и lambdaProlog. Наконец, в семантической унификации или E-унификации равенство определяется на основе фоновых знаний, а переменные принимают значения из различных областей. Эта версия используется в SMT-решателях, алгоритмах переписывания термов и анализе криптографических протоколов.

Формальное определение

Проблема унификации — это конечный набор уравнений, подлежащих решению, где lᵢ, rᵢ принадлежат множеству термов или выражений. В зависимости от того, какие выражения или термы допускаются в наборе уравнений или задаче унификации, и какие выражения считаются равными, выделяют несколько подходов к унификации. Если в выражении разрешены переменные высшего порядка, то есть переменные, представляющие функции, то процесс называется унификацией высшего порядка, иначе — унификацией первого порядка. Если требуется найти решение, при котором обе части каждого уравнения были бы буквально равны, то процесс называется синтаксической или свободной унификацией, иначе — семантической или уравнительной унификацией, или E-унификацией, или унификацией по теории. Если правая часть каждого уравнения замкнута (не содержит свободных переменных), то задача называется сопоставлением (с образцом). Левая часть (с переменными) каждого уравнения называется образцом.

Набор растворов

Замена σ является решением задачи унификации E, если lᵢσ ≡ rᵢσ для всех i. Такая замена также называется унификатором для E. Например, если ⊕ ассоциативна, то задача унификации { x ⊕ a ≐ a ⊕ x } имеет решения {x ↦ a}, {x ↦ a ⊕ a}, {x ↦ a ⊕ a ⊕ a} и т.д., в то время как задача { x ⊕ a ≐ a } не имеет решений. Для заданной задачи унификации E, множество S унификаторов называется полным, если каждая замена-решение подчинена некоторой замене из S. Полное множество замен всегда существует (например, множество всех решений), но в некоторых системах (таких как унификация высшего порядка без ограничений) проблема определения, существует ли хотя бы одно решение (то есть, является ли полное множество замен непустым), является неразрешимой. Множество S называется минимальным, если ни один из его элементов не подчиняет другой. В зависимости от системы, полное и минимальное множество замен может содержать ноль, один, конечное или бесконечное число элементов, или вообще не существовать из-за бесконечной цепочки избыточных элементов. Таким образом, в общем случае, алгоритмы унификации вычисляют конечное приближение полного множества, которое может быть или не быть минимальным, хотя большинство алгоритмов стараются избегать избыточных унификаторов, когда это возможно. предложил алгоритм, который сообщает о неразрешимости или вычисляет единственный унификатор, который сам по себе образует полное и минимальное множество замен, называемое наиболее общим унификатором.

Проверка

Попытка унифицировать переменную x с термом, содержащим x как строгий подтерм, например, x ≐ f( , x, ), приведет к бесконечному терму в качестве решения для x, поскольку x будет входить в себя как подтерм. В множестве (конечных) термов первого порядка, определенных выше, уравнение x ≐ f( , x, ) не имеет решения; следовательно, правило исключения может быть применено только если x ∉ vars(t). Поскольку эта дополнительная проверка, называемая проверкой на вхождение, замедляет алгоритм, она опускается, например, в большинстве систем Prolog. С теоретической точки зрения, отказ от этой проверки эквивалентен решению уравнений над бесконечными деревьями, см. #Унификация бесконечных термов ниже.

Примеры синтаксического объединения терминов первого порядка

В синтаксической конвенции Prolog символ, начинающийся с большой буквы, является именем переменной; символ, начинающийся с маленькой буквы, является символом функции; запятая используется в качестве логического И-оператора. Для математической нотации x, y, z используются как переменные, f, g как символы функций, а a, b как константы. Prolog нотация Математическая нотация Унифицирующая подстановка Пояснение a = a { a = a } {} Успешно. (тавтология) a = b { a = b } ⊥ a и b не совпадают X = X { x = x } {} Успешно. (тавтология) a = X { a = x } { x ↦ a } x унифицируется с константой a X = Y { x = y } { x ↦ y } x и y становятся алиасами f(a,X) = f(a,b) { f(a,x) = f(a,b) } { x ↦ b } Символы функций и констант совпадают, x унифицируется с константой b f(a) = g(a) { f(a) = g(a) } ⊥ f и g не совпадают f(X) = f(Y) { f(x) = f(y) } { x ↦ y } x и y становятся алиасами f(X) = g(Y) { f(x) = g(y) } ⊥ f и g не совпадают f(X) = f(Y,Z) { f(x) = f(y,z) } ⊥ Неудача. Символы функции f имеют разную арность f(g(X)) = f(Y) { f(g(x)) = f(y) } { y ↦ g(x) } y унифицируется с термом g(x) f(g(X),X) = f(Y,a) { f(g(x),x) = f(y,a) } { x ↦ a, y ↦ g(a) } x унифицируется с константой a, а y с термом g(a) X = f(X) { x = f(x) } должно быть ⊥ Возвращает ⊥ в логике первого порядка и многих современных диалектах Prolog (обеспечивается проверкой на вхождение). Успешно в традиционном Prolog и Prolog II, унифицируя x с бесконечным термом x=f(f(f(f(…)))). X = Y, Y = a { x = y, y = a } { x ↦ a, y ↦ a } Оба x и y унифицируются с константой a a = Y, X = Y { a = y, x = y } { x ↦ a, y ↦ a } Как выше (порядок уравнений в наборе не имеет значения) X = a, b = X { x = a, b = x } ⊥ Неудача. a и b не совпадают, поэтому x не может быть унифицирован с обоими.

Наиболее общий унификатор синтаксической задачи унификации первого порядка размера n может иметь размер 2^n. Например, задача (((a*z)*y)*x)*w \doteq w*(x*(y*(z*a))) имеет наиболее общий унификатор \{ z ↦ a, y ↦ a*a, x ↦ (a*a)*(a*a), w ↦ ((a*a)*(a*a))*((a*a)*(a*a)) \} , см. рисунок. Чтобы избежать экспоненциальной временной сложности, вызванной таким ростом, продвинутые алгоритмы унификации работают с направленными ациклическими графами (DAG), а не с деревьями.

Применение: унификация структуры признаков

Унификация применялась в различных областях вычислительной лингвистики.

Порядочное объединение

Логика сортировки порядка позволяет присвоить каждому терму сортировку или тип и объявить сортировку s1 подсортировкой другой сортировки s2, обычно записываемую как s1 ⊆ s2. Например, при рассуждениях о биологических существах полезно объявить сортировку dog подсортировкой сортировки animal. Везде, где требуется терм некоторой сортировки s, вместо него может быть подставлен терм любого подсорта s. Например, если предположить объявление функции mother: animal → animal и объявление константы lassie: dog, терм mother(lassie) вполне допустим и имеет сортировку animal. Чтобы указать, что мать собаки, в свою очередь, является собакой, можно выдать другое объявление mother: dog → dog; это называется перегрузкой функций, аналогичной перегрузке в языках программирования. Вальтер предложил алгоритм унификации для термов в логике сортировки порядка, требующий для любых двух объявленных сортировок s1 и s2 также объявить их пересечение s1 ∩ s2: если x1 и x2 — переменные сортировок s1 и s2 соответственно, то уравнение x1 ≐ x2 имеет решение {x1 = x, x2 = x}, где x: s1 ∩ s2. После включения этого алгоритма в автоматический доказатель теорем, основанный на клаузах, он смог решить задачу-эталон, преобразовав её в логику сортировки порядка, тем самым уменьшив её на порядок величины, поскольку многие унарные предикаты превратились в сортировки. Смолка обобщил логику сортировки порядка, чтобы разрешить параметрический полиморфизм. В его фреймворке объявления подсортировок распространяются на сложные выражения типов. В качестве примера программирования можно объявить параметрическую сортировку list(X) (где X — параметр типа, как в шаблоне C++), и из объявления подсортировки int ⊆ float автоматически выводится отношение list(int) ⊆ list(float), что означает, что каждый список целых чисел также является списком чисел с плавающей точкой. Шмидт Шаусс обобщил логику сортировки порядка, чтобы разрешить объявления термов. Например, если предположить объявления подсортировок even ⊆ int и odd ⊆ int, объявление терма ∀ i : int. (i + i) : even позволяет объявить свойство сложения целых чисел, которое нельзя выразить обычной перегрузкой.