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

В логике и информатике , в частности в автоматизированном рассуждении , унификация — это алгоритмический процесс решения уравнений между символическими выражениями , каждое из которых имеет форму Левая часть = Правая часть . Например, используя x , y , z в качестве переменных и принимая f в качестве неинтерпретируемой функции , набор одноэлементных уравнений { f (1, y ) = f ( x ,2) } представляет собой синтаксическую задачу унификации первого порядка, которая имеет замена { x ↦ 1, y ↦ 2 } как единственное решение.

Соглашения различаются в отношении того, какие значения могут принимать переменные и какие выражения считаются эквивалентными. При синтаксической унификации первого порядка переменные варьируются в пределах терминов первого порядка , и эквивалентность является синтаксической. Эта версия унификации имеет уникальный «лучший» ответ и используется в логическом программировании и реализации системы типов языка программирования , особенно в Хиндли-Милнера на основе вывода типа алгоритмах . При унификации более высокого порядка, которая, возможно, ограничена унификацией шаблонов более высокого порядка , термины могут включать лямбда-выражения, а эквивалентность сводится к бета-редукции. например Isabelle , Twelf иlambdaProlog Эта версия используется в помощниках по доказательству и логическом программировании высшего порядка , . Наконец, при семантической унификации или электронной унификации равенство зависит от базовых знаний, а переменные варьируются в различных областях. Эта версия используется в решателях SMT , алгоритмах перезаписи терминов и анализе криптографических протоколов .

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

Проблема объединения — это конечное множество E = { l ₁ ≐ r ₁ , ..., l _n ≐ r _n } уравнений, которые необходимо решить, где l _i , r _i находятся в множестве $T$терминов ​ или выражений . В зависимости от того, какие выражения или термины могут встречаться в наборе уравнений или задаче унификации и какие выражения считаются равными, различают несколько рамок унификации. переменные более высокого порядка, то есть переменные, представляющие функции Если в выражении разрешены , процесс называется унификацией высшего порядка , в противном случае — унификацией первого порядка . Если требуется решение, чтобы сделать обе стороны каждого уравнения буквально равными, этот процесс называется синтаксической или свободной унификацией , иначе семантической или эквациональной унификацией , или E-унификацией , или теорией унификации по модулю .

Если правая часть каждого уравнения замкнута (нет свободных переменных), проблема называется сопоставлением (образца) . Левая часть (с переменными) каждого уравнения называется шаблоном .

Предварительные условия

Формально унификационный подход предполагает

• Бесконечный набор $V$переменных ​ . Для объединения более высокого порядка удобно выбрать $V$ не пересекается с набором связанных переменных лямбда-члена .
• Множество $T$ терминов что таких, $V\subseteq T$. Для объединения первого порядка $T$обычно представляет собой набор термов первого порядка (терминов, построенных из символов переменных и функций). Для объединения высшего порядка $T$ состоит из термов первого порядка и лямбда-терминов (терминов, содержащих некоторые переменные более высокого порядка).
• Отображение ${\text{vars}}\colon T\rightarrow$ $\mathbb {P}$$(V)$, присваивая каждому члену $t$ набор ${\text{vars}}(t)\subsetneq V$ свободных переменных , встречающихся в $t$.
• Теория или отношение эквивалентности $\equiv$ на $T$, указывая, какие члены считаются равными. Для электронного объединения первого порядка $\equiv$отражает базовые знания об определенных функциональных символах; например, если $\oplus$ считается коммутативным, $t\equiv u$ если $u$ результаты из $t$ путем замены аргументов $\oplus$ в некоторых (возможно, во всех) случаях. В наиболее типичном случае, когда фоновые знания отсутствуют вообще, тогда равными считаются только буквально или синтаксически идентичные термины. В этом случае ≡ называется свободной теорией (поскольку это свободный объект ), пустой теорией (поскольку множество эквациональных предложений или фоновые знания пусты), теорией неинтерпретируемых функций (поскольку объединение выполняется на неинтерпретируемые термины ) или теорию конструкторов (поскольку все функциональные символы просто создают термины данных, а не работают с ними). Для объединения более высокого порядка обычно $t\equiv u$ если $t$ и $u$ являются альфа-эквивалентными .

В качестве примера того, как набор терминов и теория влияют на набор решений, синтаксическая задача унификации первого порядка { y = cons (2, y )} не имеет решения над множеством конечных терминов . Однако оно имеет единственное решение { y ↦ cons (2, cons (2, cons (2,...))) } над множеством членов бесконечного дерева . Аналогично, семантическая задача объединения первого порядка { a ⋅ x = x ⋅ a } имеет каждую замену вида { x ↦ a ⋅...⋅ a } как решение в полугруппе , т. е. если (⋅) считается ассоциативным . Но та же проблема, рассматриваемая в абелевой группе , где (⋅) также считается коммутативной , вообще имеет любую замену в качестве решения.

В качестве примера унификации высшего порядка можно привести одноэлементный набор { a = y ( x ) }, который представляет собой синтаксическую задачу унификации второго порядка, поскольку y является функциональной переменной. Одним из решений является { x ↦ a , y ↦ ( тождественная функция ) }; другой — { y ↦ ( постоянная функция , отображающая каждое значение в a ), x ↦ (любое значение) }.

Замена

Основная статья: Замена (логика)

Замена – это отображение $\sigma :V\rightarrow T$от переменных к термам; обозначение $\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$ относится к замене, отображающей каждую переменную $x_{i}$ к сроку $t_{i}$, для $i=1,...,k$и каждая другая переменная сама по себе; тот $x_{i}$должны быть попарно различны. Применение этой замены к термину $t$ записывается в постфиксной записи как $t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$; это означает (одновременную) замену каждого вхождения каждой переменной $x_{i}$ в срок $t$ к $t_{i}$. Результат $t\tau$ применения замены $\tau$ на срок $t$ называется экземпляром этого термина $t$. В качестве примера первого порядка, применив замену { x ↦ h ( a , y ), z ↦ b } к термину

	$f($	${\textbf {x}}$	$,a,g($	${\textbf {z}}$	$),y)$
урожайность
	$f($	${\textbf {h}}({\textbf {a}},{\textbf {y}})$	$,a,g($	${\textbf {b}}$	$),y).$

Обобщение, специализация

Если срок $t$ имеет экземпляр, эквивалентный термину $u$, то есть, если $t\sigma \equiv u$ для какой-то замены $\sigma$, затем $t$ называется более общим , чем $u$, и $u$ называется более специальным , чем или отнесенным к нему, $t$. Например, $x\oplus a$ является более общим, чем $a\oplus b$ если ⊕ коммутативен , так как тогда $(x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b$.

Если ≡ — буквальное (синтаксическое) тождество терминов, то термин может быть как более общим, так и более специальным, чем другой, только если оба термина различаются только именами переменных, а не синтаксической структурой; такие термины называются вариантами или переименованиями друг друга. Например, $f(x_{1},a,g(z_{1}),y_{1})$ это вариант $f(x_{2},a,g(z_{2}),y_{2})$, с

$$f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})$$

и

$$f(x_{2},a,g(z_{2}),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1},a,g(z_{1}),y_{1}).$$

Однако, $f(x_{1},a,g(z_{1}),y_{1})$ это не вариант $f(x_{2},a,g(x_{2}),x_{2})$, поскольку никакая замена не может превратить последний член в первый. Следовательно, последний термин более специальный, чем первый.

Для произвольного $\equiv$, термин может быть как более общим, так и более специальным, чем структурно другой термин. Например, если ⊕ идемпотент , то есть если всегда $x\oplus x\equiv x$, то срок $x\oplus y$ является более общим, чем $z$, и наоборот, хотя $x\oplus y$ и $z$ имеют различную структуру.

Замена $\sigma$ , более специфичен чем или отнесен к ней замена $\tau$ если $t\sigma$ относится к $t\tau$ за каждый семестр $t$. Мы также говорим, что $\tau$ является более общим, чем $\sigma$. Более формально, возьмем непустое бесконечное множество $V$ вспомогательных переменных таких, что ни одно уравнение $l_{i}\doteq r_{i}$ в задаче объединения содержит переменные из $V$. Тогда замена $\sigma$ включается другой заменой $\tau$ если есть замена $\theta$ такой, что для всех условий $X\notin V$, $X\sigma \equiv X\tau \theta$. Например $\{x\mapsto a,y\mapsto a\}$ относится к $\tau =\{x\mapsto y\}$, с использованием $\theta =\{y\mapsto a\}$, но $\sigma =\{x\mapsto a\}$ не относится к $\tau =\{x\mapsto y\}$, как $f(x,y)\sigma =f(a,y)$ не является примером $f(x,y)\tau =f(y,y)$.

Набор решений

Замена σ является решением задачи объединения E , если l _i σ ≡ r _i σ для $i=1,...,n$. замену еще унификатором E. называют Такую Например, если ⊕ ассоциативен , проблема объединения { x ⊕ a ≐ a ⊕ x } имеет решения { x ↦ a }, { x ↦ a ⊕ a }, { x ↦ a ⊕ a ⊕ a } и т. д., а задача { x ⊕ a ≐ a } не имеет решения.

Для данной задачи объединения E набор S унификаторов называется полным, каждая замена решения включается некоторой заменой в S. если Полный набор замен всегда существует (например, набор всех решений), но в некоторых структурах (например, неограниченная унификация высшего порядка) проблема определения того, существует ли какое-либо решение (т. е. непусто ли полный набор замен) неразрешима.

Множество S называется минимальным , если ни один из его членов не включает в себя другой. В зависимости от структуры полный и минимальный набор подстановок может иметь ноль, один, конечное или бесконечное число членов или может вообще не существовать из-за бесконечной цепочки избыточных членов. Таким образом, в целом алгоритмы унификации вычисляют конечную аппроксимацию полного набора, который может быть минимальным, а может и не быть, хотя большинство алгоритмов по возможности избегают избыточных унификаторов. Для синтаксической унификации первого порядка Мартелли и Монтанари дал алгоритм, который сообщает о неразрешимости или вычисляет единственный унификатор, который сам по себе образует полный и минимальный набор подстановок, называемый наиболее общим унификатором .

Синтаксическая унификация терминов первого порядка

Схематическая треугольная диаграмма синтаксически объединяющих терминов t ₁ и t ₂ заменой σ.

Синтаксическая унификация терминов первого порядка является наиболее широко используемой структурой унификации. Он основан на том, что T является набором термов первого порядка (по некоторому заданному набору V переменных, C констант и F _n n -арных функциональных символов), а ≡ является синтаксическим равенством . В этой структуре каждая разрешимая проблема объединения { l ₁ ≐ r ₁ , ..., l _n ≐ r _n } имеет полный и, очевидно, минимальный одноэлементный набор решений { σ } . Его член σ называется наиболее общим унификатором ( mgu ) задачи. Члены в левой и правой частях каждого потенциального уравнения становятся синтаксически равными, когда применяется mgu, т. е. l ₁ σ = r ₁ σ ∧ ... ∧ l _n σ = r _n σ . Любой объединитель проблемы относится к категории по mgu σ . Mgu уникален с точностью до вариантов: если S ₁ и S ₂ являются полным и минимальным множествами решений одной и той же задачи синтаксического объединения, то S ₁ = { σ ₁ } и S ₂ = { σ ₂ } для некоторых замен σ ₁ и σ ₂ , а xσ ₁ является вариантом xσ ₂ для каждой переменной x , встречающейся в задаче.

Например, проблема объединения { x ≐ z , y ≐ f ( x ) } имеет объединитель { x ↦ z , y ↦ f ( z ) }, потому что

Икс	{ Икс ↦ z , y ↦ ж ( z ) }	=	С	=	С	{ Икс ↦ z , y ↦ ж ( z ) }	, и
и	{ Икс ↦ z , y ↦ ж ( z ) }	=	ж ( я )	=	е ( х )	{ Икс ↦ z , y ↦ ж ( z ) }	.

Это также самый общий унификатор. Другими унификаторами для той же проблемы являются, например, { x ↦ f ( x ₁ ), y ↦ f ( f ( x ₁ )), z ↦ f ( x ₁ ) }, { x ↦ f ( f ( x ₁ )), y ↦ f ( f ( f ( x ₁ ))), z ↦ f ( f ( x ₁ )) } и так далее; подобных объединителей бесконечно много.

В качестве другого примера, проблема g ( x , x ) ≐ f ( y ) не имеет решения в отношении того, что ≡ является буквальным тождеством, поскольку любая замена, примененная к левой и правой части, сохранит самые внешние g и f соответственно, и термины с разными внешними функциональными символами синтаксически различны.

Алгоритмы унификации

Алгоритм объединения Робинсона 1965 года

показывать

Symbols are ordered such that variables precede function symbols. Terms are ordered by increasing written length; equally long terms are ordered lexicographically. For a set T of terms, its disagreement path p is the lexicographically least path where two member terms of T differ. Its disagreement set is the set of subterms starting at p, formally: { t|_p : $t\in T$ }.

Algorithm:
Given a set T of terms to be unified
Let $\sigma$ initially be the identity substitution
do forever
    if $T\sigma$ is a singleton set then
        return $\sigma$
    fi
    let D be the disagreement set of $T\sigma$
    let s, t be the two lexicographically least terms in D
    if s is not a variable or s occurs in t then
        return "NONUNIFIABLE"
    fi
    $\sigma :=\sigma \{s\mapsto t\}$
done

Жак Эрбран обсудил основные концепции унификации и набросал алгоритм в 1930 году. Но большинство авторов приписывают первый алгоритм объединения Джону Алану Робинсону (см. вставку). Алгоритм Робинсона имел экспоненциальное поведение в худшем случае как во времени, так и в пространстве. Многие авторы предложили более эффективные алгоритмы унификации. Алгоритмы с наихудшим поведением в линейном времени были независимо открыты Мартелли и Монтанари (1976) и Патерсоном и Вегманом (1976). Баадер и Снайдер (2001) используют тот же метод, что и Патерсон-Вегман, поэтому он линейный, но, как и большинство алгоритмов унификации с линейным временем, он медленнее, чем версия Робинсона, на входных данных небольшого размера из-за накладных расходов на предварительную обработку входных данных и постобработку выходных данных, например построение представления DAG . де Шампо (2022) также имеет линейную сложность по размеру входных данных, но конкурирует с алгоритмом Робинсона на входных данных небольшого размера. Ускорение достигается за счет использования объектно-ориентированного представления исчисления предикатов, которое позволяет избежать необходимости предварительной и последующей обработки, вместо этого возлагая на переменные объекты ответственность за создание замены и работу с псевдонимами. де Шампо утверждает, что возможность добавлять функциональность к исчислению предикатов, представленному в виде программных объектов, также предоставляет возможности для оптимизации других логических операций.

Следующий алгоритм широко представлен и взят из работы Мартелли и Монтанари (1982) . Учитывая конечное множество $G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}$потенциальных уравнений, алгоритм применяет правила для преобразования его в эквивалентный набор уравнений вида { Икс ₁ ≐ ты ₁ , ..., Икс _м ≐ ты _м } где x ₁ , ..., x _m - различные переменные, а u ₁ , ..., um _- термины, не содержащие ни одного из x _i . Набор такой формы можно считать заменой. Если решения нет, алгоритм завершается нажатием ⊥; используют «Ом» или « провал другие авторы в этом случае ». Операцию замены всех вхождений переменной x в задаче G на терм t обозначается G { x ↦ t }. Для простоты константные символы рассматриваются как функциональные символы, имеющие нулевые аргументы.

$G\cup \{t\doteq t\}$	$\Rightarrow$	$G$		удалить
$G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k})\}$	$\Rightarrow$	$G\cup \{s_{0}\doteq t_{0},...,s_{k}\doteq t_{k}\}$		разлагать
$G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}$	$\Rightarrow$	$\bot$	если $f\neq g$ или $k\neq m$	конфликт
$G\cup \{f(s_{0},...,s_{k})\doteq x\}$	$\Rightarrow$	$G\cup \{x\doteq f(s_{0},...,s_{k})\}$		менять
$G\cup \{x\doteq t\}$	$\Rightarrow$	$G\{x\mapsto t\}\cup \{x\doteq t\}$	если $x\not \in {\text{vars}}(t)$ и $x\in {\text{vars}}(G)$	устранять
$G\cup \{x\doteq f(s_{0},...,s_{k})\}$	$\Rightarrow$	$\bot$	если $x\in {\text{vars}}(f(s_{0},...,s_{k}))$	проверять

Происходит проверка

Основная статья: Проверка происходит

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

Доказательство прекращения действия

Для доказательства завершения алгоритма рассмотрим тройку $\langle n_{var},n_{lhs},n_{eqn}\rangle$где n _var — количество переменных, которые встречаются в наборе уравнений более одного раза, n _lhs — количество функциональных символов и констант. в левых частях потенциальных уравнений, а n _eqn — количество уравнений. правило исключения Когда применяется , n _var уменьшается, поскольку x исключается из G и сохраняется только в { x ≐ t }. Применение любого другого правила никогда не сможет снова увеличить n _var . Когда правило decompose , конфликт или замена применяется , n _lhs левой части уменьшается, так как по крайней мере крайний f исчезает. Применение любого из оставшихся правил delete или check не может увеличить n _lhs , но уменьшит n _eqn . Следовательно, любое применение правил уменьшает тройную $\langle n_{var},n_{lhs},n_{eqn}\rangle$ относительно лексикографического порядка , что возможно только конечное число раз.

Конор МакБрайд наблюдает что «путем выражения структуры, которую использует унификация» на зависимо типизированном языке, таком как Epigram , алгоритм унификации Робинсона может быть сделан рекурсивным по количеству переменных , и в этом случае отдельное доказательство завершения становится ненужным.

Примеры синтаксической унификации терминов первого порядка

В синтаксическом соглашении Пролога символ, начинающийся с заглавной буквы, является именем переменной; символ, начинающийся со строчной буквы, является функциональным символом; запятая используется как логический оператор . Для математической записи x,y,z используются как переменные, f,g как функциональные символы и a,b как константы.

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

Два термина с экспоненциально большим деревом для их наименее распространенного экземпляра. Его даг- представление (крайняя правая, оранжевая часть) по-прежнему имеет линейный размер.

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

Применение: унификация в логическом программировании

Концепция унификации является одной из основных идей логического программирования . В частности, унификация является основным строительным блоком разрешения , правилом вывода для определения выполнимости формулы. В Прологе символ равенства =подразумевает синтаксическую унификацию первого порядка. Он представляет собой механизм связывания содержимого переменных и может рассматриваться как своего рода одноразовое присвоение.

В Прологе:

1. Переменная . может быть объединена с константой, термином или другой переменной, тем самым фактически становясь ее псевдонимом Во многих современных диалектах Пролога и в логике первого порядка переменная не может быть объединена с содержащим ее термином; это так называемая проверка на наличие событий .
2. Две константы могут быть объединены только в том случае, если они идентичны.
3. Аналогично, термин может быть унифицирован с другим термином, если верхние функциональные символы и арии термов идентичны и если параметры могут быть унифицированы одновременно. Обратите внимание, что это рекурсивное поведение.
4. Большинство операций, в том числе +, -, *, /, не оцениваются =. Так например 1+2 = 3невыполнимо, поскольку они синтаксически различны. Использование ограничений целочисленной арифметики #= вводит форму E-унификации, для которой эти операции интерпретируются и оцениваются.

Применение: вывод типа

Алгоритмы вывода типа обычно основаны на унификации, в частности на выводе типа Хиндли-Милнера , который используется функциональными языками Haskell и ML . Например, при попытке определить тип выражения Haskell True : ['x'], компилятор будет использовать тип a -> [a] -> [a] функции построения списка (:), тип Bool из первого аргумента Trueи тип [Char] второго аргумента ['x']. Переменная полиморфного типа a будет унифицирован с Bool и второй аргумент [a] будет унифицирован с [Char]. a не может быть и то, и другое Bool и Char в то же время, поэтому это выражение набрано неправильно.

Как и в Прологе, можно задать алгоритм вывода типа:

1. Любая переменная типа объединяется с любым выражением типа и создается для этого выражения. Конкретная теория может ограничить это правило проверкой возникновения.
2. Константы двух типов объединяются, только если они относятся к одному и тому же типу.
3. Две конструкции типов объединяются только в том случае, если они являются приложениями одного и того же конструктора типа и все типы их компонентов рекурсивно унифицируются.

Приложение: унификация структуры функций

См. также: Структура функций.

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

Объединение по порядку

Логика упорядоченной сортировки позволяет присвоить сорт или тип каждому термину и объявить сорт s ₁ подсортом s другого сорта 2 _, обычно записываемого как s ₁ ⊆ s ₂ . Например, рассуждая о биологических существах, полезно объявить породистую собаку разновидностью породистого животного . Везде, где требуется термин какого-либо типа s термин любого подвида s , вместо него может быть указан . Например, предполагая объявление функции mother : Animal → Animal и объявление константы lassie : Dog , термин Mother ( lassie ) совершенно допустим и имеет вид Animal . Для предоставления информации о том, что мать собаки в свою очередь является собакой, другое заявление мать : собака → собака может быть выдано ; это называется перегрузкой функций , аналогично перегрузке в языках программирования .

Вальтер предложил алгоритм объединения терминов в логике с упорядоченной сортировкой, требуя, чтобы для любых двух объявленных сортов s ₁ , s ₂ их пересечение s ₁ ∩ s ₂ также было объявлено : если x ₁ и x ₂ являются переменными сорта s ₁ и s ₂ соответственно, уравнение x ₁ ≐ x ₂ имеет решение { x ₁ = x , x ₂ = x }, где x : s ₁ ∩ s ₂ . Включив этот алгоритм в автоматизированный механизм доказательства теорем на основе предложений, он смог решить контрольную задачу, переведя ее в логику упорядоченной сортировки, тем самым уменьшив ее на порядок, поскольку многие унарные предикаты превратились в сортировки.

Смолка обобщил логику упорядоченной сортировки, допускающую параметрический полиморфизм . В его рамках объявления подсортировки передаются в выражения сложного типа. В качестве примера программирования параметрический список сортировки ( X можно объявить ) (где X является параметром типа, как в шаблоне C++ ), и из объявления подсортировки int ⊆ float отношений список ( int ) ⊆ list ( float автоматически создается ). это означает, что каждый список целых чисел также является списком чисел с плавающей запятой.

Шмидт-Шаус обобщил логику упорядоченной сортировки, позволяющую объявлять термины. В качестве примера, предполагая, что объявления подсортировки четные ⊆ int и нечетные ⊆ int , объявление термина типа ∀ i : int . ( i + i ) : позволяет даже объявить свойство сложения целых чисел, которое невозможно выразить обычной перегрузкой.

Объединение бесконечных терминов

Фон на бесконечных деревьях:

• Б. Курсель (1983). «Фундаментальные свойства бесконечных деревьев» . Теория. Вычислить. Наука . 25 (2): 95–169. дои : 10.1016/0304-3975(83)90059-2 .
• Майкл Дж. Махер (июль 1988 г.). «Полные аксиоматизации алгебр конечных, рациональных и бесконечных деревьев». Учеб. Третий ежегодный симпозиум IEEE. по логике в информатике, Эдинбург . стр. 348–357.
• Джоксан Джаффар; Питер Дж. Стаки (1986). «Семантика программирования на основе бесконечной древовидной логики» . Теоретическая информатика . 46 : 141–158. дои : 10.1016/0304-3975(86)90027-7 .

Алгоритм объединения, Пролог II:

• А. Кольмерауэр (1982). К.Л. Кларк; С.-А. Тарнлунд (ред.). Пролог и бесконечные деревья . Академическая пресса.
• Ален Кольмерауэр (1984). «Уравнения и неравенства на конечных и бесконечных деревьях». В ICOT (ред.). Учеб. Межд. Конф. о компьютерных системах пятого поколения . стр. 85–99.

Приложения:

• Фрэнсис Джаннезини; Жак Коэн (1984). «Генерация парсера и манипулирование грамматикой с использованием бесконечных деревьев Пролога» . Журнал логического программирования . 1 (3): 253–265. дои : 10.1016/0743-1066(84)90013-X .

Электронное объединение

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

Например, если a и b — разные константы, уравнение ​ $x*a\doteq y*b$не имеет решения что касается чисто синтаксической унификации , где ничего не известно об операторе $*$. Однако, если $*$известно, что он коммутативен , тогда замена { x ↦ b , y ↦ a } решает приведенное выше уравнение, с

	$x*a$	{ Икс ↦ б , у ↦ а }
=	$b*a$		по заявке на замену
=	$a*b$		по коммутативности $*$
=	$y*b$	{ Икс ↦ б , у ↦ а }	путем (обратного) применения замены

Базовые знания E могли бы утверждать коммутативность $*$по всеобщему равенству " $u*v=v*u$ для всех и , v ".

Конкретные базовые наборы знаний E

Используемые соглашения об именах

∀ ты , v , ш :	$u*(v*w)$	=	$(u*v)*w$	А	Ассоциативность $*$
∀ u , v :	$u*v$	=	$v*u$	С	Коммутативность $*$
∀ ты , v , ш :	$u*(v+w)$	=	$u*v+u*w$	Д л	Левая дистрибутивность $*$ над $+$
∀ ты , v , ш :	$(v+w)*u$	=	$v*u+w*u$	Д р	Правая дистрибутивность $*$ над $+$
∀ в :	$u*u$	=	в	я	Идемпотентность $*$
∀ в :	$n*u$	=	в	Н л	Левый нейтральный элемент n относительно $*$
∀ в :	$u*n$	=	в	NНет	Правый нейтральный элемент n относительно $*$

Говорят, что объединение теории разрешимо , если для нее разработан алгоритм объединения, завершающийся при любой входной задаче. Говорят, что объединение является полуразрешимым для теории, если для нее разработан алгоритм объединения, который завершается при любой разрешимой входной задаче, но может продолжать поиск решения неразрешимой входной проблемы вечно.

Объединение разрешимо для следующих теорий:

• А
• А , С
• А , С , Я
• А , С , Н _л
• А , я
• A , N _l , N _r (моноид)
• С
• Булевы кольца
• Абелевы группы , даже если сигнатура расширена произвольными дополнительными символами (но не аксиомами)
• K4 Модальные алгебры

Унификация полуразрешима для следующих теорий:

• А , Д _л , Д _р
• А , С , Д _л
• Коммутативные кольца

Односторонняя парамодуляция

Если существует конвергентная система переписывания терминов R, доступная для E , алгоритм односторонней парамодуляции можно использовать для перечисления всех решений заданных уравнений.

Правила односторонней парамодуляции

грамм ∪ { ж ( s 1 ,..., s п ) ≐ ж ( т 1 ,..., т п ) }	; С	⇒	г ∪ { s 1 ≐ т 1 , ..., s n ≐ т n }	; С		разлагать
г ∪ { Икс ≐ т }	; С	⇒	г { Икс ↦ т }	; S { Икс ↦ т } ∪ { Икс ↦ т }	если переменная x не встречается в t	устранять
г ∪ { ж ( s 1 ,..., s п ) ≐ т }	; С	⇒	г ∪ { s 1 ≐ ты 1 , ..., s п ≐ ты п , р ≐ т }	; С	если f ( u 1 ,..., un ) → r — правило из R	мутировать
г ∪ { ж ( s 1 ,..., s п ) ≐ y }	; С	⇒	г ∪ { s 1 ≐ y 1 , ..., s n ≐ y n , y ≐ ж ( y 1 ,..., y n ) }	; С	если y 1 ,..., y n — новые переменные	подражать

Начиная с G — решаемой проблемы объединения, а S — замены идентичности, правила применяются недетерминировано до тех пор, пока пустое множество не станет фактическим G , и в этом случае фактическое S является объединяющей заменой. В зависимости от порядка применения правил парамодуляции, выбора фактического уравнения из G и выбора R правил в mutate возможны разные пути вычислений. Лишь некоторые из них приводят к решению, тогда как другие заканчиваются на G ≠ {}, где дальнейшее правило не применимо (например, G = { f (...) ≐ g (...) }).

Пример системы перезаписи терминов R

1	приложение ( ноль , z )	→ я
2	приложение ( x . y , z )	→ х . приложение ( y , z )

Например, термин «система перезаписи R» используется , определяющий оператор добавления списков, построенных из cons и nil ; где cons ( x , y ) записывается в инфиксной записи как x . y для краткости; например приложение ( a.b.nil ​ ​ ​ ​ , c.d.nil ​ ​ ​ ) → a . приложение ( б . ноль , c . d . ноль ) → а . б . приложение ( ноль , c . d . ноль ) → а . б . в . д . nil демонстрирует объединение списков a . б . ноль и c . д . nil , используя правила перезаписи 2, 2 и 1. Эквациональная теория E, соответствующая R представляет собой конгруэнтное замыкание R , , оба рассматриваемые как бинарные отношения в терминах. Например app ( a.b.nil ​ ​ ​ ​ , c.d.nil ​ ​ . ) ≡ a , б . в . д . ноль ≡ приложение ( a . b . c . d . ноль , ноль ). Алгоритм парамодуляции перечисляет решения уравнений относительно этого E при использовании примера R .

Успешный пример пути вычислений для задачи объединения { app ( x , app ( y , x )) ≐ a . а . ноль } показано ниже. Чтобы избежать конфликтов имен переменных, правила перезаписи последовательно переименовываются каждый раз перед их использованием с помощью правила mutate ; v ₂ , v ₃ , ... — это имена переменных, генерируемые компьютером для этой цели. В каждой строке выбранное уравнение из G выделено красным. Каждый раз, когда изменения применяется правило , выбранное правило перезаписи ( 1 или 2 ) указывается в круглых скобках. Из последней строки объединяющая замена S = { y ↦ nil , x ↦ a . ноль } можно получить. Фактически, приложение ( Икс , приложение ( y , Икс )) { y ↦ ноль , Икс ↦ а . ноль } = приложение ( а . ноль , приложение ( ноль , а . ноль )) ≡ приложение ( а . ноль , а . ноль ) ≡ а . приложение ( ноль , а . ноль ) ≡ а . а . nil решает данную проблему. Второй успешный путь вычислений, который можно получить, выбрав «mutate(1), mutate(2), mutate(2), mutate(1)», приводит к замене S = { y ↦ a . а . ноль , х ↦ ноль }; здесь это не показано. Никакой другой путь не приведет к успеху.

Пример унификации вычислений

Используемое правило		г	С
		{ приложение ( x , приложение ( y , x )) ≐ а . а . ноль }	{}
мутировать(2)	⇒	{ Икс ≐ v 2 . v 3 , приложение ( y , x ) ≐ v 4 , v2 . приложение ( v 3 , v 4 ) ≐ a . а . ноль }	{}
разлагать	⇒	{ Икс ≐ v 2 . v 3 , приложение ( y , x ) ≐ v 4 , v 2 ≐ a , приложение ( v 3 , v 4 ) ≐ a . ноль }	{}
устранять	⇒	{ app ( y , v 2 . v 3 ) ≐ v 4 , v 2 ≐ а , приложение ( v 3 , v 4 ) ≐ а . ноль }	{ Икс ↦ v 2 . v 3 }
устранять	⇒	{ приложение ( y , а . v 3 ) ≐ v 4 , приложение ( v 3 , v 4 ) ≐ a . ноль }	{ Икс ↦ а . v 3 }
мутировать(1)	⇒	{ у ≐ ноль , а . v 3 ≐ v 5 , v 5 ≐ v 4 , приложение ( v 3 , v 4 ) ≐ a . ноль }	{ Икс ↦ а . v 3 }
устранять	⇒	{ у ≐ ноль , а . v 3 ≐ v 4 , приложение ( v 3 , v 4 ) ≐ a . ноль }	{ Икс ↦ а . v 3 }
устранять	⇒	{ а . v 3 ≐ v 4 , приложение ( v 3 , v 4 ) ≐ a . ноль }	{ у ↦ ноль , Икс ↦ а . v 3 }
мутировать(1)	⇒	{ а . v 3 ≐ v 4 , v 3 ≐ ноль , v 4 ≐ v 6 , v 6 ≐ а . ноль }	{ у ↦ ноль , Икс ↦ а . v 3 }
устранять	⇒	{ а . v 3 ≐ v 4 , v 3 ≐ ноль , v 4 ≐ а . ноль }	{ у ↦ ноль , Икс ↦ а . v 3 }
устранять	⇒	{ а . ноль ≐ v 4 , v 4 ≐ а . ноль }	{ у ↦ ноль , Икс ↦ а . ноль }
устранять	⇒	{ и . ноль ≐ а . ноль }	{ у ↦ ноль , Икс ↦ а . ноль }
разлагать	⇒	{ а ≐ а , ноль ≐ ноль }	{ у ↦ ноль , Икс ↦ а . ноль }
разлагать	⇒	{ ноль ≐ ноль }	{ у ↦ ноль , Икс ↦ а . ноль }
разлагать	⇒	{}	{ у ↦ ноль , Икс ↦ а . ноль }

Сужение

Треугольная диаграмма шага сужения s ↝ t в позиции p в терме s с объединяющей заменой σ (нижний ряд) с использованием правила перезаписи l → r (верхний ряд)

Если R — сходящаяся система переписывания термов для E , подход, альтернативный предыдущему разделу, состоит в последовательном применении « сужения шагов »; в конечном итоге это приведет к перечислению всех решений данного уравнения. Шаг сужения (см. рисунок) заключается в

• выбор неизменяемого подтерма текущего термина,
• синтаксически объединяя его с левой частью правила из R и
• замена правой части созданного правила на конкретизированный термин.

Формально, если l → r — это переименованная копия правила перезаписи из R , не имеющая общих переменных с термом s и подтерм s | _p не является переменной и его можно объединить с l через mgu σ , тогда s можно сузить до термина t = sσ [ rσ ] _p , т.е. до термина sσ подтерма в p , с заменой на rσ . Ситуацию, когда s можно сузить до t, обычно обозначают как s ↝ t . Интуитивно последовательность сужающих шагов t ₁ ↝ t ₂ ↝ ... ↝ t _n можно рассматривать как последовательность шагов перезаписи t ₁ → t ₂ → ... → t _n , но с начальным t ₁ членом далее и далее реализуются по мере необходимости, чтобы каждое из используемых правил стало применимым.

пример Приведенный выше расчета парамодуляции соответствует следующей сужающей последовательности («↓» указывает на создание экземпляра здесь):

приложение (

Икс

, приложение ( и ,

Икс

))

↓

↓

Икс ↦ v 2 . в 3

приложение (

в 2 . v3

, приложение ( и ,

в 2 . v3

))

→

в 2 . приложение ( v 3 , приложение (

и

, т 2 . в 3 ))

↓

и ↦ ноль

в 2 . приложение ( v 3 , приложение (

ноль

, т 2 . в 3 ))

→

v 2 . app (

vv3

, т 2 .

vv3

)

↓

↓

v 3 ↦ ноль

v 2 . app (

ноль

, т 2 .

ноль

)

→

в 2 . в 2 . ноль

Последний член, v ₂ . в ₂ . nil может быть синтаксически унифицирован с исходным термином правой части a . а . ноль .

Лемма о сужении гарантирует, что всякий раз, когда экземпляр термина s может быть переписан в термин t с помощью конвергентной системы переписывания терминов, тогда s и t могут быть сужены и переписаны в термины s ′ и t ′ соответственно, так что t ′ является экземпляром из s ' .

Формально: всякий раз, когда sσ → ∗ t выполняется для некоторой замены σ, то существуют члены s ′ , t ′ такие, что s ↝ ∗ s ′ и t → ∗ t ′ и s ′ τ = t ′ для некоторой замены τ.

Объединение высшего порядка

У Гольдфарба сведение 10-й проблемы Гильберта к унифицируемости второго порядка, уравнение $X_{1}*X_{2}=X_{3}$ соответствует изображенной проблеме объединения с функциональными переменными $F_{i}$ соответствующий $X_{i}$ и $G$ свежий .

Многие приложения требуют учитывать унификацию типизированных лямбда-термов вместо термов первого порядка. Такое объединение часто называют объединением высшего порядка . Объединение высшего порядка неразрешимо , и такие проблемы унификации не имеют наиболее общих унификаторов. Например, проблема объединения { f ( a , b , a ) ≐ d ( b , a , c ) } , где единственной переменной является f , имеет решения { ж ↦ λ Икс .λ y .λ z . d ( y , Икс , c ) }, { ж ↦ λ Икс .λ y .λ z . d ( y , z , c ) }, { ж ↦ λ Икс .λ y .λ z . d ( y , а , c ) }, { ж ↦ λ Икс .λ y .λ z . d ( б , х , с ) }, { ж ↦ λ Икс .λ y .λ z . d ( б , z , c ) } и { ж ↦ λ Икс .λ y .λ z . д ( б , а , в ) }. Хорошо изученной ветвью унификации высшего порядка является проблема объединения просто типизированных лямбда-термов по модулю равенства, определяемого преобразованиями αβη. Жерар Юэ предложил полуразрешимый алгоритм (предварительного) объединения. позволяющий осуществлять систематический поиск в пространстве объединителей (обобщающий алгоритм объединения Мартелли-Монтанари с правилами для терминов, содержащих переменные более высокого порядка), который, кажется, работает достаточно хорошо на практике. Хюэт и Жиль Доук написали статьи, посвященные этой теме.

Некоторые подмножества унификации более высокого порядка хорошо себя ведут, поскольку они разрешимы и имеют наиболее общий унификатор для решаемых задач. Одним из таких подмножеств являются ранее описанные члены первого порядка. Объединение шаблонов высшего порядка , благодаря Дейлу Миллеру, еще одно такое подмножество. Языки логического программирования высшего порядка λProlog и Twelf перешли от полной унификации высшего порядка к реализации только фрагмента шаблона; Удивительно, но унификация шаблона достаточна почти для всех программ, если каждая проблема унификации, не связанная с шаблоном, приостанавливается до тех пор, пока последующая замена не поместит унификацию во фрагмент шаблона. Надмножество унификации шаблонов, называемое унификацией функций как конструкторов, также хорошо себя ведет. Средство доказательства теоремы Ципперпозиции имеет алгоритм, объединяющий эти подмножества с хорошим поведением в полный алгоритм объединения более высокого порядка.

В компьютерной лингвистике одна из наиболее влиятельных теорий эллиптического построения заключается в том, что эллипсы представляются свободными переменными, значения которых затем определяются с использованием унификации высшего порядка. Например, семантическое представление фразы «Джон любит Мэри и Питер тоже» имеет вид ( j , m ) ∧ R( p ) , а значение R (семантическое представление многоточия) определяется уравнением типа ( j , м ) знак равно р( j ) . Процесс решения таких уравнений называется унификацией высшего порядка.

Уэйн Снайдер дал обобщение как унификации высшего порядка, так и E-унификации, то есть алгоритм унификации лямбда-членов по модулю эквациональной теории.

См. также

• Переписывание
• Допустимое правило
• Явная замена в лямбда-исчислении
• Решение математических уравнений
• Разъединение : решение неравенств между символическими выражениями
• Антиунификация : вычисление наименее общего обобщения (lgg) двух терминов, двойственное вычислению наиболее общего экземпляра (mgu).
• Решетка включения , решетка, имеющая объединение как встречу и антиобъединение как соединение.
• Выравнивание онтологии (используйте унификацию с семантической эквивалентностью )

Дальнейшее чтение

• Франц Баадер и Уэйн Снайдер (2001). «Теория объединения». Архивировано 8 июня 2015 г. в Wayback Machine . Джон Алан Робинсон и Андрей Воронков , редакторы, «Справочник по автоматическому рассуждению» , том I, страницы 447–533. Издательство Elsevier Science.
• Жиль Довек (2001). «Объединение и сопоставление высшего порядка». Архивировано 15 мая 2019 г. в Wayback Machine . В Справочнике по автоматизированному рассуждению .
• Франц Баадер и Тобиас Нипков (1998). Переписывание терминов и все такое . Издательство Кембриджского университета.
• Франц Баадер и Йорг Х. Зикманн (1993). «Теория объединения». В Справочнике по логике в искусственном интеллекте и логическом программировании .
• Жан-Пьер Жуанно и Клод Киршнер (1991). «Решение уравнений в абстрактных алгебрах: обзор унификации на основе правил». В вычислительной логике: Очерки в честь Алана Робинсона .
• Нахум Дершовиц и Жан-Пьер Жуанно , Rewrite Systems , в: Ян ван Леувен (ред.), Справочник по теоретической информатике , том B Формальные модели и семантика , Elsevier, 1990, стр. 243–320.
• Йорг Х. Зикманн (1990). «Теория объединения». В Клоде Киршнере (редактор) Unification . Академическая пресса.
• Кевин Найт (март 1989 г.). «Унификация: междисциплинарный обзор» (PDF) . Обзоры вычислительной техники ACM . 21 (1): 93–124. CiteSeerX   10.1.1.64.8967 . дои : 10.1145/62029.62030 . S2CID   14619034 .
• Жерар Юэ и Дерек К. Оппен (1980). «Уравнения и правила перезаписи: обзор» . Технический отчет. Стэндфордский Университет.
• Раулефс, Питер; Зикманн, Йорг; Сабо, П.; Унверихт, Э. (1979). «Краткий обзор современного состояния проблем сопоставления и унификации». Бюллетень ACM SIGSAM . 13 (2): 14–20. дои : 10.1145/1089208.1089210 . S2CID   17033087 .
• Клод Киршнер и Элен Киршнер. Переписывание, решение, доказательство . В подготовке.