Prolog: why is this a "bad" program?

Question

max(M,N,M):-M >= N,!.
max(M,N,N).

I'm reading a textbook that says the declarative and procedural meanings differ...I don't understand how.

Could someone point me in the right direction?

Answer 1

tl;dr: it's not a relation.

There is a non-green cut in it. Actually a red cut. To see this, remove the cut and you will note that you get two different solutions for

?- max(1,0,N). % without the cut
   N = 1
;  N = 0.

It would be a green cut, if the second clause would read:

max(M,N,N) :- M < N.

What is the exact condition the cut occurs? It is not M >= N but rather a further condition is implied namely, A1 = A3, ... That is not directly visible, as it only shows by the repeated occurrence of a variable:

max(M,N,M):-M >= N,!.
        ^
        |
        + hidden equality

By exploiting that hidden equality, we can easily construct an inconsistent example: Take M and N such that M > N and put N in the third arg (although we know that this is wrong).

?- max(1, 0, 0).   % the original version
true.              % very wrong!
?- max(1, non_number, non_number).
true.              % even wronger!
?- max(an-other, non_number, non_number).
true.              % wrongest!!

To fix this, we have to delay unification after the cut.

max(M,N,R):- M >= N,!, R = M.
max(M,N,N).

Is now everything fixed? Unfortunately not ...

What is the result? Is it a number?

?- max(1+0,0, R).
   R = 1+0.

Not always. Maybe rather take as definition:

max(M,N,R):- M >= N,!, R is M.
max(M,N,R) :- R is N.

What about

?- max(0,N,1).
ERROR: Arguments are not sufficiently instantiated

But .... there is only a single solution to this! Namely, N = 1

Complex, isn't it? Well, originally, Prolog did not do arithmetics at all. It was rather patched into it later on. The best way to currently formulate that relation is to use the current library(clpz) (@SICStus, @Scryer) or its no longer maintained thus less reliable predecessor library(clpfd) (@SWI).

:- op(150, fx, #).   % only needed on SWI
max(M, N, Max) :-
   max(#M,#N) #= #Max.

This now really defines the maximum relation for integers (but not for floats...).

Answer 2

I will leave to someone else to explain the perils of head argument output unifications in the presence of cuts. Instead, let's look into cases where the predicate fails to unify the third argument with the maximum of the first two arguments. We can define the following property that the max/3 predicate should satisfy:

property(M,N,Max) :-
    (   max(M,N,Max) ->
        Max >= M, Max >= N
    ;   nonvar(Max)
    ).

I.e. if max/3 succeeds, then Max must be equal or greater than the first two arguments. If max/3 fails, that must result from a bound third argument that fails to unify with the maximum of the two input arguments.

Let's QuickCheck it using Logtalk's lgtunit implementation (which you can run with most Prolog systems; here I will be using SWI-Prolog):

$ swilgt
...

?- {lgtunit(loader)}.
...
% (0 warnings)
true.

?- [user].
|: max(M,N,M):-M >= N,!.
|: max(M,N,N).

Warning: user://1:102:
Warning:    Singleton variables: [M]
|: property(M,N,Max) :-
|:     (   max(M,N,Max) ->
|:         Max >= M, Max >= N
|:     ;   nonvar(Max)
|:     ).
|: ^D% user://1 compiled 0.01 sec, 3 clauses
true.

Note that we want to generate random tests where the first two arguments are integers but the third argument can be either a variable or an integer:

?- lgtunit::quick_check(property(+integer, +integer, ?integer), [n(20000)]).
*     quick check test failure (at test 5484 after 9 shrinks):
*       property(1,0,0)
false.

As you can see in the reported failure, your definition of the max/3 predicate can fail when called with all arguments bound. The goal max(1,0,0) doesn't unify with the head of the first clause. Thus, the second clause is used resulting in a successful goal where a failure is expected.

We can correct the bug (exposed by QuickCheck) by moving the unification with the output argument to after the cut:

max(M,N,Max):- M >= N,!, Max = M.
max(_,N,N).

But is this definition correct? A quick test with the case above suggest that the bug is fixed:

?- max(1,0,0).
false.

Let's QuickCheck it also (using the same property):

?- lgtunit::quick_check(property(+integer, +integer, ?integer), [n(20000)]).
% 20000 random tests passed
true.

Looks good but remember: QuickCheck can expose bugs but cannot prove that they do not exist. In fact, if we used the default number of tests (100), we could have missed the bug. In some cases, it helps test with a narrow arguments. For example, using the original, buggy, definition of max/3:

?- lgtunit::quick_check(
       property(
           +between(integer,-2,2),
           +between(integer,-2,2),
           ?between(integer,-2,2)
       )
   ).
*     quick check test failure (at test 23 after 0 shrinks):
*       property(1,-1,-1)
false.