Нежелательные свойства CLPB

Question

library(clpb) В настоящее время доступен в SICStus (оригинальная версия) и SWI (по мат). Позвольте мне прийти к сути довольно быстро:

?- X = 1+1, sat(X), X = 1+1.
X = 1+1.

?-          sat(X), X = 1+1.
false.

Так что это аналогичная проблема, поскольку она существует в состоянии по умолчанию library(clpfd),

Что делать в такой ситуации?

Обновление: В library(clpfd) мата, теперь есть функтор # /1 для этого. В идеале, сопровождается декларацией оператора op(100,fx,#)Теперь мы можем написать:

?- X = 1+1, #X #= Y.
ERROR: Type error: `integer' expected, found `1+1' (a compound)

Для обеспечения полных алгебраических свойств нужно объявить:

:- set_prolog_flag(clpfd_monotonic, true).

Теперь переменные, которые остаются неоднозначными (то есть являются целыми числами или выражениями), вызывают ошибки при создании:

?-  1 + 1 #= Y.
ERROR: Arguments are not sufficiently instantiated
?- 1 + 1 #= #Y.
Y = 2.

Answer 1

Что делать в такой ситуации?

А пока также library(clpb) обеспечивает монотонность, аналогичную library(clpz)/ library(clfd). В этом режиме выполнения явные переменные должны быть украшены (v)/1.

      ?- set_prolog_flag(clpb_monotonic,true).
true.

?- sat(X).
ERROR: Arguments are not sufficiently instantiated

?- set_prolog_flag(clpb_monotonic,true).
true.

?- current_prolog_flag(clpb_monotonic,X).
X = true.

?- sat(X).
ERROR: Arguments are not sufficiently instantiated

?- sat(v(X)).
X = 1.

В Скрайере скажите:

      ?- use_module(library(clpb)).
   true.
?- asserta(clpb:monotonic).
   true.
?- sat(X).
caught: error(instantiation_error,instantiation_error(unknown(_67),1))
?- sat(v(X)).
   X = 1
;  false.

Answer 2

Да, то же самое в CLP(FD) и CLP(B):

ситуация

CLP(FD), (+)/2 действует как сложение в конечной области:

?- X = 1+1, X #= 2.
X = 1+1.

?- X #= 2.
X = 2

?- X #= 2, X = 1+1.
false.

CLP (B), (+)/2 действует как дизъюнкция в логическом домене:

?- X = 1+1, sat(X)
X = 1+1

?- sat(X)
X = 1

?- sat(X), X = 1+1.
false

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

?- X = 3, X \= 4.
X = 3.

?- X \= 4, X = 3.
false.

проблема

Итак, что мы должны сказать студентам? Я не думаю, что здесь виноваты CLP(FD) или CLP (B).

Это больше укоренилось в (=)/2, и невозможность подключиться к (=)/2, так что он делает больше, чем verify_attribute/3.

В идеальном мире (=) / 2 будет работать алгебраически, и X=1+1 не сработает, система увидит, что 1 + 1 равно 2 (случай FD), соответственно 1 + 1 равно 1 (случай B).

Но для этого системе Пролога в качестве начала потребуются типы, в противном случае (=) / 2 не сможет интерпретировать (+)/2, в нашем примере она имеет две разные интерпретации.

Решение

Решение состоит в том, чтобы воздерживаться от использования (=) / 2 там, где нужны определенные типы. Настоящим я рекомендую прочитать:

Программирование логики ограничений с использованием ECLiPSe
Кшиштоф Р. Апт и Марк Уоллес,
16 мая 2006 г., полный текст PDF

Приведенная выше статья немного подчеркивает мотивацию знака хеша (#) в качестве префикса для таких операторов, как (=)/2, (<) / 2 и т. Д.). Это уже аннотация типа. В этой статье есть еще один префикс, а именно знак доллара ($).

В ECLiPSe Prolog знак хеша (#) подразумевает ограничение целых чисел /1, а знак доллара ($) подразумевает ограничение реалов /1. Эти ограничения также могут использоваться независимо, как показано в следующем примере:

?- integers([X,Y]), X = 3, Y = 4.5.
No

?- reals(X), X = [1,2.1,a].
No

Возвращаясь к вашей проблеме некоммутативности (=)/2. Хотя (=) / 2 некоммутативен, (#=)/2 и его логический брат, конечно, коммутативны. У нас есть:

CLP(FD), (+)/2 действует как сложение в конечной области, и с (#=)/2 коммутация есть:

?- X #= 1+1, X #= 2.
X = 2

?- X #= 2, X #= 1+1.
X = 2

CLP (B), (+)/2 действует как дизъюнкция в булевой области, и с коммутацией sat/1 и (=:=)/2 есть:

?- sat(X=:=1+1), sat(X).
X = 1.

?- sat(X), sat(X=:=1+1).
X = 1

Хук verify_attribute / 3 вызовет только те ограничения, которые могут дополнительно завершиться объединением домена Herbrand. Но они не могут оценить термины на лету, прежде чем присваивать им переменную Prolog.

Только пробужденные ограничения могут присваивать значения другим переменным. Но, например, текущая спецификация SICStus для verify_atribute/3 даже рекомендует не делать это напрямую, а только в очереди продолжения. Смотрите недавнее обсуждение группы SWI-Prolog.

Итак, длинный разговор, краткое объяснение: никогда не забывайте, что (=)/1 работает только для области Гербранда в Прологе, даже если мы подключаем ограничения. Я не говорю, что система Пролог не может работать по-другому, но это состояние Искусства Стада или систем Пролога.

до свидания