Is it possible to declare an ascending list?

Question

I can make lists of ascending integer like so:

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

I know I can also generate values using:

?- length(_,X).

But I don't think I can use this in a findall, as things like 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 last method seems best to me as it is the most declarative, and does not use once/1 or between/3 or findall/3 etc.

Are there other ways to do this? Is there a declarative way to do this in 'pure' Prolog? Is there a 'best' way?

`chain(List, #<)` does precisely what you ask for: It is true for a list of strictly ascending integers. Using CLP(FD) constraints is the most elegant and general way to describe such a list. The solution with `numlist/3` is less general: It only is true for a concrete list starting with a specific integer, and proceeding in increments of 1. This is not a truly general relation describing "a list of ascending integers". — mat, Sep 16 '15 at 18:50

score 3 · Accepted Answer · edited May 23 '17 at 11:58

The "best" way depends on your concrete use cases! Here's another way to do it using clpfd:

:- use_module(library(clpfd)).

We define predicate equidistant_stride/2 as suggested by @mat in a comment to 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.

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

Let's run some queries! First, your original 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 quite general queries—and get logically sound 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.

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

Comparison of old vs new version with @mat's clpfd:

First up, 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 let's switch to the new version and ask the same queries!

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

Let's add some redundant constraints with equidistantRED_stride/2:

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

Sample query:

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

Done? Not yet! In general we don't want a quadratic number of redundant constraints. Here'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 the double-negation trick, the residuum remains in cases that succeed ...

?- 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 detect failure in more cases than we did before!

Let's dig a little deeper! Can we detect failure early in even more generalized uses?

With code presented so far, these two logically false queries do not terminate:

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

Got fix? Got 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 doesn't guarantee termination of the redundant constraint "part", but IMO it's not too bad for a quick first shot. The test integer/1 upon instantiation of any variable in Zs is meant to allow the clpfd solver to constrain variable domains to singletons, while the instantiation with cons-pairs (which directly leads to non-termination of list-based predicates) is suppressed.

I do realize that the hack can be broken quite easily in more than one way (e.g., using cyclic terms). Any suggestions and comments are welcome!

@WillNess. Check out the new improved alternative implementation of `equidistant_stride/2` in my pimped answer! — repeat, Sep 24 '15 at 21:24
so they are now "all in it together", not just by the pairs. nice! (btw I didn't get pinged; -at-name only works if name is on the list of addressees - that's an OP, an answerer, and perhaps editors). — Will Ness, Sep 25 '15 at 01:39
still, `equidistant_stride([_,4,_,_,14],D).` succeeds... perhaps it's possible to create more connections, but I fear it'll be a quadratic number of them, and that might affect the efficiency. right now we have {4=x+d*1, 14=x+d*4}. the first element is still treated as privileged. — Will Ness, Sep 25 '15 at 01:55
@WillNess. clpfd has to strike a balance. Actually, I'm surprised how much clpfd can infer even without `labeling`. Even with its imperfections, I like this approach to getting explanations: if some generalization succeeds (but would/should still fail), our analysis only gets less precise, but stays correct. the same basically applies to generalizations that throw "instantiation error" exceptions. — repeat, Sep 25 '15 at 04:42
@WillNess. Make believe that `equidistant_stride/2` is an importnt constraint used in lots of important applications (which in *some* sense it really is). Posting a quadratic number of redundant constraints may indeed work if used like this: When the constraint is used a linear chain of constraints is posted. Then, the quadratic number of redundant constraints is tentatively posted and the resulting domain restrictions are saved where backtracking does not erase that info. The quadratic number of redundant constraints are all retracted and the noted domain restrictions are enforced. — repeat, Sep 25 '15 at 09:23
@WillNess. For a start, the only info that needs to be preserved is failure/success, like so: `post_linear(Xs), \+ \+ post_quadratic(Xs)`. Of course, and I do not want to endorse *that* kind of coding style, but in some cases this could actually work well. OTOH this can easily lead to overengineering some corner cases that are not *that* important... — repeat, Sep 25 '15 at 09:37
@mat. In general, we want an implementation of `post_quadratic/1` which *always* terminates universally---and use it like this `\+ \+ post_quadratic(Xs), post_linear(Xs)`, agreed? — repeat, Sep 25 '15 at 12:08
I think there are now different issues being somewhat confounded: The original wording was about ascending integers, but apparently meant *consecutive* integers, which are easier to propagate. Your (more general!) version makes good use of constraint propagation by relating everything to a common anchor element. For scalability, I consider O(`n^2`) already the border of feasibility for propagation with larger inputs. From a quick glance, it looks like adding constraints involving integral division (`///2`) involving strides and distances may help with some cases. In any case, very nice job! — mat, Sep 25 '15 at 13:14
@mat. Thanks! I'll take `O(n^2)` if I can get (more, better) generalized variants that still fail. In practise some meta-logical code for selecting an anchor would probably fare even better. Be that as it may, to me it is "thinking aloud" together, using code:) Great! — repeat, Sep 25 '15 at 13:55

score 3 · Answer 2 · edited Jul 24 '19 at 16:08

In the following we discuss the code presented in this previous answer.

The goal consecutive_ascending_integers_from_1([2,3,5,8|non_list]) fails, but why?

Let's proceed step-by-step:

Here's 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).

First, we make (some) unifications 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).

We follow the method and conventions introduced in this fine answer:

By removing goals, we can generalize a program. Here is my favorite way to do it. By adding a predicate (*)/1 like so:
```
:- op(950,fy, *).

*_.
```
@WillNess rightly noted that:

consecutive_ascending_integers_from_1([2|_]) fails, so its specialization consecutive_ascending_integers_from_1([2,3,5,8|non_list]) must fail too.

If maximally generalize the code so that consecutive_ascending_integers_from_1([2|_]) fails, we "know for sure: something in the visible remaining part of the program has to 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).

Let's have another explanation!

With version #2 (see above), we observe the following generalized goal fails, too:
```
?- consecutive_ascending_integers_from_1([_,_,_,_|non_list]).
false.
```
Why does this fail? Let's maximally generalize the code suchthat the goal fails:

    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 does the goal consecutive_ascending_integers_from_1([2,3,5,8|non_list]) fail?

Up to now, we have seen two explanations, but there may be more...

The truth is out there: Join the hunt!

(btw, in case you didn't know, @-notifications from an answer's body do not work...) — Will Ness, Sep 30 '15 at 23:46
@WillNess. I was aware of that, thx. I use it for the sake of brevity... do you find that irritating? — repeat, Oct 01 '15 at 06:05
no, no, I said it just in case you didn't know and expected it to work. yes, we need to mark users somehow; an *easy* functionality for this *is* missing. and thanks a lot for the bounty. :) :) :) I feel almost dirty, like cheating -- you explained it all, I just applied your reasoning. twice. :) — Will Ness, Oct 01 '15 at 12:21
@WillNess. Yes, that functionality is missing, but we shan’t let that bother us... Regarding the bounties: you simply got what you deserved for I felt like I reach you. If *you* feel like cheating, what should the students of user "false" feel like? They can get explanations like these (and others kinds like [tag:failure-slice], too) automatically by pressing a single key. — repeat, Oct 01 '15 at 14:05
@WillNess. I feel like we (all) should carry on developing this methodology of "debugging" together. Many ideas may be worth considering. — repeat, Oct 01 '15 at 14:13

score 1 · Answer 3 · edited May 23 '17 at 11:44

1

We'll define ascending lists as such that contain at least two elements which are increasing integer numbers (non-decreasing lists could be empty, or singleton, but "ascending" is a more definite property). It's a somewhat arbitrary determination.

In SWI Prolog:

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

To easily fill'em up, we could use

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

Testing:

15 ?- ascending(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] ;
false.

As to the bounty question, according to https://stackoverflow.com/tags/logical-purity/info,

Only monotonic (also called: "monotone") predicates are pure: If the predicate succeeds for any arguments, then it does not fail for any generalization of these arguments, and if it fails for any combination of arguments, then it does not succeed for any 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]) must fail too.

For the extended bounty " consecutive_ascending_integers_from_1([2,3,5,8|non_list]) fails, but why?", additional failing goals are: ( 1 )

consecutive_ascending_integers_from_1([_,3|_])

for the 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 unchanged, because C1 becomes 3 #= 1 + 1*1. Also, ( 2 and 3 )

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

both fail with the unchanged code, because the 1st defines

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

and the 2nd defines

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

Yet another possibility ( 4 ) is

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

with the 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 like modified code, the goal ( 5 )

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

because

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

and also the ( 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. Yet another possible code generalization is to leave D uninitialized (with the rest of the original code unchanged):

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

so that the goal ( 5 ) ...[_,3,_,8|_]... again fails, because of

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

but,

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

so ...[_,3,5|_]... would succeed (indeed it does). ( 10 )

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

fails, as well, for the same reason.

There might be some more combinations, but the general gist of it becomes clearer: it all depends on how the constraints created by this predicate operate.

edited May 23 '17 at 11:44

Community

1
1

answered Sep 22 '15 at 23:23

Will Ness

70,110
9
98
181

I see that your answer fits the title of the question... But, judging from the code presented by the OP and by comments, didn't the OP actually refer to ascending consecutive integers? – repeat Sep 23 '15 at 20:17
@repeat yes, but sometimes it's nice to have the more general functionality to then solve the smaller problem with it. – Will Ness Sep 23 '15 at 22:53
You are right! Composition of small versatile parts is nice! (PS. the bounty hunt is still open...) – repeat Sep 24 '15 at 05:32
1

@repeat `consecutive_ascending_integers_from_1([2|B])` fails, so its specialization `consecutive_ascending_integers_from_1([2,3,5,8|non_list])` must fail too. Is that what you meant? – Will Ness Sep 24 '15 at 09:16
1

Exactly! What about other different specializations? IIRC there are at least 4 more. Hint: Try generalizing some subterms of `[2,3,5,8|non_list]`. – repeat Sep 24 '15 at 10:15
1

The reason you point at could be stated more precisely by taking the predicate definition of `consecutive_ascending_integers_from_1` into account. Consider this generalisation: `consecutive_ascending_integers_from(Zs,Z0) :- Zs = [Z0|_].` – repeat Sep 24 '15 at 10:30
1

Also note the composability of this kind of explanations: We can disregard all other clauses and boldly state: if we want the query to succeed, we *have to* change something in the small remaining fragment. (The same holds true for all other explanations of this kind.) – repeat Sep 24 '15 at 10:43
1

@repeat to your http://stackoverflow.com/questions/32611228/is-it-possible-to-declare-an-ascending-list/32728617#comment53357243_32728617, this was my first thought precisely, but then to just go looking inside the definitions doesn't fit your requirements. :) The other generalizations you mention don't come into play (I guess that's what monotonicity *is* about); the one *more* general than mine is perhaps `A #> 1, consecutive_ascending_integers_from_1([A|B])` AFAIU. – Will Ness Sep 24 '15 at 11:20
1

Right, my *specs* were quite vague:) Generalizing an integer value to an integer constraint is a *really fine idea*: `A #> 1` includes `A=2`; but why not something even more general like `A #\= 1`? – repeat Sep 24 '15 at 11:33
You made my day:) I will add an answer showing some ideas I came up with. I guess you already noted that this method (of explaining unexpected failure of pure Prolog programs) does not state "there may be an error in the query data" or "there may be an error in the program code"... It reads: to get rid of unexpected failure, we *must* change something in one or both. – repeat Sep 24 '15 at 11:49
The method relies on 3 pillars: (1) the query/data, (2) the program code, and (3) the expected result. In the best case, we can use that method for three kinds of errors: (1) we use bad query/data, the program code and our expected result are ok; (2) the query/data is ok, so is our expected result, but the program code is faulty; (3) the query/data is ok, so is the program, but expectation of "should the query succeed or not" is wrong. – repeat Sep 24 '15 at 11:54
What about `?- consecutive_ascending_integers_from_1([_,3,5|_]).` I guess one could say that the other explanation does not come into play (procedurally, as failure occurs early). But from a declarative viewpoint other answers may be more interesting and/or easier to comprehend (than the first one). – repeat Sep 24 '15 at 11:56
1

It's really great to see such declarative reasoning on Stackoverflow by you two! The declarative aspects of Prolog are in my view currently way undervalued in Prolog material. The meta-predicates that @repeat has built show that one can retain purity while still keeping the programs deterministic and efficient in many cases. – mat Sep 24 '15 at 12:42
@repeat yes, the `from_1([_,3,5|_])` example is interesting: the `=1` "constraint" doesn't "fire" until the second element is determined. You could equally have used `from_1([_,_,_,_,_,5|_])` etc.. – Will Ness Sep 24 '15 at 13:40
@mat that's less Prolog, and more Constraint Programming model, I think. repeat's `equidistant_stride` for example, replaces the normal Prolog's sequential *control* flow with reified structure of constraints, which will trigger its own execution mechanism when fired - at whatever part of the structure (re: my above comment). It in effect replaces Prolog's execution mechanism with another one, based on constraint propagation. – Will Ness Sep 24 '15 at 13:43
1

@repeat on the second thought the `=1` will be executed right away anyway; but you get my meaning there. For instance, `equidistant_stride([1,_,_,_,14|_],D)` should fail (although it succeeds). – Will Ness Sep 24 '15 at 13:46
I don't quite get that, please explain that more. The idea I had when I constructed that particular query was that several kind of explanations should be possible. Informally, in no particular order: (*) The list must start with `1`. (*) the stride must always be `1`, (*) more general: the stride must always be the same, (*) the last tail may not be `non_list`. – repeat Sep 24 '15 at 13:49
@repeat no, my bad. I was expecting of the constraints too much -- I meant, there is no integral leap distance to leap from 1 to 14 in 4 leaps -- but that's a job for something more sophisticated, like theorem prover or something, I guess. – Will Ness Sep 24 '15 at 13:57
@repeat about the `[_,_,_,_,_,5]` example, I was thinking about `L=[_,_,_,_,_,5], equidistant_stride(L,1), consecutive_ascending_integers_from_1(L).` which indeed fails (using `L=[_,_,_,_,_,5|_]`, it hangs). About "reified structure of constraints" what I meant was, after `L=[_,_,_,_,_,5], equidistant_stride(L,1)` has been executed, the fold has created a corresponding chain of constraints. It is that chain of constraints that I had in mind. – Will Ness Sep 24 '15 at 14:01
1

Right, `equidistant_stride([1,_,_,_,14|_],D)` does not fail. But it does not succeed (with ground answer substitutions) either. Instead, we get an answer with pending goals which must hold for the answer in order to become one or more solutions. cf. http://stackoverflow.com/a/26450510/4609915 – repeat Sep 24 '15 at 17:27
1

IMO one can tackle *that* problem on different levels. (1) use a solver that invests more effort into consistency checking. (2) find a smarter implementation of `equidistant_stride/2`, (3) utilize redundant constraints, (4) use a different execution strategy (depth-limited or DFID). OTOH getting non-termination for queries that should fail is unfortunate, but it is not a show-stopper. If we execute candidate explanations with some time-out capability, we may at least get *some* good answers and "I don't know" in some other cases... – repeat Sep 24 '15 at 17:33
2

The code I gave has some room for improvement. `?- equidistant_stride([1,X,Y,Z,14],D).` succeeds with delayed goals, so does `?- equidistant_stride([1,X,Y,Z,14],D), 1+D*K#=14.` ... but `?- equidistant_stride([1,X,Y,Z,14],D), 1+D*K#=14, (D #> 0 ; D #=< 0).` fails. – repeat Sep 24 '15 at 17:41
Regarding that non-termination issue: this is for real and it must be dealt with, but the issue itself doesn't taint the generalizations for which we can actually prove that they must fail. – repeat Sep 24 '15 at 17:44
2

One more thing about "control flow". If you see coroutining as a valid extension of Prolog's execution model, then we have little choice but to admit "constraint solving" as well. Consider the clpfd implementation by @mat, for example: 100% Prolog with attributed variables. Sweet! – repeat Sep 24 '15 at 17:49
*"with some time-out capability, we may at least get some good answers and "I don't* [__yet__ ?] *know" in some other cases..."* I think Dijkstra had described something like that, with simultaneous execution of branches (?). Anyway, thanks for the bounty and the interesting discussion and stuff, to chew on! You're right on the coroutining thing of course. :) My beef with constraints is that they are not integrated into Prolog as much as I'd like, they are too "separate" from it. e.g. unification is kind of equality *constraint* on symbolic data. it's just different types - integers, terms, – Will Ness Sep 24 '15 at 20:26
@repeat (contd.) ... each type with its specific laws, specific sets of constraints. it's a vague idea. – Will Ness Sep 24 '15 at 20:28
Are you probably refering to "communicating sequential processes" (CSP) by Sir Tony Hoare (yes, **the** Tony Hoare, the inventor of QuickSort)? Regarding the integration of CLP into Prolog processors, I agree. I want to write `N in 1..5, length(Xs,N)` and have it terminate like `N in 1..5,indomain(N),length(Xs,N)` – repeat Sep 24 '15 at 21:22
I think I saw it mentioned somewhere that in Dijkstra's sketches (snippets) when he used a case (switch) statement, every clause was supposed to be executed *concurrently*, and the first one to produce the result, its result would get used, and the others got shut down after that. – Will Ness Sep 25 '15 at 00:48
This may be clear anyway, but still I want to explicitly state that: The new bounty aims at widening that stream of thoughts/ideas which help us *explain failure of monotone Prolog programs*, starting where the previous bounty led us to. JTBC https://upload.wikimedia.org/wikipedia/commons/c/c0/I_want_you.jpg :) – repeat Sep 25 '15 at 07:32
1

Regarding constraints and coroutines, I would like to add that an operational view of Prolog (also without constraints) is very limited: To really understand Prolog execution in procedural terms, you already have to think in two independent control flows (and/or). Realistically, humans do not have the mental capacitiy to fully go through with this approach and push it to its ultimate consequences involving all modes of possible usage, so any procedural understanding you have about Prolog is in my view likely an illusion in any case. Monotonicity etc. are very stable properties though. – mat Sep 25 '15 at 13:22
Check out the explanations in my recent answer http://stackoverflow.com/a/32865304/4609915 ... Join the bounty hunt with an explanation of why `consecutive_ascending_integers_from_1([2,3,5|_])` fails! – repeat Sep 30 '15 at 17:27
@repeat thanks for summing it all up, I was getting lost in all the variants... will read your new answer and see where it leads. :) – Will Ness Sep 30 '15 at 23:37

Is it possible to declare an ascending list?

3 Answers3

Linked