纯append/3模式（-，+，+）不会留下选择点

Question

通常的append/3是纯粹的，但它为模式（-，+，+）留下了一个选择点：

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

e 是上述结果中的一个选择点，例如 SWI-Prolog 提供提示符，然后显示“;”传递错误。我想出了这个解决方案来避免选择点：

append2(X, Y, Z) :-
   reverse(Z, H),
   reverse(Y, J),
   append(J, K, H),
   reverse(K, X).

这个新的append2/3不再留下选择点：

?- append2(X, [3], [1,2,3]).
X = [1, 2].

但是还有比reverse/2 cludge更好的解决方案吗？请注意，有一个谓词 last/3 可用于仅从末尾删除一个元素的示例。但模式 (-,+,+) 应该适用于第二个参数中的任意长列表。

Answer 1

您的

append2

不会为（-，+，+）模式留下选择点，而是为其他模式引入它们。我不知道是否可以在不检查操作模式的情况下使用

var/1

或其他东西来编写它。

这是 mercury 库 手册中关于相关模式的评论。

% The following mode is semidet in the sense that it doesn't
% succeed more than once - but it does create a choice-point,
% which means it's inefficient and that the compiler can't deduce
% that it is semidet. Use remove_suffix instead.
% :- mode append(out, in, in) is semidet.

remove_suffix

谓词在汞中实现如下：

remove_suffix(List, Suffix, Prefix) :-
    list.length(List, ListLength),
    list.length(Suffix, SuffixLength),
    PrefixLength = ListLength - SuffixLength,
    list.split_list(PrefixLength, List, Prefix, Suffix).

Answer 2

但是有比反向/2 拼凑更好的解决方案吗？

有更好的解决方案，但不是最佳解决方案：

:- use_module(library(reif)).

append2u(Xs, Ys, Zs) :-
   if_(Ys = Zs,
      Xs = [],
      ( Xs = [X|Xs1], Zs = [X|Zs1], append2u(Xs1, Ys, Zs1) )
   ).

?- append2u(Xs, [3], [1,2,3]).
   Xs = [1,2].

库

reif

内置于 Scryer 中，也可用于 SICStus 和 SWI。

甚至查询...

?- append2u(Xs, Ys, Ys).
   Xs = [].

...现在可以了！

请注意，与append/3 等效需要启用发生检查。在具有理性树的系统中（因此不会发生检查），我们得到的答案比单一解决方案更多：

?- append(Xs, Ys, Ys).
   Xs = []
;  Xs = [_A], Ys = [_A|Ys]        % infinite list Ys = [_A,_A,_A, ...]
;  Xs = [_A,_B], Ys = [_A,_B|Ys]  % infinite list Ys = [_A,_B,_A,_B,_A,_B, ...]
;  ... .

尽管如此，

?- append2u([], Ys, Zs).
   Ys = Zs
;  false.

这通常是确定的。

但是，终止属性仍然完好无损！事实上，

append2u/3

的终止效果比常见的

append/3

好一些，如上面第一种情况所示。

Answer 3

刚刚用reverse/3跳过了进一步的解决方案，
消除内部追加/3。

append3(X, Y, Z) :-
   reverse(Z, H),
   reverse(Y, K, H),
   reverse(K, X).

reverse(X, Y) :-
  reverse(X, [], Y).

reverse([], X, X).
reverse([X|Y], Z, T) :- 
   reverse(Y, [X|Z], T).

似乎有效，没有选择点。
并且比 append2u 性能更高：

?- append3(X, [3], [1,2,3]).
X = [1, 2]

?- length(P,100), length(Q,200), 
   time((between(1,40,_),append3(X, P, Q), fail; true)).
% Up 9 ms, GC 0 ms, Threads 8 ms (Current 12/19/20 08:57:49)
Yes

?- length(P,100), length(Q,200), 
   time((between(1,40,_),append2u(X, P, Q), fail; true)).
% Up 875 ms, GC 9 ms, Threads 862 ms (Current 12/19/20 08:57:45)
Yes

但也有一点危险：

?- append3([1], [2,3], X).
X = [1, 2, 3] ;
%%% hangs