Does `setup_call_cleanup/3` detect determinism portably?

Question

There is a very detailed Draft proposal for setup_call_cleanup/3.

Let me quote the relevant part for my question:

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.

And this example:

setup_call_cleanup(S=1,G=2,write(S+G)).
   Succeeds, unifying S = 1, G = 2.
   Either: outputs '1+2'
   Or: outputs on backtracking '1+_' prior to failure.
   Or (?): outputs on backtracking '1+2' prior to failure.

In my understanding, this is basically because a unification is a backtrackable goal; it simply fails on reexecution. Therefore, it is up to the implementation to decide whether to call the cleanup just after the fist execution (because there will be no more observable effects of the goal), or postpone until the second execution of the goal which now fails.

So it seems to me that this cannot be used to detect determinism portably. Only a few built-in constructs like true, fail, ! etc. are genuinely non-backtrackable.

Is there any other way to check determinism without executing a goal twice? I'm currently using SWI-prolog's deterministic/1, but I'd certainly appreciate portability.

So what do you mean by determinism? The presence of choice-points - that's clearly implementation dependent! You can't even rely on the same result in the very same implementation. SWI is particularly prone to do JIT indexing from-time-to-time but not in a very reproducible manner. — false
@false: I meant the logical one, but any one will do as long as it implies X=2 is deterministic on the top level. — mnish

false false · Accepted Answer · 2016-10-03T15:19:19

No. setup_call_cleanup/3 cannot detect determinism in a portable manner. For this would restrict an implementation in its freedom. Systems have different ways how they implement indexing. They have different trade-offs. Some have only first argument indexing, others have more than that. But systems which offer "better" indexing behave often quite randomly. Some systems do indexing only for nonvar terms, others also permit clauses that simply have a variable in the head - provided it is the last clause. Some may do "manual" choice point avoidance with safe tests prior to cuts and others just omit this. Brief, this is really a non-functional issue, and insisting on portability in this area is tantamount to slowing systems down.

However, what still holds is this: If setup_call_cleanup/3 detects determinism, then there is no further need to use a second goal to determine determinism! So it can be used to implement determinism detection more efficiently. In the general case, however, you will have to execute a goal twice.

The current definition of setup_call_cleanup/3 was also crafted such as to permit an implementation to also remove unnecessary choicepoints dynamically.

It is thinkable (not that I have seen such an implementation) that upon success of Call and the internal presence of a choicepoint, an implementation may examine the current choicepoints and remove them if determinism could be detected. Another possibility might be to perform some asynchronous garbage collection in between. All these options are not excluded by the current specification. It is unclear if they will ever be implemented, but it might happen, once some applications depend on such a feature. This has happened in Prolog already a couple of times, so a repetition is not completely fantasy. In fact I am thinking of a particular case to help DCGs to become more determinate. Who knows, maybe you will go that path!

Here is an example how indexing in SWI depends on the history of previous queries:

?- [user].
p(_,a). p(_,b). end_of_file.

true.

?- p(1,a).
true ;
false.

?- p(_,a).
true.

?- p(1,a).
true.       % now, it's determinate!

Here is an example, how indexing on the second argument is strictly weaker than first argument indexing:

?- [user].
q(_,_). q(0,0). end_of_file.

true.

?- q(X,1).
true ;           % weak
false.

?- q(1,X).
true.

Does `setup_call_cleanup/3` detect determinism portably?

2 Answers