В логике и информатике , объединение является алгоритмическим процессом решения уравнений между символическими выражениями .
В зависимости от того, какие выражения (также называемые терминами ) могут встречаться в наборе уравнений (также называемые проблемой унификации ) и какие выражения считаются равными, различают несколько структур унификации. Если в выражении допускаются переменные высшего порядка, то есть переменные, представляющие функции , процесс называется объединением высшего порядка , в противном случае объединением первого порядка . Если требуется решение, чтобы сделать обе стороны каждого уравнения буквально равными, процесс называется синтаксическим или свободным объединением , в противном случае семантическим или уравнительным объединением или E-объединением., или объединение по модулю теории .
Решение задачи объединения обозначается как замещения , то есть, отображение , присваивающее символическое значение для каждого переменных выражений Проблемы в. Алгоритм унификации должен вычислять для данной проблемы полный и минимальный набор подстановки, то есть набор, охватывающий все ее решения и не содержащий лишних элементов. В зависимости от структуры полный и минимальный набор подстановок может иметь не более одного, не более конечного числа, или, возможно, бесконечно много членов, или может не существовать вовсе. [примечание 1] [1] В некоторых фреймворках обычно невозможно решить, существует ли какое-либо решение. Для синтаксической унификации первого порядка Мартелли и Монтанари [2] предложили алгоритм, который сообщает о неразрешимости или вычисляет полный и минимальный одноэлементный набор подстановок, содержащий так называемый самый общий унификатор .
Например, при использовании x , y , z в качестве переменных набор одноэлементных уравнений { cons ( x , cons ( x , nil )) = cons (2, y )} представляет собой синтаксическую задачу унификации первого порядка, которая имеет замену { x ↦ 2, y ↦ cons (2, nil )} в качестве единственного решения. Синтаксическая проблема объединения первого порядка { y = cons (2, y )} не имеет решения на множестве конечных членов ; однако он имеет единственное решение { y ↦ cons (2, cons (2, cons (2, ...)))} над множеством бесконечных деревьев . Семантическая задача объединения первого порядка { a ⋅ x = x ⋅ a } имеет каждую подстановку вида { x ↦ a ⋅ ... ⋅ a } как решение в полугруппе , т. Е. Если (⋅) считается ассоциативным ; та же проблема, рассматриваемая в абелевой группе , где (⋅) считается также коммутативным , вообще имеет любую замену в качестве решения. Одноэлементный набор { a = y ( x )} представляет собой синтаксическую проблему унификации второго порядка, поскольку y - это функциональная переменная. Одно из решений - { x ↦ a , y ↦ ( тождественная функция )}; другой - { y ↦ ( постоянная функция, отображающая каждое значение в a ), x ↦ (любое значение) }.
Алгоритм объединения был впервые обнаружен Эрбрано , [3] [4] [5] в то время как первое официальное расследование можно отнести к Джону Алан Робинсону , [6] [7] , который использовал первый порядок синтаксического объединения в качестве основного строительного блока его процедуры разрешения для логики первого порядка, большой шаг вперед в технологии автоматизированных рассуждений , поскольку он устранил один источник комбинаторного взрыва: поиск экземпляров терминов. Сегодня автоматическое мышление по-прежнему является основной прикладной областью унификации. Синтаксическая унификация первого порядка используется в логическом программировании и реализации системы типов на языке программирования , особенно в алгоритмах вывода типов на основе Хиндли-Милнера . Семантическая унификация используется в решателях SMT , алгоритмах перезаписи терминов и анализе криптографических протоколов . Унификация высшего порядка используется в помощниках проверки, например Isabelle и Twelf , а ограниченные формы унификации более высокого порядка (объединение шаблонов высшего порядка ) используются в некоторых реализациях языков программирования, таких как lambdaProlog , поскольку шаблоны высшего порядка выразительны. , но связанная с ними процедура объединения сохраняет теоретические свойства ближе к объединению первого порядка.
Общие формальные определения
Предпосылки
Формально унификационный подход предполагает
- Бесконечный набор от переменных . Для объединения более высокого порядка удобно выбратьне пересекаются с набором переменных, связанных лямбда-членами .
- Множество таких терминов , что. Для унификации первого и высшего порядка,обычно представляет собой набор терминов первого порядка (термины, построенные из переменных и функциональных символов) и лямбда-терминов (термины, содержащие некоторые переменные более высокого порядка) соответственно.
- Вары сопоставления : ℙ, присваивая каждому термину набор из свободных переменных , происходящих в.
- Отношение эквивалентности на , указывая, какие термины считаются равными. Для унификации более высокого порядка обычно если а также являются альфа-эквивалентами . Для электронного объединения первого порядка,отражает базовые знания о некоторых функциональных символах; например, если считается коммутативным, если результаты из путем замены аргументов в некоторых (возможно, во всех) случаях. [примечание 2] Если базовых знаний нет вообще, то только буквально или синтаксически идентичные термины считаются равными; в этом случае ≡ называется свободной теорией (потому что это свободный объект ), пустой теорией (потому что набор эквациональных предложений или фоновых знаний пуст), теорией неинтерпретируемых функций (поскольку унификация выполняется на неинтерпретированные термины ) или теории конструкторов (потому что все функциональные символы просто создают термины данных, а не оперируют ими).
Срок первого порядка
Учитывая набор переменных символов, набор постоянных символов и множеств из п -значных функциональных символов, также называемые операторные символы для каждого натурального числа, набор (неотсортированных) терминов первого порядка является рекурсивно определяется как наименьший набор со следующими свойствами: [8]
- каждый переменный символ - это термин: ,
- каждый постоянный символ - это термин: ,
- из каждых n терминов, и каждый n- мерный функциональный символ, больший термин можно построить.
Например, если переменный символ, - постоянный символ, а является двоичным функциональным символом, тогда , и поэтому) согласно правилу построения первого, второго и третьего сроков соответственно. Последний термин обычно записывается как, используя инфиксную нотацию и более общий символ оператора + для удобства.
Член высшего порядка
Замена
Замещение является отображениемот переменных к терминам; обозначение относится к отображению подстановки каждой переменной к сроку , для , а все остальные переменные - к себе. Применение этой замены к терминузаписывается в постфиксной записи как; это означает (одновременно) заменять каждое вхождение каждой переменной в срок от . Результат применения замены к сроку называется экземпляром этого термина. В качестве примера первого порядка, применяя замену { x ↦ h ( a , y ), z ↦ b } к члену
дает | |||||
Обобщение, специализация
Если срок имеет экземпляр, эквивалентный термину , то есть если для некоторой замены , тогда называется более общим, чем, а также называется более особенным, чем, или относится к. Например, более общий, чем если коммутативно , так как тогда.
Если ≡ является буквальным (синтаксическим) тождеством терминов, термин может быть как более общим, так и более специальным, чем другой, только если оба термина различаются только именами переменных, а не их синтаксической структурой; такие термины называются вариантами или переименованием друг друга. Например, это вариант , поскольку
а также
.
Тем не мение, это не вариант, так как никакая замена не может преобразовать последний член в первый. Следовательно, последний термин более особенный, чем первый.
Для произвольных , термин может быть как более общим, так и более специальным, чем структурно другой термин. Например, если ⊕ идемпотентно , то есть всегда, то член более общий, чем , [примечание 3] и наоборот, [примечание 4] хотя а также имеют разное строение.
Замена это более особенным , чем, или отнесены на замену, если более особенный, чем на каждый срок . Мы также говорим, что более общий, чем . Например более особенный, чем , но нет, как не более особенный, чем . [9]
Проблема объединения, набор решений
Проблема объединения конечное множество { л 1 ≐ г 1 , ..., л п ≐ г п } потенциальных уравнений, где л я , R I ∈ T . Замена σ является решением этой проблемы, если l i σ ≡ r i σ для. Такую замену еще называют объединителем проблемы объединения. Например, если ⊕ ассоциативно , задача объединения { x ⊕ a ≐ a ⊕ x } имеет решения { x ↦ a }, { x ↦ a ⊕ a }, { x ↦ a ⊕ a ⊕ a } и т. Д. а проблема { x ⊕ a ≐ a } не имеет решения.
Для данной задачи объединения множество унификаторов S называется полным, если каждая подстановка решения заменяется некоторой заменой σ ∈ S ; множество S называется минимальным, если ни один из его членов не включает другого.
Синтаксическая унификация терминов первого порядка
Синтаксическая унификация терминов первого порядка - наиболее широко используемая структура унификации. Он основан на Т быть множество членов первого порядка ( в течение некоторого заданного множества V переменных, С констант и Р п из п -ичными функциональные символы) и ≡ быть синтаксическое равенство . В этой структуре каждая разрешимая задача объединения { l 1 ≐ r 1 , ..., l n ≐ r n } имеет полное и, очевидно, минимальное, одноэлементное множество решений { σ } . Его член σ называется наиболее общим объединителем ( mgu ) задачи. Члены в левой и правой частях каждого потенциального уравнения становятся синтаксически равными, когда применяется mgu, т.е. l 1 σ = r 1 σ ∧ ... ∧ l n σ = r n σ . Любой объединитель проблемы включается [примечание 5] в mgu σ . Mgu уникален с точностью до вариантов: если S 1 и S 2 являются полными и минимальными наборами решений одной и той же синтаксической проблемы унификации, то S 1 = { σ 1 } и S 2 = { σ 2 } для некоторых замен σ 1 и σ 2 , а xσ 1 - вариант xσ 2 для каждой переменной x, встречающейся в задаче.
Например, проблема объединения { x ≐ z , y ≐ f ( x )} имеет объединитель { x ↦ z , y ↦ f ( z )}, потому что
Икс { x ↦ z , y ↦ f ( z )} знак равно z знак равно z { x ↦ z , y ↦ f ( z )} , а также y { x ↦ z , y ↦ f ( z )} знак равно f ( z ) знак равно f ( x ) { x ↦ z , y ↦ f ( z )} .
Это также самый общий объединитель. Другими объединителями для той же задачи являются, например, { x ↦ f ( x 1 ), y ↦ f ( f ( x 1 )), z ↦ f ( x 1 )}, { x ↦ f ( f ( x 1 )), y ↦ f ( f ( f ( x 1 ))), z ↦ f ( f ( x 1 ))} и так далее; подобных объединителей бесконечно много.
В качестве другого примера, проблема g ( x , x ) ≐ f ( y ) не имеет решения относительно того, что ≡ является буквальным тождеством, поскольку любая подстановка, применяемая к левой и правой стороне, сохранит внешние g и f , соответственно, и термины с разными внешними функциональными символами синтаксически различаются.
Алгоритм унификации
Символы упорядочены таким образом, что переменные предшествуют функциональным символам. Условия упорядочиваются путем увеличения письменной длины; одинаково длинные термины упорядочены лексикографически . [10] Для набора T терминов его путь несогласия p является лексикографически наименьшим путем, где два члена T различаются. Множество его несогласий - это набор подтерминов, начинающихся с p , формально: { t | p : }. [11]
Алгоритм: [12]
Учитывая набор Т терминов, подлежащих унификацииПозволять первоначально быть заменой идентичностиделай навсегда, если является одноэлементным набором, затем верните фи пусть D - множество разногласий пусть s , t - два лексикографически наименьших члена в D если s не является переменной или s встречается в t, то верните "НЕОДНОРОДНЫЙ" fi Выполнено
Первый алгоритм, предложенный Робинсоном (1965), был довольно неэффективным; ср. коробка. Следующий более быстрый алгоритм был разработан Мартелли, Монтанари (1982). [примечание 6] В этой статье также перечислены предыдущие попытки найти эффективный алгоритм синтаксической унификации, [13] [14] [15] [16] [17] [18]] и утверждается, что алгоритмы линейного времени были независимо открыты Мартелли, Монтанари. (1976) [15] и Патерсон, Вегман (1978). [16] [примечание 7]
Учитывая конечное множество потенциальных уравнений алгоритм применяет правила для преобразования его в эквивалентную систему уравнений вида { x 1 ≐ u 1 , ..., x m ≐ u m }, где x 1 , ..., x m - различные переменные и u 1 , ..., u m - члены, не содержащие ни одного из x i . Набор этой формы можно рассматривать как замену. Если решения нет, алгоритм завершается нажатием ⊥; другие авторы используют в этом случае "Ω", "{}" или " fail ". Операция замены всех вхождений переменной x в задаче G термом t обозначается G { x ↦ t }. Для простоты постоянные символы рассматриваются как функциональные символы, не имеющие аргументов.
Удалить разлагать если или же конфликт менять если а также исключить [примечание 8] если проверять
Происходит проверка
Попытка объединить переменную x с термином, содержащим x в качестве строгого подтерма x ≐ f (..., x , ...), приведет к бесконечному члену в качестве решения для x , поскольку x будет возникать как подтермин самого себя . В наборе (конечных) членов первого порядка, как определено выше, уравнение x ≐ f (..., x , ...) не имеет решения; следовательно, исключить правило может быть применено только в случае х ∉ вары ( т ). Поскольку эта дополнительная проверка, называемая проверкой происходит , замедляет алгоритм, она, например, опускается в большинстве систем Prolog. С теоретической точки зрения пропуск проверки равносилен решению уравнений над бесконечными деревьями, см. Ниже .
Доказательство расторжения
Для доказательства остановки алгоритма рассмотрим тройку где n var - количество переменных, которые встречаются в наборе уравнений более одного раза, n lhs - количество функциональных символов и констант в левых частях потенциальных уравнений, а n eqn - количество уравнений. Когда правило устранения применяется, п переменная уменьшается, так как х исключается из G и хранится только в { х ≐ т }. Применение любого другого правила никогда не может снова увеличить n var . Когда применяется разложение правила , конфликт или замена , n lhs уменьшается, так как по крайней мере крайнее f левой стороны исчезает. Применение любого из оставшихся правил удаления или проверки не может увеличить n lhs , но уменьшает n eqn . Следовательно, любое применение правила уменьшает тройноеотносительно лексикографического порядка , что возможно только конечное число раз.
Конор МакБрайд замечает [19], что «выражая структуру, которую использует унификация» на языке с зависимой типизацией, таком как Epigram , алгоритм Робинсона можно сделать рекурсивным по количеству переменных , и в этом случае отдельное доказательство завершения становится ненужным.
Примеры синтаксической унификации терминов первого порядка
В синтаксическом соглашении Пролога символ, начинающийся с заглавной буквы, является именем переменной; символ, начинающийся с строчной буквы, является функциональным символом; запятая используется как логические и оператор. Для математической записи x, y, z используются как переменные, f, g как функциональные символы, а a, b как константы.
Обозначение Пролога | Математические обозначения | Объединяющая замена | Объяснение |
---|---|---|---|
a = a | { а = а } | {} | Успешно. ( тавтология ) |
a = b | { a = b } | ⊥ | а и б не совпадают |
X = X | { х = х } | {} | Успешно. ( тавтология ) |
a = X | { а = х } | { x ↦ a } | x объединяется с константой a |
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(g(X)) = f(Y) | { f ( g ( x )) = f ( y )} | { y ↦ g ( x )} | Объединяет y с термином |
f(g(X),X) = f(Y,a) | { f ( g ( x ), x ) = f ( y , a )} | { x ↦ a , y ↦ g ( a )} | Объединяет x с константой a , а y с членом |
X = f(X) | { х = f ( x )} | должно быть ⊥ | Возвращает ⊥ в логике первого порядка и во многих современных диалектах Пролога (принудительно проверяется с помощью проверки ). Преуспевает в традиционном Прологе и в Прологе II, объединяя x с бесконечным членом |
X = Y, Y = a | { х = у , у = а } | { x ↦ a , y ↦ a } | И x, и y объединены константой a |
a = Y, X = Y | { а = у , х = у } | { x ↦ a , y ↦ a } | Как указано выше (порядок уравнений в системе не имеет значения) |
X = a, b = X | { x = a , b = x } | ⊥ | Терпит неудачу. a и b не совпадают, поэтому x не может быть объединен с обоими |
Самый общий объединитель синтаксической задачи унификации первого порядка размера n может иметь размер 2 n . Например, проблема имеет самый общий объединитель , ср. картина. Чтобы избежать экспоненциальной временной сложности, вызванной таким раздутием, передовые алгоритмы унификации работают с ориентированными ациклическими графами (дагами), а не с деревьями. [20]
Применение: унификация в логическом программировании
Концепция унификации - одна из основных идей логического программирования , наиболее известная на языке Prolog . Он представляет собой механизм привязки содержимого переменных и может рассматриваться как своего рода одноразовое присвоение. В Прологе эта операция обозначается символом равенства =
, но также выполняется при создании экземпляров переменных (см. Ниже). Он также используется в других языках с использованием символа равенства =
, но и в сочетании с большим количеством операций , в том числе +
, -
, *
, /
. Алгоритмы вывода типов обычно основаны на унификации.
В Прологе:
- Переменная , которая uninstantiated-то ранее не были выполнены унификации на нем-могут быть объединены с атомом, термин, или другой переменной uninstantiated, таким образом , эффективно став его псевдонимом. Во многих современных диалектах Пролога и в логике первого порядка переменная не может быть объединена с термином, который ее содержит; это так называемая проверка происходит .
- Два атома могут быть объединены только в том случае, если они идентичны.
- Аналогичным образом , термин может быть объединен с другим термином , если верхние функциональные символы и арностей терминов идентичны и , если параметры могут быть объединены одновременно. Обратите внимание, что это рекурсивное поведение.
Применение: вывод типа
Унификация используется во время вывода типа, например, в функциональном языке программирования Haskell . С одной стороны, программисту не нужно предоставлять информацию о типе для каждой функции, с другой стороны, она используется для обнаружения опечаток. Выражение Haskell True : ['x', 'y', 'z']
набрано неправильно. Функция построения списка (:)
имеет тип a -> [a] -> [a]
, и для первого аргумента True
переменная полиморфного типа a
должна быть объединена с True
типом Bool
. Второй аргумент ['x', 'y', 'z']
имеет тип [Char]
, но a
не может быть одновременно Bool
и тем, и другим Char
.
Как и в случае с Прологом, можно дать алгоритм вывода типов:
- Любая переменная типа объединяется с любым выражением типа и создается для этого выражения. Конкретная теория может ограничить это правило проверкой на наличие событий.
- Константы двух типов объединяются, только если они одного типа.
- Конструкции двух типов объединяются, только если они являются приложениями конструктора одного и того же типа и все их типы компонентов рекурсивно объединяются.
Из-за декларативного характера порядок в последовательности унификаций (обычно) не важен.
Обратите внимание, что в терминологии логики первого порядка атом является основным предложением и унифицирован аналогично термину Пролога.
Унификация по порядку
Заказ отсортированные логики позволяет назначить вид или тип , к каждому члену, и объявить своего рода с 1 subsort другого рода с 2 , обычно записываетсявиде s 1 ⊆ s 2 . Например, рассуждая о биологических существах, полезно объявитьсортовую собаку разновидностью сортового животного . Везде, где требуется член некоторого вида s ,вместо него может быть указанчлен любой подгруппы s . Например, предполагая объявление функции mother : animal → animal и постоянное объявление lassie : dog , термин « мать» ( lassie ) вполне допустим и имеет вид животного . Для предоставления информации о том, что мать собаки, в свою очередь, является собакой, может быть оформленоеще одно заявление мать : собака → собака ; это называется перегрузкой функции , аналогично перегрузке в языках программирования .
Вальтер дал алгоритм объединения для терминов в логике сортировки по порядку, требуя, чтобы для любых двух объявленных сортов s 1 , s 2 также было объявлено их пересечение s 1 ∩ s 2 : если x 1 и x 2 - переменные вида s 1 и ев 2 , соответственно, уравнение х 1 ≐ х 2 имеет решение { х 1 = х , х 2 = х }, где х : s 1 ∩ s 2 . [21] После включения этого алгоритма в автоматическое средство доказательства теорем, основанное на предложениях, он смог решить задачу эталонного теста, переведя ее в логику с упорядоченной сортировкой, тем самым уменьшив ее на порядок, поскольку многие унарные предикаты превратились в сортировки.
Обобщенная логика Smolka с сортировкой по порядку для параметрического полиморфизма . [22] В его структуре объявления подсортировки распространяются на выражения сложных типов. В качестве примера программирования может быть объявлен список параметрической сортировки ( X ) (где X является параметром типа, как в шаблоне C ++ ), и из объявления подсортировки int ⊆ float автоматически создается список отношений ( int ) ⊆ list ( float ). выведено, что означает, что каждый список целых чисел также является списком чисел с плавающей запятой.
Schmidt-Schauß обобщенная логика упорядоченной сортировки, позволяющая декларировать термины. [23] В качестве примера предположим, что объявления подсортировки четные ⊆ int и нечетные ⊆ int , объявление термина типа i : int . ( i + i ): даже позволяет объявить свойство целочисленного сложения, которое не может быть выражено обычной перегрузкой.
Объединение бесконечных сроков
Фон на бесконечных деревьях:
- Б. Курсель (1983). «Основные свойства бесконечных деревьев» (PDF) . Теорет. Comput. Sci . 25 (2): 95–169. DOI : 10.1016 / 0304-3975 (83) 90059-2 . Архивировано из оригинального (PDF) 21 апреля 2014 года . Проверено 28 июня 2013 .
- Майкл Дж. Махер (июль 1988 г.). «Полная аксиоматизация алгебр конечных, рациональных и бесконечных деревьев». Proc. 3-й ежегодный симпозиум IEEE. по логике в компьютерных науках, Эдинбург . С. 348–357.
- Джоксан Джаффар; Питер Дж. Стаки (1986). "Семантика программирования с использованием бесконечной древовидной логики" . Теоретическая информатика . 46 : 141–158. DOI : 10.1016 / 0304-3975 (86) 90027-7 .
Алгоритм унификации, Пролог II:
- А. Колмерауэр (1982). К.Л. Кларк; С.-А. Тарнлунд (ред.). Пролог и бесконечные деревья . Академическая пресса.
- Ален Колмерауэр (1984). «Уравнения и неравенства на конечных и бесконечных деревьях». В ICOT (ред.). Proc. Int. Конф. по компьютерным системам пятого поколения . С. 85–99.
Приложения:
- Фрэнсис Джаннесини; Жак Коэн (1984). «Генерация парсеров и манипуляции с грамматикой с использованием бесконечных деревьев Пролога». J. Логическое программирование . 1 (3): 253–265. DOI : 10.1016 / 0743-1066 (84) 90013-X .
Электронная унификация
E-унификация является задачей нахождения решения данной совокупности уравнений , принимая во внимание некоторые эквациональных фона знаний E . Последний задается как набор универсальных равенств . Для некоторых конкретных наборов E были разработаны алгоритмы решения уравнений (также известные как алгоритмы E-унификации ); для других было доказано, что таких алгоритмов не может быть.
Например, если a и b - разные константы, уравнение не имеет решения относительно чисто синтаксической унификации , где ничего не известно об операторе. Однако еслиизвестно, что оно коммутативно , то замена { x ↦ b , y ↦ a } решает указанное выше уравнение, поскольку
{ x ↦ b , y ↦ a } знак равно по заявке на замену знак равно коммутативностью знак равно { x ↦ b , y ↦ a } по (обратному) заявлению на замену
Базовые знания E могут утверждать коммутативность всеобщим равенством "для всех u , v ".
Наборы специальных базовых знаний E
∀ u , v , w : | знак равно | А | Ассоциативность | ||
∀ u , v : | знак равно | C | Коммутативность | ||
∀ u , v , w : | знак равно | D l | Левая распределенность над | ||
∀ u , v , w : | знак равно | D r | Правильная распределенность над | ||
∀ u : | знак равно | ты | я | Идемпотентность | |
∀ u : | знак равно | ты | N l | Левый нейтральный элемент n относительно | |
∀ u : | знак равно | ты | N r | Правый нейтральный элемент n относительно |
Говорят, что унификация разрешима для теории, если для нее разработан алгоритм унификации, который завершается для любой входной задачи. Говорят, что унификация является полуразрешимой для теории, если для нее разработан алгоритм унификации, который завершается для любой решаемой входной задачи, но может вечно искать решения неразрешимой входной проблемы.
Объединение разрешимо для следующих теорий:
- A [24]
- A , C [25]
- A , C , I [26]
- A , C , N l [примечание 9] [26]
- A , I [27]
- A , N l , N r (моноид) [28]
- C [29]
- Логические кольца [30] [31]
- Абелевы группы , даже если подпись расширена произвольными дополнительными символами (но не аксиомами) [32]
- Модальные алгебры K4 [33]
Объединение полуразрешимо для следующих теорий:
- A , D l , D r [34]
- A , C , D l [примечание 9] [35]
- Коммутативные кольца [32]
Односторонняя парамодуляция
Если существует сходящаяся система перезаписи терминов R, доступная для E , алгоритм односторонней парамодуляции [36] может использоваться для перечисления всех решений данных уравнений.
G ∪ { f ( s 1 , ..., s n ) ≐ f ( t 1 , ..., t n )} | ; S | ⇒ | G ∪ { s 1 ≐ t 1 , ..., s n ≐ t n } | ; S | разлагать | |
G ∪ { x ≐ t } | ; S | ⇒ | G { x ↦ t } | ; S { x ↦ t } ∪ { x ↦ t } | если переменная x не входит в t | Устранить |
G ∪ { f ( s 1 , ..., s n ) ≐ t } | ; S | ⇒ | G ∪ { s 1 ≐ u 1 , ..., s n ≐ u n , r ≐ t } | ; S | если f ( u 1 , ..., u n ) → r - правило из R | мутировать |
G ∪ { f ( s 1 , ..., s n ) ≐ y } | ; S | ⇒ | G ∪ { s 1 ≐ y 1 , ..., s n ≐ y n , y ≐ f ( y 1 , ..., y n )} | ; S | если y 1 , ..., y n - новые переменные | подражать |
Начиная с G, являющейся проблемой унификации, которую необходимо решить, и S, являющейся заменой идентичности, правила применяются недетерминированно до тех пор, пока пустое множество не появится как фактическая G , и в этом случае фактическая S является объединяющей заменой. В зависимости от того , правила paramodulation применяются, по выбору фактического уравнения из G , и по выбору R правил «S в мутировать , различные вычисления , пути возможны. Только некоторые приводят к решению, в то время как другие заканчиваются на G ≠ {}, где никакое другое правило не применимо (например, G = { f (...) ≐ g (...)}).
1 | приложение ( ноль , z ) | → z |
2 | приложение ( x . y , z ) | → х . приложение ( y , z ) |
Например, термин система перезаписи R используется для определения оператора добавления списков, построенных из cons и nil ; где cons ( x , y ) записывается в инфиксной записи как x . y для краткости; например app ( a . b . nil , c . d . nil ) → a . app ( b . nil , c . d . nil ) → a . б . app ( nil , c . d . nil ) → a . б . c . d . nil демонстрирует объединение списков a . б . ноль и c . d . ноль , используя правило перезаписи 2,2 и 1. эквациональная теорию E , соответствующая R является замыканием конгруэнтности из R , как рассматривать как бинарные отношения на условиях. Например, приложение ( . Б . Ноль , с . Д . Ноль ) ≡ . б . c . d . nil ≡ app ( a . b . c . d . nil , nil ). Алгоритм paramodulation перечисляет решения уравнений относительно этих Е при скармливании примера R .
Успешный пример пути вычисления для задачи объединения { app ( x , app ( y , x )) ≐ a . а . nil } показан ниже. Чтобы избежать конфликтов имен переменных, правила перезаписи последовательно переименовываются каждый раз перед их использованием с помощью правила mutate ; v 2 , v 3 , ... - имена переменных, сгенерированные компьютером для этой цели. В каждой строке выбранное уравнение из G выделено красным. Каждый раз , когда мутируют применяется правило, выбранное правило перезаписи ( 1 или 2 ) , указано в скобках. Из последней строки объединяющая подстановка S = { y ↦ nil , x ↦ a . nil } можно получить. В самом деле, приложение ( х , приложение ( у , х )) { у ↦ ноль , х ↦ . nil } = app ( a . nil , app ( nil , a . nil )) ≡ app ( a . nil , a . nil ) ≡ a . app ( nil , a . nil ) ≡ a . а . nil решает данную проблему. Второй успешный путь вычисления, который можно получить, выбрав "мутируют (1), мутируют (2), мутируют (2), мутируют (1)" приводит к замене S = { у ↦ . а . nil , x ↦ nil }; здесь он не показан. Никакой другой путь к успеху не ведет.
Используемое правило | грамм | S | |
---|---|---|---|
{ приложение ( х , приложение ( у , х )) ≐ а . а . ноль } | {} | ||
мутировать (2) | ⇒ | { х ≐ v 2 . v 3 , приложение ( y , x ) ≐ v 4 , v 2 . приложение ( v 3 , v 4 ) ≐ а . а . ноль } | {} |
разлагать | ⇒ | { х ≐ v 2 . v 3 , приложение ( y , x ) ≐ v 4 , v 2 ≐ a , app ( v 3 , v 4 ) ≐ a . ноль } | {} |
Устранить | ⇒ | { Приложение ( у , v 2 . V 3 ) ≐ v 4 , v 2 ≐ , приложение ( v 3 , v 4 ) ≐ . ноль } | { х ↦ v 2 . v 3 } |
Устранить | ⇒ | { app ( y , a . v 3 ) ≐ v 4 , app ( v 3 , v 4 ) ≐ a . ноль } | { x ↦ a . v 3 } |
мутировать (1) | ⇒ | { y ≐ nil , a . v 3 ≐ v 5 , v 5 ≐ v 4 , приложение ( v 3 , v 4 ) ≐ a . ноль } | { x ↦ a . v 3 } |
Устранить | ⇒ | { y ≐ nil , a . v 3 ≐ v 4 , приложение ( v 3 , v 4 ) ≐ a . ноль } | { x ↦ a . v 3 } |
Устранить | ⇒ | { а . v 3 ≐ v 4 , приложение ( v 3 , v 4 ) ≐ a . ноль } | { y ↦ nil , x ↦ a . v 3 } |
мутировать (1) | ⇒ | { а . v 3 ≐ v 4 , v 3 ≐ ноль , v 4 ≐ v 6 , v 6 ≐ a . ноль } | { y ↦ nil , x ↦ a . v 3 } |
Устранить | ⇒ | { а . v 3 ≐ v 4 , v 3 ≐ ноль , v 4 ≐ a . ноль } | { y ↦ nil , x ↦ a . v 3 } |
Устранить | ⇒ | { а . ноль ≐ v 4 , v 4 ≐ a . ноль } | { y ↦ nil , x ↦ a . ноль } |
Устранить | ⇒ | { а . ноль ≐ a . ноль } | { y ↦ nil , x ↦ a . ноль } |
разлагать | ⇒ | { a ≐ a , nil ≐ nil } | { y ↦ nil , x ↦ a . ноль } |
разлагать | ⇒ | { nil ≐ nil } | { y ↦ nil , x ↦ a . ноль } |
разлагать | ⇒ | {} | { y ↦ nil , x ↦ a . ноль } |
Сужение
Если R является конвергентной системой переписывания терминов для E , подход, альтернативный предыдущему разделу, состоит в последовательном применении « сужающих шагов »; это в конечном итоге перечислит все решения данного уравнения. Шаг сужения (см. Рисунок) состоит в
- выбор неизменяемого подтерма текущего термина,
- синтаксически объединяя его с левой частью правила из R , и
- заменяя правую часть созданного правила на конкретизированный термин.
Формально, если l → r - это переименованная копия правила перезаписи из R , не имеющая общих переменных с термом s , а подтерм s | p не является переменной и объединяется с l через mgu σ , тогда s можно сузить до члена t = sσ [ rσ ] p , то есть до члена sσ , с заменой подтермина в p на rσ . Ситуация, когда s можно сузить до t , обычно обозначается как s ↝ t . Интуитивно последовательность шагов сужения t 1 ↝ t 2 ↝ ... ↝ t n можно представить как последовательность шагов перезаписи t 1 → t 2 → ... → t n , но с начальным членом t 1, равным далее и далее, если необходимо, чтобы применить каждое из используемых правил.
В выше примере paramodulation вычисления соответствует следующему сужающейся последовательности ( «↓» с указанием экземпляра здесь):
приложение ( | Икс | , приложение ( y , | Икс | )) | |||||||||||||
↓ | ↓ | х ↦ v 2 . v 3 | |||||||||||||||
приложение ( | v 2 . v 3 | , приложение ( y , | v 2 . v 3 | )) | → | v 2 . приложение ( версия 3 , приложение ( | y | , v 2 . v 3 )) | |||||||||
↓ | да ↦ ноль | ||||||||||||||||
v 2 . приложение ( версия 3 , приложение ( | ноль | , v 2 . v 3 )) | → | v 2 . приложение ( | v 3 | , v 2 . | v 3 | ) | |||||||||
↓ | ↓ | v 3 ↦ ноль | |||||||||||||||
v 2 . приложение ( | ноль | , v 2 . | ноль | ) | → | v 2 . v 2 . ноль |
Последний член, ст. 2 . v 2 . nil может быть синтаксически унифицирован с исходным членом в правой части a . а . ноль .
Сужение лемма [37] гарантирует , что всякий раз , когда экземпляр термин ы может быть переписан в перспективе т на термин сходящегося переписывания системы, то ев и т может быть сужен и переписан на срок сек « и т » , соответственно, такие , что t ' является экземпляром s ' .
Формально: всякий раз, когда sσ t выполняется для некоторой подстановки σ, то существуют члены s ', t ' такие, что s s ' и t t ' и s ' τ = t ' для некоторой замены τ.
Объединение высшего порядка
Во многих приложениях требуется рассмотреть объединение типизированных лямбда-терминов вместо терминов первого порядка. Такое объединение часто называют объединением более высокого порядка . Хорошо изученной ветвью объединения высшего порядка является проблема объединения просто типизированных лямбда-членов по модулю равенства, определяемого преобразованиями αβη. У таких проблем унификации нет самых общих объединителей. В то время как объединение высшего порядка неразрешимо , [38] [39] [40] Жерар Юэ дал полуразрешимый (пред-) алгоритм объединения [41], который позволяет систематический поиск пространства объединителей (обобщая алгоритм объединения Мартелли -Montanari [2] с правилами для терминов, содержащих переменные более высокого порядка), который, кажется, достаточно хорошо работает на практике. Huet [42] и Gilles Dowek [43] написали статьи, посвященные этой теме.
Дейл Миллер описал то, что сейчас называется объединением паттернов более высокого порядка . [44] Это подмножество унификации высшего порядка разрешимо, и у разрешимых задач унификации есть унификаторы наиболее общего вида. Многие компьютерные системы, содержащие унификацию более высокого порядка, такие как языки логического программирования высокого порядка λProlog и Twelf , часто реализуют только фрагмент шаблона, а не полную унификацию более высокого порядка.
В компьютерной лингвистике одна из самых влиятельных теорий многоточия заключается в том, что эллипсы представлены свободными переменными, значения которых затем определяются с помощью унификации высшего порядка (HOU). Например, семантическое представление «Джону нравится Мэри, и Питер тоже» выглядит как ( j , m ) ∧ R ( p ), а значение R (семантическое представление многоточия) определяется уравнением вида ( j , т ) = R ( j ) . Процесс решения таких уравнений называется объединением высшего порядка. [45]
Например, задача объединения { 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 )}.
Уэйн Снайдер дал обобщение как унификации высшего порядка, так и Е-унификации, то есть алгоритм для унификации лямбда-членов по модулю эквациональной теории. [46]
Смотрите также
- Перезапись
- Допустимое правило
- Явная подстановка в лямбда-исчислении
- Решение математических уравнений
- Dis-объединение : решение неравенств между символическим выражением
- Антиунификации : вычисление наименьшее общее обобщение (LGG) двух членов, двойственный к вычислению наиболее общий случай (MGU)
- Согласование онтологий (используйте унификацию с семантической эквивалентностью )
Заметки
- ^ в этом случае все еще существует полный набор подстановок (например, набор всех решений вообще); однако каждый такой набор содержит избыточные элементы.
- ^ Например, a ⊕ ( b ⊕ f ( x )) ≡ a ⊕ ( f ( x ) ⊕ b ) ≡ ( b ⊕ f ( x )) ⊕ a ≡ ( f ( x ) ⊕ b ) ⊕ a
- ^ с тех пор
- ^ так как z { z ↦ x ⊕ y } = x ⊕ y
- ^ формально: каждый объединитель τ удовлетворяет ∀ x : xτ = ( xσ ) ρ для некоторой подстановки ρ
- ^ Alg.1, p.261. Их правило (а) соответствует замене правилздесь, (б) для удаления , (в) для разложения и конфликта и (г) для устранения и проверки .
- ^ См Мартелли Монтанари (1982), [2] sect.1, p.259. Статья Патерсона и Вегмана датирована 1978 годом; однако издательство журнала получило его в сентябре 1976 года.
- ^ Хотя правило сохраняет x ≐ t в G , оно не можетповторятьсябесконечно, поскольку его предусловие x ∈ vars ( G ) аннулируется его первым применением. В более общем смысле, алгоритм всегда гарантированно завершается, см. Ниже .
- ^ a b при наличии равенства C равенства N l и N r эквивалентны, аналогичны для D l и D r
Рекомендации
- ^ Фаж, Франсуа; Юэ, Жерар (1986). «Полные наборы объединителей и матчеров в теории уравнений». Теоретическая информатика . 43 : 189–200. DOI : 10.1016 / 0304-3975 (86) 90175-1 .
- ^ а б в Мартелли, Альберто; Монтанари, Уго (апрель 1982 г.). «Эффективный алгоритм объединения». ACM Trans. Программа. Lang. Syst . 4 (2): 258–282. DOI : 10.1145 / 357162.357169 . S2CID 10921306 .
- ↑ J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie , Class III, Sciences Mathématiques et Physiques, 33, 1930.
- ^ Клаус-Питер Вирт; Йорг Зикманн; Кристоф Бензмюллер; Серж Autexier (2009). Лекции о Жаке Эрбранде как логике (Отчет SEKI). DFKI. arXiv : 0902.4682 . Здесь: стр.56
- ^ Жак Эрбранд (1930). Исследования по теории демонстрации (PDF) (докторская диссертация). А. 1252 . Université de Paris. Здесь: с.96-97
- ^ а б в г Дж. А. Робинсон (январь 1965 г.). «Машинно-ориентированная логика, основанная на принципе разрешения». Журнал ACM . 12 (1): 23–41. DOI : 10.1145 / 321250.321253 . S2CID 14389185 .; Здесь: раздел 5.8, стр.32
- ^ Дж. А. Робинсон (1971). «Вычислительная логика: объединение вычислений» (PDF) . Машинный интеллект . 6 : 63–72.
- ^ CC Chang ; Х. Джером Кейслер (1977). Теория моделей . Исследования по логике и основам математики. 73 . Северная Голландия.; здесь: Раздел 1.3
- ^ KR Apt. «От логического программирования к Прологу», с. 24. Прентис Холл, 1997.
- ^ Робинсон (1965); [6] №2.5, 2.14, стр.25
- ^ Робинсон (1965); [6] №5.6, стр.32
- ^ Робинсон (1965); [6] №5.8, стр.32
- ^ Льюис Денвер Бакстер (февраль 1976 г.). Практически линейный алгоритм унификации (PDF) (Res. Report). CS-76-13. Univ. Ватерлоо, Онтарио.
- ^ Жерар Юэ (сентябрь 1976 г.). Resolution d'Equations dans des Langages d'Ordre 1,2, ... ω (Эти слова). Парижский университет VII.
- ^ а б Альберто Мартелли и Уго Монтанари (июль 1976 г.). Объединение в линейном времени и пространстве: структурированная презентация (внутреннее примечание). IEI-B76-16. Consiglio Nazionale delle Ricerche, Пиза. Архивировано из оригинала на 2015-01-15.
- ^ а б в Майкл Стюарт Патерсон и М. Н. Вегман (апрель 1978 г.). «Линейное объединение». J. Comput. Syst. Sci . 16 (2): 158–167. DOI : 10.1016 / 0022-0000 (78) 90043-0 .
- ^ Дж. А. Робинсон (январь 1976 г.). «Быстрое объединение» . В Вудро В. Бледсо , Майкл М. Рихтер (ред.). Proc. Мастерская доказательства теорем Обервольфах . Отчет о семинаре в Обервольфахе. 1976/3.[ постоянная мертвая ссылка ]
- ^ М. Вентурини-Зилли (октябрь 1975 г.). «Сложность алгоритма унификации выражений первого порядка». Calcolo . 12 (4): 361–372. DOI : 10.1007 / BF02575754 . S2CID 189789152 .
- ^ Макбрайд, Конор (октябрь 2003 г.). «Объединение первого порядка посредством структурной рекурсии» . Журнал функционального программирования . 13 (6): 1061–1076. CiteSeerX 10.1.1.25.1516 . DOI : 10.1017 / S0956796803004957 . ISSN 0956-7968 . Проверено 30 марта 2012 года .
- ^ например, Патерсон, Вегман (1978), [16] раздел 2, стр.159
- ^ Вальтер, Кристоф (1985). «Механическое решение парового катка Шуберта с помощью многоуровневого разрешения» (PDF) . Артиф. Intell . 26 (2): 217–224. DOI : 10.1016 / 0004-3702 (85) 90029-3 .
- ^ Смолка, Герт (ноябрь 1988 г.). Логическое программирование с полиморфно упорядоченными типами (PDF) . Int. Практикум по алгебраическому и логическому программированию. LNCS. 343 . Springer. С. 53–70. DOI : 10.1007 / 3-540-50667-5_58 .
- ^ Шмидт-Шаус, Манфред (апрель 1988 г.). Вычислительные аспекты упорядоченной логики с объявлениями термов . LNAI. 395 . Springer.
- ^ Гордон Д. Плоткин , Теоретико-решеточные свойства подписки , Меморандум MIP-R-77, Univ. Эдинбург, июнь 1970 г.
- ^ Марк Э. Стикель , Алгоритм объединения ассоциативно-коммутативных функций , J. Assoc. Comput. Машины, т. 28, № 3, с. 423–434, 1981
- ^ a b Ф. Фагес, Ассоциативно-коммутативное объединение , J. Symbolic Comput., том 3, № 3, стр. 257–275, 1987
- ^ Франц Баадер, Объединение в идемпотентных полугруппах имеет нулевой тип , J. Automat. Рассуждения, том 2, номер 3, 1986
- ^ Маканин Дж . Проблема разрешимости уравнений в свободной полугруппе. АН СССР, т. 233, № 2, 1977 г.
- ^ Ф. Фагес (1987). «Ассоциативно-коммутативное объединение» (PDF) . J. Symbolic Comput . 3 (3): 257–275. DOI : 10.1016 / s0747-7171 (87) 80004-4 .
- ^ Мартин У., Нипков Т. (1986). «Объединение в булевых кольцах». В Jörg H. Siekmann (ed.). Proc. 8-й CADE . LNCS. 230 . Springer. С. 506–513.CS1 maint: несколько имен: список авторов ( ссылка )
- ^ А. Буде; JP Jouannaud; М. Шмидт-Шаус (1989). «Объединение булевых колец и абелевых групп». Журнал символических вычислений . 8 (5): 449–477. DOI : 10.1016 / s0747-7171 (89) 80054-9 .
- ^ a b Баадер и Снайдер (2001), стр. 486.
- ^ Ф. Баадер и С. Гиларди, Унификация модальных и описательных логик , Logic Journal of the IGPL 19 (2011), no. 6. С. 705–730.
- ^ П. Сабо, Unifikationstheorie erster Ordnung ( теория объединения первого порядка ), Диссертация, Univ. Карлсруэ, Западная Германия, 1982 г.
- ^ Йорг Х. Зикманн, Универсальное объединение , Proc. 7-й Int. Конф. on Automated Deduction, Springer LNCS vol.170, pp. 1–42, 1984.
- ^ Н. Дершовиц и Г. Сивакумар, Решение задач в уравнительных языках , Proc. 1-й Int. Семинар по системам условной перезаписи терминов, Springer LNCS, том 308, стр. 45–55, 1988 г.
- ^ Фэй (1979). «Объединение первого порядка в теории уравнений». Proc. 4-й семинар по автоматическому вычету . С. 161–167.
- ^ Уоррен Д. Гольдфарб (1981). «Неразрешимость проблемы объединения второго порядка». TCS . 13 (2): 225–230. DOI : 10.1016 / 0304-3975 (81) 90040-2 .
- ^ Жерар П. Юэ (1973). «Неразрешимость объединения в логике третьего порядка» . Информация и контроль . 22 (3): 257–267. DOI : 10.1016 / S0019-9958 (73) 90301-X .
- ^ Клаудио Луччеси: Неразрешимость проблемы унификации для языков третьего порядка (Отчет об исследовании CSRR 2059; Департамент компьютерных наук, Университет Ватерлоо, 1972)
- ^ Жерар Юэ: алгоритм объединения для типизированного лямбда-исчисления []
- ↑ Жерар Юэ: Объединение высшего порядка 30 лет спустя
- ^ Жиль Доук: Объединение и соответствие высшего порядка. Справочник по автоматическому мышлению 2001: 1009–1062
- ^ Миллер, Дейл (1991). «Язык логического программирования с лямбда-абстракцией, функциональными переменными и простой унификацией» (PDF) . Журнал логики и вычислений . 1 (4): 497–536. DOI : 10.1093 / logcom / 1.4.497 .
- ^ Гардент, Клэр; Кольхейз, Майкл ; Конрад, Карстен (1997). «Многоуровневый подход объединения высшего порядка к многоточию». Представлен Европейской ассоциацией компьютерной лингвистики (EACL) . CiteSeerX 10.1.1.55.9018 .
- ^ Уэйн Снайдер (июль 1990 г.). «Электронное объединение высшего порядка». Proc. 10-я конференция по автоматическому отчислению . LNAI. 449 . Springer. С. 573–587.
дальнейшее чтение
- Франц Баадер и Уэйн Снайдер (2001). "Unification Theory". Архивировано 8 июня 2015 г. в Wayback Machine . В Джон Алан Робинсон и Андрей Воронков , редактора, Справочник автоматизированного Рассуждения , том I, стр 447-533. Издательство Elsevier Science. [ мертвая ссылка ]
- Жиль Довек (2001). «Объединение и согласование высшего порядка» . В Справочнике по автоматизированному мышлению .
- Франц Баадер и Тобиас Нипков (1998). Перезапись терминов и все такое . Издательство Кембриджского университета.
- Франц Баадер и Йорг Х. Зикманн (1993). «Теория объединения». В Справочнике по логике в искусственном интеллекте и логическом программировании .
- Жан-Пьер Жуанно и Клод Киршнер (1991). «Решение уравнений в абстрактных алгебрах: обзор унификации на основе правил». В вычислительной логике: очерки в честь Алана Робинсона .
- Нахум Дершовиц и Жан-Пьер Жуанно , Rewrite Systems , в: Ян ван Леувен (редактор), Справочник по теоретической информатике , том B Формальные модели и семантика , Elsevier, 1990, стр. 243–320
- Йорг Х. Зикманн (1990). «Теория объединения». В Клода Киршнера (редактор) Unification . Академическая пресса.
- Кевин Найт (март 1989 г.). «Объединение: междисциплинарный обзор» (PDF) . ACM Computing Surveys . 21 (1): 93–124. CiteSeerX 10.1.1.64.8967 . DOI : 10.1145 / 62029.62030 . S2CID 14619034 .
- Жерар Юэ и Дерек К. Оппен (1980). «Уравнения и правила перезаписи: обзор» . Технический отчет. Стэндфордский Университет.
- Раулефс, Питер; Siekmann, Jörg; Szabó, P .; Unvericht, E. (1979). «Краткий обзор современного состояния проблем сопоставления и унификации». Бюллетень ACM SIGSAM . 13 (2): 14–20. DOI : 10.1145 / 1089208.1089210 . S2CID 17033087 .
- Клод Киршнер и Элен Киршнер. Переписывание, решение, доказательство . В процессе подготовки.