Purity of Prolog predicates that use impure primitives

Question

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:

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

---

This question follows the discussion on this answer.

Answer 1

1. 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 ...

?- plus(3,2,3+2).
false.

?- plus(3,2,3+b).
ERROR: </2: Arithmetic: `b/0' is not a function

?- plus(3,2,3+Z).
ERROR: </2: Arguments are not sufficiently instantiated

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.

2. 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.

Answer 2

Regarding the question "is the above plus/3 really pure?" I can only say: I have no idea which properties are preserved here, because the code, due to all these extra-logical predicates, is so complicated and hard to follow that it is hard to tell what it is actually doing. And I really must say doing in this case, because this is far from declarative code that is describing something we can comparatively easily talk about. All kinds of properties we expect from declarative code may be destroyed in this case.

The best way to generally prove that a relation is pure is to restrict yourself to the pure and monotonic subset of Prolog. It is for this reason that this property is so important, because this subset is closed under composition. Once you leave this subset, it quickly gets really hard to prove any properties whatsoever about your programs, as your example nicely demonstrates.

For example, to prove your plus/3 monotonic, you need to show, among many other things, that if ?- plus(X, _, _), X = T fails for any term T, then ?- X = T, plus(X, _, _) does not succeed. Since it is in general not decidable whether a query fails, loops or succeeds and we therefore in general cannot even determine a single side of this implication, let alone both, I can only say: Good luck with that!