是否可以声明升序列表？
Is it possible to declare an ascending list?
我可以像这样列出升序整数：
?- findall(L,between(1,5,L),List).
我知道我还可以使用以下方法生成值：
?- length(_,X).
但我不认为我可以在 findall 中使用它，就像下面的循环一样：
?- findall(X,(length(_,X),X<6),Xs).
我还可以使用 clpfd 生成列表。
:- use_module(library(clpfd)).
list_to_n(N,List) :-
length(List,N),
List ins 1..N,
all_different(List),
once(label(List)).
或
list_to_n2(N,List) :-
length(List,N),
List ins 1..N,
chain(List,#<),
label(List).
最后一种方法对我来说似乎最好，因为它是最具声明性的，并且不使用 once/1 或 between/3 或 findall/3 等
还有其他方法吗？在 'pure' Prolog 中是否有一种声明式的方式来做到这一点？有'best'方法吗？
"best" 方式取决于您的具体用例！这是使用 clpfd 的另一种方法：
:- use_module(library(clpfd)).
我们按照 @mat 在对 a previous answer of a related question 的评论中的建议定义谓词 equidistant_stride/2:
equidistant_stride([],_).
equidistant_stride([Z|Zs],D) :-
foldl(equidistant_stride_(D),Zs,Z,_).
equidistant_stride_(D,Z1,Z0,Z1) :-
Z1 #= Z0+D.
基于equidistant_stride/2，我们定义：
consecutive_ascending_integers(Zs) :-
equidistant_stride(Zs,1).
consecutive_ascending_integers_from(Zs,Z0) :-
Zs = [Z0|_],
consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
consecutive_ascending_integers_from(Zs,1).
让我们运行一些查询！首先，您的原始用例：
?- length(Zs,N), consecutive_ascending_integers_from_1(Zs).
N = 1, Zs = [1]
; N = 2, Zs = [1,2]
; N = 3, Zs = [1,2,3]
; N = 4, Zs = [1,2,3,4]
; N = 5, Zs = [1,2,3,4,5]
...
有了 clpfd，我们可以提出非常笼统的问题——并且也能得到合乎逻辑的答案！
?- consecutive_ascending_integers([A,B,0,D,E]).
A = -2, B = -1, D = 1, E = 2.
?- consecutive_ascending_integers([A,B,C,D,E]).
A+1#=B, B+1#=C, C+1#=D, D+1#=E.
equidistant_stride/2的替代实现：
我希望新代码能更好地利用约束传播。
感谢@WillNess 建议的测试用例促使了这次重写！
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,N,D) :-
Z #= Z0 + N*D,
N1 #= N+1,
equidistant_from_nth_stride(Zs,Z0,N1,D).
equidistant_stride([],_).
equidistant_stride([Z0|Zs],D) :-
equidistant_from_nth_stride(Zs,Z0,1,D).
新旧版本与@mat 的 clpfd 的比较：
首先，旧版本：
?- equidistant_stride([1,_,_,_,14],D).
_G1133+D#=14,
_G1145+D#=_G1133,
_G1157+D#=_G1145,
1+D#=_G1157. % succeeds with Scheinlösung
?- equidistant_stride([1,_,_,_,14|_],D).
_G1136+D#=14, _G1148+D#=_G1136, _G1160+D#=_G1148, 1+D#=_G1160
; 14+D#=_G1340, _G1354+D#=14, _G1366+D#=_G1354, _G1378+D#=_G1366, 1+D#=_G1378
... % does not terminate universally
现在让我们切换到新版本并提出相同的问题！
?- equidistant_stride([1,_,_,_,14],D).
false. % fails, as it should
?- equidistant_stride([1,_,_,_,14|_],D).
false. % fails, as it should
更多，现在，再一次！我们能否通过暂时采用冗余约束来更早地失败？
之前，我们建议使用约束 Z1 #= Z0+D*1, Z2 #= Z0+D*2, Z3 #= Z0+D*3 而不是 Z1 #= Z0+D, Z2 #= Z1+D, Z3 #= Z2+D
（此答案中的第一版代码就是这样做的）。
再次感谢@WillNess 通过
注意到目标 equidistant_stride([_,4,_,_,14],D) 并没有失败，而是成功了，但有未决的目标：
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D).
Zs = [_G2650, 4, _G2656, _G2659, 14],
14#=_G2650+4*D,
_G2659#=_G2650+3*D,
_G2656#=_G2650+2*D,
_G2650+D#=4.
让我们添加一些冗余约束 equidistantRED_stride/2:
equidistantRED_stride([],_).
equidistantRED_stride([Z|Zs],D) :-
equidistant_from_nth_stride(Zs,Z,1,D),
equidistantRED_stride(Zs,D).
示例查询：
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D), equidistantRED_stride(Zs,D).
false.
完成了吗？还没有！一般来说，我们不想要二次数的冗余约束。原因如下：
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D).
Zs = [_G2683, _G2686, _G2689, _G2692, 14],
14#=_G2683+4*D,
_G2692#=_G2683+3*D,
_G2689#=_G2683+2*D,
_G2686#=_G2683+D.
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D), equidistantRED_stride(Zs,D).
Zs = [_G831, _G834, _G837, _G840, 14],
14#=_G831+4*D,
_G840#=_G831+3*D,
_G837#=_G831+2*D,
_G834#=_G831+D,
14#=_G831+4*D,
_G840#=_G831+3*D,
_G837#=_G831+2*D,
_G834#=_G831+D,
D+_G840#=14,
14#=2*D+_G837,
_G840#=D+_G837,
14#=_G834+3*D,
_G840#=_G834+2*D,
_G837#=_G834+D.
但是如果我们使用双重否定技巧，在成功的情况下剩余部分仍然存在...
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
Zs = [_G454, _G457, _G460, _G463, 14],
14#=_G454+4*D,
_G463#=_G454+3*D,
_G460#=_G454+2*D,
_G457#=_G454+D.
...和...
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
false.
...我们发现故障的情况比以前多！
让我们更深入地挖掘一下！我们能否在更广泛的使用中尽早发现故障？
到目前为止给出的代码，这两个逻辑错误的查询不会终止：
?- Zs = [_,4,_,_,14|_], \+ \+ equidistantRED_stride(Zs,D), equidistant_stride(Zs,D).
... % Execution Aborted
?- Zs = [_,4,_,_,14|_], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
... % Execution Aborted
修好了吗？ 成功了！
?- use_module(library(lambda)).
true.
?- Zs = [_,4,_,_,14|_],
\+ ( term_variables(Zs,Vs),
maplist(\X^when(nonvar(X),integer(X)),Vs),
\+ equidistantRED_stride(Zs,D)),
equidistant_stride(Zs,D).
false.
黑客并不能保证冗余约束的终止"part"，但在我看来，这对于快速的第一枪来说还算不错。 Zs 中任何变量实例化时的测试 integer/1 旨在允许 clpfd 求解器将变量域约束为单例，而实例化与对（直接导致非基于列表的谓词的终止）被抑制。
我确实意识到可以通过不止一种方式（例如，使用循环项）很容易地破解黑客攻击。欢迎任何建议和意见！
我们将定义升序列表，这样至少包含两个递增整数的元素（非递减列表可以是空的，或者是单例的，但是"ascending" 是一个更明确的 属性)。这是一个有点武断的决定。
在 SWI Prolog 中：
ascending( [A,B|R] ):-
freeze(A,
freeze(B, (A < B, freeze(R, (R=[] -> true ; ascending([B|R])))) )).
为了轻松填满，我们可以使用
mselect([A|B],S,S2):- select(A,S,S1), mselect(B,S1,S2).
mselect([], S2, S2).
测试：
15 ?- ascending(LS),mselect(LS,[10,2,8,5],[]).
LS = [2, 5, 8, 10] ;
false.
16 ?- mselect(LS,[10,2,8,5],[]), ascending(LS).
LS = [2, 5, 8, 10] ;
false.
关于赏金问题，根据https://whosebug.com/tags/logical-purity/info，
Only monotonic (also called: "monotone") predicates are pure: If the predicate succeeds for any arguments, then it does not fail for any generalization of these arguments, and if it fails for any combination of arguments, then it does not succeed for any specialization of these arguments.
consecutive_ascending_integers_from_1([2|B]) 失败，所以它的专业化 consecutive_ascending_integers_from_1([2,3,5,8|non_list]) 也必须失败。
对于扩展赏金 ，额外的失败目标是：( 1 )
consecutive_ascending_integers_from_1([_,3|_])
求代码
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,I0,D) :-
Z #= Z0 + I0*D, % C1
*( I1 #= I0 + 1 ),
equidistant_from_nth_stride(Zs,Z0,I1,D).
其余不变，因为C1变为3 #= 1 + 1*1。此外，( 2 和 3 )
consecutive_ascending_integers_from_1([A,B,5|_])
consecutive_ascending_integers_from_1([A,B,C,8|_])
都失败了，代码不变，因为第一个定义了
A = 1, B #= 1 + 1*1, 5 #= 1 + 2*1
第二个定义
A = 1, B #= 1 + 1*1, C #= 1 + 2*1, 8 #= 1 + 3*1
另一种可能性（4）是
consecutive_ascending_integers_from_1([_,3,5|_])
与广义
consecutive_ascending_integers_from_1(Zs) :-
*( Z0 = 1 ),
consecutive_ascending_integers_from(Zs,Z0).
consecutive_ascending_integers_from(Zs,Z0) :-
*( Zs = [Z0|_] ),
consecutive_ascending_integers(Zs).
因为
26 ?- 3 #= Z + 1*1, 5 #= Z + 2*1.
false.
类似地，修改后的代码，目标（5）
consecutive_ascending_integers_from_1([_,3,_,8|_])
因为
27 ?- 3 #= Z + 1*1, 8 #= Z + 3*1.
false.
还有 ( 6 ... 9 )
consecutive_ascending_integers_from_1([2,3,_,8|_])
consecutive_ascending_integers_from_1([2,_,_,8|_])
consecutive_ascending_integers_from_1([2,_,5,8|_])
consecutive_ascending_integers_from_1([2,_,5|_])
出于同样的原因。另一种可能的代码概括是让 D 保持未初始化（原始代码的其余部分不变）：
consecutive_ascending_integers(Zs) :-
*( D = 1 ),
equidistant_stride(Zs,D).
因此目标 ( 5 ) ...[_,3,_,8|_]... 再次失败，因为
49 ?- 3 #= 1 + 1*D, 8 #= 1 + 3*D.
false.
但是，
50 ?- 3 #= 1 + 1*D, 5 #= 1 + 2*D.
D = 2.
所以 ...[_,3,5|_]... 会成功（确实如此）。 ( 10 )
consecutive_ascending_integers_from_1([_,_,5,8|_])
也因为同样的原因失败了。
可能还有更多组合，但总的要点变得更加清晰：这完全取决于此谓词创建的约束如何运作。
下面我们讨论中的代码。
目标 consecutive_ascending_integers_from_1([2,3,5,8|non_list]) 失败了，但为什么？
让我们一步步来：
这是我们开始的代码：
:- use_module(library(clpfd)).
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,I0,D) :-
Z #= Z0 + I0*D,
I1 #= I0 + 1,
equidistant_from_nth_stride(Zs,Z0,I1,D).
equidistant_stride([],_).
equidistant_stride([Z0|Zs],D) :-
equidistant_from_nth_stride(Zs,Z0,1,D).
consecutive_ascending_integers(Zs) :-
equidistant_stride(Zs,1).
consecutive_ascending_integers_from(Zs,Z0) :-
Zs = [Z0|_],
consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
consecutive_ascending_integers_from(Zs,1).
首先，我们使（某些）统一更加明确：
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,I0,D) :-
Z #= Z0 + I0*D,
I1 #= I0 + 1,
equidistant_from_nth_stride(Zs,Z0,I1,D).
equidistant_stride([],_).
equidistant_stride([Z0|Zs],D) :-
I = 1,
equidistant_from_nth_stride(Zs,Z0,I,D).
consecutive_ascending_integers(Zs) :-
D = 1,
equidistant_stride(Zs,D).
consecutive_ascending_integers_from(Zs,Z0) :-
Zs = [Z0|_],
consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
Z0 = 1,
consecutive_ascending_integers_from(Zs,Z0).
我们遵循方法和约定introduced in this fine answer:
By removing goals, we can generalize a program. Here is my favorite way to do it. By adding a predicate (*)/1 like so:
:- op(950,fy, *).
*_.
@WillNess 正确地指出：
consecutive_ascending_integers_from_1([2|_]) fails, so its specialization consecutive_ascending_integers_from_1([2,3,5,8|non_list]) must fail too.
如果最大限度地概括代码以致 consecutive_ascending_integers_from_1([2|_]) 失败，我们 "know for sure: something in the visible remaining part of the program has to be fixed."
consecutive_ascending_integers_from(Zs,Z0) :-
Zs = [Z0|_],
* consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
Start = 1,
consecutive_ascending_integers_from(Zs,Start).
让我们再另一个解释！
对于版本 #2（见上文），我们观察到以下通用目标也失败了：
?- consecutive_ascending_integers_from_1([_,_,_,_|non_list]).
false.
为什么 this 会失败？让我们最大限度地概括代码，使目标失败：
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,I0,D) :-
* Z #= Z0 + I0*D,
* I1 #= I0 + 1,
equidistant_from_nth_stride(Zs,Z0,I1,D).
equidistant_stride([],_).
equidistant_stride([Z0|Zs],D) :-
* I = 1,
equidistant_from_nth_stride(Zs,Z0,I,D).
consecutive_ascending_integers(Zs) :-
* D = 1,
equidistant_stride(Zs,D).
consecutive_ascending_integers_from(Zs,Z0) :-
* Zs = [Z0|_],
consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
* Start = 1,
consecutive_ascending_integers_from(Zs,Start).
为什么目标 consecutive_ascending_integers_from_1([2,3,5,8|non_list]) 失败了？
到目前为止，我们已经看到了两种解释，但可能还有更多...
真相大白：加入狩猎！
我可以像这样列出升序整数：
?- findall(L,between(1,5,L),List).
我知道我还可以使用以下方法生成值：
?- length(_,X).
但我不认为我可以在 findall 中使用它，就像下面的循环一样：
?- findall(X,(length(_,X),X<6),Xs).
我还可以使用 clpfd 生成列表。
:- use_module(library(clpfd)).
list_to_n(N,List) :-
length(List,N),
List ins 1..N,
all_different(List),
once(label(List)).
或
list_to_n2(N,List) :-
length(List,N),
List ins 1..N,
chain(List,#<),
label(List).
最后一种方法对我来说似乎最好，因为它是最具声明性的，并且不使用 once/1 或 between/3 或 findall/3 等
还有其他方法吗？在 'pure' Prolog 中是否有一种声明式的方式来做到这一点？有'best'方法吗？
"best" 方式取决于您的具体用例！这是使用 clpfd 的另一种方法：
:- use_module(library(clpfd)).
我们按照 @mat 在对 a previous answer of a related question 的评论中的建议定义谓词 equidistant_stride/2:
equidistant_stride([],_).
equidistant_stride([Z|Zs],D) :-
foldl(equidistant_stride_(D),Zs,Z,_).
equidistant_stride_(D,Z1,Z0,Z1) :-
Z1 #= Z0+D.
基于equidistant_stride/2，我们定义：
consecutive_ascending_integers(Zs) :-
equidistant_stride(Zs,1).
consecutive_ascending_integers_from(Zs,Z0) :-
Zs = [Z0|_],
consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
consecutive_ascending_integers_from(Zs,1).
让我们运行一些查询！首先，您的原始用例：
?- length(Zs,N), consecutive_ascending_integers_from_1(Zs).
N = 1, Zs = [1]
; N = 2, Zs = [1,2]
; N = 3, Zs = [1,2,3]
; N = 4, Zs = [1,2,3,4]
; N = 5, Zs = [1,2,3,4,5]
...
有了 clpfd，我们可以提出非常笼统的问题——并且也能得到合乎逻辑的答案！
?- consecutive_ascending_integers([A,B,0,D,E]). A = -2, B = -1, D = 1, E = 2. ?- consecutive_ascending_integers([A,B,C,D,E]). A+1#=B, B+1#=C, C+1#=D, D+1#=E.
equidistant_stride/2的替代实现：
我希望新代码能更好地利用约束传播。
感谢@WillNess 建议的测试用例促使了这次重写！
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,N,D) :-
Z #= Z0 + N*D,
N1 #= N+1,
equidistant_from_nth_stride(Zs,Z0,N1,D).
equidistant_stride([],_).
equidistant_stride([Z0|Zs],D) :-
equidistant_from_nth_stride(Zs,Z0,1,D).
新旧版本与@mat 的 clpfd 的比较：
首先，旧版本：
?- equidistant_stride([1,_,_,_,14],D).
_G1133+D#=14,
_G1145+D#=_G1133,
_G1157+D#=_G1145,
1+D#=_G1157. % succeeds with Scheinlösung
?- equidistant_stride([1,_,_,_,14|_],D).
_G1136+D#=14, _G1148+D#=_G1136, _G1160+D#=_G1148, 1+D#=_G1160
; 14+D#=_G1340, _G1354+D#=14, _G1366+D#=_G1354, _G1378+D#=_G1366, 1+D#=_G1378
... % does not terminate universally
现在让我们切换到新版本并提出相同的问题！
?- equidistant_stride([1,_,_,_,14],D). false. % fails, as it should ?- equidistant_stride([1,_,_,_,14|_],D). false. % fails, as it should
更多，现在，再一次！我们能否通过暂时采用冗余约束来更早地失败？
之前，我们建议使用约束 Z1 #= Z0+D*1, Z2 #= Z0+D*2, Z3 #= Z0+D*3 而不是 Z1 #= Z0+D, Z2 #= Z1+D, Z3 #= Z2+D
（此答案中的第一版代码就是这样做的）。
再次感谢@WillNess 通过
注意到目标 equidistant_stride([_,4,_,_,14],D) 并没有失败，而是成功了，但有未决的目标：
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D).
Zs = [_G2650, 4, _G2656, _G2659, 14],
14#=_G2650+4*D,
_G2659#=_G2650+3*D,
_G2656#=_G2650+2*D,
_G2650+D#=4.
让我们添加一些冗余约束 equidistantRED_stride/2:
equidistantRED_stride([],_).
equidistantRED_stride([Z|Zs],D) :-
equidistant_from_nth_stride(Zs,Z,1,D),
equidistantRED_stride(Zs,D).
示例查询：
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D), equidistantRED_stride(Zs,D).
false.
完成了吗？还没有！一般来说，我们不想要二次数的冗余约束。原因如下：
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D).
Zs = [_G2683, _G2686, _G2689, _G2692, 14],
14#=_G2683+4*D,
_G2692#=_G2683+3*D,
_G2689#=_G2683+2*D,
_G2686#=_G2683+D.
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D), equidistantRED_stride(Zs,D).
Zs = [_G831, _G834, _G837, _G840, 14],
14#=_G831+4*D,
_G840#=_G831+3*D,
_G837#=_G831+2*D,
_G834#=_G831+D,
14#=_G831+4*D,
_G840#=_G831+3*D,
_G837#=_G831+2*D,
_G834#=_G831+D,
D+_G840#=14,
14#=2*D+_G837,
_G840#=D+_G837,
14#=_G834+3*D,
_G840#=_G834+2*D,
_G837#=_G834+D.
但是如果我们使用双重否定技巧，在成功的情况下剩余部分仍然存在...
?- Zs = [_,_,_,_,14], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D).
Zs = [_G454, _G457, _G460, _G463, 14],
14#=_G454+4*D,
_G463#=_G454+3*D,
_G460#=_G454+2*D,
_G457#=_G454+D.
...和...
?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D). false.
...我们发现故障的情况比以前多！
让我们更深入地挖掘一下！我们能否在更广泛的使用中尽早发现故障？
到目前为止给出的代码，这两个逻辑错误的查询不会终止：
?- Zs = [_,4,_,_,14|_], \+ \+ equidistantRED_stride(Zs,D), equidistant_stride(Zs,D). ... % Execution Aborted ?- Zs = [_,4,_,_,14|_], equidistant_stride(Zs,D), \+ \+ equidistantRED_stride(Zs,D). ... % Execution Aborted
修好了吗？ 成功了！
?- use_module(library(lambda)).
true.
?- Zs = [_,4,_,_,14|_],
\+ ( term_variables(Zs,Vs),
maplist(\X^when(nonvar(X),integer(X)),Vs),
\+ equidistantRED_stride(Zs,D)),
equidistant_stride(Zs,D).
false.
黑客并不能保证冗余约束的终止"part"，但在我看来，这对于快速的第一枪来说还算不错。 Zs 中任何变量实例化时的测试 integer/1 旨在允许 clpfd 求解器将变量域约束为单例，而实例化与对（直接导致非基于列表的谓词的终止）被抑制。
我确实意识到可以通过不止一种方式（例如，使用循环项）很容易地破解黑客攻击。欢迎任何建议和意见！
我们将定义升序列表，这样至少包含两个递增整数的元素（非递减列表可以是空的，或者是单例的，但是"ascending" 是一个更明确的 属性)。这是一个有点武断的决定。
在 SWI Prolog 中：
ascending( [A,B|R] ):-
freeze(A,
freeze(B, (A < B, freeze(R, (R=[] -> true ; ascending([B|R])))) )).
为了轻松填满，我们可以使用
mselect([A|B],S,S2):- select(A,S,S1), mselect(B,S1,S2).
mselect([], S2, S2).
测试：
15 ?- ascending(LS),mselect(LS,[10,2,8,5],[]).
LS = [2, 5, 8, 10] ;
false.
16 ?- mselect(LS,[10,2,8,5],[]), ascending(LS).
LS = [2, 5, 8, 10] ;
false.
关于赏金问题，根据https://whosebug.com/tags/logical-purity/info，
Only monotonic (also called: "monotone") predicates are pure: If the predicate succeeds for any arguments, then it does not fail for any generalization of these arguments, and if it fails for any combination of arguments, then it does not succeed for any specialization of these arguments.
consecutive_ascending_integers_from_1([2|B]) 失败，所以它的专业化 consecutive_ascending_integers_from_1([2,3,5,8|non_list]) 也必须失败。
对于扩展赏金
consecutive_ascending_integers_from_1([_,3|_])
求代码
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,I0,D) :-
Z #= Z0 + I0*D, % C1
*( I1 #= I0 + 1 ),
equidistant_from_nth_stride(Zs,Z0,I1,D).
其余不变，因为C1变为3 #= 1 + 1*1。此外，( 2 和 3 )
consecutive_ascending_integers_from_1([A,B,5|_])
consecutive_ascending_integers_from_1([A,B,C,8|_])
都失败了，代码不变，因为第一个定义了
A = 1, B #= 1 + 1*1, 5 #= 1 + 2*1
第二个定义
A = 1, B #= 1 + 1*1, C #= 1 + 2*1, 8 #= 1 + 3*1
另一种可能性（4）是
consecutive_ascending_integers_from_1([_,3,5|_])
与广义
consecutive_ascending_integers_from_1(Zs) :-
*( Z0 = 1 ),
consecutive_ascending_integers_from(Zs,Z0).
consecutive_ascending_integers_from(Zs,Z0) :-
*( Zs = [Z0|_] ),
consecutive_ascending_integers(Zs).
因为
26 ?- 3 #= Z + 1*1, 5 #= Z + 2*1.
false.
类似地，修改后的代码，目标（5）
consecutive_ascending_integers_from_1([_,3,_,8|_])
因为
27 ?- 3 #= Z + 1*1, 8 #= Z + 3*1.
false.
还有 ( 6 ... 9 )
consecutive_ascending_integers_from_1([2,3,_,8|_])
consecutive_ascending_integers_from_1([2,_,_,8|_])
consecutive_ascending_integers_from_1([2,_,5,8|_])
consecutive_ascending_integers_from_1([2,_,5|_])
出于同样的原因。另一种可能的代码概括是让 D 保持未初始化（原始代码的其余部分不变）：
consecutive_ascending_integers(Zs) :-
*( D = 1 ),
equidistant_stride(Zs,D).
因此目标 ( 5 ) ...[_,3,_,8|_]... 再次失败，因为
49 ?- 3 #= 1 + 1*D, 8 #= 1 + 3*D.
false.
但是，
50 ?- 3 #= 1 + 1*D, 5 #= 1 + 2*D.
D = 2.
所以 ...[_,3,5|_]... 会成功（确实如此）。 ( 10 )
consecutive_ascending_integers_from_1([_,_,5,8|_])
也因为同样的原因失败了。
可能还有更多组合，但总的要点变得更加清晰：这完全取决于此谓词创建的约束如何运作。
下面我们讨论
目标 consecutive_ascending_integers_from_1([2,3,5,8|non_list]) 失败了，但为什么？
让我们一步步来：
这是我们开始的代码：
:- use_module(library(clpfd)). equidistant_from_nth_stride([],_,_,_). equidistant_from_nth_stride([Z|Zs],Z0,I0,D) :- Z #= Z0 + I0*D, I1 #= I0 + 1, equidistant_from_nth_stride(Zs,Z0,I1,D). equidistant_stride([],_). equidistant_stride([Z0|Zs],D) :- equidistant_from_nth_stride(Zs,Z0,1,D). consecutive_ascending_integers(Zs) :- equidistant_stride(Zs,1). consecutive_ascending_integers_from(Zs,Z0) :- Zs = [Z0|_], consecutive_ascending_integers(Zs). consecutive_ascending_integers_from_1(Zs) :- consecutive_ascending_integers_from(Zs,1).
首先，我们使（某些）统一更加明确：
equidistant_from_nth_stride([],_,_,_). equidistant_from_nth_stride([Z|Zs],Z0,I0,D) :- Z #= Z0 + I0*D, I1 #= I0 + 1, equidistant_from_nth_stride(Zs,Z0,I1,D). equidistant_stride([],_). equidistant_stride([Z0|Zs],D) :- I = 1, equidistant_from_nth_stride(Zs,Z0,I,D). consecutive_ascending_integers(Zs) :- D = 1, equidistant_stride(Zs,D). consecutive_ascending_integers_from(Zs,Z0) :- Zs = [Z0|_], consecutive_ascending_integers(Zs). consecutive_ascending_integers_from_1(Zs) :- Z0 = 1, consecutive_ascending_integers_from(Zs,Z0).
我们遵循方法和约定introduced in this fine answer:
By removing goals, we can generalize a program. Here is my favorite way to do it. By adding a predicate
(*)/1like so::- op(950,fy, *). *_.
@WillNess 正确地指出：
consecutive_ascending_integers_from_1([2|_])fails, so its specializationconsecutive_ascending_integers_from_1([2,3,5,8|non_list])must fail too.如果最大限度地概括代码以致
consecutive_ascending_integers_from_1([2|_])失败，我们 "know for sure: something in the visible remaining part of the program has to be fixed."
consecutive_ascending_integers_from(Zs,Z0) :-
Zs = [Z0|_],
* consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
Start = 1,
consecutive_ascending_integers_from(Zs,Start).
让我们再另一个解释！
对于版本 #2（见上文），我们观察到以下通用目标也失败了：
?- consecutive_ascending_integers_from_1([_,_,_,_|non_list]). false.
为什么 this 会失败？让我们最大限度地概括代码，使目标失败：
equidistant_from_nth_stride([],_,_,_).
equidistant_from_nth_stride([Z|Zs],Z0,I0,D) :-
* Z #= Z0 + I0*D,
* I1 #= I0 + 1,
equidistant_from_nth_stride(Zs,Z0,I1,D).
equidistant_stride([],_).
equidistant_stride([Z0|Zs],D) :-
* I = 1,
equidistant_from_nth_stride(Zs,Z0,I,D).
consecutive_ascending_integers(Zs) :-
* D = 1,
equidistant_stride(Zs,D).
consecutive_ascending_integers_from(Zs,Z0) :-
* Zs = [Z0|_],
consecutive_ascending_integers(Zs).
consecutive_ascending_integers_from_1(Zs) :-
* Start = 1,
consecutive_ascending_integers_from(Zs,Start).
为什么目标 consecutive_ascending_integers_from_1([2,3,5,8|non_list]) 失败了？
到目前为止，我们已经看到了两种解释，但可能还有更多...
真相大白：加入狩猎！