3

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.

Community
  • 1
  • 1
mnish
  • 385
  • 2
  • 11
  • 1
    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 Oct 03 '16 at 14:42
  • 1
    @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 Oct 03 '16 at 15:14

2 Answers2

3

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.
Community
  • 1
  • 1
false
  • 10,264
  • 13
  • 101
  • 209
  • Thank you very much. I naively thought of a lattice of some well-behaving implementations, so that the presence of choicepoints and determinism could be reasoned in some orderly manner. Things turned out to be much more involved than that! Your advice to use it as an optimization is nice, I will do that in my code. – mnish Oct 04 '16 at 12:10
  • @mnish: If you have a certain algebraic leaning, I recommend you look at the notion of a [tag:failure-slice]. There you have it all: lattices, anti-chains, you name it! [Start here](http://stackoverflow.com/a/10141181/772868). – false Oct 04 '16 at 18:49
  • Now things are much clearer! Is it correct to say a 'cut' is only guaranteed to cut the pending "successes and observable effects" in scope, and not some implementation-dependent object? For example in `call(((true;long_failing_branch),!))`, this `!` is actually a no-op? – mnish Oct 05 '16 at 13:25
  • @mnish: You mean probably `setup_call_cleanup(true, ((true;long_failing_branch),!), Cleanup)` ... This cut will remove all CP in its scope, but it **might** again introduce a new CP! Since you can add `(true;false)` whereever you like. This includes also the place in `Call` immediately after the cut. Only a cut after `setup_call_cleanup/3` guarantees to execute the `Cleanup`. – false Oct 05 '16 at 13:29
1

As you're interested in portability, Logtalk's lgtunit tool defines a portable deterministic/1 predicate for 10 of its supported backend Prolog compilers:

http://logtalk.org/library/lgtunit_0.html https://github.com/LogtalkDotOrg/logtalk3/blob/master/tools/lgtunit/lgtunit.lgt (starting around line 1051)

Note that different systems use different built-in predicates that approximate the intended functionality.

Paulo Moura
  • 18,373
  • 3
  • 23
  • 33
  • What happens for `deterministic((X=1;X=2))` and `deterministic(false)`? – false Oct 04 '16 at 12:02
  • 1
    Supporting 10 implementations! I will sure look into LogTalk. Nice to see there is a QuickCheck for Prolog too. Error reporting is always hard ;-) – mnish Oct 04 '16 at 13:58
  • @false With such a wide choice of supported backend Prolog compilers, plus the documentation linked above, what prevents you from finding the answers to your own question? – Paulo Moura Oct 04 '16 at 14:29
  • @PauloMoura: I did read the documentation which did not mention the case at all. – false Oct 04 '16 at 14:36
  • @mnish: Note that `deterministic/1` will most probably not reflect what you are after. – false Oct 04 '16 at 14:59
  • @false: Paulo's or SWI's? What I'm really after is the implication `a goal is provably deterministic in the debug version ===> it is provably deterministic in the release` (without re-execution). But I must conclude that this is not possible. – mnish Oct 05 '16 at 13:32
  • @mnish: Paulo can only base his definition of `deterministic/1` on existing implementations where he has no influence on the way how CPs are created or avoided. You assertion sounds reasonable, but at least what concerns SWI, it does not hold - as I have shown in my first example (about the influence of history). – false Oct 05 '16 at 13:35