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

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

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

Антиунификация не должна путаться с дезунификацией . Последняя означает процесс решения систем неравенств , то есть нахождения значений переменных, таких, что все заданные неравенства выполняются. ^{[примечание 2]} Эта задача весьма отличается от нахождения обобщений.

Формально антиобъединительный подход предполагает

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

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

• каждый переменный символ является термином: 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, используя инфиксную нотацию и более распространенный символ оператора + для удобства.

Подстановка — это отображение переменных в термины; обозначение относится к подстановке, отображающей каждую переменную в термин , для , и каждую другую переменную в себя. Применение этой подстановки к термину 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 i=1,\ldots ,k}$${\displaystyle t\{x_{1}\mapsto t_{1},\ldots ,x_{k}\mapsto t_{k}\}}$${\displaystyle x_{i}}$${\displaystyle t_{i}}$${\displaystyle \{x\mapsto h (a,y),z\mapsto b\}}$

ж (	х	, а , г (	з	), у )	урожайность
ж (	ч ( а , у )	, а , г (	б	), у )	.

Если термин имеет экземпляр, эквивалентный термину , то есть, если для некоторой подстановки , то называется более общим , чем , и называется более специальным , чем или включенным в . Например, является более общим, чем , если является коммутативным , так как тогда .${\displaystyle т}$${\displaystyle u}$${\displaystyle t\sigma \equiv u}$${\displaystyle \сигма}$${\displaystyle т}$${\displaystyle u}$${\displaystyle u}$${\displaystyle т}$${\displaystyle x\oplus a}$${\displaystyle а\oplus б}$${\displaystyle \oplus}$${\displaystyle (x\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 \сигма}$${\displaystyle \тау}$${\displaystyle x\сигма}$${\displaystyle x\тау }$${\displaystyle x}$${\displaystyle \{x\mapsto f(u),y\mapsto f(f(u))\}}$${\displaystyle \{x\mapsto z,y\mapsto f(z)\}}$${\displaystyle f(u)}$${\displaystyle f(f(u))}$${\displaystyle z}$${\displaystyle f(z)}$

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

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

Плоткин ^{[1] [2]} дал алгоритм для вычисления lgg двух данных терминов. Он предполагает инъективное отображение , то есть отображение, назначающее каждой паре терминов собственную переменную , так что никакие две пары не разделяют одну и ту же переменную. ^{[примечание 4]} Алгоритм состоит из двух правил:${\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*x}$

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

This section needs expansion with: explain main results from papers below, relate their approaches to each other. You can help by adding to it. (June 2020)

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

• Одна ассоциативная и коммутативная операция: Потье, Лоик (февраль 1989 г.), «Алгоритмы завершения и обобщения в логике первого порядка» (These de Doctorat); Поттье, Лоик (1989), Обобщение терминов в уравнениях теории – Cas associatif-commutatif , Отчет INRIA, том. 1056, ИНРИА
• Коммутативные теории: Баадер, Франц (1991). «Унификация, слабая унификация, верхняя граница, нижняя граница и проблемы обобщения». Труды 4-й конференции по методам переписывания и приложениям (RTA) . LNCS. Том 488. Springer. стр.  86–91 . doi :10.1007/3-540-53904-2_88.
• Свободные моноиды: Бьер, А. (1993), Normalisierung, Unifikation und Antiunifikation in Freien Monoiden (PDF) , Univ. Карлсруэ, Германия
• Регулярные классы конгруэнтности: Хайнц, Биргит (декабрь 1995 г.), Anti-Unifikation modulo Gleichungstheorie und deren Anwendung zur Lemmagenerierung , GMD Berichte, vol. 261, ТУ Берлин, ISBN 978-3-486-23873-0; Бургхардт, Йохен (2005). «E-обобщение с использованием грамматик». Искусственный интеллект . 165 (1): 1– 35. arXiv : 1403.8118 . doi :10.1016/j.artint.2005.01.008. S2CID  5328240.
• A-, C-, AC-, ACU-теории с упорядоченными сортировками: Альпуэнте, Мария; Эскобар, Сантьяго; Эсперт, Хавьер; Месегер, Хосе (2014). «Модулярный упорядоченно-сортированный эквациональный алгоритм обобщения». Информация и вычисления . 235 : 98– 136. doi : 10.1016/j.ic.2014.01.006 . hdl : 2142/25871 .
• Чисто идемпотентные теории: Cerna, David; Kutsia, Temur (2020). «Идемпотентное антиунифицирование». ACM Transactions on Computational Logic . 21 (2): 1– 32. doi :10.1145/3359060. hdl :10.1145/3359060. S2CID  207861304.

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

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

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

This section needs expansion with: (as above). You can help by adding to it. (June 2020)

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