What are the requirements a computer function must meet to be considered "monotonic"?

Question

What are the requirements a computer function/procedure/predicate must meet to be considerd "monotonic"?

Let A be some thing ,
Let B be some thing ,
Let R be a monotonic relationship between A and B ,
Let R_ be a non-monotonic relationship between A and B ,
Let R become false if R_ is true ,
Let R_ become true if R is false ,
Let C be a constraint in consideration of R ,
Let C become false if R_ is true ,
Let D be the collection of constraints C (upon relationship R) .

**What is D ?**

I have reviewed some literature, e.g. a Wikipedia article "monotonic function". I am most interested in a practical set of criteria I can apply when pragmatically involved with computer programming. What are some tips and best practices I should follow when creating and designing my functions, such that they are more likely to be "monotonic"?

Answer 1

In logic programming, and also in logic, the classification "monotonic" almost invariably refers to monotonicity of entailment.

This fundamental property is encountered for example in classical first-order logic: When you are able to derive a consequence from a set of clauses, then you can also derive the consequence when you extend the set of clauses. Conversely, removing a clause does not entail consequences that were previously not the case.

In the pure subset of Prolog, this property also holds, from a declarative perspective. We therefore sometimes call it the pure monotonic subset of Prolog, since impurities do not completely coincide with constructs that destroy monotonicity.

Monotonicity of entailment is the basis and sometimes even necessary condition for several approaches that reason over logic programs, notably declarative debugging.

Note that Prolog has several language constructs that may prevent such reasoning in general. Consider for example the following Prolog program:

f(a).
f(b).
f(c).

And the following query:

?- setof(., f(X), [_,_]).
false.

Now I remove one of the facts from the program, which I indicate by strikethrough text:

f(a) :- false.
f(b).
f(c).

If Prolog programs were monotonic, then every query that previously failed would definitely now fail all the more, since I have removed something that was previously the case.

However, we now have:

?- setof(X, f(X), [_,_]).
true.

So, setof/3 is an example of a predicate that violates monotonicity!