Purity of Prolog predicates that use impure primitives

I know that var/1, nonvar/1 and !/0 are impure primitives, but does their use make every program that uses them impure?

I wrote the following predicate plus/3 that behaves as if it were pure or at least that is what I claim. The predicate is demonstrative, not designed to be efficient.

% nat(X) is true if X is a natural number

nat(0).
nat(X):- nonvar(X), !, X > 0.
nat(X):- nat(X1), X is X1 + 1.

% plus(A, B, C) is true if A,B and C are natural numbers and A+B=C

plus(A, B, C):-
    nat(A),
    (nonvar(C), C < A, !, false ; true),
    plus_(B, A, C).

plus_(A, B, C):-
    nat(A),
    (nonvar(C), C < A, !, false ; true),
    C1 is A + B,
    (C = C1 ; nonvar(C), C < C1, !, false).

I have two questions:

Is the above predicate plus/3 really pure?
In general, how can you prove that a particular relation has logical purity?

This question follows the discussion on this answer.

Solution

Is the above predicate plus/3 really pure?

It has some odd behavior: Sometimes it accepts arithmetic expressions, and sometimes not ; and this although all arguments are evaluated:

?- plus(3,5-3,5).
   true
;  false.
?- plus(3,2,3+2).
   false.
?- plus(3,2,3+b).
   error(type_error(evaluable,b/0),(is)/2).
?- plus(3,2,3+Z).
   error(instantiation_error,(is)/2).

I would rather be concerned about the inefficiency of nat/1 for cases like:

?- time( ( nat(X), X > 9999 ) ).
% 50,025,002 inferences, 27.004 CPU in 27.107 seconds (100% CPU, 1852480 Lips)
X = 10000 ;
% 10,006 inferences, 0.015 CPU in 0.015 seconds (99% CPU, 650837 Lips)
X = 10001 ;
% 10,005 inferences, 0.016 CPU in 0.016 seconds (99% CPU, 631190 Lips)
X = 10002 ...

So, it looks to me that your definition is pure. However, this very style of programming makes it quite difficult to guarantee this property. A minimal change will have disastrous effects.

In general, how can you prove that a particular relation has logical purity?

The easiest way is by construction. That is, by using only pure monotonic building blocks. I.e., Prolog without any built-ins and using only conjunction and disjunction of regular goals. Any program built this manner will be pure and monotonic, too. Then, execute this program with Prolog flag occurs check set to true or error.

Add to this pure built-ins like (=)/2 and dif/2.

Add to this built-ins that try to emulate pure relations and that produce instantiation errors when they are unable to do so. Think of (is)/2 and the arithmetic comparison predicates. Some of these are quite on the borderline like call/N which might call some impure predicates.

Add library(clpfd) with flag clpfd_monotonic set to true.

Many constructs are fine and pure for certain uses, but impure for others. Think of if-then-else which is perfect for arithmetic comparison:

 ..., ( X > Y -> ... ; ... ), ...

but which does not work together with a pure goal like

 ..., ( X = Y -> ... ; ... ), ...  % impure

What remains are impure built-ins that can be used to construct predicates that behave in a pure manner ; but whose definition as such is no longer pure.

As an example, consider truly green cuts. These are extremely rare, and even rarer here on SO. See this and that.

Another common pattern to provide a pure relation are conditionals like:

..., ( var(V) -> something with var ; the equivalent with nonvar ), ...

And to guard against cases that are not cleanly covered, errors can be thrown.