Logical purity of when/2 and ground/1

The question

I have a question related to logical purity.

Is this program pure?

when(ground(X), X > 2).

Some [ir]relevant details about the context

I'm trying to write pure predicates with good termination properties. For instance, I want to write a predicate list_length/2 that describes the relation between a list and its length. I want to achieve the same termination behaviour as the built-in predicate length/2.

My question seeks to find if the following predicate is pure:

list_length([], 0).
list_length([_|Tail], N):-
    when(ground(N), (N > 0, N1 is N - 1)),
    when(ground(N1), N is N1 + 1),
    list_length(Tail, N1).

I can achieve my goal with clpfd ...

:- use_module(library(clpfd)).
:- set_prolog_flag(clpfd_monotonic, true).

list_length([], 0).
list_length([_|Tail], N):-
    ?(N) #> 0,
    ?(N1) #= ?(N) - 1,
    list_length(Tail, N1).

... or I can use var/1, nonvar/1 and !/0, but then is hard to prove that the predicate is pure.

list_length([],0).
list_length([_|Tail], N):-
    nonvar(N), !,
    N > 0,
    N1 is N - 1,
    list_length(Tail, N1).
list_length([_|Tail], N):-
    list_length(Tail, N1),
    N is N1 + 1.

Logical purity of when/2 and ground/1

Note that there is the ISO built-in ground/1 which is just as impure as nonvar/1. But it seems you are rather talking about the conditions for when/2. In fact, any accepted condition for when/2 is as pure as it can get. So this is not only true for ground/1.

Is this program pure?
when(ground(X), X > 2).

Yes, in the current sense of purity. That is, in the very same sense that considers library(clpfd) as pure. In the very early days of logic programming and Prolog, say in the 1970s, a pure program would have been only one that succeeds if it is true and fails if it is false. Nothing else.

However, today, we accept that ISO errors, like type errors are issued in place of silent failure. In fact, this makes much more sense from a practical point of view. Think of X = non_number, when(ground(X), X > 2 ). Note that this error system was introduced relatively late into Prolog.

While Prolog I reported errors of built-ins explicitly¹ the subsequent DEC10-Prolog (as of, e.g. 1978, 1982) nor C-Prolog did not contain a reliable error reporting system. Instead, a message was printed and the predicate failed thus confusing errors with logical falsity. From this time, there is still the value warning of the Prolog flag unknown (7.11.2.4 in ISO/IEC 13211-1:1995) which causes the attempt to execute an undefined predicate to print a warning and fail.

So where's the catch? Consider

?- when(ground(X), X> 2), when(ground(X), X < 2).
when(ground(X), X>2),
when(ground(X), X<2).

These when/2s, while perfectly correct, now contribute a lot to producing inconsistencies as answers. After all, above reads:

Yes, the query is true, provided the very same query is true.

Contrast this to SICStus' or SWI's library(clpfd):

| ?- X #> 2, X #< 2.
no

So library(clpfd) is capable of detecting this inconsistency, whereas when/2 has to wait until its argument is ground.

Getting such conditional answers is often very confusing. In fact, many prefer in many situations a more mundane instantiation error to the somewhat cleaner when.

There is no obvious general answer to this. After all, many interesting theories for constraints are undecidable. Yes, the very harmless-looking library(clpfd) permits you to formulate undecidable problems already! So we will have to live with such conditional answers that do not contain solutions.

However, once you get a pure unconditional solution or once you get real failure you do know that this will hold.

`list_length/2`

Your definition using library(clpfd) is actually slightly better w.r.t. termination than what has been agreed upon for the Prolog prologue. Consider:

?- N in 1..3, list_length(L, N).

Also, the goal length(L,L) produces a type error in a very natural fashion. That is, without any explicit tests.

Your version using when/2 has some "natural" irregularities, like length(L,0+0) fails but length(L,1+0) succeeds. Otherwise it seems to be fine — by construction alone.

1) The earliest account is on p.9 of G. Battani, H. Meloni. Interpréteur du langage de programmation Prolog. Rapport de D.E.A. d'informatique appliquée, 1973. There, a built-in in error was replaced by a goal that was never resolved. In current terms plus/3 of II-3-6 a, p.13 would be in current systems with freeze/2:

plus(X, Y, Z) :-
   (  integer(X), integer(Y), ( var(Z) ; integer(Z) )
   -> Z is X+Y
   ;  freeze(_,erreur(plus(X,Y,Z)))
   ).

So plus/3 was not "multi-directional".