Пролог: почему это «плохая» программа?

Question

max(M,N,M):-M >= N,!.
max(M,N,N).

Я читаю учебник, в котором говорится, что декларативное и процедурное значения различаются ... Я не понимаю, как.

Может ли кто-нибудь указать мне правильное направление?

Answer 1

tl; dr: это не отношение.

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

?- max(1,0,N). % without the cut
   N = 1
;  N = 0.

Это будет зеленым срезом, если второе предложение будет иметь вид:

max(M,N,N) :- M < N.

В каком именно состоянии происходит разрез? Это не M >= N, а скорее подразумевается еще одно условие, а именно: A1 = A3, ... Это непосредственно не видно, как показывает только повторное вхождение переменной:

max(M,N,M):-M >= N,!.
        ^
        |
        + hidden equality

Используя это скрытое равенство, мы можем легко построить противоречивый пример: взять M и N, такие что M > N и поставить N в третьем аргументе (хотя мы знаем, что это неправильно).

?- max(1, 0, 0).   % the original version
true.              % very wrong!
?- max(1, non_number, non_number).
true.              % even wronger!
?- max(an-other, non_number, non_number).
true.              % wrongest!!

Чтобы исправить это, мы должны отложить объединение после вырезания.

max(M,N,R):- M >= N,!, R = M.
max(M,N,N).

Теперь все исправлено? К сожалению нет ...

Каков результат? Это число?

?- max(1+0,0, R).
   R = 1+0.

Не всегда. Может быть, лучше принять в качестве определения:

max(M,N,R):- M >= N,!, R is M.
max(M,N,R) :- R is N.

А как насчет

?- max(0,N,1).
ERROR: Arguments are not sufficiently instantiated

Но ... есть только одно решение для этого! А именно, N = 1

Комплекс, не так ли? Ну, originallz, Пролог вообще не занимался арифметикой. Это было довольно исправлено позже. Лучший способ сформулировать это отношение в настоящее время - использовать текущий library(clpz) (@SICStus, @Scryer) или его более не поддерживаемый, поэтому менее надежный предшественник library(clpfd) (@SWI).

:- op(150, fx, #).   % only needed on SWI
max(M, N, Max) :-
   max(#M,#N) #= #Max.

This теперь действительно определяет максимальное отношение для целых чисел (но не для чисел с плавающей запятой ...).

Answer 2

Я оставлю кому-то еще объяснять опасности головных объединений вывода аргументов при наличии порезов. Вместо этого давайте рассмотрим случаи, когда предикату не удается объединить третий аргумент с максимумом первых двух аргументов. Мы можем определить следующее свойство, которому должен удовлетворять предикат max/3:

property(M,N,Max) :-
    (   max(M,N,Max) ->
        Max >= M, Max >= N
    ;   nonvar(Max)
    ).

Т.е. в случае успеха max/3 значение Max должно быть равным или превышать первые два аргумента. Если max/3 терпит неудачу, это должно произойти из-за связанного третьего аргумента, который не может объединиться с максимумом из двух входных аргументов.

Давайте QuickCheck это с помощью реализации lgtunit Logtalk (которую вы можете запустить с большинством Prolog системы; здесь я буду использовать SWI-Prolog):

$ swilgt
...

?- {lgtunit(loader)}.
...
% (0 warnings)
true.

?- [user].
|: max(M,N,M):-M >= N,!.
|: max(M,N,N).

Warning: user://1:102:
Warning:    Singleton variables: [M]
|: property(M,N,Max) :-
|:     (   max(M,N,Max) ->
|:         Max >= M, Max >= N
|:     ;   nonvar(Max)
|:     ).
|: ^D% user://1 compiled 0.01 sec, 3 clauses
true.

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

?- lgtunit::quick_check(property(+integer, +integer, ?integer), [n(20000)]).
*     quick check test failure (at test 5484 after 9 shrinks):
*       property(1,0,0)
false.

Как видно из сообщения об ошибке, определение предиката max/3 может завершиться неудачно при вызове со всеми связанными аргументами. Цель max(1,0,0) не объединяется с главой первого предложения. Таким образом, используется второе предложение, приводящее к успешной цели, где ожидается сбой.

Мы можем исправить ошибку (выставленную QuickCheck), переместив объединение с выходным аргументом в после сокращение:

max(M,N,Max):- M >= N,!, Max = M.
max(_,N,N).

Но правильно ли это определение? Быстрый тест с приведенным выше случаем показывает, что ошибка исправлена:

?- max(1,0,0).
false.

Давайте также QuickCheck (используя то же свойство):

?- lgtunit::quick_check(property(+integer, +integer, ?integer), [n(20000)]).
% 20000 random tests passed
true.

Выглядит хорошо, но помните: QuickCheck может выявлять ошибки, но не может доказать, что они не существуют. Фактически, если бы мы использовали количество тестов по умолчанию (100), мы могли бы пропустить ошибку. В некоторых случаях это помогает проверить с узкими аргументами. Например, используя оригинальное, глючное, определение max/3:

?- lgtunit::quick_check(
       property(
           +between(integer,-2,2),
           +between(integer,-2,2),
           ?between(integer,-2,2)
       )
   ).
*     quick check test failure (at test 23 after 0 shrinks):
*       property(1,-1,-1)
false.