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.
Note that there is the ISO built-in
ground/1
which is just as impure asnonvar/1
. But it seems you are rather talking about the conditions forwhen/2
. In fact, any accepted condition forwhen/2
is as pure as it can get. So this is not only true forground/1
.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 explicitly1 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 flagunknown
(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
These
when/2
s, while perfectly correct, now contribute a lot to producing inconsistencies as answers. After all, above reads:Contrast this to SICStus' or SWI's
library(clpfd)
:So
library(clpfd)
is capable of detecting this inconsistency, whereaswhen/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: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, likelength(L,0+0)
fails butlength(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
:So
plus/3
was not "multi-directional".