list - 是否可以声明一个升序列表？

Question

我可以像这样制作升序整数列表:

?- 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等等。

还有其他方法可以做到这一点吗？在“纯” Prolog 中是否有声明式方法可以做到这一点？有“最好”的方法吗？

Answer 1

“最佳”方式取决于您的具体用例!这是使用 clpfd 的另一种方法:

:- use_module(library(clpfd)).

我们定义谓词 equidistant_stride/2正如@mat 在对 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).

让我们运行一些查询!首先，您的原始用例:

?- 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.

---

An alternative implementation of equidistant_stride/2:

I hope the new code makes better use of constraint propagation.

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 的比较:

首先是旧版本:

?- 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

---

More, now, again! Can we fail earlier by tentatively employing redundant constraints?

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).

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 添加一些冗余约束:

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)。
错误的。

...我们检测到的失败情况比以前更多!

让我们再深入一点! 我们能否在更广泛的用途中及早发现故障？

使用到目前为止提供的代码，这两个逻辑错误的查询不会终止:

?- Zs = [_,4,_,_,14|_],\+\+ equidistantRED_stride(Zs,D), equidistant_stride(Zs,D)。
... % 执行中止

?- Zs = [_,4,_,_,14|_], equidistant_stride(Zs,D),\+\+ equidistantRED_stride(Zs,D)。
... % 执行中止

修好了吗？被黑了!

?- use_module(library(lambda))。
真的。

?- Zs = [_,4,_,_,14|_],
\+ ( term_variables(Zs,Vs),
maplist(\X^when(nonvar(X),integer(X)),Vs),
\+ 等距RED_stride(Zs,D)),
equidistant_stride(Zs,D)。
错误的。

hack 不保证冗余约束“部分”的终止，但 IMO 对于快速的第一次射击来说还不错。测试 integer/1在 Zs 中实例化任何变量时旨在允许 clpfd求解器将变量域限制为单例，而使用 cons-pairs 的实例化(直接导致基于列表的谓词的非终止)被抑制。

我确实意识到可以通过不止一种方式(例如，使用循环项)很容易地破解黑客攻击。欢迎任何建议和意见!