Document non counted backtracking

[hurufu]

While reading loader.pl module it was not obvious to me at all what exactly does non_counted_backtracking to the predicates and should I use it for new predicates in that module or not. After reading sources I came up with new documentation. Basically there is a single counter which is incremented on every instruction that is an "inference", but for "default" instructions (instructions that start with default_ prefix) that counter isn't incremented and isn't checked. When counter reaches a limit (defined for example when you use call_with_inference_limit/3) it forces unconditional exit and stops evaluating rest of instructions (I hope I got that part right).

UPDT:
There is only a single inference counter and a single variable that holds a max inference limit, that's why when you use nested calls to call_with_inference_limit/3 old limit value is overwritten. I don't know exactly how it behaves on backtracking though.

[triska]

It is very important that nesting of call_with_inference_limit/3 calls works as expected, with each call limiting the inferences of its goal correctly, and independent of what other (surrounding or inner) limits say.

From a few quick tests, this also seems to work as expected. For instance, with the following definition:

natnum(0).
natnum(s(N)) :- natnum(N).

I get:

?- call_with_inference_limit(natnum(N), 10, R).
   N = 0, R = true
;  N = s(0), R = true
;  N = s(s(0)), R = true
;  N = s(s(s(0))), R = true
;  N = s(s(s(s(0)))), R = true
;  R = inference_limit_exceeded.

?- call_with_inference_limit(call_with_inference_limit(natnum(N), 10, R), 3, R).
   N = 0, R = true
;  R = inference_limit_exceeded.

?- call_with_inference_limit(call_with_inference_limit(natnum(N), 10, R), 10_000, R).
   N = 0, R = true
;  N = s(0), R = true
;  N = s(s(0)), R = true
;  N = s(s(s(0))), R = true
;  N = s(s(s(s(0)))), R = true
;  R = inference_limit_exceeded.

Note especially the second example, where the outer limit (3) is lower than the inner limit (10), and therefore the outer limit is the limiting factor here, as expected. Whereas in the last example, the inner limit is the lower bound, yielding the same answer as the first query, also as expected.

If nesting were not to work as expected, then that would itself be a major mistake in the implementation! Could you please give an example of where a limit gets unexpectedly "overwritten" in nested calls, i.e., any call unexpectedly gaining or losing more inferences than stated in that call?

[hurufu]

My observations are superficial and might not be correct, but I came up with the following example:

:- use_module(library(iso_ext)).

p :- call_with_inference_limit(p, 5, _).
p :- call_with_inference_limit(p, 5, _).

And the following query:

?- call_with_inference_limit(p, 10, B).
   B = true
;   % non-termination (unexpected?)

It's a contrived example, and I don't understand exact details of how inference counting works, so my explanations in original post are handy-wavy.

[hurufu]

I think that infinite loop happens, because counter is constantly getting reset and it never reaches the inference limit (5 in this case).

[triska]

Excellent catch! I have filed #2535 for this!

[triska]

This documents behaviour that is wrong!

In particular:

1. non_counted_backtracking should not be an operator, since it makes Scryer not strictly conforming. (already discussed in Assorted small fixes #2533, comment apparently no longer visible).
2. nesting of call_with_inference_limit/3 should work correctly, see Nesting call_with_inference_limit/3 does not reliably limit the inferences #2535.

[hurufu]

For the first I think it might be fixed easily by removing op/3 from ops_and_meta_predicate.pl file, and defining this operator only in modules that actually use it. Do you think it's a good idea?

[triska]

Personally, I think there should not be an operator for this at all. We can simply write such directives in functional notation.

[triska]

One other point about this change: implementation specific has a meaning defined in the ISO standard:

3.92 implementation specific: Undefined by this part of
ISO/IEC 13211 but supported by a conforming processor.

NOTE - This part of ISO/IEC 13211 does not require an
implementation specific feature to be supported by a conforming
Processor, but it preserves the syntax and semantics of a strictly
conforming Prolog text which does not use it, for example,
defining a term order on variables, or defining unification for
terms which are STO (3.165).

I see no reason to remove this information from the documentation (which this PR did).

We have:

5.5.2 Predefined operators

A processor may support one or more additional predefined
operators (table 7) as an implementation specific feature.

This is an independent point, another comment about such documentation changes.

[hurufu]

@triska I've re-added "implementation specific" part. Merged code imho didn't change meaning of the original comment.