可以声明一个升序列表吗?

The "best" way depends on your concrete use cases! Here's another way to do it using clpfd::- use_module(library(clpfd)).我们定义@@ mat在对相关问题的先前答案的注释中建议的谓词equidistant_stride/2:We define predicate equidistant_stride/2 as suggested by @mat in a comment to a previous answer of a related question: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).让我们运行一些查询！首先，您的原始用例:Let's run some queries! First, your original use case:?- 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 ，我们可以问得一般查询-并在逻辑上也得到合理的答案！With clpfd, we can ask quite general queries—and get logically sound answers, too!?- 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的另一种实现:An alternative implementation of equidistant_stride/2:我希望新代码能更好地利用约束传播.I hope the new code makes better use of constraint propagation.感谢@WillNess提出了促使这种重写的测试用例！Thanks to @WillNess for suggesting the test-cases that motivated this rewrite!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比较旧版本与新版本:Comparison of old vs new version with @mat's 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现在让我们切换到新版本并询问相同的查询！Now let's switch to the new version and ask the same queries!?- equidistant_stride([1,_,_,_,14],D).false. % fails, as it should?- equidistant_stride([1,_,_,_,14|_],D).false. % fails, as it should 现在再说一次！我们可以通过暂时采用冗余约束来使我们更早失败吗?More, now, again! Can we fail earlier by tentatively employing redundant constraints?以前，我们建议使用约束Z1 #= Z0+D*1, Z2 #= Z0+D*2, Z3 #= Z0+D*3代替Z1 #= Z0+D, Z2 #= Z1+D, Z3 #= Z2+D(此答案的第一个版本的代码就是这样做的.)Previously, we proposed using constraints Z1 #= Z0+D*1, Z2 #= Z0+D*2, Z3 #= Z0+D*3 instead of Z1 #= Z0+D, Z2 #= Z1+D, Z3 #= Z2+D(which the 1st version of code in this answer did).再次，感谢@WillNess激励了这个小实验，注意到目标equidistant_stride([_,4,_,_,14],D)不会失败，而是会通过未完成的目标而成功:Again, thanks to @WillNess for motivating this little experiment bynoting that the goal equidistant_stride([_,4,_,_,14],D) does not fail but instead succeeds with pending goals:?- 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添加一些冗余约束:Let's add some redundant constraints with 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.完成了吗?还没有！通常，我们不需要二次数量的冗余约束.原因如下:Done? Not yet! In general we don't want a quadratic number of redundant constraints. Here's why:?- 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.但是，如果我们使用双重否定技巧，则在成功的情况下，残留物仍会保留...But if we use the double-negation trick, the residuum remains in cases that succeed ...?- 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. ...与以前相比，我们发现失败的情况更多！... we detect failure in more cases than we did before! 让我们深入研究吧！我们可以在更广泛的用途中及早发现故障吗?Let's dig a little deeper! Can we detect failure early in even more generalized uses?到目前为止，在提供代码的情况下，这两个逻辑错误的查询不会终止:With code presented so far, these two logically false queries do not terminate:?- 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. hack不能保证冗余约束"part"的终止，但是IMO对于快速的第一枪来说还算不错.对Zs中的任何变量进行实例化后的测试integer/1旨在允许 clpfd 求解器将变量域约束为单例，而抑制了使用cons对的实例化(直接导致基于列表的谓词的非终止).The hack doesn't guarantee termination of the redundant constraint "part", but IMO it's not too bad for a quick first shot. The test integer/1 upon instantiation of any variable in Zs is meant to allow the clpfd solver to constrain variable domains to singletons, while the instantiation with cons-pairs (which directly leads to non-termination of list-based predicates) is suppressed.我做意识到可以很容易地以多种方式(例如，使用循环术语)破解该hack.欢迎任何建议和评论！I do realize that the hack can be broken quite easily in more than one way (e.g., using cyclic terms). Any suggestions and comments are welcome! 这篇关于可以声明一个升序列表吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！ 上岸，阿里云！