^{从 — 开始的小问题名称:sequences/1 建议一个序列列表(无论序列是什么)，它应该是 sequence/1.}

您需要很多糟糕的 Prolog 系统:您需要更强的一致性.我想不惜任何代价.

我的即时反应(使用library(clpfd)！)不起作用，让我们看看为什么

?- length(Xs,N),Xs ins 1..4, all_distinct(Xs).

它的循环次数和你的版本一样多，***用这个 失败切片:

?- length(Xs,N), false, Xs ins 1..4, all_distinct(Xs).

所以只有 length/2 是错误的.也许我重申一下您的程序，并尝试找出您的程序没有终止的原因:

序列([]):- 假.序列([H|T]):-地图列表(dif(H)，T)，假之间(1, 4, H),序列(T).?- 序列(X)，假.

我们最亲爱的声明式海报孩子maplist/2被抓到了！好吧，也许我们不应该那么苛刻.毕竟，诚实地不终止谓词总是比肆无忌惮地不健全或不完整的黑客更可取.

我们需要了解的是，all_distinct/1 需要知道列表的长度，并且所有域也必须存在.

sequence(Xs) :-序列辅助(Xs，[]).序列辅助([]，_).sequence_aux([X|Xs], Ys) :-1..4 中的 X，all_distinct([X|Ys]),序列辅助(Xs，[X|Ys]).?-序列(X).

现在终止.

@mat 可能会注意到 all_distinct([_]) 可能会被删除.可能还不止这些.

如果你不喜欢这个解决方案，因为它使用了一个额外的参数，你需要实现一个更安全的maplist/2.

fmaplist(C_1, Xs) :-冻结(Xs​​，fmaplist_aux(C_1，Xs)).fmaplist_aux(_C_1, []).fmaplist_aux(C_1, [X|Xs]) :-呼叫(C_1，X)，冻结(Xs​​，fmaplist_aux(C_1，Xs)).

现在您可以逐字使用您的原始程序.但我感觉不太好.了解冻结程序中非终止的精确边界要困难得多.

顺便说一句:您可能会尝试在 SWI 中获取正确的变量名称以进行答案替换，因为类似于 _G772 的编号不允许将答案重新粘贴回*** shell 并获得正确答案结果.

This question came up while answering another question on *** on (generalizing a bit) generating all sequences formed out of a finite set of elements with no duplicate occurrences.

As Boris rightly indicated in the comments, there are many existing solutions to this problem. However, I am interested in a solution that does not use an accumulator (i.e., a list of already picked elements against which a newly selected element is to be compared) but that uses dif/2 statements instead.

To illustrate, in my following program I have 4 elements and, after 4 recursive calls, a couple of div/2 statements which state that the 4 elements that have been chosen until now are pairswise dissimilar. From this one can deduce that it makes no sense to continue the recursion and look for a fifth element, since there are no elements left given the div/2 statements. Is there a way to encode this 'knowledge' into the program so that it no longer loops?

:- use_module(library(apply)).
:- use_module(library(dif)).

sequences([]).
sequences([H|T]):-
  maplist(dif(H), T),
  between(1, 4, H),
  sequences(T).

Current, looping behavior:

?- sequences(X).
X = [] ;
X = [1] ;
...
X = [4, 3, 1, 2] ;
X = [4, 3, 2, 1] ;
<LOOP>

^{Tiny issue to start with — the name: sequences/1 suggests a list of sequences (whatever a sequence is), it should be rather sequence/1.}

You are demanding quite a lot of a poor Prolog system: You are demanding stronger consistency. At any price, I presume.

My immediate reactio (use library(clpfd)!) does not work, let's see why

?- length(Xs,N),Xs ins 1..4, all_distinct(Xs).

It loops just as much as your version, which can be best seen with this failure-slice:

?- length(Xs,N), false, Xs ins 1..4, all_distinct(Xs).

So already length/2 alone is wrong. Maybe I reiterate to your program, and try to identify why your program does not terminate:

sequences([]) :- false.
sequences([H|T]):-
  maplist(dif(H), T), false
  between(1, 4, H),
  sequences(T).

?- sequences(X), false.

Our dearest declarative poster child maplist/2 caught in flagranti! OK, maybe we should not be that harsh. After all, honest non-termination of a predicate is always preferable to an unscrupulously unsound or incomplete hack.

What we need to understand is that all_distinct/1 requires the length of the list to be known, and all domains must be present, too.

sequence(Xs) :-
   sequence_aux(Xs, []).

sequence_aux([], _).
sequence_aux([X|Xs], Ys) :-
   X in 1..4,
   all_distinct([X|Ys]),
   sequence_aux(Xs, [X|Ys]).

 ?- sequence(X). 

Now terminates.

@mat may note that all_distinct([_]) might be removed. Maybe even more than that.

If you do not like this solution because it uses an extra argument, you will need to implement a safer maplist/2.

fmaplist(C_1, Xs) :-
    freeze(Xs, fmaplist_aux(C_1, Xs)).

fmaplist_aux(_C_1, []).
fmaplist_aux(C_1, [X|Xs]) :-
   call(C_1, X),
   freeze(Xs, fmaplist_aux(C_1, Xs)).

Now you can use your original program verbatim. But I do not feel very good at it. Understanding the precise borders of non-termination in a program with freeze is much more difficult.

---

As an aside: you might try to get correct variable names in SWI for answer substitutions because the _G772-like numbering does not permit to re-paste an answer back into the toplevel shell and get correct results.