Блог

 ordering(A, B, C) :-
    integer(A),
    integer(B),
    integer(C),
    A > B,
    B > C,
    A > 0,
    10 > C.
 

удовлетворяется ordering(3,2,1). . Но когда я оставляю одну или несколько переменных в качестве переменных ordering(3,X,1). , она вычисляется false .

Чего мне не хватает?

Обновление: спасибо за все подробные ответы. Я кое-чему научился у всех из них.

integer/1 сбой, если аргумент не является целым числом, например, если вы передаете несвязанную переменную. Я считаю, что вы должны использовать CLP (FD) для таких задач. В противном случае вы можете вручную привязать / протестировать переменные в некотором целочисленном диапазоне, используя between/3 для установки этого диапазона.

Например.:

 ordering(A, B, C) :-
   between(0, 100, A),  % A is an integer in the range [0,100]
   between(0, 100, B),  % same for B
   between(0, 100, C),  % and C
   A > B,
   B > C,
   A > 0,
   10 > C.
 

Пример запуска:

 ?- ordering(3,X,1).
X = 2 ;
false.
 

Это неудивительно.

Очевидно integer(X) , что с X unbound немедленно произойдет сбой. В этом отношении это очень «важно».

Кроме того, предикат завершится ошибкой с C unbound из-за 10 > C .

В лучшем случае вы могли бы написать предикат can_be/2 так, чтобы can_be(integer,X) он выполнялся успешно, когда несвязанная переменная X «все еще может стать целым числом», а в противном случае не выполняется.

По расширению было бы a can_be_ordered(A, B, C) , который терпит неудачу, если он уверен, что [A,B,C] никогда не может быть упорядочен из-за значений, которые они уже обозначают, или завершается успешно, если [A,B,C] все еще может быть упорядочен в зависимости от того, какие значения любые несвязанные переменные в нем принимают в будущем.

Было бы еще лучше уточнить значение истинности:

ordering(List,Result)

где Result

• true : Да, упорядочено и останется упорядоченным.
• false : Определенно не упорядочено, и это не изменится.
• unknown/maybe : Нет четких доказательств того, что он неупорядоченный или упорядоченный.

Затем вы также можете присоединяться ordering(List,Result) к несвязанным переменным, которые повторно проверяют порядок всякий раз, когда одна из переменных становится связанной, используя freeze/2 . Это в основном выполняет работу CLP (FD).

Вы можете отложить сравнение до инициализации переменных:

 ordering(A, B, C) :-
    greater(A, B),
    greater(B, C).

greater(X, Y) :-
    when((nonvar(X), nonvar(Y)), X > Y).
 

Тесты:

 ?- greater(3, 2).
true.

?- ordering(3, 2, 1).
true.

?- ordering(3, 2, 2).
false.

?- ordering(3, X, 1).
when(nonvar(X), 3>X),
when(nonvar(X), X>1).