Что такое простой наихудший случай для проверки в Прологе?

Question

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

         X1 = f(X0, X0),
   X2 = f(X1, X1),
   ..
   Xn-1 = f(Xn-2, Xn-2),
   Xn = f(Xn-1, Xn-1).

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

Если в системе Пролог нет occurs_check=trueфлаг, можно попробовать unify_with_occurs_check/2на месте (=)/2.

Answer 1

Вот сравнение. Я протестировал задачу эквациональной унификации внутри тела предложения. Ссылка на исходный код теста и результаты тестов находятся в конце этого ответа:

      test :-
    B = f(A, A),
    C = f(B, B),
    D = f(C, C),
    X = f(D, D).

Etc..

Jekejeke Prolog 1.4.6 и SWI-Prolog 8.3.17 по-прежнему линейны. Jekejeke Prolog использует статический анализ, работает не всегда. SWI-Prolog делает это динамически, я думаю, это побочный эффект работы с циклическими терминами. Но GNU Prolog 1.4.5 экспоненциален. Я использовал n=4, 6, 8 и 10:

Открытый исходный код:

Линейный или экспоненциальный?
https://gist.github.com/jburse/2d5fd1d3dd8436acceca52fdfc537581#file-size-pl

Answer 2

Еще не полностью проверенная гипотеза. Есть некоторое подтверждение того, что мы можем посмотреть код ВМ. Есть опасность, что я все еще смотрю, смотрю, смотрю… и ничего не вижу.

Вот мое подозрение на SWI-Prolog. Относительно этой
проблемы эквациональной унификации, теперь в теле статьи:

      X1 = f(X0, X0),
X2 = f(X1, X1),
..
Xn-1 = f(Xn-2, Xn-2),
Xn = f(Xn-1, Xn-1).

Только одно уравнение оптимизируется, когда exists_check=true? Это могло бы
объяснить разное количество LIPS и разную производительность:

      /* (=)/2, occurs_check=false */
% % 2,000,000 inferences, 0.222 CPU in 0.226 seconds (98% CPU, 9007995 Lips)

/* unify_with_occurs_check/2 */
% % 12,000,000 inferences, 1.382 CPU in 1.411 seconds (98% CPU, 8680009 Lips)

/* (=)/2, occurs_check=true */
% 11,000,000 inferences, 1.264 CPU in 1.270 seconds (100% CPU, 8704963 Lips)

Оки Доки.