是否总能用累加器替代append/3？下述代码中的append/3能否替换？

核心结论 #

可以替换，你之前多次替换失败大概率是实现的累加器版本没有对齐原select1/3的回溯语义和输出顺序要求。

原实现语义说明 #

原代码中的select1(X,L,L1)作用是从列表L中任选一个元素X，返回去掉X后剩余元素保持原有顺序的新列表L1，支持回溯输出所有X的可选取值。

% 原实现
select1(X,L,L1) :- append(L2,[X|L3],L), append(L2,L3,L1).

这种用两次append/3的写法是Prolog中实现「不定位置元素选取」的经典极简写法，非常符合Jens Otten的lean系列证明器追求代码极简、逻辑直观的设计风格。

累加器替换实现 #

下面的累加器版本完全对齐原实现的语义，可以直接替换原有实现：

select1(X, L, L1) :-
    select1_acc(X, L, [], L1).

% 累加器辅助谓词：遍历列表时用Acc存储已经过的前序元素
select1_acc(X, [X|Rest], Acc, L1) :-
    reverse(Acc, RevAcc),
    append(RevAcc, Rest, L1).
select1_acc(X, [Y|Rest], Acc, L1) :-
    select1_acc(X, Rest, [Y|Acc], L1).

替换注意事项 #

• 必须保留回溯能力：如果你的累加器实现加了剪枝!，只会返回第一个匹配的X，会破坏后续证明规则的搜索逻辑，导致证明器无法正常工作
• 必须保证剩余元素顺序不变：如果拼接新列表时没有反转累加器，会导致前序元素顺序颠倒，后续公式匹配逻辑出错，这也是最常见的替换失败原因

原作者选用append的原因 #

对于相继式演算证明器来说，上下文列表G（前件）和D（后件）的长度通常都非常小，append/3带来的性能损耗可以完全忽略，而两行append的实现比累加器版本可读性高很多，代码更短，符合leanseq的设计目标。

内容的提问来源于stack exchange，提问作者Joseph Vidal-Rosset