Антиобъединение

О решении систем неравенств см. «Разъединение» .

Антиунификация — это процесс построения обобщения, общего для двух данных символических выражений. Как и в унификации , различают несколько фреймворков в зависимости от того, какие выражения (также называемые терминами) разрешены и какие выражения считаются равными. Если в выражении разрешены переменные, представляющие функции, процесс называется «антиунификацией высшего порядка», в противном случае — «антиунификацией первого порядка». Если требуется, чтобы обобщение имело экземпляр, буквально равный каждому входному выражению, этот процесс называется «синтаксической антиунификацией», в противном случае «Е-анти-унификация» или «теория анти-унификации по модулю».

Алгоритм антиунификации должен вычислять для заданных выражений полный и минимальный набор обобщений, то есть набор, охватывающий все обобщения и не содержащий избыточных элементов соответственно. В зависимости от структуры полный и минимальный набор обобщения может иметь один, конечное или, возможно, бесконечное количество членов или может не существовать вообще; оно не может быть пустым, поскольку тривиальное обобщение в любом случае существует. За синтаксическое антиунификацию первого порядка Гордон Плоткин дал алгоритм, который вычисляет полный и минимальный одноэлементный набор обобщений, содержащий так называемое «наименьшее общее обобщение» (lgg).

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

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

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

• Бесконечный V переменных набор . Для антиобъединения более высокого порядка удобно выбрать V , непересекающуюся из множества связанных переменных лямбда-члена .
• Множество T , таких термов что V ⊆ T . Для антиунификации первого и более высокого порядка T обычно представляет собой набор термов первого порядка (терминов, построенных из символов переменных и функций) и лямбда-терминов (терминов, содержащих некоторые переменные более высокого порядка) соответственно.
• Отношение эквивалентности $\equiv$ на $T$, указывая, какие члены считаются равными. Для антиобъединения более высокого порядка, как правило, $t\equiv u$ если $t$ и $u$ являются альфа-эквивалентными . Для E-анти-объединения первого порядка, $\equiv$ отражает базовые знания об определенных функциональных символах; например, если $\oplus$ считается коммутативным, $t\equiv u$ если $u$ результат $t$ путем замены аргументов $\oplus$ в некоторых (возможно, во всех) случаях. Если фоновых знаний вообще нет, то равными считаются только буквально или синтаксически идентичные термины.

Срок первого порядка

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

Учитывая набор $V$ переменных символов, набор $C$ постоянных символов и множеств $F_{n}$ из $n$-арные функциональные символы, также называемые операторными символами, для каждого натурального числа $n\geq 1$, набор термов (несортированного первого порядка) $T$ как рекурсивно определяется наименьшее множество со следующими свойствами:

• каждый переменный символ является термом: V ⊆ T ,
• каждый постоянный символ является термом: C ⊆ T ,
• из каждых n термов t ₁ ,..., t _n и каждого n -арного функционального символа f ∈ F _n больший терм $f(t_{1},\ldots ,t_{n})$ можно построить.

Например, если x € V — переменный символ, 1 € C — константа, а add € F ₂ — символ двоичной функции, то x € T , 1 € T и (следовательно) add( x ,1) ∈ T по первому, второму и третьему правилам построения членов соответственно. Последний термин обычно записывается как x +1, используя для удобства инфиксную нотацию и более распространенный символ оператора +.

Член высшего порядка

Основная статья: лямбда-исчисление

Замена

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

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

е (	х	, а , г (	С	), и )	урожайность
е (	есть ​ ,y)	, а , г (	б	), и )	.

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

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

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

Замена $\sigma$ более специфичен , чем замена или отнесен к ней $\tau$ если $x\sigma$ является более особенным, чем $x\tau$ для каждой переменной $x$.Например, $\{x\mapsto f(u),y\mapsto f(f(u))\}$ является более особенным, чем $\{x\mapsto z,y\mapsto f(z)\}$, с $f(u)$ и $f(f(u))$ является более особенным, чем $z$ и $f(z)$, соответственно.

Проблема антиунификации, множество обобщений

Проблема антиобъединения – это пара $\langle t_{1},t_{2}\rangle$ терминов.Срок $t$ общим обобщением или антиобъединителем является $t_{1}$ и $t_{2}$ если $t\sigma _{1}\equiv t_{1}$ и $t\sigma _{2}\equiv t_{2}$ для некоторых замен $\sigma _{1},\sigma _{2}$.Для данной проблемы антиунификации набор $S$ антиобъединителей называется полным, если в каждое обобщение входит некоторый термин $t\in S$; набор $S$ называется минимальным, если ни один из его членов не включает в себя другой.

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

Структура синтаксической антиунификации первого порядка основана на $T$ являющийся набором термов первого порядка (по некоторому заданному множеству $V$ переменных, $C$ констант и $F_{n}$ из $n$-арные функциональные символы) и на $\equiv$ равенство синтаксическое .В этих рамках каждая проблема, направленная против объединения, $\langle t_{1},t_{2}\rangle$ имеет полный и, очевидно, минимальный набор одноэлементных решений $\{t\}$. Его член $t$ называется наименьшим общим обобщением (lgg) задачи, оно имеет экземпляр, синтаксически равный $t_{1}$ и еще один, синтаксически равный $t_{2}$.Любое общее обобщение $t_{1}$ и $t_{2}$ включает в себя $t$.lgg уникален с точностью до вариантов: если $S_{1}$ и $S_{2}$ являются как полным, так и минимальным набором решений одной и той же синтаксической проблемы антиунификации, тогда $S_{1}=\{s_{1}\}$ и $S_{2}=\{s_{2}\}$ на некоторые условия $s_{1}$ и $s_{2}$, которые являются переименованиями друг друга.

Плоткин дал алгоритм для вычисления lgg двух заданных терминов.Оно предполагает инъективное отображение $\phi :T\times T\longrightarrow V$, то есть отображение, присваивающее каждой паре $s,t$ терминов собственная переменная $\phi (s,t)$, так что никакие две пары не имеют одну и ту же переменную. Алгоритм состоит из двух правил:

$f(s_{1},\dots ,s_{n})\sqcup f(t_{1},\ldots ,t_{n})$	$\rightsquigarrow$	$f(s_{1}\sqcup t_{1},\ldots ,s_{n}\sqcup t_{n})$
$s\sqcup t$	$\rightsquigarrow$	$\phi (s,t)$	если предыдущее правило неприменимо

Например, $(0*0)\sqcup (4*4)\rightsquigarrow (0\sqcup 4)*(0\sqcup 4)\rightsquigarrow \phi (0,4)*\phi (0,4)\rightsquigarrow x*x$; это наименее общее обобщение отражает общее свойство обоих входных данных — квадратные числа.

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

Теория антиобъединения первого порядка по модулю

• Якобсен, Эрик (июнь 1991 г.), Унификация и антиунификация (PDF) , Технический отчет
• Оствальд, Бьярте М. (апрель 2004 г.), Функциональная реконструкция антиунификации (PDF) , NR Note, vol. DART/04/04, Норвежский вычислительный центр
• Бойчева, Светла; Марков, Здравко (2002). «Алгоритм наименьшего обобщения при относительной импликации» . Учеб. ФЛЕРС-02 . АААИ. стр. 322–326.
• Куция, Темур; Леви, Хорди; Вилларе, Матеу (2014). «Противоунификация условий и хеджирования без рейтинга» (PDF) . Журнал автоматизированного рассуждения . 52 (2): 155–190. дои : 10.1007/s10817-013-9285-6 . Программное обеспечение.

Эквациональные теории

• Одна ассоциативно-коммутативная операция: Поттье, Лоик (февраль 1989 г.), Алгоритмы завершения и обобщения в логике первого порядка (доктор философии) ; Поттье, Лоик (1989), Обобщение терминов в эквациональной теории - Ассоциативно-коммутативный случай , Отчет INRIA, том. 1056, ИНРИА
• Коммутативные теории: Баадер, Франц (1991). «Унификация, слабая унификация, верхняя граница, нижняя граница и проблемы обобщения» . Учеб. 4-я Конф. по методам и приложениям переписывания (RTA) . ЛНКС. Том. 488. Спрингер. стр. 86–91. дои : 10.1007/3-540-53904-2_88 .
• Бесплатные моноиды: Бьер, А. (1993), Нормализация, унификация и антиунификация в свободных моноидах (PDF) , Univ. Карлсруэ, Германия
• Регулярные занятия по конгруэнтности: Хайнц, Биргит (декабрь 1995 г.), Теория уравнений против объединения по модулю и ее применение к генерации лемм , отчеты GMD, том. 261, ТУ Берлин, ISBN  978-3-486-23873-0 ; Бургхардт, Йохен (2005). «Электронное обобщение с использованием грамматик». Искусственный интеллект . 165 (1): 1–35. arXiv : 1403.8118 . дои : 10.1016/j.artint.2005.01.008 . S2CID   5328240 .
• A-, C-, AC-, ACU-теории с упорядоченными сортами: Альпуэнте, Мария; Эскобар, Сантьяго; Эсперт, Хавьер; Месегер, Хосе (2014). «Модульный алгоритм эквационального обобщения с порядковой сортировкой» . Информация и вычисления . 235 : 98–136. дои : 10.1016/j.ic.2014.01.006 . hdl : 2142/25871 .
• Чисто идемпотентные теории: Черна, Дэвид; Куция, Темур (2020). «Идемпотентное антиобъединение» . Транзакции ACM в вычислительной логике . 21 (2): 1–32. дои : 10.1145/3359060 . hdl : 10.1145/3359060 . S2CID   207861304 .

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

• Таксономические виды: Фриш, Алан М.; Пейдж, Дэвид (1990). «Обобщение таксономической информации». АААИ : 755–761. ; Фриш, Алан М.; Пейдж-младший, К. Дэвид (1991). «Обобщение атомов в логике ограничений» . Учеб. Конф. о представлении знаний . ; Фриш, AM; Пейдж, компакт-диск (1995). «Преобразование теорий в конкретизацию». В Меллиш, CS (ред.). Учеб. 14-й IJCAI . Морган Кауфманн. стр. 1210–1216. CiteSeerX   10.1.1.32.1610 .
• Условия использования: Плаза, Э. (1995). «Случаи как термины: подход с использованием специальных терминов к структурированному представлению случаев». Учеб. 1-я Международная конференция по прецедентному рассуждению (ICCBR) . ЛНКС. Том. 1010. Спрингер. стр. 265–276. ISSN   0302-9743 .
• Идестам-Алмквист, Питер (июнь 1993 г.). «Обобщение, подразумеваемое рекурсивным антиунификацией» . Учеб. 10-я Конф. по машинному обучению . Морган Кауфманн. стр. 151–158.
• Фишер, Корнелия (май 1994 г.), PAnTUDE - Алгоритм против унификации для выражения уточненных обобщений (PDF) , Отчет об исследовании, том. ТМ-94-04, ДФКИ
• A-, C-, AC-, ACU-теории с упорядоченными сортами: см. выше.

Номинальное антиобъединение

• Баумгартнер, Александр; Куция, Темур; Леви, Хорди; Вилларет, Матеу (июнь 2013 г.). Номинальное антиобъединение . Учеб. RTA 2015. Том 36 LIPics. Замок Дагштуль, 57-73. Программное обеспечение.

Приложения

• Анализ программы:
  • Булычев, Петр; Минея, Мариус (2008). «Обнаружение дубликатов кода с использованием антиунификации» . Материалы весенне-летнего коллоквиума молодых исследователей по программной инженерии (2). ;
  • Булычев Петр Евгеньевич; Костылев Егор Владимирович; Захаров, Владимир А. (2009). «Алгоритмы против унификации и их применение в анализе программ» . У Амира Пнуэли, Ирины Вирбицкайте и Андрея Воронкова (ред.). Перспективы системной информатики (PSI) – 7-я Международная конференция памяти Андрея Ершова . ЛНКС. Том. 5947. Спрингер. стр. 413–423. дои : 10.1007/978-3-642-11486-1_35 . ISBN  978-3-642-11485-4 .
• Факторинг кода:
  • Коттрелл, Райлан (сентябрь 2008 г.), Полуавтоматическое повторное использование мелкомасштабного исходного кода посредством структурного соответствия (PDF) , Univ. Калгари
• Индукция доказывает:
  • Хайнц, Биргит (1994), Открытие леммы путем антиунификации регулярных сортов , Технический отчет, том. 94–21, ТУ Берлина
• Извлечение информации:
  • Томас, Бернд (1999). «Обучение T-оберток для извлечения информации на основе антиунификации» (PDF) . Технический отчет AAAI . WS-99-11: 15–20.
• Аргументация по делу:
  • Арменгол; Плаза, Энрик (2005). «Использование символических описаний для объяснения сходства на {CBR}» . В Беатрис Лопес, Хоакиме Мелендесе, Петиа Радева и Хорди Витриа (ред.). Исследования и разработки искусственного интеллекта, учеб. 8-й Межд. Конф. ACIA, CCIA . ИОС Пресс. стр. 239–246.
• Синтез программ. Идея обобщения терминов по отношению к эквациональной теории восходит к Манне и Вальдингеру (1978, 1980), которые хотели применить ее в синтезе программ. В разделе «Обобщение» они предлагают (на стр. 119 статьи 1980 года) обобщить реверс ( l ) и реверс ( Tail ( l ))<>[ head ( l )] для получения реверса (l')<>m ' . Это обобщение возможно только в том случае, если фоновое уравнение u <>[]= u рассматривается .
  • Зоар Манна ; Ричард Уолдингер (декабрь 1978 г.). Дедуктивный подход к синтезу программ (PDF) (Техническая записка). НИИ Интернешнл . Архивировано из оригинала (PDF) 27 февраля 2017 г. Проверено 29 сентября 2017 г. - препринт статьи 1980 г.
  • Зохар Манна и Ричард Уолдингер (январь 1980 г.). «Дедуктивный подход к синтезу программ». Транзакции ACM в языках и системах программирования . 2 : 90–121. дои : 10.1145/357084.357090 . S2CID   14770735 .
• Обработка естественного языка:
  • Амиридзе, Нино; Куция, Темур (2018). «Антиунификация и обработка естественного языка» . Пятый семинар по естественному языку и информатике, NLCS'18 . Препринты EasyChair. Отчет EasyChair № 203. doi : 10.29007/fkrh . S2CID   49322739 .

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

• Расчет конструкций:
  • Пфеннинг, Фрэнк (июль 1991 г.). «Унификация и антиунификация в строительном исчислении» (PDF) . Учеб. 6-й ЛИКС . Спрингер. стр. 74–85.
• Простое лямбда-исчисление (Входные данные: термины в бета-нормальной форме длиной этана. Выходные данные: шаблоны более высокого порядка):
  • Баумгартнер, Александр; Куция, Темур; Леви, Хорди; Вилларет, Матеу (июнь 2013 г.). Вариант антиобъединения высшего порядка . Учеб. РТА 2013. Том. 21 ЛИПиков. Замок Дагштуль, 113–127. Программное обеспечение.
• Простое типизированное лямбда-исчисление (Входные данные: термины в бета-нормальной форме длиной этана. Выходные данные: различные фрагменты простого типизированного лямбда-исчисления, включая шаблоны):
  • Черна, Дэвид; Куция, Темур (июнь 2019 г.). «Общая основа для обобщений высшего порядка» (PDF) . 4-я Международная конференция по формальным структурам вычислений и дедукции, FSCD, 24–30 июня 2019 г., Дортмунд, Германия . Замок Дагштуль - Центр информатики Лейбница. стр. 74–85.
• Ограниченные замены высшего порядка:
  • Вагнер, Ульрих (апрель 2002 г.), Комбинаторно ограниченное антиобъединение высшего порядка , Берлинский технический университет ; Шмидт, Мартин (сентябрь 2010 г.), Ограниченное антиунификация высшего порядка для проекции эвристических теорий (PDF) , PICS-Report, vol. 31–2010, ун-т. Оснабрюк, Германия, ISSN   1610-5389.