Prolog: missing feature?

Question

Any programmer with some experience in Prolog knows the advantages of use unary notation for numbers. By example, if we represent a number as list of 1" ("4" is list "[1,1,1,1]" and so on), we can define:

unary_succ(X,[1|X]).

the following queries does what is expected:

?- X=[1,1],unary_succ(X,Y).
X = [1, 1],
Y = [1, 1, 1].

?- unary_succ(X,Y),X=[1,1].
X = [1, 1],
Y = [1, 1, 1].

?- unary_succ(X,Y),Y=[1,1].
X = [1],
Y = [1, 1].

In this way, statement unary_succ(X,Y) "binds" X and Y in a way that, if after the fact is stated, one of these variables is bound to a value, the other one does.

However, this behaviour is not possible if we use the internal number representation:

?- X=2,succ(X,Y).
X = 2,
Y = 3.

?- succ(X,Y),X=2.
ERROR: succ/2: Arguments are not sufficiently instantiated

?- succ(X,Y),Y=2.
ERROR: succ/2: Arguments are not sufficiently instantiated

In my opinion, it will be very useful that previous statements and similar ones does what is expected. That is, we need to link two variables in a way that, when one of them is bound to a value, the other does following the previously established rule.

My questions are:

a) some easy way to do that in Prolog.

b) if not possible, any other programming language that supports this feature?

Any comment is welcome.

Thanks to everybody.

* Addendum I *

Another example is:

user_id(john,1234).
user_id(tom,5678).

and queries:

X=john,user_id(X,Y).
user_id(X,Y),X=john

that currently are solved by backtracking.

Answer 1

This topic is known as coroutining, and to be solved in fairly general way - afaik - requires extension to the basic Prolog computation model. Fortunately, most Prologs have such extension... So, let's try in SWISH to build your own 'reactive' extension:

my_succ(X, Y) :- when((nonvar(X);nonvar(Y)), succ(X, Y)).

edit not completely on point, but Jan posted on SWI-Prolog mailing list a simple example of coroutining application:

?- freeze(X, writeln(X)), findall(X, between(1,3,X), Xs).
1
2
3
Xs = [1, 2, 3],
freeze(X, writeln(X)).

Answer 2

The problem you describe exists as long as the answers by a Prolog system are restricted to (syntactic) answer substitutions. In your example, the goal succ(X, Y) would require infinitely many answers to describe the entire set of solutions. For this reason, an instantiation_error is issued instead.

To address this problem we need to extend answers. So answers not only include answer substitutions but some more elaborate way to describe some sets.

library(clpfd) offering constraints over Z (and most prominently finite domains).

?- use_module(library(clpfd)).
?- Y #= X+1.
X+1#=Y.

Note that such solvers are not very strong for the general case:

?- Y #= X+1, X #= Y+1.
Y+1#=X,
X+1#=Y.

You may expect the system to fail, however it produces an answer which essentially restated the query. At least the answer is not incorrect, for it simply states: yes, there is a solution provided this relation holds (which it does not, similar to the fine print in insurance contracts or guarantee certificates).

when/2 is also known as coroutining and is in many cases weaker than what you get with clpfd. But, in a few cases it is stronger to some implementations of clpfd. Consider dif/2 which can be expressed as when(?=(X,Y), X \== Y) and

| ?- dif(X, Y), X = Y.
no

... whereas (in SICStus)

| ?- X #\= Y, X #= Y.
Y #= X,
Y #\= X,
Y in inf..sup,
X in inf..sup ? ;
no

library(clpq) offers a solver that is stronger in many situations but lacks integer specific constraints like mod/2. In many situations it is still interesting to use, as here in SICStus:

| ?- use_module(library(clpq)).
yes
| ?- {Y=X+1}.
{X = -1+Y} ?
yes
| ?- {Y=X+1}, {X=Y+1}.
no