Пролог согласование против объединения miniKanren

Question

В Прологе - Программирование искусственного интеллекта, Братко говорит следующее на странице 58.

«Matching в Прологе соответствует тому, что называется объединение в логике Однако, мы избегаем слов унификации, потому что соответствие. , по соображениям эффективности в большинстве систем Prolog реализуется таким образом, который точно не соответствует унификации. Надлежащая унификация требует так называемой проверки на наличие: возникает ли данная переменная в данном термине? Проверка на происшествие сделает совпадение неэффективным «.

Мои вопросы: если унификация в miniKanren страдает от этого снижения эффективности или как эта проблема решена?

Answer 1

Здесь есть несколько заблуждений. Во-первых, объединение звука доступно также в Prolog, используя предикат ISO unify_with_occurs_check/2.

Во-вторых, это объединение звука может быть включено в некоторых системах Prolog по умолчанию для все унификаций. См. Например флаг occurs_check Prolog в SWI-Prolog.

В-третьих, легко построить примеры, в которых включение проверки происходит, делает ваши программные заказы от быстрее, чем отключение проверки.

В-четвертых, использование термина соответствия описать, что объединениях опускаем происходит проверка очень плохая идея: Matching означает одностороннее объединение в функциональных языках. В Prolog унификации всегда работают во всех направлениях, также если проверка происходит отключена.

Итак, для части вопроса о Прологе я настоятельно рекомендую включить проверку, чтобы протестировать ваши программы, если ваша система Prolog поддерживает ее. Как правило, объединение, в котором происходит проверка, соответствует указывает на ошибку программирования в программах Prolog. По этой причине вы можете, например, установить флаг таким образом, чтобы система выбрала исключение , где оно иначе создало бы циклический термин.