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

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

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

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

Цикл по пропущенному происходит проверка

Реализация пролога

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

Наивное упущение проверки «происходит» приводит к созданию циклических структур и может вызвать бесконечный цикл унификации. Современные реализации, основанные на Прологе II Колмерауэра,^[4][5][6][7]использовать рациональное объединение деревьев Чтобы избежать зацикливания, см. изображение для примера выполнения алгоритма унификации, приведенного в Унификация (информатика) # Алгоритм унификации, пытаясь решить цель ${\displaystyle cons(x,y){\stackrel {?}{=}}cons(1,cons(x,cons(2,y)))}$, однако без происходит проверка правила (там называется "проверка"); вместо этого применение правила «исключить» приводит к циклическому графу (т.е. бесконечному члену) на последнем шаге.

Реализации ISO Prolog имеют встроенный предикат unify_with_occurs_check / 2 для надежной унификации, но могут свободно использовать необоснованные или даже циклические алгоритмы, когда унификация вызывается в противном случае, при условии, что алгоритм работает правильно для всех случаев, которые «не подлежат проверке на наличие происшествий» (NSTO).^[8]

Реализации, предлагающие звуковую унификацию для всех унификаций, - это Qu-Prolog и Клубничный пролог и (необязательно через флаг времени выполнения): XSB, SWI-Prolog и Тау Пролог.

Смотрите также

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

Примечания

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

Рекомендации

1. Дэвид А. Даффи (1991). Принципы автоматизированного доказательства теорем. Вайли.; здесь: с.143
2. Неформально и принимая ${\displaystyle p(x,y)}$ означать, например, "x любит y", формула гласит"Если все кого-то любят, значит, должен существовать один человек, которого все любят."
3. Ф. Перейра; Д. Уоррен; Д. Боуэн; Л. Берд; Л. Перейра (1983). Руководство пользователя C-Prolog Версия 1.2 (Технический отчет). SRI International. Получено 21 июн 2013.
4. А. Колмерауэр (1982). К.Л. Кларк; С.-А. Тарнлунд (ред.). Пролог и бесконечные деревья. Академическая пресса.
5. M.H. ван Эмден; J.W. Ллойд (1984). «Логическая реконструкция Пролога II». J. Логическое программирование. 2: 143–149.
6. Джоксан Джаффар; Питер Дж. Стаки (1986). "Семантика программирования с использованием бесконечной древовидной логики". Теоретическая информатика. 46: 141–158. Дои:10.1016/0304-3975(86)90027-7.
7. Б. Курсель (1983). «Основные свойства бесконечных деревьев» (PDF). Теоретическая информатика. 25: 95–169. Дои:10.1016/0304-3975(83)90059-2. Архивировано из оригинал (PDF) на 2014-04-21. Получено 2013-06-21.
8. 7.3.4 Нормальная унификация в Прологе ISO / IEC 13211-1: 1995.

Статья основана на материалах, взятых из Бесплатный онлайн-словарь по вычислительной технике до 1 ноября 2008 г. и зарегистрированы в соответствии с условиями «перелицензирования» GFDL, версия 1.3 или новее.