замораживание / блокировка 2 целей для переменных, которые стали недостижимыми

TL; DR: ошибка в SWI больше нет !

Вы создаете 500 000 замороженных целей, которые впоследствии недостижимы. Что означают эти цели? Системы Prolog не анализируют цель на предмет ее семантической значимости (до ее фактического выполнения). Поэтому мы должны предположить, что цели могут быть семантически релевантными. Поскольку цели уже не связаны друг с другом, единственный семантический эффект, который они могут иметь, состоит в том, чтобы оказаться ложным и, таким образом, сделать следующий ответ ложным.

Так что вместо этого достаточно рассмотреть freeze(_,false).

Семантически предикаты p/0 и q/0 эквивалентны:

p :-
   false.

q :-
   freeze(_,false).

Однако с процедурной точки зрения первая цель не выполняется, а вторая достигается. В таких ситуациях важно различать решения и ответы. Когда Prolog завершается успешно, он выдает ответ, обычно это называется подстановкой ответа в Прологе без ограничений, где подстановки ответов всегда содержат одно или бесконечно много решений ¹. При наличии ограничений или грубой сопрограммы ответ теперь может содержать замороженные цели или ограничения, которые необходимо принять во внимание, чтобы понять, какие решения фактически описаны.

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

В SICStus это отображается следующим образом:

| ?- q.
prolog:freeze(_A,user:false) ? ;
no

В SWI и YAP эти цели не отображаются по умолчанию, и поэтому есть вероятность, что таких ошибок, как эта, не обнаружено.

PS: В прошлом было сравнение между различными системами, касающимися GC и ограничений, при этом SICStus в то время был единственным, кто прошел все тесты. Тем временем некоторые системы улучшились.

Я сначала посмотрел на цифры SICStus: 216 байт на замораживание! Это 27 слов, из которых 13 только для термина, представляющего цель. Так что просто 14 слов для остановки. Не так плохо.

PPS: замороженная цель была throw/2, она должна была быть throw/1

^{Мелкий шрифт 1: некоторые примеры: подстановка ответов X = 1 содержит ровно одно решение, а X = [_A] содержит бесконечно много решений, таких как X = [a] и многие, многие другие. Все это становится намного сложнее в контексте ограничений.}

Восстановление замороженных целей невозможно в определенных настройках. Например, в CC это будет запрещено, поскольку программа имеет как минимум 3 результата:

Есть статья Эвана Тика, объясняющая CC:

Программа успешно завершается, когда, начиная с первоначального пользовательского запроса (конъюнкция атомов), после некоторого количества шагов сокращения не остается ни одной цели, которую нужно выполнить, или она приостанавливается. Как вариант, программа заходит в тупик, если остаются только приостановленные цели. Третий результат - сбой программы, который более формально определяется ниже.

РАЗВИТИЕ СОВМЕСТНЫХ ЯЗЫКОВ ЛОГИЧЕСКОГО ПРОГРАММИРОВАНИЯ
Эван Тик - 1995
https://core.ac.uk/download/pdf/82787481.pdf

Вот пример, иллюстрирующий проблему. freeze / 2 более примитивен, чем CLP (FD). Таким образом, CLP (FD) иногда может делать следующее:

Welcome to SWI-Prolog (threaded, 64 bits, version 7.7.21)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

?- [user].
test(A,B) :- A #< X, X #< B.

?- test(1,2).
false

?- test(1,3).
true

Но теперь, если я сделаю то же самое с замораживанием, я потеряю всю информацию, поскольку SWI-Prolog восстанавливает замороженные цели:

?- [user].
test2(A,B) :- freeze(X,(integer(X),A<X)), freeze(X,(integer(X),X<B)).

?- test2(1,2).
true.

?- test2(1,3).
true.

Возможно, требуется более тонкий контроль над поведением сборки мусора.

Редактировать 1: для более тонкого управления в SWI-Prolog предлагается обернуть его с помощью call_residue_vars / 2. Я не знаю, является ли это самым умным решением, но, по крайней мере, это решение:

?- call_residue_vars(test2(1,2),L).
L = [_5538],
freeze(_5538,  (integer(_5538), 1<_5538)),
freeze(_5538,  (integer(_5538), _5538<2)).

?- call_residue_vars(test2(1,3),L).
L = [_5544],
freeze(_5544,  (integer(_5544), 1<_5544)),
freeze(_5544,  (integer(_5544), _5544<3)).