?- integer(X).
false.
Here, the system tells us: “There are no solutions whatsover.“, because this is what "false" means: No solutions whatsoever. But that's wrong, because in fact there are solutions, as we can also verify: ?- integer(0).
true.
So, in fact there are solutions! But that's not what the system said initially. So, this means that we can no longer rely on what the system is saying: In the above example, it tells us that there are no solutions, even though there are solutions.By monotonicity, I expect that if a query succeeds unconditionally, then a generalization certainly does not fail (otherwise, adding a constraint would increase the set of solutions). But this is obviously the case here, so monotonicity is violated: Adding a constraint can make a query succeed that previously failed.
?- integer(X).
false.
?- X = 0, integer(X).
X = 0.
If an instantiation error is raised, then that clearly indicates that no decision can be made at this point, whereas "false" means that there are no solutions whatsoever, which in this case violates monotonicity, a core property we expect to hold when reasoning about logic programs.If monotonicity is broken, then iterative deepening is no longer applicable, because increasing the depth of the search may now invalidate conclusions that were derived earlier. However, one of the foremost attractions of Prolog is the prospect of executing the same program with different evaluation strategies.
And, yes: The above behaviour of integer/1 is in fact prescribed by the ISO standard. Unfortunately, DEC 10 Prolog chose to replace instantiation errors by silent failures, and this has been perpetuated in the Edinburgh tradition for type tests including the standard.
A way to correct this is therefore to introduce a new family of type tests, the ..._si/1 family of predicates as available in library(si). They are what the standard type tests should have been in the first place to preserve these desirable logical properties.