Making "deterministic success" of Prolog goals explicit

Question

Good news everyone: setup_call_cleanup/3 (currently a draft proposal for ISO) lets you do that in a quite portable and beautiful way.

See the example:

setup_call_cleanup(true, (X=1;X=2), Det=yes)

succeeds with Det == yes when there are no more choice points left.

---

EDIT: Let me illustrate the awesomeness of this construct, or rather of the very closely related predicate call_cleanup/2, with a simple example:

In the excellent CLP(B) documentation of SICStus Prolog, we find in the description of labeling/1 a very strong guarantee:

Enumerates all solutions by backtracking, but creates choicepoints only if necessary.

This is really a strong guarantee, and at first it may be hard to believe that it always holds. Luckily for us, it is extremely easy to formulate and generate systematic test cases in Prolog to verify such properties, in essence using the Prolog system to test itself.

We start with systematically describing what a Boolean expression looks like in CLP(B):

:- use_module(library(clpb)).
:- use_module(library(lists)).

sat(_) --> [].
sat(a) --> [].
sat(~_) --> [].
sat(X+Y) --> [_], sat(X), sat(Y).
sat(X#Y) --> [_], sat(X), sat(Y).

There are in fact many more cases, but let us restrict ourselves to the above subset of CLP(B) expressions for now.

Why am I using a DCG for this? Because it lets me conveniently describe (a subset of) all Boolean expressions of specific depth, and thus fairly enumerate them all. For example:

?- length(Ls, _), phrase(sat(Sat), Ls).
Ls = [] ;
Ls = [],
Sat = a ;
Ls = [],
Sat = ~_G475 ;
Ls = [_G475],
Sat = _G478+_G479 .

Thus, I am using the DCG only to denote how many available "tokens" have already been consumed when generating expressions, limiting the total depth of the resulting expressions.

Next, we need a small auxiliary predicate labeling_nondet/1, which acts exactly as labeling/1, but is only true if a choice-point still remains. This is where call_cleanup/2 comes in:

labeling_nondet(Vs) :-
        dif(Det, true),
        call_cleanup(labeling(Vs), Det=true).

Our test case (and by this, we actually mean an infinite sequence of small test cases, which we can very conveniently describe with Prolog) now aims to verify the above property, i.e.:

If there is a choice-point, then there is a further solution.

In other words:

The set of solutions of labeling_nondet/1 is a proper subset of that of labeling/1.

Let us thus describe what a counterexample of the above property looks like:

counterexample(Sat) :-
        length(Ls, _),
        phrase(sat(Sat), Ls),
        term_variables(Sat, Vs),
        sat(Sat),
        setof(Vs, labeling_nondet(Vs), Sols),
        setof(Vs, labeling(Vs), Sols).

And now we use this executable specification in order to find such a counterexample. If the solver works as documented, then we will never find a counterexample. But in this case, we immediately get:

| ?- counterexample(Sat).
Sat = a+ ~_A,
sat(_A=:=_B*a) ? ;

So in fact the property does not hold. Broken down to the essence, although no more solutions remain in the following query, Det is not unified with true:

| ?- sat(a + ~X), call_cleanup(labeling([X]), Det=true).
X = 0 ? ;
no

In SWI-Prolog, the superfluous choice-point is obvious:

?- sat(a + ~X), labeling([X]).
X = 0 ;
false.

I am not giving this example to criticize the behaviour of either SICStus Prolog or SWI: Nobody really cares whether or not a superfluous choice-point is left in labeling/1, least of all in an artificial example that involves universally quantified variables (which is atypical for tasks in which one uses labeling/1).

I am giving this example to show how nicely and conveniently guarantees that are documented and intended can be tested with such powerful inspection predicates...

... assuming that implementors are interested to standardize their efforts, so that these predicates actually work the same way across different implementations! The attentive reader will have noticed that the search for counterexamples produces quite different results when used in SWI-Prolog.

In an unexpected turn of events, the above test case has found a discrepancy in the call_cleanup/2 implementations of SWI-Prolog and SICStus. In SWI-Prolog (7.3.11):

?- dif(Det, true), call_cleanup(true, Det=true).
dif(Det, true).

?- call_cleanup(true, Det=true), dif(Det, true).
false.

whereas both queries fail in SICStus Prolog (4.3.2).

This is the quite typical case: Once you are interested in testing a specific property, you find many obstacles that are in the way of testing the actual property.

In the ISO draft proposal, we see:

Failure of [the cleanup goal] is ignored.

In the SICStus documentation of call_cleanup/2, we see:

Cleanup succeeds determinately after performing some side-effect; otherwise, unexpected behavior may result.

And in the SWI variant, we see:

Success or failure of Cleanup is ignored

Thus, for portability, we should actually write labeling_nondet/1 as:

labeling_nondet(Vs) :-
        call_cleanup(labeling(Vs), Det=true),
        dif(Det, true).

There is no guarantee in setup_call_cleanup/3 that it detects determinism, i.e. missing choice points in the success of a goal. The 7.8.11.1 Description draft proposal only says:

c) The cleanup handler is called exactly once; no later than
upon failure of G. Earlier moments are:
If G is true or false, C is called at an implementation
dependent moment after the last solution and after the last
observable effect of G.

So there is currently no requirement that:

setup_call_cleanup(true, true, Det=true)

Returns Det=true in the first place. This is also reflected in the test cases 7.8.11.4 Examples that the draf proposal gives, we find one test case which says:

setup_call_cleanup(true, true, X = 2).
Either: Succeeds, unifying X = 2.
Or: Succeeds.

So its both a valid implementation, to detect determinism and not to detect determinism.