Monotonicity vs magic

[dcnorris]

I'm very gradually coming to an understanding of the complaint about clpz's non-monotonicity, and am working toward appreciating its implications (if any) for my own applications to oncology dose-finding trials. After much discussion with @triska, my understanding is currently this: Our bare-minimum expectation for a system is that it will tell us "what holds" or "what there is." So a very worrisome behavior of a system would be that we ask it for "everything", it reports "everything" and then we ask whether a specific thing holds that wasn't in the report, and the system says "oh, yeah — that too."

A system behaving like this loses our confidence, in much the same way as a taxpayer who acknowledges previously unreported income, when confronted with specific bank records.

Anyway ... as I consider assertz(clpz:monotonic) for my own Prolog code, I've undertaken this exploration, which I excerpt here:

%% Exploration of non-monotonicity in CLP(ℤ)

:- use_module(library(clpz)).
:- use_module(library(error)).

n_factorial(0, 1).
n_factorial(N, F) :-
    N #> 0,
    N1 #= N - 1,
    F #= N * F1,
    n_factorial(N1, F1).

%% Although the ordinary programmer might think this is 'pretty cool',
%% for the logic programmer this is perhaps closer to the bare minimum:
%% "Tell me everything that holds."

%?- n_factorial(N, F).
%@    N = 0, F = 1
%@ ;  N = 1, F = 1
%@ ;  N = 2, F = 2
%@ ;  N = 3, F = 6
%@ ;  N = 4, F = 24
%@ ;  N = 5, F = 120
%@ ;  N = 6, F = 720
%@ ;  ...

%% But check THIS out! Does this not seem slightly magical?

%?- n_factorial(N+2, F-1).
%@    N = -1, F = 2
%@ ;  N = 0, F = 3
%@ ;  N = 1, F = 7
%@ ;  N = 2, F = 25
%@ ;  N = 3, F = 121
%@ ;  N = 4, F = 721
%@ ;  N = 5, F = 5041
%@ ;  ...

%% But WAIT A MINUTE! Where's my N = -2, F = 2 answer?
%?- N #= -2, F #= 2, n_factorial(N+2, F-1).
%@ false.

%?- n_factorial(-2+2, 2-1). % <-- very strong 'hints' indeed!
%@ false.

%% Even very strong hints don't help elicit this solution! What went wrong here?
%% Should I have implemented the base case in some more general fashion?

n_fact(Zero, One) :-
    Zero #= 0,
    One #= 1.
n_fact(N, F) :- % identical to general clause of n_factorial/2 above
    N #> 0,
    N1 #= N - 1,
    F #= N * F1,
    n_fact(N1, F1).

%?- n_fact(N+2, F-1).
%@    N = -2, F = 2 % PHEW! We got it this time.
%@ ;  N = -1, F = 2
%@ ;  N = 0, F = 3
%@ ;  N = 1, F = 7
%@ ;  N = 2, F = 25
%@ ;  N = 3, F = 121
%@ ;  N = 4, F = 721
%@ ;  ...

%% All the above was done with non-monotonic clpz:
%?- clpz:monotonic.
%@ false.

%% So what happens if I now demand monotonicity?
%?- assertz(clpz:monotonic).
%@    true.

%?- n_factorial(N, F).
%@    N = 0, F = 1
%@ ;  caught: error(instantiation_error,instantiation_error(unknown(_1384246),1))

%% Oops! I forgot I would have to rewrite to avoid defaulty representation...

m_factorial(0, 1).
m_factorial(N, F) :-
    #N #> 0,
    #N1 #= #N - 1,
    #F #= #N * #F1,
    m_factorial(N1, F1).

%?- m_factorial(N, F).
%@    N = 0, F = 1
%@ ;  N = 1, F = 1
%@ ;  N = 2, F = 2
%@ ;  N = 3, F = 6
%@ ;  N = 4, F = 24
%@ ;  ...

%% So monotonicity doesn't ruin our 'bare minimum' requirements of course.
%% But do we still get the magic?

%?- m_factorial(N-1, F).
%@ caught: error(type_error(integer,_1384249-1),must_be/2) % The magic is gone! 8^(

%?- m_factorial(1, F).
%@    F = 1
%@ ;  false.

%?- m_factorial(10, F).
%@    F = 3628800
%@ ;  false.

%?- m_factorial(N, 6).
%@    N = 3
%@ ;  false.

%% Do I dare ...?
%?- m_factorial(N, 3628800).
%@    N = 10
%@ ;  false.

%?- m_factorial(N, 3628801).
%@ false.

[dcnorris]

Epilogue: I now appreciate that whatever 'magic' there is in getting unexpected behavior from a program (in my application area at least!) is bad magic! So I have modernized my code to use the clean representation with #/1 functor. The git diff is here, and feels totally right now that I've done it. I had worried about 'littering' my 'beautiful' code with #/1 but perhaps you will agree that no actual damage has been done.

[triska]

Wow, thank you for sharing this!

This is, to my knowledge, the first ever use of the monotonic execution mode in an actual application!

I hope that over time, we will be able to gradually make the monotonic execution mode the default, so that this very desirable logical property is guaranteed in applications. Monotonicity is a prerequisite for alternative execution strategies such as iterative deepening, and of course extremely important for reasoning about the code in terms of generalizations and specializations.

[UWN]

There is also a slightly different perspective. Many programs are written in such a manner that they accept "evaluable functors" some times and reject them by silent failure in other cases. This alone is not desirable regardless of the property of monotonicity. In your original case:

?- n_factorial(0, F).
   F = 1
;  false.
?- n_factorial(0-0, F).
false.         % unexpected, given success of all other integer expressions greater than zero
?- n_factorial(1-0, F).
   F = 1
; false.

[lf94]

Could someone explain to me, a new Prolog user, how this is a problem? It appears using negative numbers in a ℤ context will logically lead to weird behavior?... Thank you!

Additionally it'd be nice to know why monotonicity is not the default already? Seems like the natural thing to do when implementing these types of things.

[triska]

@lf94 : "Monotonicity" in this context refers to monotonicity of the logical consequence relation: Logically, weakening constraints that we impose on solutions can never lead to fewer solutions; it can at most lead to more solutions. If adding constraints to a program yields more solutions than before, then the program is not monotonic, and is not amenable to declarative reasoning methods that presuppose this basic logical property which holds in first order predicate logic.

In the current default execution mode, library(clpz) is not monotonic. For example, we have:

?- X #= 5.
   X = 5.

So, according to this answer, X = 5 is the only solution.

But wait! What about the term 2+3? It turns out that it is a solution too, even though the system failed to tell us that:

?- X = 2+3, X #= 5.
   X = 2+3.

On the other hand, if we ask in a slightly different way, which logically ought to be equivalent, the system tells us that 2+3 is in fact not a solution:

?- X #= 5, X = 2+3.
false.

So, which is it? Is 2+3 a solution or not? The fact that this is not entirely clear from the queries above is a fault of the default execution mode that is currently used by library(clpz). Note that all arising numbers in these examples are positive: It is not required to use negative numbers for these problems to arise.

In the monotonic execution mode, these problems do not arise:

?- assertz(clpz:monotonic).
   true.
?- X #= 5.
caught: error(instantiation_error,instantiation_error(unknown(_7721),1))
?- X = 2+3, X #= 5.
   X = 2+3.
?- X #= 5, X = 2+3.
caught: error(instantiation_error,instantiation_error(unknown(_7721),1))

Here, we get clean instantiation errors as an indication that too little is known at the moment to give a definite answer. In contrast to type and domain errors, instantiation errors cannot be replaced by silent failure.

I have not yet enabled the monotonic execution mode by default in order to allow a smoother porting phase of existing programs to Scryer Prolog. However, with more applications depending on the monotonic execution mode due to safety considerations and the increasing necessity and demand for declarative debugging and reasoning methods about Prolog programs, enabling the monotonic execution mode by default becomes ever more tempting. To choose the best time for enabling the monotonic execution mode by default, I greatly appreciate input from Prolog programmers who use Scryer Prolog in their applications!