Какую оптимизацию выполняет SWI Prolog?

Question

Процитируем руководство SICStus Prolog :

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

Тем не менее, я запустил эти тесты ( тесты Prolog) и увидел довольно незначительные различия (менее 20%) в SWI Prolog между включенной и выключенной проверкой событий (OC):

OC выключен: :- set_prolog_flag(occurs_check, false). в (перезапущен)

      ?- run_interleaved(10).
% 768,486,984 inferences, 91.483 CPU in 91.483 seconds (100% CPU, 8400298 Lips)
true.

?- run(1).
'Program'            Time     GC
================================
boyer               0.453  0.059
browse              0.395  0.000
chat_parser         0.693  0.000
crypt               0.481  0.000
fast_mu             0.628  0.000
flatten             0.584  0.000
meta_qsort          0.457  0.000
mu                  0.523  0.000
nreverse            0.406  0.000
poly_10             0.512  0.000
prover              0.625  0.000
qsort               0.574  0.000
queens_8            0.473  0.000
query               0.494  0.000
reducer             0.595  0.000
sendmore            0.619  0.000
simple_analyzer     0.620  0.000
tak                 0.486  0.000
zebra               0.529  0.000
           average  0.534  0.003
true.

OC включен: :- set_prolog_flag(occurs_check, true). в .swiplrc (перезапущен)

      ?- run_interleaved(10).
% 853,189,814 inferences, 105.545 CPU in 105.580 seconds (100% CPU, 8083669 Lips)
true.

?- run(1).
'Program'            Time     GC
================================
boyer               0.572  0.060
browse              0.618  0.000
chat_parser         0.753  0.000
crypt               0.480  0.000
fast_mu             0.684  0.000
flatten             0.767  0.000
meta_qsort          0.659  0.000
mu                  0.607  0.000
nreverse            0.547  0.000
poly_10             0.541  0.000
prover              0.705  0.000
qsort               0.660  0.000
queens_8            0.491  0.000
query               0.492  0.000
reducer             0.867  0.000
sendmore            0.629  0.000
simple_analyzer     0.757  0.000
tak                 0.550  0.000
zebra               0.663  0.000
           average  0.634  0.003
true.

Эти тесты не репрезентативны для реального использования? (Я помню, что где-то читал, что они были специально выбраны как «достаточно репрезентативные») Реализует ли SWI Prolog некоторые приемы оптимизации, о которых сотрудники SICStus не знают, которые делают стоимость OC незначительной? Если да, то публикуются ли они? (Я нашел кучу статей об этом из 90-х, но не знаю, современные ли они)

Answer 1

Основная оптимизация делает унификацию локальных переменных постоянной операцией.

Многие абстрактные машины, такие как PLM, ZIP, WAM, VAM, предоставляют особый случай для логических переменных, которые не могут быть подтерминами какой-либо структуры (называемых локальными переменными). Унификация с такими переменными вообще не требует проверки на наличие событий и, следовательно, может быть постоянной. Таким образом, большие термины могут быть «возвращены» без необходимости дополнительной проверки.

Без этой оптимизации обработка грамматик (для синтаксического анализа заданного списка) получает накладные расходы, квадратичные по количеству токенов. Каждый раз, когда «список ввода» передается обратно (так, говоря графическим языком, каждый раз, когда вы пересекаете запятую после нетерминала в теле грамматики), оставшийся список ввода необходимо сканировать на предмет наличия этой локальной переменной. (Это лучше, чем квадратичный по количеству символов, поскольку регулярные выражения в основном кодируются хвостовой рекурсией).

Эта оптимизация была введена в версии 5.6.39 2007 года . Удивительно, что ваши измерения показывают накладные расходы даже в таких случаях, как tak, когда вообще не построено ни одной конструкции. Насколько я помню, объединение событий-проверки в SWI 5.6.39 выполнялось немного быстрее, чем объединение рациональных деревьев (для простых случаев), поскольку (в то время) дополнительных настроек не требовалось.

Есть еще достаточно места для многих дальнейших оптимизаций с проверкой событий. Но это произойдет только в том случае, если люди будут использовать эту функцию. Что касается SWI, за последние 13 лет произошло немногое.

Но подумайте: самый первый Пролог, называемый Пролог 0, по умолчанию поддерживал проверку на наличие событий. Но начиная с Пролога I («Марсельский Пролог») использовались только отговорки (вроде тех, которые вы цитируете). И, по крайней мере, стандарт не исключает объединение по умолчанию с проверкой происшествий, определяя только выполнение NSTO и требуя unify_with_occurs_check/2 и <tcode id="534437"></tcode>. И теперь прологи, такие как SWI и Tau, предоставляют это необязательно через флаг.

Дальнейшая оптимизация в том же направлении - это тег NEW_UNBOUND Иоахима Бера, который позволяет избежать также проверок некоторых переменных кучи за счет более сложной схемы. См. Еще раз «Проблема проверки возникновения». JLP 5 (3) 1988. И LNCS 404.

Answer 2

Вот тестовый пример, в котором проверка «происходит» удваивает время выполнения запроса. Возьмите этот код, чтобы вычислить нормальную форму отрицания. Поскольку (=) / 2 находится в конце правила, посещенные соединения становятся квадратичными:

      /* Variant 1 */
norm(A, R) :- var(A), !, R = pos(A).
norm((A+B), R) :- !, norm(A, C), norm(B, D), R = or(C,D).
norm((A*B), R) :- !, norm(A, C), norm(B, D), R = and(C,D).
Etc..

Мы можем сравнить с этим вариантом, где (=) / 2 выполняется первым, пока соединение еще не создано:

      /* Variant 2 */
norm(A, R) :- var(A), !, R = pos(A).
norm((A+B), R) :- !, R = or(C,D), norm(A, C), norm(B, D).
norm((A*B), R) :- !, R = and(C,D), norm(A, C), norm(B, D).
Etc..

Вот некоторые измерения для SWI-Prolog 8.3.19. Для варианта 1 установка флажка проверки на истинное значение удваивает время, необходимое для преобразования некоторых пропозициональных формул из принципа математики:

      /* Variant 1 */
/* occurs_check=false */
?- time((between(1,1000,_),test,fail;true)).
% 3,646,000 inferences, 0.469 CPU in 0.468 seconds (100% CPU, 7778133 Lips)
true.

/* occurs_check=true */
?- time((between(1,1000,_),test,fail;true)).
% 6,547,000 inferences, 0.984 CPU in 0.983 seconds (100% CPU, 6650921 Lips)
true.

С другой стороны, перемещение (=) / 2 вперед благоприятно меняет картину:

      /* Variant 2 */
/* occurs_check=false */
?- time((between(1,1000,_),test,fail;true)).
% 3,646,000 inferences, 0.453 CPU in 0.456 seconds (99% CPU, 8046345 Lips)
true.

/* occurs_check=true */
?- time((between(1,1000,_),test,fail;true)).
% 6,547,000 inferences, 0.703 CPU in 0.688 seconds (102% CPU, 9311289 Lips)
true.

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

Нормальная форма отрицания, нехвостовая рекурсивная
https://gist.github.com/jburse/7705ace654af0df6f4fdd12eee80aaec#file-norm-pl

Нормальная форма отрицания, рекурсивный хвост
https://gist.github.com/jburse/7705ace654af0df6f4fdd12eee80aaec#file-norm2-pl

193 тестовых примера логики высказываний от Principia.
https://gist.github.com/jburse/7705ace654af0df6f4fdd12eee80aaec#file-principia-pl