为何Prolog谓词weave/3会重复成功并返回相同绑定？

你的问题根源在于两个终止子句的重叠匹配：当两个输入列表同时为空时，weave(_, [], [])和weave([], _, [])这两个子句都能成功匹配，从而产生重复的解；而不同长度的列表触发的终止子句不同，导致了不同的回溯行为：

分情况解析 #

• 第二个列表更长：比如测试weave([1,2], [a,b,c,d], Res)，递归最终会到weave([], [c,d], [])，此时只有weave([], _, [])能匹配，没有其他可选子句，所以仅返回一次正确结果。
• 第一个列表更长：比如测试weave([1,2,3], [a,b], Res)，递归最终到weave([3], [], [])，此时weave(_, [], [])匹配并返回正确结果；回溯时会尝试另一个终止子句weave([], _, [])，但[3]不是空列表，匹配失败，所以按;会得到false。
• 两列表长度相同：比如测试weave([1,2], [a,b], Res)，递归最终到weave([], [], [])，此时两个终止子句都能匹配，两次匹配都会生成相同的Res，因此会返回两次完全一样的绑定。

修正方案 #

要解决这个问题，需要让终止子句互斥，避免同时匹配的情况。可以把终止逻辑拆分为三种明确的、无重叠的情况：

% 两列表均为空时终止
weave([], [], []).
% 第一个列表非空、第二个为空时终止
weave([_|_], [], []).
% 第一个列表为空、第二个非空时终止
weave([], [_|_], []).

weave([H1|T1], [H2|T2], Res) :-
  weave(T1, T2, Ts),
  append([H1, H2], Ts, Res).

这样每个终止场景都唯一对应，不会出现重叠匹配，测试时就只会返回一次正确结果，不会有重复解或多余的回溯失败。

内容的提问来源于stack exchange，提问作者Avrohom Yisroel