Антиунификация (информатика) - Anti-unification (computer science)

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

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

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

Предпосылки

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

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

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

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

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

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

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

Замена

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

f (	Икс	, а , г (	z	), у )	дает
f (	ч ( а , у )	, а , г (	б	), у )	.

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

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

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

Подстановка является более особенным , чем, или отнесены на, замену , если это более особенным , чем для каждой переменной . Например, более особенным, чем , поскольку и более особенным, чем и , соответственно. ${\ displaystyle \ sigma}$${\ Displaystyle \ тау}$${\ Displaystyle х \ sigma}$${\ Displaystyle х \ тау}$${\ displaystyle x}$${\ Displaystyle \ {х \ mapsto f (u), y \ mapsto f (f (u)) \}}$${\ Displaystyle \ {х \ mapsto z, y \ mapsto f (z) \}}$${\ displaystyle f (u)}$${\ Displaystyle f (е (и))}$${\ displaystyle z}$${\ displaystyle f (z)}$

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

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

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

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

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

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

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

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

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

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

Уравнительные теории

• Одна ассоциативная и коммутативная операция: Поттье, Лоик (февраль 1989 г.), Алгоритмы завершения и обобщения в логике первого порядка.; Pottier, Loic (1989), Generalization de termes en theorie equalle - Cas associatif-commutatif , Отчет INRIA, 1056 , INRIA
• Коммутативные теории: Баадер, Франц (1991). «Объединение, слабое объединение, верхняя граница, нижняя граница и проблемы обобщения». Proc. 4-я конф. по методам и приложениям перезаписи (RTA) . LNCS. 488 . Springer. С. 86–91.
• Свободные моноиды: Biere, A. (1993), Normalisierung, Unifikation und Antiunifikation in Freien Monoiden (PDF) , Univ. Карлсруэ, Германия
• Регулярные занятия по конгруэнтности: Хайнц, Биргит (декабрь 1995 г.), Anti-Unifikation modulo Gleichungstheorie und deren Anwendung zur Lemmagenerierung , GMD Berichte, 261 , TU Berlin, ISBN 978-3-486-23873-0; Бургхардт, Йохен (2005). «Электронное обобщение с использованием грамматик». Искусственный интеллект . 165 (1): 1–35. arXiv : 1403,8118 . DOI : 10.1016 / j.artint.2005.01.008 .
• A-, C-, AC-, ACU-теории с упорядоченными сортами: Alpuente, Maria; Эскобар, Сантьяго; Эсперт, Хавьер; Месегер, Хосе (2014). «Модульный алгоритм обобщения по уравнениям с сортировкой по порядку» (PDF) . Информация и вычисления . 235 : 98–136. DOI : 10.1016 / j.ic.2014.01.006 . ЛВП : 2142/25871 .
• Чисто идемпонентные теории: Черна, Дэвид; Куция, Темур (2019). «Идемпотентное антиобъединение» . ACM-транзакции в вычислительной логике . 21 (2). HDL : 10,1145 / 3359060 .

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

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

Номинальная антиунификация

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

Приложения

• Программный анализ: Булычев Петр; Минея, Мариус (2008). «Обнаружение повторяющегося кода с помощью антиунификации» . Цитировать журнал требует |journal=( помощь ); Булычев, Петр Е .; Костылев, Егор В .; Захаров, Владимир А. (2009). «Алгоритмы антиунификации и их приложения в программном анализе». Цитировать журнал требует |journal=( помощь )
• Факторинг кода: Коттрелл, Райлан (сентябрь 2008 г.), Полуавтоматическое повторное использование мелкомасштабного исходного кода через структурную корреспонденцию (PDF) , Univ. Калгари
• Индукционное доказательство: Хайнц, Биргит (1994), открытие леммы путем антиунификации регулярных видов , Технический отчет, 94–21, TU Berlin.
• Извлечение информации: Томас, Бернд (1999). «Обучение T-Wrappers для извлечения информации на основе антиунификации» (PDF) . Технический отчет AAAI . WS-99-11: 15–20.
• Рассуждения по прецедентам: Арменгол, Ева; Плаза, Энрик (2005). «Использование символических описаний для объяснения сходства на CBR» (PDF) . Цитировать журнал требует |journal=( помощь )
• Синтез программ: идея обобщения терминов по отношению к эквациональной теории восходит к Манна и Уолдингеру (1978, 1980), которые хотели применить ее при синтезе программ. В разделе «Обобщение» они предлагают (на стр. 119 статьи 1980 г.) обобщить обратное ( l ) и обратное ( хвост ( l )) <> [ head ( l )], чтобы получить обратное (l ') <> m ' . Это обобщение возможно только при рассмотрении фонового уравнения u <> [] = u .

Зохар Манна ; Ричард Уолдингер (декабрь 1978 г.). Дедуктивный подход к синтезу программ (PDF) (Техническая записка). SRI International . - препринт статьи 1980 г.

Зохар Манна и Ричард Уолдингер (январь 1980 г.). «Дедуктивный подход к синтезу программ». Транзакции ACM по языкам и системам программирования . 2 : 90–121. DOI : 10.1145 / 357084.357090 .

• Обработка естественного языка: Амиридзе, Нино; Куция, Темур (2018). «Антиунификация и обработка естественного языка» . Пятый семинар по естественному языку и информатике, NLCS'18 . Отчет EasyChair № 203.

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

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

Примечания

использованная литература