我可以像这样创建升序整数列表:
?- 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中是否有声明性的方法来做到这一点?有没有"最好"的方法?
"最佳"方式取决于您的具体用例!下面是使用clpfd:
的另一种方法:- use_module(library(clpfd)).
我们定义谓词equidistant_stride/2，正如@mat在前面一个相关问题的回答的注释中所建议的那样:
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)。假。%失败，正如它应该的那样? - equidistant_stride ([1 _ _ _ 14 | _), D)。假。%失败，正如它应该的那样之前更多，现在，再来!我们可以通过试探性地使用冗余约束来提前失败吗?
之前，我们建议使用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.
…和…
<>之前? - z =[4 _, _、_、14],equidistant_stride (z D) + + equidistantRED_stride (z D)。假。之前…我们在比以前更多的情况下检测到失败!
让我们再深入一点!我们能在更广泛的使用中及早发现故障吗?
使用目前提供的代码，这两个逻辑错误的查询不会终止:
<>之前? - z =[4 _, _, _, 14所示 |_], + + equidistantRED_stride (z D), equidistant_stride (z D)。…% 执行中止? - z =[14 | _ 4 _、_、_],equidistant_stride (z D) + + equidistantRED_stride (z D)。…% 执行中止之前有解决吗?有黑客!
<>之前? - use_module(图书馆(λ))。真实的。?- Zs = [_，4，_，_，14]，+ (term_variables(Zs, v)，maplist ( X ^当(nonvar (X)整数(X)), Vs), + equidistantRED_stride (z D)),equidistant_stride (z D)。假。之前黑客不能保证终止冗余约束"部分"，但在我看来，这对于快速的第一次射击来说并不是太糟糕。Zs中任何变量实例化后的测试integer/1意味着允许clpfd求解器将变量域约束为单例，而使用cons-pair的实例化(直接导致基于列表的谓词不终止)将被抑制。
我确实意识到黑客可以很容易地通过多种方式(例如，使用循环项)被破解。欢迎提出任何建议和评论!
下面我们讨论上一个答案中提供的代码。
目标consecutive_ascending_integers_from_1([2,3,5,8|non_list])失败了，但为什么?
让我们一步一步地进行:
-
我们开始的代码是:
<>之前: - use_module(图书馆(clpfd))。equidistant_from_nth_stride ([],_,_,_).Z0 equidistant_from_nth_stride ([Z | Z],钱数,D): -z# = z0 + i0 * d，I1 #= i0 + 1equidistant_from_nth_stride (z, Z0 I1, D)。_ equidistant_stride([])。equidistant_stride ([Z0 | z), D): -equidistant_from_nth_stride (z, Z0 1 D)。consecutive_ascending_integers (z): -equidistant_stride (z, 1)。Z0 consecutive_ascending_integers_from (z): -Zs = [Z0|_]，consecutive_ascending_integers (z)。consecutive_ascending_integers_from_1 (z): -consecutive_ascending_integers_from (z, 1)。 -
首先，我们使(一些)统一更明确:
<>之前equidistant_from_nth_stride ([],_,_,_).Z0 equidistant_from_nth_stride ([Z | Z],钱数,D): -z# = z0 + i0 * d，I1 #= i0 + 1equidistant_from_nth_stride (z, Z0 I1, D)。_ equidistant_stride([])。equidistant_stride ([Z0 | z), D): -I = 1，equidistant_from_nth_stride (z, Z0 , D)。consecutive_ascending_integers (z): -D = 1，equidistant_stride (z D )。Z0 consecutive_ascending_integers_from (z): -Zs = [Z0|_]，consecutive_ascending_integers (z)。consecutive_ascending_integers_from_1 (z): -Z0 = 1，consecutive_ascending_integers_from (z Z0 )。 -
我们遵循这个好答案中介绍的方法和约定:
<>之前:- op(950,fy， *)。* _。通过去掉目标，我们可以泛化程序。这是我最喜欢的方法。通过像这样添加谓词
(*)/1: -
@WillNess正确地指出:
consecutive_ascending_integers_from_1([2|_])失败了，所以它的专门化consecutive_ascending_integers_from_1([2,3,5,8|non_list])也必须失败。如果最大限度地泛化代码使
consecutive_ascending_integers_from_1([2|_])失败，我们"可以肯定地知道:程序中可见的剩余部分中的某些东西必须被修复。"
让我们给另一个解释!
对于版本#2(见上文)，我们观察到以下一般化目标也失败了: <>之前? - consecutive_ascending_integers_from_1 ([_,_,_,_| non_list])。假的。之前为什么这个失败?让我们最大限度地泛化代码，使目标失败:
为什么目标consecutive_ascending_integers_from_1([2,3,5,8|non_list])失败?
到目前为止，我们已经看到了两种解释，但可能还有更多……
真相就在那里:加入搜寻!
我们将升序列表定义为包含至少两个递增整数元素的列表(非递减列表可以是空的，也可以是单元素的，但"升序"是一个更明确的属性)。这是一个有点武断的决定。
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 ? -提升(LS)、mselect (LS,[10、2、8、5],[])。
LS = [2,5,8,10] ;
假的。
16 ?- mselect(LS，[10,2,8,5]，[])，升序(LS)。
LS = [2,5,8,10] ;
假的。
关于赏金问题，根据https://stackoverflow.com/tags/logical-purity/info，
只有单调(也称为"单调")谓词是纯谓词:如果谓词对任何参数成功，则对这些参数的泛化不会失败;如果对任何参数的组合失败，则对这些参数的专门化不会成功。
consecutive_ascending_integers_from_1([2|B])失败了，所以它的专门化consecutive_ascending_integers_from_1([2,3,5,8|non_list])也必须失败。
对于扩展赏金" 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|_])
也失败了。
可能还有更多的组合，但它的一般要点变得更加清晰:这一切都取决于该谓词创建的约束如何操作。