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

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

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

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

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

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

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

Предпосылки

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

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

Замена

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

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

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

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

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

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

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

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

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

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

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

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

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

Например, задача объединения { x ≐ z , y ≐ f ( x ) } имеет объединитель { x ↦ z , y ↦ f ( 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 года

Символы упорядочены таким образом, что переменные предшествуют символам функций. Термины упорядочены по возрастанию длины записи; термины одинаковой длины упорядочены лексикографически . ^[6] Для набора терминов T его путь несогласия p является лексикографически наименьшим путем, где два члена термина T различаются. Его множество несогласия — это набор подтерминов , начинающихся с p , формально: { t | p  : ${\displaystyle t\in T}$ }. ^[7]

Алгоритм: ^[8]
Given a set T of terms to be unified
Let ${\displaystyle \sigma }$ initially be the identity substitution
do forever
    if ${\displaystyle T\sigma }$ is a singleton set then
        return ${\displaystyle \sigma }$
    fi
    let D be the disagreement set of ${\displaystyle 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
    ${\displaystyle \sigma :=\sigma \{s\mapsto t\}}$
done

Жак Эрбран обсудил основные концепции унификации и набросал алгоритм в 1930 году. ^{[9] [10] [11]} Однако большинство авторов приписывают первый алгоритм унификации Джону Алану Робинсону (см. вставку). ^{[12] [13] [примечание 5]} Алгоритм Робинсона имел наихудшее экспоненциальное поведение как во времени, так и в пространстве. ^{[11] [15]} Многочисленные авторы предложили более эффективные алгоритмы унификации. ^[16] Алгоритмы с худшим поведением линейного времени были обнаружены независимо Мартелли и Монтанари (1976) и Патерсоном и Вегманом (1976) ^{[примечание 6]} Баадер и Снайдер (2001) используют похожую технику, что и Патерсон-Вегман, поэтому являются линейными, ^[17] но, как и большинство алгоритмов унификации линейного времени, они медленнее версии Робинсона на входах небольшого размера из-за накладных расходов на предварительную обработку входов и постобработку выходных данных, таких как построение представления DAG . де Шампо (2022) также имеет линейную сложность по размеру входных данных, но может конкурировать с алгоритмом Робинсона на входах небольшого размера. Ускорение достигается за счет использования объектно-ориентированного представления исчисления предикатов, которое избегает необходимости предварительной и постобработки, вместо этого возлагая ответственность за создание подстановки и обработку псевдонимов на переменные объекты. де Шампо утверждает, что возможность добавления функциональности к исчислению предикатов, представленному в виде программных объектов, предоставляет возможности для оптимизации и других логических операций. ^[15]

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

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

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

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

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

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

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

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

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

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

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

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

В Прологе:

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

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

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

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

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

Применение: Унификация структуры функций

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

Унификация с сортировкой по порядку

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

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

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

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

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

Предыстория бесконечных деревьев:

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

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

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

Приложения:

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

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

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

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

Базовые знания E могли бы сформулировать коммутативность ⁠ ⁠ ${\displaystyle *}$ с помощью универсального равенства « ⁠ ⁠ ${\displaystyle u*v=v*u}$ для всех u , v ».

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

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

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

• А ^[26]
• А , С ^[27]
• А , С , Я ^[28]
• А , С , Н1 ^{[примечание 9]} _[ ^28]
• А , Я ^[29]
• A , N _l , N _r (моноид) ^[30]
• С ^[31]
• Булевы кольца ^{[32] [33]}
• Абелевы группы , даже если сигнатура расширена произвольными дополнительными символами (но не аксиомами) ^[34]
• Модальные алгебры K4 ^[35]

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

• А , Дл , Др ^[ _{36 ]}
• А , С , Дл ^{[примечание 9]} _[ ^37]
• Коммутативные кольца ^[34]

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

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

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

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

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

Сужение

Треугольная диаграмма сужающегося шага 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 _{1 ,} который все больше и больше конкретизируется по мере необходимости, чтобы сделать каждое из используемых правил применимым.

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

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

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

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

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

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

Во многих приложениях требуется рассматривать унификацию типизированных лямбда-термов вместо термов первого порядка. Такая унификация часто называется унификацией высшего порядка . Унификация высшего порядка неразрешима , ^{[40] [41] [42]} , и такие проблемы унификации не имеют самых общих унификаторов. Например, проблема унификации { f ( a , b , a ) ≐ d ( b , a , c )}, где единственной переменной является f , имеет решения { f ↦ λ x.λ y.λ z . d ( y , x , c )}, { f ↦ λ x.λ y.λ z . d ( y , z , c ) } , { f ↦ λ x.λ y.λ z . d ( y , a , c ) }, { f ↦ λ x .λ y .λ z . d ( b , x , c ) }, { f ↦ λ x .λ y .λ z . d ( b , z , c ) } и { f ↦ λ x .λ y .λ z . d ( b , a , c ) }. Хорошо изученной ветвью унификации высшего порядка является проблема унификации просто типизированных лямбда-терминов по модулю равенства, определяемого преобразованиями αβη. Жерар Юэ дал полуразрешимый алгоритм (пред)унификации ^[43] , который позволяет проводить систематический поиск пространства унификаторов (обобщая алгоритм унификации Мартелли-Монтанари ^[5] с правилами для термов, содержащих переменные высшего порядка), который, по-видимому, достаточно хорошо работает на практике. Юэ ^[44] и Жиль Довек ^[45] написали статьи, посвященные обзору этой темы.

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

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

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

Смотрите также

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

Примечания

1. Например , a ⊕ ( b ⊕ f ( x )) ≡ a ⊕ ( f ( x ) ⊕ b ) ≡ ( b ⊕ f ( x )) ⊕ a ≡ ( f ( x ) ⊕ b ) ⊕ a
2. с тех пор ${\displaystyle (x\oplus y)\{x\mapsto z,y\mapsto z\}=z\oplus z\equiv z}$
3. поскольку z { z ↦ x ⊕ y } = x ⊕ y
4. формально: каждый объединитель τ удовлетворяет ∀ x : xτ = ( xσ ) ρ для некоторой замены ρ
5. Робинсон использовал синтаксическую унификацию первого порядка в качестве базового строительного блока своей процедуры разрешения для логики первого порядка, что стало большим шагом вперед в технологии автоматизированного рассуждения , поскольку она устранила один из источников комбинаторного взрыва : поиск инстанциации терминов. ^[14]
6. Независимое открытие указано в Martelli & Montanari (1982) sect.1, p.259. Издатель журнала получил Paterson & Wegman (1978) в сентябре 1976 года.
7. 1 , стр. 261. Их правило (a) соответствует здесь замене правил , (b) удалению , (c) как разложению , так и конфликту , и (d) как устранению, так и проверке .
8. Хотя правило сохраняет x ≐ t в G , оно не может зацикливаться вечно, поскольку его предварительное условие x ∈ vars ( G ) становится недействительным при первом применении. В более общем смысле, алгоритм гарантированно всегда завершается, см. ниже.
9. при наличии равенства C равенства N _l и N _r равносильны, аналогичные для D _l и D _r

Ссылки

1. Dowek, Gilles (1 января 2001 г.). «Высшее объединение и сопоставление». Справочник по автоматизированному рассуждению. Elsevier Science Publishers BV, стр. 1009–1062. ISBN 978-0-444-50812-6. Архивировано из оригинала 15 мая 2019 . Получено 15 мая 2019 .
2. Вукмирович, Петар; Бенткамп, Александр; Нуммелин, Виса (14 декабря 2021 г.). «Эффективное полное объединение высшего порядка». Логические методы в информатике . 17 (4): 6919. arXiv : 2011.09507 . doi : 10.46298/lmcs-17(4:18)2021 .
3. Апт, Кшиштоф Р. (1997). От логического программирования к Прологу (1-е изд.). Лондон Мюнхен: Prentice Hall. стр. 24. ISBN 013230368X.
4. Фаж, Франсуа; Юэ, Жерар (1986). «Полные наборы объединителей и сопоставлений в теориях уравнений». Теоретическая информатика . 43 : 189–200. дои : 10.1016/0304-3975(86)90175-1 .
5. Мартелли, Альберто; Монтанари, Уго (апрель 1982 г.). «Эффективный алгоритм унификации». ACM Trans. Program. Lang. Syst . 4 (2): 258–282. doi :10.1145/357162.357169. S2CID  10921306.
6. Робинсон (1965) № 2.5, 2.14, стр. 25
7. Робинсон (1965) № 5.6, стр. 32
8. Робинсон (1965) № 5.8, стр. 32
9. Ж. Эрбран: Исследования по теории демонстрации. Travaux de la société des Sciences et des Lettres de Varsovie , класс III, Sciences Mathématiques et Physiques, 33, 1930.
10. Жак Эрбран (1930). Recherches sur la théorie de laдемонстрировать (PDF) (докторская диссертация). А. Том. 1252. Парижский университет.Здесь: стр.96-97
11. Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). Лекции о Жаке Эрбране как логике (отчет SEKI). DFKI. arXiv : 0902.4682 .Здесь: стр.56
12. Робинсон, JA (январь 1965). «Машинно-ориентированная логика, основанная на принципе разрешения». Журнал ACM . 12 (1): 23–41. doi : 10.1145/321250.321253 . S2CID  14389185.; Здесь: раздел 5.8, стр.32
13. JA Robinson (1971). «Вычислительная логика: унификация вычислений». Machine Intelligence . 6 : 63–72.
14. Дэвид А. Даффи (1991). Принципы автоматического доказательства теорем . Нью-Йорк: Wiley. ISBN 0-471-92784-8.Здесь: Введение в раздел 3.3.3 «Унификация» , стр.72.
15. de Champeaux, Dennis (август 2022 г.). «Быстрый линейный алгоритм объединения» (PDF) . Журнал автоматизированного рассуждения . 66 : 845–860. doi :10.1007/s10817-022-09635-1.
16. Пер Мартелли и Монтанари (1982):
    • Льюис Денвер Бакстер (февраль 1976 г.). Практически линейный алгоритм унификации (PDF) (Res. Report). Том CS-76-13. Univ. of Waterloo, Ontario.
    • Жерар Юэ (сентябрь 1976 г.). Резолюция d'Equations dans des Langages d'Ordre 1,2,...ω (Эти государственные). Парижский университет VII.
    • Мартелли, Альберто и Монтанари, Уго (июль 1976 г.). Объединение в линейном времени и пространстве: структурированное изложение (Внутренняя заметка). Том. ИЭИ-В76-16. Consiglio Nazionale delle Ricerche, Пиза. Архивировано из оригинала 15 января 2015 г.
    • Paterson, MS; Wegman, MN (май 1976 г.). Chandra, Ashok K.; Wotschke, Detlef; Friedman, Emily P.; Harrison, Michael A. (ред.). Линейное объединение . Труды восьмого ежегодного симпозиума ACM по теории вычислений (STOC). ACM. стр. 181–186. doi : 10.1145/800113.803646 .
    • Paterson, MS ; Wegman, MN (апрель 1978 г.). «Линейное объединение». J. Comput. Syst. Sci . 16 (2): 158–167. doi : 10.1016/0022-0000(78)90043-0 .
    • JA Robinson (январь 1976 г.). "Быстрая унификация". В Woodrow W. Bledsoe , Michael M. Richter (ред.). Proc. Theorem Proving Workshop Oberwolfach . Oberwolfach Workshop Report. Vol. 1976/3.^{[ постоянная мертвая ссылка ]}
    • М. Вентурини-Цилли (октябрь 1975 г.). «Сложность алгоритма унификации для выражений первого порядка». Calcolo . 12 (4): 361–372. doi :10.1007/BF02575754. S2CID  189789152.
17. Баадер, Франц; Снайдер, Уэйн (2001). «Теория объединения» (PDF) . Справочник по автоматизированному рассуждению . С. 445–533. doi :10.1016/B978-044450813-3/50010-2.
18. Макбрайд, Конор (октябрь 2003 г.). «Унификация первого порядка с помощью структурной рекурсии». Журнал функционального программирования . 13 (6): 1061–1076. CiteSeerX 10.1.1.25.1516 . doi :10.1017/S0956796803004957. ISSN  0956-7968. S2CID  43523380. Получено 30 марта 2012 г. 
19. например, Патерсон и Вегман (1978) раздел 2, стр. 159
20. "Декларативная целочисленная арифметика". SWI-Prolog . Получено 18 февраля 2024 г.
21. Джонатан Колдер, Майк Рип и Хэнк Зееват,, Алгоритм генерации в унифицированной категориальной грамматике. В трудах 4-й конференции Европейского отделения Ассоциации компьютерной лингвистики, страницы 233-240, Манчестер, Англия (10–12 апреля), Институт науки и технологий Манчестерского университета, 1989.
22. Грэм Херст и Дэвид Сент-Онж, [1] Лексические цепочки как представление контекста для обнаружения и исправления малапропизмов, 1998.
23. Вальтер, Кристоф (1985). "Механическое решение парового катка Шуберта с помощью многосортного разрешения" (PDF) . Artif. Intell . 26 (2): 217–224. doi :10.1016/0004-3702(85)90029-3. Архивировано из оригинала (PDF) 2011-07-08 . Получено 2013-06-28 .
24. Смолка, Герт (ноябрь 1988 г.). Логическое программирование с полиморфно упорядоченными типами (PDF) . Международный семинар по алгебраическому и логическому программированию. LNCS. Том 343. Springer. С. 53–70. doi :10.1007/3-540-50667-5_58.
25. Шмидт-Шаус, Манфред (апрель 1988 г.). Вычислительные аспекты упорядоченной логики с декларациями терминов . Конспект лекций по искусственному интеллекту (LNAI). Том 395. Springer.
26. Гордон Д. Плоткин , Теоретические свойства решеток применительно к субсубпозиции , Меморандум MIP-R-77, Эдинбургский университет, июнь 1970 г.
27. Марк Э. Стикель , Алгоритм унификации для ассоциативно-коммутативных функций , Журнал Ассоциации вычислительной техники, т. 28, № 3, стр. 423–434, 1981
28. F. Fages, Ассоциативно-коммутативное объединение , J. Symbolic Comput., т. 3, № 3, стр. 257–275, 1987
29. Франц Баадер, Унификация в идемпотентных полугруппах имеет нулевой тип , Журнал автоматических рассуждений, т. 2, № 3, 1986
30. Дж. Маканин, Проблема разрешимости уравнений в свободной полугруппе , АН СССР, т.233, №2, 1977
31. F. Fages (1987). «Ассоциативно-коммутативное объединение» (PDF) . J. Symbolic Comput . 3 (3): 257–275. doi :10.1016/s0747-7171(87)80004-4. S2CID  40499266.
32. Мартин, У., Нипков, Т. (1986). «Унификация в булевых кольцах». В Jörg H. Siekmann (ред.). Proc. 8th CADE . LNCS. Том 230. Springer. стр. 506–513.{{cite book}}: CS1 maint: multiple names: authors list (link)
33. A. Boudet; JP Jouannaud; M. Schmidt-Schauss (1989). «Унификация булевых колец и абелевых групп». Journal of Symbolic Computation . 8 (5): 449–477. doi : 10.1016/s0747-7171(89)80054-9 .
34. Баадер и Снайдер (2001), с. 486.
35. Ф. Баадер и С. Гиларди, Унификация в модальной и дескриптивной логике , Logic Journal of the IGPL 19 (2011), № 6, стр. 705–730.
36. П. Сабо, Unifikationstheorie erster Ordnung ( Теория объединения первого порядка ), Thesis, Univ. Карлсруэ, Западная Германия, 1982 г.
37. Йорг Х. Зикманн, Универсальная унификация , Труды 7-й Международной конференции по автоматизированной дедукции, Springer LNCS т. 170, стр. 1–42, 1984 г.
38. Н. Дершовиц и Г. Сивакумар, Решение задач в эквациональных языках , Труды 1-го Международного семинара по системам переписывания условных термов, Springer LNCS т. 308, стр. 45–55, 1988 г.
39. Фэй (1979). «Унификация первого порядка в эквациональной теории». Труды 4-го семинара по автоматизированной дедукции . С. 161–167.
40. Уоррен Д. Голдфарб (1981). «Неразрешимость проблемы объединения второго порядка». TCS . 13 (2): 225–230. doi : 10.1016/0304-3975(81)90040-2 .
41. Жерар П. Юэ (1973). «Неразрешимость объединения в логике третьего порядка». Информация и управление . 22 (3): 257–267. doi : 10.1016/S0019-9958(73)90301-X .
42. Клаудио Луккези: Неразрешимость проблемы унификации для языков третьего порядка (Исследовательский отчет CSRR 2059; Кафедра компьютерных наук, Университет Ватерлоо, 1972)
43. Жерар Юэ: Алгоритм объединения типизированного лямбда-исчисления []
44. Жерар Юэ: Объединение высшего порядка 30 лет спустя
45. Жиль Довек: Унификация и сопоставление высшего порядка. Справочник по автоматизированному рассуждению 2001: 1009–1062
46. Миллер, Дейл (1991). «Язык логического программирования с лямбда-абстракцией, функциональными переменными и простой унификацией» (PDF) . Журнал логики и вычислений . 1 (4): 497–536. doi :10.1093/logcom/1.4.497.
47. Либал, Томер; Миллер, Дейл (май 2022 г.). «Унификация функций как конструкторов высшего порядка: расширенная унификация шаблонов». Annals of Mathematics and Artificial Intelligence . 90 (5): 455–479. doi : 10.1007/s10472-021-09774-y .
48. Гардент, Клэр ; Кольхазе, Майкл ; Конрад, Карстен (1997). «Многоуровневый, высокопорядковый унифицированный подход к эллипсису». Представлено в Европейскую ассоциацию компьютерной лингвистики (EACL) . CiteSeerX 10.1.1.55.9018 . 
49. Уэйн Снайдер (июль 1990 г.). «Высшее электронное объединение». Труды 10-й конференции по автоматизированной дедукции . LNAI. Т. 449. Springer. С. 573–587.

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

• Франц Баадер и Уэйн Снайдер (2001). «Теория объединения» Архивировано 2015-06-08 в Wayback Machine . В книге Джона Алана Робинсона и Андрея Воронкова , редакторов, Handbook of Automated Reasoning , том I, страницы 447–533. Elsevier Science Publishers. ^{[ мертвая ссылка ]}
• Жиль Доуек (2001). "Высшее объединение и сопоставление" Архивировано 2019-05-15 в Wayback Machine . В Handbook of Automated Reasoning .
• Франц Баадер и Тобиас Нипков (1998). Переписывание терминов и все такое. Cambridge University Press.
• Франц Баадер и Йорг Х. Зикманн  [de] (1993). «Теория объединения». В Handbook of Logic in Artificial Intelligence and Logic Programming .
• Жан-Пьер Жуанно и Клод Киршнер (1991). «Решение уравнений в абстрактных алгебрах: обзор унификации на основе правил». В Computational Logic: Essays in Honor of Alan Robinson .
• Нахум Дершовиц и Жан-Пьер Жуанно , Системы перезаписи , в: Ян ван Леувен (ред.), Справочник по теоретической информатике , том B Формальные модели и семантика , Elsevier, 1990, стр. 243–320
• Йорг Х. Зикман (1990). «Теория объединения». В Клоде Киршнере (редактор) Объединение . Academic Press.
• Кевин Найт (март 1989 г.). «Унификация: многопрофильное исследование» (PDF) . ACM Computing Surveys . 21 (1): 93–124. CiteSeerX  10.1.1.64.8967 . doi :10.1145/62029.62030. S2CID  14619034.
• Жерар Юэ и Дерек К. Оппен (1980). «Уравнения и правила перезаписи: обзор». Технический отчет. Стэнфордский университет.
• Раулефс, Питер; Зикманн, Йорг; Сабо, П.; Унферихт, Э. (1979). «Краткий обзор современного состояния проблем сопоставления и объединения». ACM SIGSAM Bulletin . 13 (2): 14–20. doi :10.1145/1089208.1089210. S2CID  17033087.
• Клод Киршнер и Элен Киршнер. Переписывание, Решение, Доказательство . В процессе подготовки.