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.

Olav

courageous question --> +1! – Somnus

The difference between red and green cuts is somehow related to this. – Inadmissible

Green cuts do not change the program's output. They could be missing and the solutions would be the same. I'm talking about programs that use red cuts (like those in the question). – Olav

[red] Cuts and nonvar/1 are essential in my rules for program termination. – Olav

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

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.

Olfe

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!

Somnus

I thought the code is easy to grasp, I tried to implement the simplest relation I could think of. I was interested in those "many other things". – Olav

Some of these many other things are: The same property for each of the 3 arguments. Then for each possible aliasing between the 3 arguments and any of their subterms. Then for each possible partitioning of all these unifications regarding their placement before or after the call. Then all these cases in the other 3 ways: If X succeeds, then Y does not fail; plus the corresponding tests in the other direction. And all these tests for an infinite set of terms in all of these cases. – Somnus

you write "if ?- plus(X, _, _), X = T fails for any term T, then ?- X = T, plus(X, _, _) [must] not succeed" is X a var here? T a more ground term? is specifying X before calling plus the specialization here? perhaps something a little bit off there in that statement, or I don't understand something. why plus(X, _, _), X = T is more general than X = T, plus(X, _, _)? – Baillieu

Yes, I had the small special case of X being a variable primarily in mind in this example, but the property must of course hold for all terms X, including variables, otherwise we cannot call the predicate a true relation. Likewise, it must hold for T being any term, not necessarily ground. A true specialisation would be to just add additional constraints, such as comparing ?- plus(A,_,_). with ?- A = Term, plus(A,_,_). If the latter succeeds, then so must the former, otherwise we cannot call this a true relation. Likewise, commutativity (A,B = B,A) must also be preserved. – Somnus