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

В информатике является проверка совпадений частью алгоритмов синтаксической унификации . объединения переменной V и структуры S, Это приводит к сбою если S содержит V .

Применение в доказательстве теорем

При доказательстве теорем объединение без проверки совпадений может привести к необоснованному выводу . Например, Пролога цель $X=f(X)$ добьется успеха, привязав X к циклической структуре, не имеющей аналогов во вселенной Эрбрана . В качестве другого примера: ^[1] без проверки наступления можно найти доказательство разрешения не-теоремы ^[2] $(\forall x\exists y.p(x,y))\rightarrow (\exists y\forall x.p(x,y))$ : отрицание этой формулы имеет конъюнктивную нормальную форму $p(X,f(X))\land \lnot p(g(Y),Y)$ , с $f$ и $g$ обозначая функцию Скулема для первого и второго квантора существования соответственно. Без проверки нахождения литералов $p(X,f(X))$ и $p(g(Y),Y)$ являются унифицируемыми, образуя опровергающее пустое предложение.

Рациональное объединение деревьев

Реализации Пролога обычно опускают проверку событий из соображений эффективности, что может привести к циклическим структурам данных и зацикливанию. Если не выполнять проверку на наличие, наихудшая сложность унификации термина $t_{1}$ со сроком $t_{2}$ во многих случаях снижается с $O({\text{size}}(t_{1})+{\text{size}}(t_{2}))$ к $O({\text{min}}({\text{size}}(t_{1}),{\text{size}}(t_{2})))$ ; в частном, частом случае унификации с переменным сроком время выполнения сокращается до $O(1)$ . ^{[номер 1]}

Современные реализации, основанные на Прологе II Колмерауэра, ^[4] ^[5] ^[6] ^[7] используйте рациональную унификацию деревьев, чтобы избежать циклов. Однако трудно сохранить сложность по времени линейной при наличии циклических членов. Примеры, когда алгоритм Колмерауэра становится квадратичным ^[8] может быть легко построено, но существуют предложения по уточнению.

На изображении приведен пример выполнения алгоритма объединения, приведенного в разделе Унификация (информатика)#Алгоритм объединения , пытающийся решить цель. $cons(x,y){\stackrel {?}{=}}cons(1,cons(x,cons(2,y)))$ , однако без правила проверки наступления (здесь оно называется «проверка»); применение вместо этого правила «устранить» приводит к циклическому графу (т.е. бесконечному члену) на последнем шаге.

Объединение звука

Реализации ISO Prolog имеют встроенный предикат unify_with_occurs_check/2 для правильной унификации, но могут свободно использовать ненадежные или даже циклические алгоритмы, когда унификация вызывается в противном случае, при условии, что алгоритм работает правильно для всех случаев, которые «не подлежат проверке возникновения» ( НСТО). ^[9] Встроенный acycl_term/1 служит для проверки конечности термов.

Реализациями, предлагающими звуковую унификацию для всех унификаций, являются Qu-Prolog и Strawberry Prolog и (опционально, через флаг времени выполнения): XSB , SWI-Prolog , Tau Prolog , Trealla Prolog и Scryer Prolog . Разнообразие ^[10]^[11] оптимизаций могут сделать надежную унификацию возможной для общих случаев.

См. также

В. П. Вейланд (1990). «Семантика логических программ без проверки на возникновение» . Теоретическая информатика . 71 : 155–174. дои : 10.1016/0304-3975(90)90194-м .

Примечания

^ В некоторых руководствах по Прологу указано, что сложность унификации без проверки событий велика. $O({\text{min}}({\text{size}}(t_{1}),{\text{size}}(t_{2})))$ (во всех случаях). ^[3] Это неверно, поскольку это означало бы сравнение произвольных основных условий в постоянное время (путем объединения $eq(t_{1},t_{2})$ с $eq(X,X)$ ).

Ссылки

^ Дэвид А. Даффи (1991). Принципы автоматического доказательства теорем . Уайли. ; здесь: стр.143
^ Неофициально и принимая $p(x,y)$ Чтобы означать, например, « x любит y », формула гласит: « Если каждый кого-то любит, то должен существовать один человек, которого любят все » .
^ Ф. Перейра; Д. Уоррен; Д. Боуэн; Л. Берд; Л. Перейра (1983). Руководство пользователя C-Prolog, версия 1.2 (Технический отчет). НИИ Интернешнл . Проверено 21 июня 2013 г.
^ А. Кольмерауэр (1982). К.Л. Кларк; С.-А. Тарнлунд (ред.). Пролог и бесконечные деревья . Академическая пресса.
^ М. Х. ван Эмден; Дж. В. Ллойд (1984). «Логическая реконструкция Пролога II». Журнал логического программирования . 2 : 143–149.
^ Джоксан Джаффар; Питер Дж. Стаки (1986). «Семантика программирования на основе бесконечной древовидной логики» . Теоретическая информатика . 46 : 141–158. дои : 10.1016/0304-3975(86)90027-7 .
^ Б. Курсель (1983). «Фундаментальные свойства бесконечных деревьев» . Теоретическая информатика . 25 (2): 95–169. дои : 10.1016/0304-3975(83)90059-2 .
^ Альберто Мартелли; Джанфранко Росси (1984). Эффективная унификация с бесконечными терминами в логическом программировании (PDF) . Международная конференция компьютерных систем пятого поколения.
^ 7.3.4 Нормальная унификация в Прологе ISO/IEC 13211-1:1995.
^ Риту Чадха; Дэвид А. Плейстед (1994). "Корректность унификации без проверки в прологе" . Журнал логического программирования . 18 (2): 99–122. дои : 10.1016/0743-1066(94)90048-5 .
^ Томас Прокош; Франсуа Брай (2020). Объединение на ходу (PDF) . 34-й Международный семинар по унификации. стр. 13:1–13:5.

[4] В некоторых руководствах по Прологу указано, что сложность унификации без проверки событий велика. $O({\text{min}}({\text{size}}(t_{1}),{\text{size}}(t_{2})))$ (во всех случаях). ^[3] Это неверно, поскольку это означало бы сравнение произвольных основных условий в постоянное время (путем объединения $eq(t_{1},t_{2})$ с $eq(X,X)$ ).

[1] Дэвид А. Даффи (1991). Принципы автоматического доказательства теорем . Уайли. ; здесь: стр.143

[2] Неофициально и принимая $p(x,y)$ Чтобы означать, например, « x любит y », формула гласит: « Если каждый кого-то любит, то должен существовать один человек, которого любят все » .

[3] Ф. Перейра; Д. Уоррен; Д. Боуэн; Л. Берд; Л. Перейра (1983). Руководство пользователя C-Prolog, версия 1.2 (Технический отчет). НИИ Интернешнл . Проверено 21 июня 2013 г.

[5] А. Кольмерауэр (1982). К.Л. Кларк; С.-А. Тарнлунд (ред.). Пролог и бесконечные деревья . Академическая пресса.

[6] М. Х. ван Эмден; Дж. В. Ллойд (1984). «Логическая реконструкция Пролога II». Журнал логического программирования . 2 : 143–149.

[7] Джоксан Джаффар; Питер Дж. Стаки (1986). «Семантика программирования на основе бесконечной древовидной логики» . Теоретическая информатика . 46 : 141–158. дои : 10.1016/0304-3975(86)90027-7 .

[8] Б. Курсель (1983). «Фундаментальные свойства бесконечных деревьев» . Теоретическая информатика . 25 (2): 95–169. дои : 10.1016/0304-3975(83)90059-2 .

[9] Альберто Мартелли; Джанфранко Росси (1984). Эффективная унификация с бесконечными терминами в логическом программировании (PDF) . Международная конференция компьютерных систем пятого поколения.

[10] 7.3.4 Нормальная унификация в Прологе ISO/IEC 13211-1:1995.

[11] Риту Чадха; Дэвид А. Плейстед (1994). "Корректность унификации без проверки в прологе" . Журнал логического программирования . 18 (2): 99–122. дои : 10.1016/0743-1066(94)90048-5 .

[12] Томас Прокош; Франсуа Брай (2020). Объединение на ходу (PDF) . 34-й Международный семинар по унификации. стр. 13:1–13:5.

[1]

[2]

[номер 1]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[3]