Я написал быстрый предикат на Прологе, опробовав CLP (FD) и его способность решать системы уравнений.
problem(A, B) :-
A-B #= 320,
A #= 21*B.
Когда я звоню в SWI, я получаю:
?- problem(A,B).
320+B#=A,
21*B#=A.
В то время как в GNU я получаю правильный ответ:
| ?- problem(A,B).
A = 336
B = 16
Что тут происходит? В идеале я бы хотел получить правильные результаты в SWI, так как это гораздо более надежная среда.
Это хорошее наблюдение.
На первый взгляд, без сомнения, недостатком SWI будет то, что он не распространяется так сильно, как GNU Prolog.
Однако здесь есть и другие факторы.
Для начала попробуйте следующий запрос в GNU Prolog:
| ?- X #= X.
Декларативно запрос можно прочитать как: X - целое число. Причины:
(#=)/2 действует только для целых чиселX #= X никоим образом не ограничивает область действия целого числа X.Однако, по крайней мере, на моей машине GNU Prolog отвечает так:
X = _#0(0..268435455)
Итак, на самом деле домен целого числа X стал конечным, хотя мы никоим образом не ограничивали его!
Для сравнения мы получаем, например, в SICStus Prolog:
?- X #= X. X in inf..sup.
Это показывает, что область целого числа X не никаким образом ограничена.
Давайте уравнять правила игры. Мы можем смоделировать описанную выше ситуацию с помощью SWI-Prolog, искусственно ограничив домены переменных, скажем, конечным интервалом 0..2 64 :
?- problem(A, B), Upper #= 2^64, [A,B] ins 0..Upper.
В ответ мы получаем с SWI-Prolog:
A = 336, B = 16, Upper = 18446744073709551616.
Итак, ограничение домена конечным подмножеством целых чисел позволило нам воспроизвести результат, который мы знаем из GNU Prolog, также с помощью решателя CLP (FD) SWI-Prolog или его преемника, CLP (Z).
Целью CLP (Z) является полная замена арифметических предикатов низкого уровня в пользовательских программах декларативными альтернативами высокого уровня, которые могут использоваться как истинные отношения и, конечно, также как вставные замены. По этой причине CLP (Z) поддерживает неограниченные целые числа, которые могут увеличиваться настолько, насколько позволяет память вашего компьютера. В CLP (Z) домен по умолчанию для всех целочисленных переменных - это набор всех целых чисел. Это означает, что определенные распространения, которые применяются для ограниченных доменов, не выполняются, пока один из доменов бесконечен.
Например:
?- X #> Y, Y #> X. X#=<Y+ -1, Y#=<X+ -1.
Это условный ответ: исходный запрос выполняется если и только если выполняются так называемые остаточные ограничения.
Напротив, с конечными доменами мы получаем:
?- X #> Y, Y #> X, [X,Y] ins -5000..2000. false.
Пока все домены конечны, мы ожидаем примерно одинаковой мощности распространения от задействованных систем.
Решение уравнений над целыми числами в целом неразрешимо. Итак, для CLP (Z) мы знаем, что не существует никакого алгоритма принятия решения, который всегда давал бы правильные результаты.
По этой причине вы иногда получаете остаточные ограничения вместо безусловного ответа. Для конечных наборов целых чисел уравнения, конечно, разрешимы: если все области конечны и вы не можете получить конкретное решение в качестве ответа, используйте один из предикатов перечисления, чтобы исчерпывающе поиск решений.
В системах, которые могут рассуждать о бесконечных наборах целых чисел, вы рано или поздно и обязательно столкнетесь с такими явлениями.
Upper #= 7^7^5 - респект!
- person false; 26.12.2017
?- problem(A,B), [A,B] ins 0..1000, label([A,B]).Лучше поместить такие детали в определение проблемы / 2, хотя - person CapelliC schedule 26.12.2017