我不理解你的谓词名称。无论如何，它都是一个干扰因素。变量的非统一命名也是一个干扰因素。让我们使用一些中性、简短的单音节名称，以便聚焦于代码本身的最清晰形式。
foo( H, [H | T], T). % 1st clause
foo( X, [H | T], [H | R]) :- foo( X, T, R). % 2nd clause
所以这是内置的
select/3。
耶！...
现在你问关于查询
foo(2，[1,2,3]，R)，
R 如何正确设置其值。 你概述中主要缺少的是当选择匹配子句时变量的重命名。查询的
解析 过程如下：
|- foo( 2, [1,2,3], R) ? { }
|- ? { foo( H1, [H1|T1], T1) = foo( 2, [1,2,3], R) }
**FAIL** (2 = 1)
**BACKTRACK to the last SELECT**
|- foo( X1, T1, R1) ?
{ foo( X1, [H1|T1], [H1|R1]) = foo( 2, [1,2,3], R) }
**OK**
|- foo( X1, T1, R1) ?
{ X1=2, [H1|T1]=[1,2,3], [H1|R1]=R }
|- foo( 2, [2,3], R1) ? { R=[1|R1] }
|- ? { foo( H2, [H2|T2], T2) = foo( 2, [2,3], R1), R=[1|R1] }
** OK **
|- ? { H2=2, T2=[3], T2=R1, R=[1|R1] }
|- ? { R=[1,3] }
在符号“|-”和“?”之间的目标是“解”，花括号内的方程式是“替换”。知识库(KB)完全隐含在符号“|-”的左侧。
在每一步中，选择解中最左边的目标，在KB中选择一个具有匹配头部的子句
(同时以一致的方式重命名子句中的所有变量，以使解中的任何变量都不被重命名的子句使用，从而避免意外的变量捕获)，并用该子句的主体替换所选目标，同时将成功的统一添加到替换中。当解为空时，查询已被证明，我们看到的是整个
and-or tree中的一个成功的“and”分支。
这是机器可能会做的方式。这里介绍“重写”步骤以方便人类理解。
因此，我们可以看到第一个成功的子句选择导致了方程式。
R = [1 | R1 ]
"
"，第一个标签，-- "
"
R1 = [3]
"
"，它们共同包含 "
"。
R = [1, 3]
这种逐步自上而下的实例化/列表详细说明是Prolog的一种典型方式。
针对赏金挑战，关于关系
foo/3（即
select/3）中的函数依赖：在
foo(A,B,C)中，任何两个确定的
B和
C值唯一地确定了
A的值（或者A不存在）。
2 ?- foo( A, [0,1,2,1,3], [0,2,1,3]).
A = 1 ;
false.
3 ?- foo( A, [0,1,2,1,3], [0,1,2,3]).
A = 1 ;
false.
4 ?- foo( A, [0,1,2,1,3], [0,1,2,4]).
false.
f ?- foo( A, [0,1,1], [0,1]).
A = 1 ;
A = 1 ;
false.
尝试通过反驳来证明其错误：
10 ?- dif(A1,A2), foo(A1,B,C), foo(A2,B,C).
Action (h for help) ? abort
Prolog无法找到反驳的论据。
尝试通过迭代加深来更仔细地观察正在发生的事情：
28 ?- length(BB,NN), foo(AA,BB,CC), XX=[AA,BB,CC], numbervars(XX),
writeln(XX), (NN>3, !, fail).
[A,[A],[]]
[A,[A,B],[B]]
[A,[B,A],[B]]
[A,[A,B,C],[B,C]]
[A,[B,A,C],[B,C]]
[A,[B,C,A],[B,C]]
[A,[A,B,C,D],[B,C,D]]
false.
29 ?- length(BB,NN), foo(AA,BB,CC), foo(AA2,BB,CC),
XX=[AA,AA2,BB,CC], numbervars(XX), writeln(XX), (NN>3, !, fail).
[A,A,[A],[]]
[A,A,[A,B],[B]]
[A,A,[A,A],[A]]
[A,A,[A,A],[A]]
[A,A,[B,A],[B]]
[A,A,[A,B,C],[B,C]]
[A,A,[A,A,B],[A,B]]
[A,A,[A,A,A],[A,A]]
[A,A,[A,A,B],[A,B]]
[A,A,[B,A,C],[B,C]]
[A,A,[B,A,A],[B,A]]
[A,A,[A,A,A],[A,A]]
[A,A,[B,A,A],[B,A]]
[A,A,[B,C,A],[B,C]]
[A,A,[A,B,C,D],[B,C,D]]
false.
"
AA和AA2总是被实例化为相同的变量。
数字3没有特殊之处，因此可以通过概括推断出，无论尝试的长度如何，它们始终如一。
"
另一种适用于Prolog的证明尝试：
ground_list(LEN,L):-
findall(N, between(1,LEN,N), NS),
member(N,NS),
length(L,N),
maplist( \A^member(A,NS), L).
bcs(N, BCS):-
bagof(B-C, A^(ground_list(N,B),ground_list(N,C),foo(A,B,C)), BCS).
as(N, AS):-
bagof(A, B^C^(ground_list(N,B),ground_list(N,C),foo(A,B,C)), AS).
proof(N):-
as(N,AS), bcs(N,BCS),
length(AS,N1), length(BCS, N2), N1 =:= N2.
这段话的意思是比较成功的B-C组合总数与它们所产生的A的数量。如果相等，则表示一对一的对应关系。
因此我们有：
2 ?- proof(2).
true.
3 ?- proof(3).
true.
4 ?- proof(4).
true.
5 ?- proof(5).
true.
因此，对于任何的
N，它都成立。速度越来越慢。编写一个通用的、无限制的查询很容易，但是速度下降似乎是指数级的。
Xs如何与R统一呢？更重要的是，R如何获得结果的值？ - Guy CoderR中返回？它不会这样做。答案返回到第三个位置，即Xs。当Xs与一个值统一时，第三个位置即为Xs将保存结果。当它与调用谓词统一时，未绑定的第三个位置将与Xs的值统一。也许这个答案可以帮助你。 - Guy CoderR的结果是如何正确的，因为如果您查看我的程序运行，Xs的值不是最终输出的[1,3]，而是[3]，它与R相统一（显然我在某个地方遗漏了什么，但我不确定是什么）。 - user9467747