Steadfastness: Definition and its relation to logical purity and termination

Question

So far, I have always taken steadfastness in Prolog programs to mean:

If, for a query Q, there is a subterm S, such that there is a term T that makes ?- S=T, Q. succeed although ?- Q, S=T. fails, then one of the predicates invoked by Q is not steadfast.

Intuitively, I thus took steadfastness to mean that we cannot use instantiations to "trick" a predicate into giving solutions that are otherwise not only never given, but rejected. Note the difference for nonterminating programs!

In particular, at least to me, logical-purity always implied steadfastness.

---

Example. To better understand the notion of steadfastness, consider an almost classical counterexample of this property that is frequently cited when introducing advanced students to operational aspects of Prolog, using a wrong definition of a relation between two integers and their maximum:

integer_integer_maximum(X, Y, Y) :-
        Y >= X,
        !.
integer_integer_maximum(X, _, X).

A glaring mistake in this—shall we say "wavering"—definition is, of course, that the following query incorrectly succeeds:

?- M = 0, integer_integer_maximum(0, 1, M).
M = 0. % wrong!

whereas exchanging the goals yields the correct answer:

?- integer_integer_maximum(0, 1, M), M = 0.
false.

A good solution of this problem is to rely on pure methods to describe the relation, using for example:

integer_integer_maximum(X, Y, M) :-
        M #= max(X, Y).

This works correctly in both cases, and can even be used in more situations:

?- integer_integer_maximum(0, 1, M), M = 0.
false.

?- M = 0, integer_integer_maximum(0, 1, M).
false.

| ?- X in 0..2, Y in 3..4, integer_integer_maximum(X, Y, M).
X in 0..2,
Y in 3..4,
M in 3..4 ? ;
no

---

Now the paper Coding Guidelines for Prolog by Covington et al., co-authored by the very inventor of the notion, Richard O'Keefe, contains the following section:

5.1 Predicates must be steadfast.

Any decent predicate must be “steadfast,” i.e., must work correctly if its output variable already happens to be instantiated to the output value (O’Keefe 1990).

That is,

?- foo(X), X = x.

and

?- foo(x).

must succeed under exactly the same conditions and have the same side effects. Failure to do so is only tolerable for auxiliary predicates whose call patterns are strongly constrained by the main predicates.

Thus, the definition given in the cited paper is considerably stricter than what I stated above.

For example, consider the pure Prolog program:

nat(s(X)) :- nat(X).
nat(0).

Now we are in the following situation:

?- nat(0).
true.

?- nat(X), X = 0.
nontermination

This clearly violates the property of succeeding under exactly the same conditions, because one of the queries no longer succeeds at all.

Hence my question: Should we call the above program not steadfast? Please justify your answer with an explanation of the intention behind steadfastness and its definition in the available literature, its relation to logical-purity as well as relevant termination notions.

Answer 1

In 'The craft of prolog' page 96 Richard O'Keef says 'we call the property of refusing to give wrong answers even when the query has an unexpected form (typically supplying values for what we normally think of as inputs*) steadfastness'

*I am not sure if this should be outputs. i.e. in your query ?- M = 0, integer_integer_maximum(0, 1, M). M = 0. % wrong! M is used as an input but the clause has been designed for it to be an output.

In nat(X), X = 0. we are using X as an output variable not an input variable, but it has not given a wrong answer, as it does not give any answer. So I think under that definition it could be steadfast.

A rule of thumb he gives is 'postpone output unification until after the cut.' Here we have not got a cut, but we still want to postpone the unification.

However I would of thought it would be sensible to have the base case first rather than the recursive case, so that nat(X), X = 0. would initially succeed .. but you would still have other problems..