Prolog 中的非破坏性通用量化

Question

一门好的逻辑编程语言应该允许程序员使用与数学家使用的语言接近的语言。因此，我一直认为 Prolog 中缺少适当的通用量词是一个重要的缺点。

今天我想到了如何定义比 forall 和 foreach 更好的东西。

`forany(Var, {Context}, Condition, Body)`

这个谓词试图证明 Body 对于所有实例化 Var 在 Condition 上连续回溯。 Condition 和 Body 中的所有变量都被视为局部变量，除非在 Var 或 Context 中列出。 Condition 不允许以任何方式修改 Context 中列出的变量，否则 forany 将无法正常工作。

下面是实现（基于 yall）：

forany(V, {Vars}, Goal1, Goal2) :-
    (   bagof(V, {V,Vars}/Goal1, Solutions)
    ->  maplist({Vars}/[V]>>Goal2, Solutions)
    ;   true ).

我的第一个问题是关于 forany 的第二个参数。我想消除它。

现在一些例子

构建前 8 个方块的列表：

?- length(X,8), forany(N, {X}, between(1,8,N), 
                      (Q is N*N, nth1(N, X, Q))).
X = [1, 4, 9, 16, 25, 36, 49, 64].

反转列表：

?- X=[1,2,3,4,5], length(X,N), length(Y,N),
     forany(I, {X,Y,N}, between(1,N,I),
           (J is N-I+1, nth1(I,X,A), nth1(J,Y,A))).
X = [1, 2, 3, 4, 5],
N = 5,
Y = [5, 4, 3, 2, 1].

子集：

subset(X, Y) :- forany(A, {X,Y}, member(A,X), member(A, Y)).

一种有趣的方式来生成列表的所有排列而不重复：

permutation(X, Y) :-
     length(X, N), length(Y, N), subset(X, Y).

?- permutation([1,2,3],X).
X = [1, 2, 3] ;
X = [1, 3, 2] ;
X = [2, 1, 3] ;
X = [2, 3, 1] ;
X = [3, 1, 2] ;
X = [3, 2, 1] ;
false.

一种对不同整数列表进行排序的有趣方法。请注意，约束用于对列表进行排序，因此不会生成大多数排列：

sorted(X) :- forany(A-B, {X}, append(_, [A,B|_], X),
                    A#<B).

?- X=[7,3,8,2,6,4,9,5,1], length(X, N), length(Y, N),
                          sorted(Y), subset(X,Y).

X = [7, 3, 8, 2, 6, 4, 9, 5, 1],
N = 9,
Y = [1, 2, 3, 4, 5, 6, 7, 8, 9] .

问题

似乎这个 forany 在不使用约束时工作得很好。此外，它可用于生成约束，但至少在 SWI-Prolog 上，当约束已经生成时会出现问题。原因是 forany 使用 bagof 并且根据 SWI-Prolog 手册：

Term-copying operations (assertz/1, retract/1, findall/3, copy_term/2, etc.) generally also copy constraints. The effect varies from ok, silent copying of huge constraint networks to violations of the internal consistency of constraint networks. As a rule of thumb, copying terms holding attributes must be deprecated. If you need to reason about a term that is involved in constraints, use copy_term/3 to obtain the constraints as Prolog goals, and use these goals for further processing.

这里是 bagof 使用约束创建的问题的演示：

?- X=[A,B,C], dif(C,D), bagof(_, K^member(K,X), _).
X = [A, B, C],
dif(C, _5306),
dif(C, _5318),
dif(C, _5330),
dif(C, D).

如您所见，创建了三个不必要的约束。

我的第二个问题是这是否只是 SWI-Prolog 的问题。

第三个问题：有没有办法在 SWI-Prolog 中解决这个问题。手册中的上述引述表明应该使用 copy_term/3 。不幸的是，我不理解这个建议，我不知道它是否对 forany.

有用

Answer 1

好消息！我很惊讶 bagof 是用 Prolog 写的。通过查看它的代码，我了解到有些我认为不可能的事情实际上是可能的。正如 SWI-Prolog 手册所建议的那样，copy_term/3 或类似的谓词 copy_term_nat/2 有所帮助。

因此，我非常高兴能够为 SWI-Prolog 提供一个完全可用的（据我所知）通用量词：

forany(V, {Vars}, Condition, Body) :-
    findall(V-Vars, Condition, Solutions),
    % For SWI-Prolog.  Can be replaced by Solutions=Clean_solutions in other systems
    copy_term_nat(Solutions, Clean_solutions),
    forany_execute_goals(Clean_solutions, Vars, V, Body).

forany_execute_goals([], _, _, _).
forany_execute_goals([Sol-NewVars|Solutions], Vars, V, Body) :-
    % The following test can be removed
    assertion(subsumes_term(NewVars, Vars)),
    % or replaced by the following more standard use of throw/1:
%   (  subsumes_term(NewVars, Vars)
%   -> true
%   ;  throw('Forbidden instantiation of context variables by the antecedent of forany')  ),
    NewVars = Vars,
    call({Vars}/[V]>>Body, Sol),
    forany_execute_goals(Solutions, Vars, V, Body).

Prolog 中的非破坏性通用量化

Non-destructive universal quantification in Prolog

prolog

swi-prolog

prolog-dif

prolog-setof

`forany(Var, {Context}, Condition, Body)`

现在一些例子

问题