Using a constrained variable with `length/2`

Question

Here is the problem:

$ swipl
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.3.6-5-g5aeabd5)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.

For help, use ?- help(Topic). or ?- apropos(Word).

?- use_module(library(clpfd)).
true.

?- N in 1..3, length(L, N).
N = 1,
L = [_G1580] ;
N = 2,
L = [_G1580, _G1583] ;
N = 3,
L = [_G1580, _G1583, _G1586] ;
ERROR: Out of global stack % after a while

(I can switch the order of the subqueries, the result is the same).

I guess I need to label N before I can use it, but I wonder what the problem is? I have not managed to choke up length/2 before.

Rabon

Exactly the same problem for: SICStus, GNU ... – Triliteral

what a nice example of intricacies of Prolog with extensions... thanks for working out this... – Prelate

I would love to see that feature come to life! – Gertrudis

@repeat: I think that, once fixed the semantic, could be pretty simple... just extend length/2 handling attributed variables... – Prelate

@CapelliC. Sounds good! But, AFAIK, the clpfd implementation (that is used in SWI and that can also be used in yap) is 100% Prolog and 0% C. When hacking the C implementation of, say, length/2 we would lose that "100% Prolog"-property... how can the coding effort be kept in reasonable bounds? – Gertrudis

@repeat: length/2 is defined at line 3069 of init.pl (it's easy to find with ?- edit(length)). And builtins can be refined (module wise) with redefine_system_predicate – Prelate

@CapelliC. Cool! Thx for the hint! So we could do it without any C code, right?! Something like: length(Xs,N) :- ..., var(N), clpfd:fd_sup(N,Sup), integer(Sup), !, ... . Do other Prolog processors like yap have similar "overloading" capabilities? – Gertrudis

@repeat: I don't think, we are in the realm of system specific extensions... by myself, I had troubles running presumed equivalent library code - rb_tree related – Prelate

@CapelliC. Please tell me more. – Gertrudis

Let us continue this discussion in chat. – Prelate

Answer 1

What's probably more useful than a slightly less nondeterministic length/2 is a proper list-length constraint. You can find an ECLiPSe implementation of it here, called len/2. With this you get the following behaviour:

?- N :: 1..3, len(Xs, N).
N = N{1 .. 3}
Xs = [_431|_482]               % note it must contain at least one element!
There is 1 delayed goal.
Yes (0.00s cpu)

You can then enumerate the valid lists either by enumerating N:

?- N :: 1..3, len(Xs, N), indomain(N).
N = 1
Xs = [_478]
Yes (0.00s cpu, solution 1, maybe more)
N = 2
Xs = [_478, _557]
Yes (0.02s cpu, solution 2, maybe more)
N = 3
Xs = [_478, _557, _561]
Yes (0.02s cpu, solution 3)

or by generating lists with good old standard length/2:

?- N :: 1..3, len(Xs, N), length(Xs, _).
N = 1
Xs = [_488]
Yes (0.00s cpu, solution 1, maybe more)
N = 2
Xs = [_488, _555]
Yes (0.02s cpu, solution 2, maybe more)
N = 3
Xs = [_488, _555, _636]
Yes (0.02s cpu, solution 3)

Turtleback

This seems to be exactly what I was looking for! Do you know if this can be implemented in SWI-Prolog, or does it use ECLiPSe-specific extensions? (the source here does contain some unfamiliar syntax, at least). – Rabon

The critial line is suspend(len(Xs,L,N), 0, [[Xs0,N]->inst,N->min]), where the goal is delayed until Xs0 or N get instantiated OR the lower bound of N changes. You would have to investigate how to do that with SWI's clpfd. – Turtleback

Why not add that feature to length/2? IMO that would be best, particularly for beginners. Or are there (technical) problems/pitfalls with that approach which I do not see yet? – Gertrudis

@Boris: Be aware that this approach trades non-termination for inconsistency! len(L,N), len([_|L],N) is such an inconsistency, len(L,L) another. If you are directly programming in such a context, you end up with a bunch of "delayed" or "floundering" goals that you are unable to understand. That said, these mechanisms may certainly be used to produce meaningful abstractions. But there are no stable notions to reason about them directly (like failure-slices are for regular Prolog). – Triliteral

@false, there is no inconsistency, delayed goals are of course part of the resolvent. Floundering ≠ true. – Turtleback

@jschimpf: This is a terminological issue: How do you call a floundering goal or some constraint store that does not have any solution? In German, I use Scheinlösung, and in English I have seen only inconsistency. – Triliteral

@jschimpf: As a quick example of common usage, please refer to this Wikipedia lemma. – Triliteral

@repeat, you need both. len/2 has constraint-like behaviour, i.e. it only makes deterministic inferences, it never makes choices. But sometimes you want to nondeterministically generate lists. – Turtleback

Answer 2

Let's start with the most obvious one. If you switch the goals, you have:

?- length(L, N), N in 1..3.

which has the same termination properties as:

?- length(L, N), false, N in 1..3.

So obviously, this must not terminate with Prolog's execution mechanism.

However, if you put N in 1..3 in front, this might affect termination. To do so, it must be possible with finite means to prove that there is no N from 4 on. How can you prove this in a system without constraints - that is, only with syntactic unification present? Well, you can't. And length/2 is commonly defined just without constraints present. With library(clpfd) things are trivial, for N #>= 4, N in 1..3 simply fails¹. Note also that library(clpfd) does not collaborate much with library(clpq) which might be an interesting candidate, too.

As a consequence you would need to define your own length — for each constraint package you are interested in. That's a bit of a pity, but currently there is no generic way to do so in sight. ((That is, if you are interested and think a bit about it, you might come up with a nice API that every constraint system should adhere to. Alas, this will take some more decades, I suspect. Currently, there is much too much divergence.))

So here is a first naive way for fd_length/2:

fd_length([], N) :-
   N #= 0.
fd_length([_|L], N0) :-
   N0 #>= 1,
   N1 #= N0-1,
   fd_length(L, N1).

OK, this could be optimized to avoid the superfluous choicepoint. But there is a more fundamental problem: If you are determining the length of a list of length N, this will create N constraint variables! But we do need only one.

fd_length(L, N) :-
   N #>= 0,
   fd_length(L, N, 0).

fd_length([], N, N0) :-
   N #= N0.
fd_length([_|L], N, N0) :-
   N1 is N0+1,
   N #>= N1,
   fd_length(L, N, N1).

Again, this is not perfect for so many reasons: It could use Brent's algorithm like current systems do ; and combine it with all the fd properties. Also, arithmetic expressions are probably not a good idea to permit ; but I would have to wait for (#)/1 in SWI...

---

^{1: Strictly speaking, this "simply fails" only for SICStus, SWI, and YAP. For in those systems, there is no accidental failure due to exhaustion of the current representation. That is, their failure can always be taken as an honest no.}

Triliteral

Similarly, one could hope that ?- N #< 0, length(L, N). should fail, but of course it does not. – Rabon

@Boris:At least for your consolation you need only one constraint-variable to define fd_length/2 - I believe we had this already a couple of times. Do you see how this is possible? – Triliteral

@Boris: labeling is not perfect, for it works only for finite cases. But nicely, both SICStus and SWI aim (correctly) for the "infinite" case, too. – Triliteral

Here is one query that does not terminate with the second definition of fd_length/2: ?- fd_length(L, N), L ins 2..sup, sum(L, #=, 1). – Rabon

@Boris: that query must not terminate! For ?- fd_length(L, N). must not terminate to describe the entire set of solutions. – Triliteral

Yes, but if should obviously fail..... ;) consider ?- L = [X], L ins 2..sup, sum(L, #=, 1). which immediately fails. This is also the intended use for an fd_length/2 (but obviously this is not part of my initial question, and your answer has already helped me to put my problem in context). – Rabon

@Boris: It is a fundamental property of non-termination in (pure) Prolog that: If P does not terminate, then P, Q, R does not terminate as well! Please do look at failure-slice! With this notion you can better understand what you can expect from Prolog, and what is simply impossible (in the context of Prolog)! – Triliteral

I admit it: I do not fully understand "termination" in the context of Prolog. Should read more. – Rabon

@Boris. Reading is good, start with the following sentences:) 1. Because of its support for non-determinism, the very term "termination" has not one but two different meanings. 2. Quoting from complang.tuwien.ac.at/ulrich/papers/PDF/sas01.pre.pdf : "Existential termination means that either the computation finitely fails or it produces one solution in finite time (then it may loop if we ask for another solution). On the other hand, universal termination means that the computation produces all solutions (if we repeatedly ask for another solution) in finite time then terminates." – Gertrudis

@Boris. So when talking about termination in the context of Prolog, we mean universal termination, not existential termination. In a nutshell, some goal G terminates universally if the conjunction G,false finitely fails. – Gertrudis

Call me biased, but if I could choose one domain that length/2 (and friends like same_length/3) could be adapted to work together with, it would be integers (clpfd). I don't see how this could be done with reasonable effort, but seeing this particular feature from a user's perspective all I can say is "WOW! That would be great!" – Gertrudis

@repeat: For quite long time, the only reasonable constraint domain was CLP(Q). Still, for many problems it's the domain of choice, think of linear equations and inequations. – Triliteral

By no means I wanted to imply that integers are the only interesting domain, not for a split second. That being said, I feel that integers are the domain of choice for length/2 and friends. – Gertrudis

Answer 3

How about the following baroque work-around based on clpfd and meta-predicate tcount/3?

:- use_module([library(clpfd), library(lambda)]).

list_FDlen(Xs, N) :-
   tcount(\_^ =(true), Xs, N).

Let's query!

?- N in 1..3, list_FDlen(Xs, N).
   N = 1, Xs = [_A]
;  N = 2, Xs = [_A,_B]
;  N = 3, Xs = [_A,_B,_C]
;  false.                             % terminates universally

?- N in inf..2, list_FDlen(Xs, N).
   N = 0, Xs = []
;  N = 1, Xs = [_A]
;  N = 2, Xs = [_A,_B]
;  false.                             % terminates universally, too

What about this particular query?

?- N in 2..sup, list_FDlen(Xs, N).
   N = 2, Xs = [_A,_B]
;  N = 3, Xs = [_A,_B,_C]
;  N = 4, Xs = [_A,_B,_C,_D]
...                                   % does not terminate (as expected)

Gertrudis

Answer 4

We present a clpfd-ish variant of length/2 that's tailored to @mat's clpfd implementation.

:- use_module(library(clpfd)).
:- use_module(library(dialect/sicstus)).

:- multifile clpfd:run_propagator/2.

The "exported" predicate lazy_len/2 is defined like this:

lazy_len(Es, N) :-
   N in 0..sup,               % lengths are always non-negative integers
   lazylist_acc_len(Es, 0, N),
   create_mutable(Es+0, State),
   clpfd:make_propagator(list_FD_size(State,N), Propagator),
   clpfd:init_propagator(N, Propagator),
   clpfd:trigger_once(Propagator).

The global constraint handler list_FD_size/3 incrementally modifies its internal state as constraint propagation occurs. All modifications are trailed and are un-done upon backtracking.

clpfd:run_propagator(list_FD_size(State,N), _MState) :- 
   get_mutable(Es0+Min0, State),
   fd_inf(N, Min),
   Diff is Min - Min0,
   length(Delta, Diff),
   append(Delta, Es, Es0),
   (  integer(N)
   -> Es = []
   ;  Delta = []
   -> true                    % unchanged
   ;  update_mutable(Es+Min, State)
   ).

lazy_len/2 tackles the problem from two sides; the clpfd constraint part of it was shown above. The tree side uses prolog-coroutining to walk down the list as far as the partial instantiation allows¹:

lazylist_acc_len(_, _, N) :-
   integer(N),
   !.
lazylist_acc_len(Es, N0, N) :-
   var(Es),
   !,
   when((nonvar(N);nonvar(Es)), lazylist_acc_len(Es,N0,N)).
lazylist_acc_len([], N, N).
lazylist_acc_len([_|Es], N0, N) :-
   N1 is N0+1,
   N  in N1..sup,
   lazylist_acc_len(Es, N1, N).   

Sample queries:

?- lazy_len(Xs, N).
when((nonvar(N);nonvar(Xs)), lazylist_acc_len(Xs,0,N)),
N in 0..sup,
list_FD_size(Xs+0, N).

?- lazy_len(Xs, 3).
Xs = [_A,_B,_C].

?- lazy_len([_,_], L).
L = 2.

?- lazy_len(Xs, L), L #> 0.
Xs = [_A|_B],
when((nonvar(L);nonvar(_B)), lazylist_acc_len(_B,1,L)),
L in 1..sup,
list_FD_size(_B+1, L).

?- lazy_len(Xs, L), L #> 2.
Xs = [_A,_B,_C|_D],
when((nonvar(L);nonvar(_D)), lazylist_acc_len(_D,3,L)),
L in 3..sup,
list_FD_size(_D+3, L).

?- lazy_len(Xs, L), L #> 0, L #> 2.
Xs = [_A,_B,_C|_D],
when((nonvar(L);nonvar(_D)), lazylist_acc_len(_D,3,L)),
L in 3..sup,
list_FD_size(_D+3, L).

And, at long last, one more query... well, actually two more: one going up—the other going down.

?- L in 1..4, lazy_len(Xs, L), labeling([up], [L]).
   L = 1, Xs = [_A]
;  L = 2, Xs = [_A,_B]
;  L = 3, Xs = [_A,_B,_C]
;  L = 4, Xs = [_A,_B,_C,_D].

?- L in 1..4, lazy_len(Xs, L), labeling([down], [L]).
   L = 4, Xs = [_A,_B,_C,_D]
;  L = 3, Xs = [_A,_B,_C]
;  L = 2, Xs = [_A,_B]
;  L = 1, Xs = [_A].

---

^{Footnote 1: Here, we focus on preserving determinism (avoid the creation of choice-points) by using delayed goals.}

Gertrudis