Работа со сложными пролопными циклами

Question

Я использую Prolog для кодирования некоторых довольно сложных правил в моем проекте. Существует много рекурсии, включая взаимную рекурсию. Часть правил выглядеть примерно так:

pred1(X) :- ... 
pred1(X) :- someguard(X), pred2(X). 

pred2(X) :- ... 
pred2(X) :- othercondition(X), pred1(X). 

Там довольно очевидно, бесконечный цикл между pred1 и pred2. К сожалению, взаимодействие между этими предикатами очень сложно и сложно выделить. Я смог исключить бесконечный цикл в этом экземпляре, передав список объектов, которые были переданы в pred1, но это очень громоздко! Фактически, это в значительной степени побеждает цель использования Prolog в этом приложении.

Как заставить Prolog избежать бесконечных циклов? Например, если в ходе проверки pred1(foo) он пытается доказать pred1(foo) в качестве подцеля, ошибки и возврата.

Можно ли это сделать с помощью meta-interpreters?

Answer 1

Одна функция, доступная в некоторых системах Prolog и которая может помочь вам решить такие проблемы, называется tabling. См. Например, related question и prolog-tabling.

Если табуляция недоступна, то да, мета-переводчики могут определенно многое помочь с этим. Например, вы можете изменить стратегию выполнения и т. Д. С помощью мета-интерпретатора.

В SWI-Prolog также проверьте call_with_inference_limit/3, чтобы строго ограничить выполнение, независимо от типа ЦП и загрузки системы.

Связанные а также полезны терминации анализаторы как cTI: Они позволяют статически получить условия прекращения.

Answer 2

Да, вы можете использовать мета-интерпретаторы для этой цели, как предполагает мат. Но для обычного случая использования это выходит далеко за рамки обычных усилий.

Вместо этого вы можете отделить функциональность цикла от вашей фактической логики, используя предикаты более высокого порядка. Это очень безопасный способ пойти — SWI даже проверяет, имеет ли все использование соответствующее определение. Эта проверка либо вызывается при вводе make. или check.

В качестве примера рассмотрим closure0/3 и path/4 которые оба обрабатывать проверки цикла «раз и навсегда».