prolog - 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).