Prolog Language
Монотонность

Рассуждение о монотонных предикатах

Монотонические предикаты можно отлаживать, применяя декларативные рассуждения.

В чистом Prolog ошибка программирования может привести к одному или ко всем следующим явлениям:

1. предикат неправильно преуспевает в случае, если он не работает
2. предикат неправильно терпит неудачу в случае, когда он должен преуспеть
3. предикат неожиданно петли, где он должен давать только конечный набор ответов.

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

Примеры монотонных предикатов

Примерами монотонных предикатов являются:

• объединение с (=)/2 или unify_with_occurs_check/2
• dif/2 , выражающих нарушение условий
• CLP (FD), такие как (#=)/2 и (#>)/2 , используя монотонный режим выполнения.

Пролог предикаты, что только монотонные цели сами по себе монотонны.

Монотонические предикаты допускают декларативные рассуждения:

1. Добавление ограничения (т. Е. Цели) к запросу может в лучшем случае сократить и не расширять набор решений.
2. Удаление цели таких предикатов может в наибольшей степени расширить , а не уменьшить набор решений.

Немонотонные предикаты

Вот примеры предикатов, которые не монотонны:

• мета-логические предикаты, такие как var/1 , integer/1 и т. д.
• (@<)/2 и (@>=)/2
• предикаты, которые используют !/0 , (\+)/1 и другие конструкции, нарушающие монотонность
• предикаты всех решений, такие как findall/3 и setof/3 .

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

Как следствие, другие свойства, которые мы полагаемся на декларативную отладку и другие аргументы, также нарушены. Например, немонотонные предикаты нарушают фундаментальное понятие коммутативности конъюнкции, известной из логики первого порядка. Следующий пример иллюстрирует это:

?- var(X), X = a.
X = a.

?- X = a, var(X).
false.

Предикаты с findall/3 решений, такие как findall/3 также ломают монотонность: добавление предложений может привести к провалу целей, которые ранее были проведены . Это также противоречит montonicity, как известно из логики первого порядка, где добавление фактов может в наибольшей степени увеличиваться , никогда не уменьшать набор последствий.

Монотонные альтернативы для немонотонных конструкций

Вот примеры использования монотонных предикатов вместо нечистых немонотонных конструкций в ваших программах:

• dif/2 предполагается использовать вместо немонотонных конструкций, подобных (\=)/2
• арифметические ограничения (CLP (FD), CLP (Q) и другие) предназначены вместо использования арифметических предикатов
• !/0 почти всегда приводит к немонотонным программам, и его следует полностью избегать .
• ошибки создания могут быть подняты в ситуациях, когда вы не можете принять правильное решение в этот момент времени.

Сочетание монотонности с эффективностью

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

Для этого нет никаких доказательств. Недавние исследования показывают, что чистое монотонное подмножество Prolog может быть не только достаточным, чтобы выражать большинство реальных программ, но также приемлемо эффективно на практике. Конструкция, которая недавно была обнаружена и поощряет эту точку зрения, - это if_/3 : она сочетает монотонность с уменьшением точек выбора. См. Индексирование dif / 2 .

Например, код формы:

pred(L, Ls) :-
    condition(L),
    then(Ls).
pred(L, Ls) :-
    \+ condition(L),
    else(Ls).

Может быть написано с if_/3 как:

pred(L, Ls) :-
    if_(condition(L),
        then(Ls),
        else(Ls)).

и сочетает монотонность с детерминизмом.