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的手册：

术语复制操作（assertz/1，retract/1，findall/3，copy_term/2等）通常也会复制约束。效果不同于ok，无声复制大型约束网络，违反约束网络的内部一致性。根据经验，必须弃用复制包含属性的术语。如果您需要推理约束中涉及的术语，请使用copy_term/3获取Prolog目标的约束，并使用这些目标进行进一步处理。

以下是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).