2

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

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

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

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

这是实现（基于 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等）通常也复制约束。效果从好的，巨大的约束网络的无声复制到违反约束网络的内部一致性。根据经验，必须不推荐复制包含属性的术语。如果您需要推理约束中涉及的术语，请使用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.

4

1 回答 1

0

好消息！我很惊讶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).
于 2019-03-03T22:13:50.160 回答