Оптимизируют ли современные компиляторы Prolog автоматическую проверку происходящего, когда это безопасно?

Изменить: этот вопрос предполагает, что вы включили проверку возникновения. Это не о настройке Пролога флаги .

30 лет назад была куча статей об оптимизации автоматической проверки событий, когда это безопасно (около 90% предикатов в типичных кодовых базах). Предлагались разные алгоритмы. Делают ли современные компиляторы Prolog (например, SWI Prolog) что-нибудь подобное (когда включена проверка появления)? Какие алгоритмы они предпочитают?

Например, удаляют ли они проверку возникновения при компиляции такого предиката:

      less(0, s(_)).
less(s(X), s(Y)) :- less(X, Y).

(из обсуждения ниже этого ответа )

Источник

3 ответа

Решение

Существует множество оптимизаций, которые могут оптимизировать проверку событий, когда флаг проверки событий установлен на «истина». Это необходимо для того, чтобы в общих случаях стало возможным разумное объединение. Типичная оптимизация - это определение линейности головы:

      linear(Head) :-
   term_variables(Head, Vars),
   term_singletons(Head, Singletons),
   Vars == Singletons.

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

      ?- linear(less(0, s(_))).
true.

?- linear(less(s(X), s(Y))).
true.

Таким образом, система Prolog может полностью опустить проверку выполнения для предиката less/2и тем не менее производят звуковое объединение. Эта оптимизация, например, наблюдается в Jekejeke Prolog при проверке промежуточного кода. Используется инструкция unify_linear:

      ?- vm_list(less/2).

less(0, s(A)).
  0  unify_linear _0, 0
  1  unify_linear _1, s(A)
less(s(X), s(Y)) :-
   less(X, Y).
  0  unify_linear _0, s(X)
  1  unify_linear _1, s(Y)
  2  goal_last less(X, Y)

В отличие от инструкции unify_term, инструкция unify_linear не выполняет проверку наличия, даже если флаг проверки возникновения установлен в значение true.

Риту Чадха; Дэвид А. Плейстед (1994). «Корректность унификации без проверки в прологе» . Журнал логического программирования. 18 (2): 99–122. DOI:10.1016 / 0743-1066(94)90048-5 .

Источник

SWI Prolog не включает проверку событий, если вы специально не попросите его:

  • Используя <tcode id="383282"></tcode> вместо =локально. (Обратите внимание, что это означает, что объединение головок не затронуто, т.е. все еще выполняется без проверки - я думаю?)
  • При включении происходит глобальная проверка через установку флага <tcode id="383284"></tcode>: set_prolog_flag(occurs_check,true)

Это проблема? Я так не думаю.

Рассмотрим связанный случай наличия утверждений на других языках программирования (или даже в Прологе, если на то пошло: <tcode id="383286"></tcode>, Очень рекомендую).

Во время разработки они будут «включены» для проверки ограничений во время выполнения при некоторой стоимости процессора. Как только вы убедитесь, что ваша программа работает (путем построения, пррофилирования и тестирования), вы «отключите их». Интерфейсы между вашей программой и любой вызывающей стороной (которая может быть злонамеренной, запутанной или ошибочной) все еще могут быть защищены <tcode id="383287"></tcode> проверяет соблюдение контрактов интерфейса.

Случай с проверкой происходит аналогичным образом: если вы подозреваете, что циклические структуры данных могут возникать и приводить к проблемам, включите проверку срабатывания. Программируйте код так, чтобы все работало правильно (и вы были уверены, что все работает правильно, желательно путем построения и доказательства). Затем снова выключите его.

Источник

Также популярно использование различий внутри переменных, таких как «свежие» и «устаревшие» переменные. «свежие» переменные обычно не требуют проверки.

Различие можно проводить динамически. Вот некоторые результаты, динамическое различие («Свежесть») также можно комбинировать с некоторым статическим анализом («Линейный»):

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

Возвращение к проблеме проверки происшествий - пиво, 1988 г.
https://core.ac.uk/download/pdf/82747799.pdf

Источник
Другие вопросы по тегам