Is it possible to declare an ascending list?

Question

I can make lists of an ascending integer like this:

?- findall(L,between(1,5,L),List). 

I know that I can generate values ​​using:

 ?- length(_,X). 

But I don’t think I can use this in findall, as in the following loop:

 ?- findall(X,(length(_,X),X<6),Xs). 

I can also generate a list using clpfd .

 :- use_module(library(clpfd)). list_to_n(N,List) :- length(List,N), List ins 1..N, all_different(List), once(label(List)). 

or

 list_to_n2(N,List) :- length(List,N), List ins 1..N, chain(List,#<), label(List). 

The latter method seems to me the best, since it is the most declarative and does not use once/1 or between/3 or findall/3 , etc.

Are there any other ways to do this? Is there a declarative way to do this in a clean prolog? Is there a "better" way?

Answer 1

The "best" way depends on your specific use cases! Here's another way to do this with clpfd :

 :- use_module(library(clpfd)). 

We define the predicate equidistant_stride/2 proposed by @mat in a comment on a previous answer to 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. 

Based on equidistant_stride/2 , we define:

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

Run some queries! First, your initial 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] ... 

With clpfd , we can ask fairly general queries - and get logical 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.

---

Alternative implementation of equidistant_stride/2 :

I hope the new code makes better use of proliferation restrictions.

Thanks to @WillNess for offering test cases that motivated this rewriting!

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

Comparison of the old vs new version with @mat clpfd:

First, the old version:

 ?- 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 go to the new version and ask the same requests!

  ? - equidistant_stride ([1, _, _, _, 14], D).      
 false  % fails, as it should

 ? - equidistant_stride ([1, _, _, _, 14 | _], D).
 false  % fails, as it should

---

Once again, again! Can we fail earlier by using redundant constraints beforehand?

Earlier, we proposed using the restrictions Z1 #= Z0+D*1, Z2 #= Z0+D*2, Z3 #= Z0+D*3 instead of Z1 #= Z0+D, Z2 #= Z1+D, Z3 #= Z2+D (which is in the 1st version of the code in this answer).

Again, thanks to @WillNess for motivating this little experiment, noting that the goal of equidistant_stride([_,4,_,_,14],D) does not fail, but succeeds with pending achievements instead:

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

Add some redundant restrictions with equidistantRED_stride/2 :

 equidistantRED_stride([],_). equidistantRED_stride([Z|Zs],D) :- equidistant_from_nth_stride(Zs,Z,1,D), equidistantRED_stride(Zs,D). 

Request example:

 ?- Zs = [_,4,_,_,14], equidistant_stride(Zs,D), equidistantRED_stride(Zs,D). false. 

Are you done? Not yet! In the general case, we do not want a quadratic number of redundant constraints. That'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 a double negation trick, the residual balance remains in those cases where success ...

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

... and ...

  ? - Zs = [_, 4, _, _, 14], equidistant_stride (Zs, D), \ + \ + equidistantRED_stride (Zs, D).
 false

... we find failure in more cases than before!

---

Let dig a little deeper! Can we detect failure earlier even for more generalized purposes?

With the code so far presented, these two logically false requests do not end:

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

Is there a fix? Got a hack!

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

The hack does not guarantee the end of the "part" of the excess restriction, but IMO is not so bad for a quick first shot. The integer/1 test when creating any variable in Zs means that clpfd solver to restrict domain variables to singletones, while instantiation with cons pairs (which directly leads to list-based predicates being interrupted) is suppressed.

I understand that hacking can be quite easily broken in several ways (for example, using cyclic terms). Any suggestions and comments are welcome!

Answer 2

Next, we discuss the code provided in this previous answer .

The purpose of consecutive_ascending_integers_from_1([2,3,5,8|non_list]) failed, but why?

Let's continue step by step:

1. Here is the code we start with:

     : - use_module (library (clpfd)).
   
    equidistant_from_nth_stride ([], _, _, _).
    equidistant_from_nth_stride ([Z | Zs], Z0, I0, D): -
       Z # = Z0 + I0 * D,
       I1 # = I0 + 1,
       equidistant_from_nth_stride (Zs, Z0, I1, D).
   
    equidistant_stride ([], _).
    equidistant_stride ([Z0 | Zs], D): -
       equidistant_from_nth_stride (Zs, Z0,1, D).
   
    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).
   

2. First, we make (some) unions more explicit:

     equidistant_from_nth_stride ([], _, _, _).
    equidistant_from_nth_stride ([Z | Zs], Z0, I0, D): -
       Z # = Z0 + I0 * D,
       I1 # = I0 + 1,
       equidistant_from_nth_stride (Zs, Z0, I1, D).
   
    equidistant_stride ([], _).
    equidistant_stride ([Z0 | Zs], D): -
       I = 1
       equidistant_from_nth_stride (Zs, Z0, I , D).
   
    consecutive_ascending_integers (Zs): -
       D = 1
       equidistant_stride (Zs, D ).
   
    consecutive_ascending_integers_from (Zs, Z0): -
       Zs = [Z0 | _] ,
       consecutive_ascending_integers (Zs).
   
    consecutive_ascending_integers_from_1 (Zs): -
       Z0 = 1 ,
       consecutive_ascending_integers_from (Zs, Z0 ).
   

3. We follow the method and conventions presented in this excellent answer :

   By removing goals, we can generalize the program. Here is my favorite way to do this. Adding the predicate (*)/1 like this:

     : - op (950, fy, *).
   
    * _.
   

4. @WillNess rightly remarked that:

   consecutive_ascending_integers_from_1([2,3,5,8|non_list]) consecutive_ascending_integers_from_1([2|_]) fails, so its specialization should also end with the specialization consecutive_ascending_integers_from_1([2,3,5,8|non_list])

   If we summarize the code as much as possible in such a way that consecutive_ascending_integers_from_1([2|_]) fails, we "know for sure: something in the visible remainder of the program must be fixed."

  consecutive_ascending_integers_from (Zs, Z0): -
        Zs = [Z0 | _],
        * consecutive_ascending_integers (Zs) .

     consecutive_ascending_integers_from_1 (Zs): -
        Start = 1,
        consecutive_ascending_integers_from (Zs, Start).

5. Let there be another explanation!

   In version No. 2 (see above), we also observe the following general goals:

     ? - consecutive_ascending_integers_from_1 ([_, _, _, _ | non_list]).
    false
   

   Why is this failing? Let us summarize the code as much as possible so that the goal is not fulfilled:

  equidistant_from_nth_stride ([], _, _, _).
     equidistant_from_nth_stride ([Z | Zs], Z0, I0, D): -
        * Z # = Z0 + I0 * D ,
        * I1 # = I0 + 1 ,
        equidistant_from_nth_stride (Zs, Z0, I1, D).

     equidistant_stride ([], _).
     equidistant_stride ([Z0 | Zs], D): -
        * I = 1 ,
        equidistant_from_nth_stride (Zs, Z0, I, D).

     consecutive_ascending_integers (Zs): -
        * D = 1 ,
        equidistant_stride (Zs, D).

     consecutive_ascending_integers_from (Zs, Z0): -
        * Zs = [Z0 | _] ,
        consecutive_ascending_integers (Zs).

     consecutive_ascending_integers_from_1 (Zs): -
        * Start = 1 ,
        consecutive_ascending_integers_from (Zs, Start).

---

Why isn't consecutive_ascending_integers_from_1([2,3,5,8|non_list]) goal of consecutive_ascending_integers_from_1([2,3,5,8|non_list]) ?

So far, we have seen two explanations, but maybe more ...

The truth is there: join the hunt!

Answer 3

We will define ascending lists as such that contain at least two elements that increase the number of integers (non-decreasing lists can be empty or single-point, and "ascending" is a more specific property). This is a somewhat arbitrary definition.

In SWI Prolog:

 ascending( [A,B|R] ):- freeze(A, freeze(B, (A < B, freeze(R, (R=[] -> true ; ascending([B|R])))) )). 

To easily fill, we could use

 mselect([A|B],S,S2):- select(A,S,S1), mselect(B,S1,S2). mselect([], S2, S2). 

Testing:

fifteen? - increase (LS), mselect (LS, [10,2,8,5], []).

LS = [2, 5, 8, 10] ;

false


16? - mselect (LS, [10,2,8,5], []), ascending (LS).

LS = [2, 5, 8, 10] ;

Lying.

---

Regarding the issue of generosity, according to fooobar.com/questions/tagged / ... ,

Only monotone (also called: "monotone") predicates are pure: if the predicate succeeds for any arguments, then it does not interrupt for any generalization of these arguments, and if it fails for any combination of arguments, then it fails for which or specialization of these arguments.

consecutive_ascending_integers_from_1([2|B]) fails, so its specialization consecutive_ascending_integers_from_1([2,3,5,8|non_list]) does not work either.

---

For extended generosity, " consecutive_ascending_integers_from_1([2,3,5,8|non_list]) fails, but why?" additional unsuccessful goals: ( 1 )

 consecutive_ascending_integers_from_1([_,3|_]) 

for code

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

and the rest is unchanged, because C1 becomes 3 #= 1 + 1*1 . In addition, ( 2 and 3 )

 consecutive_ascending_integers_from_1([A,B,5|_]) consecutive_ascending_integers_from_1([A,B,C,8|_]) 

both do not work with immutable code because 1st defines

 A = 1, B #= 1 + 1*1, 5 #= 1 + 2*1 

and the second determines

 A = 1, B #= 1 + 1*1, C #= 1 + 2*1, 8 #= 1 + 3*1 

Another possibility ( 4 ) -

 consecutive_ascending_integers_from_1([_,3,5|_]) 

with generalized

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

because

 26 ?- 3 #= Z + 1*1, 5 #= Z + 2*1. false. 

Similarly, with the modified code, the goal ( 5 )

 consecutive_ascending_integers_from_1([_,3,_,8|_]) 

because

 27 ?- 3 #= Z + 1*1, 8 #= Z + 3*1. false. 

as well as ( 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|_]) 

for the same reason. Another possible generalization of the code is to leave D uninitialized (the rest of the source code has not changed):

 consecutive_ascending_integers(Zs) :- *( D = 1 ), equidistant_stride(Zs,D). 

so the goal ( 5 ) ...[_,3,_,8|_]... will fail again, due to

 49 ?- 3 #= 1 + 1*D, 8 #= 1 + 3*D. false. 

but

 50 ?- 3 #= 1 + 1*D, 5 #= 1 + 2*D. D = 2. 

therefore ...[_,3,5|_]... will be successful (indeed, it is). ( 10 )

 consecutive_ascending_integers_from_1([_,_,5,8|_]) 

also does not work for the same reason.

There may be several more combinations, but the general meaning of this becomes clearer: it all depends on how the constraints created by this predicate work.