listsum(L, S) 成功当且仅当 L 是必须从 1 开始的连续整数列表，并且 S 是该列表的总和

Question

我正在为即将到来的序言考试而学习，一个我无法弄清楚的练习需要我编写以下谓词：

listsum(L, S) 成功当且仅当 L 是必须从 1 开始的连续整数列表，并且 S 是该列表的总和。

重要的是，当给定 S 时，它能够生成列表。允许使用 numlist/3、is/2 和数学运算符。

例如：

?- listsum(L, 6).
   L = [1,2,3]
;  false.
?- listsum(L, 7).
false.
?- listsum([2,3], 5).
false.
?- listsum([2,4], 6).
false.

你会如何写这个谓词？

编辑：非常感谢大家！

Answer 1

如果允许使用库 clpfd，另一个可能的解决方案如下：

:- use_module(library(clpfd)).

listsum(List, Sum) :-
    dif(List, []),
    listsum(Sum, 1, List).

listsum(0, _, []).
listsum(S, X, [X|Xs]) :-
    S #> 0,
    S1 #= S - X,
    X1 #= X + 1,
    listsum(S1, X1, Xs).

一些示例：

?- listsum(L, S).
L = [1],
S = 1 ;
L = [1, 2],
S = 3 ;
L = [1, 2, 3],
S = 6 ;
L = [1, 2, 3, 4],
S = 10 ;
...

?- listsum([1, 2, 3, 4], S).
S = 10 ;
false.

?- listsum(L, 10).
L = [1, 2, 3, 4] ;
false.

?- listsum([1, 2, 3, 4], 10).
true ;
false.

?- listsum([1, 2, 3, 4], 11).
false.

Answer 2

由于前 n 个自然数的总和< /a> 是 s = n(n+1) / 2 我们可以使用有趣的内置 length/2，并编写

listsum_len(L,S) :-
    L=[1|_],
    length(L,N),
    successors(L),
    S is N*(N+1)/2.

successors([_]).
successors([I,J|Ns]) :-
    J is I+1,
    successors([J|Ns]).

涵盖大多数要求的关系：

?- listsum_len([1,2,3],S).
S = 6 ;
false.

?- listsum_len(L,6).
L = [1, 2, 3] .

?- listsum_len(L,S).
L = [1],
S = 1 ;
L = [1, 2],
S = 3 ;

当然是问题是在某些情况下，当通过 length/2 生成列表时，它不会终止。
这会在回溯时发生，例如因为我们明确要求它，或者因为我们导致 length/2 之后的某些调用失败，可能传递了错误的总和。

?- listsum_len(L,3).
L = [1, 2] ;
Action (h for help) ? abort
% Execution Aborted
?- listsum_len(L,2).
Action (h for help) ? abort
% Execution Aborted
?- 

解决这个问题并不容易，但是在需要的地方进行实例化检查，我们得到了正确的解决方案：

listsum([1|L],S) :-
    listsum([1|L],0,S).

listsum([Z],A,S) :-
    S is A+Z.
listsum([I,J|Ns],A,S) :-
    J is I+1,
    B is A+I,
    ( var(S), ! ; B < S ),
    listsum([J|Ns],B,S).

Answer 3

假设您可以使用 numlist/3 和数学运算符，并假设您不能使用 clp(FD) ，那么您可以将问题一分为二，一个用于基本总和，另一个用于计算总和计算总和：

listsum(L, S):-
 integer(S),   % ground sum
 End is (-1 + sqrt(1+8*S))/2, % compute ending number
 IEnd is integer(End),
 IEnd =:= End, % checking the sum is an actual valid ending integer
 numlist(1, IEnd, L).
listsum(L, S):-
  var(S),
  numlist2(L, 1, 1, S).
  

numlist2([Cur], Cur, S, S).
numlist2([Cur|L], Cur, CurS, S):-
  Cur1 is Cur + 1,
  CurS1 is CurS + Cur1,
  numlist2(L, Cur1, CurS1, S).

Answer 4

虽然不优雅，但如果提供了 nonvar 参数，这将生成并明智地终止：

listsum(Lst, Sum) :-
    % Check open list without unintentionally closing it
    (var(Lst) -> true ; \+ \+ (length(Lst, Len), !, numlist(1, Len, Lst))),
    % Reduce unwanted choicepoints
    ((is_list(Lst) ; nonvar(Sum)) -> Once = true ; Once = false),
    listsum_([1|Tail], Tail, Lst, 2, 1, Sum),
    (Once == true -> ! ; true).

% Closing open Lst with empty-list Tail
listsum_(Lst, [], Lst, _Next, Sum, Sum).
listsum_(LU, Tail, Lst, Next, SumU, Sum) :-
    SumU1 is Next + SumU,
    % Terminate if gone past nonvar arguments
    (var(Sum) -> true ; SumU1 =< Sum),
    % Appending to rear of list
    Tail = [Next|Tail1],
    Next1 is Next + 1,
    listsum_(LU, Tail1, Lst, Next1, SumU1, Sum).

导致 swi-prolog：

?- listsum(L, S).
L = [1],
S = 1 ;
L = [1,2],
S = 3 ;
L = [1,2,3],
S = 6 ;
L = [1,2,3,4],
S = 10 ;
L = [1,2,3,4,5],
S = 15 ;

?- listsum(L, 6).
L = [1,2,3].