4

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.

false
  • 10,264
  • 13
  • 101
  • 209
pasaba por aqui
  • 3,446
  • 16
  • 40
  • 3
    In SWI Prolog, I think you can do with with clpfd library. You might want to check out its source code to see how it is implemented. – nhahtdh May 22 '15 at 08:43
  • Hi. Thanks for your colaboration. Added to the question another example to clarify. – pasaba por aqui May 22 '15 at 08:45
  • 4
    I second the CLP(FD) suggestion by @nhahtdh: At least for integers, using CLP(FD) constraints is definitely the relational solution you are looking for, and provided by all major Prolog implementations. Simply write `X #= 2, Y #= X + 1` or equivalently `Y #= X + 1, X #= 2`. – mat May 22 '15 at 09:08

2 Answers2

3

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)).
CapelliC
  • 59,646
  • 5
  • 47
  • 90
  • Thanks a lot, I didn't know this statement exists. – pasaba por aqui May 22 '15 at 09:39
  • 2
    `when/2` exists in SICStus (origin), YAP, and SWI. – false May 22 '15 at 10:47
  • 3
    +1 for mentioning coroutining in general. However, this particular example is not very fortunate in my view, because `Y #= X + 1` is more conveniently and much more fittingly solved with CLP(FD) constraints. I suggest you give a didactically more valuable example for `when/2` instead of the current one. – mat May 22 '15 at 11:40
  • 1
    @false: thanks, effectively when/2 seems not so widely supported. I thought it was be based on freeze/2, but this it's not the case... Otoh Ciao Prolog offers a library (at least for freeze/2), XSB team motivates the lacking of the construct because of the unclear semantic in presence of tabling, while B-Prolog takes an entirely different path. – CapelliC May 22 '15 at 12:42
  • 2
    At least, `when/2` is better than `freeze/2` because you can have conditions like `ground/1` and also combine them. See [SICStus' manual](https://sicstus.sics.se/sicstus/docs/latest4/html/sicstus.html/mpg_002dref_002dwhen.html#mpg_002dref_002dwhen). However, for many purposes it is still a hack comparable to `freeze/2` - think of subsumption testing (which is also the reason for XSB to be cautious). – false May 22 '15 at 15:46
  • @mat: I could not think about a more simple/instructive example, my bad... I thought about attributed variables binding visualization, but it's a lot more complex... – CapelliC May 26 '15 at 07:48
  • 2
    @CappeliC: How about `my_dif/2`, expressing the semantics of `dif/2` in terms of `when/2`? – mat May 26 '15 at 08:21
3

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
false
  • 10,264
  • 13
  • 101
  • 209