Much of the work on semantics of logic programs, particularly with negation, attempts to define the (unique) meaning of a logic program. Authors argue that the meaning they define is more natural than any other. For definite programs, the consensus amongst these authors is that the minimum model is the meaning (the set of true atoms). We have argued that this is typically not the case. Furthermore, there is no unique meaning, even for definite programs. Here we consider possible meanings of the merge/3 program (Figure 1) again (in Section 6 we give further examples). An alternative description is as follows (a ``run'' being a maximal sorted sublist):
merge(As, Bs, Cs): Cs is an interleaving of the lists of integers As and Bs and the number of runs in Cs is the maximum number of runs in As and Bs
This could be refined to define the interleaving more precisely. Implementing this second specification (or verifying an implementation) requires different reasoning from the first and the implementation is likely to be used in different ways (a different version of merge sort, for example). The two specifications correspond to distinct three-valued models of merge/3 which are natural and useful. In the first an atom is inadmissible if As or Bs are not sorted lists of numbers. In the second an atom is inadmissible if As or Bs are not lists of integers (for example, with heterogeneous lists of integers and floats an implementation which uses the standard ordering over terms may produce wrong answers). Thus the different interpretations are incomparable. Each interpretation is a model of many reasonable merge/3 programs and some merge/3 programs have both these interpretations (and others) as models.
Ignoring the type of the list elements and comparison operator, our second intended interpretation has more information about how the predicate should behave. Implementers of Prolog built-in and library predicates surely know and care about how their predicates behave at least as much as typical Prolog programmers, but documentation for the various versions of merge/3 almost always restrict attention to sorted lists and I have never seen a more informative high level description used. The description of merge/3 (and many other predicates) can also be made more precise by considering other possible modes. If we say that merge/3 atoms in which the third argument is a sorted list are also admissible we have another model, capturing the fact that merge/3 can work ``backwards'' to nondeterministically split a sorted list into two, assuming a suitable computation rule, or to check if a sorted list can be split into two given terms. We often restrict our attention to certain modes and this leads to less precise understanding of program behaviour from a declarative as well as procedural view. Similarly, most people are taught how to use accumulators in Prolog without gaining a precise high level understanding of the code. Many programmers intend their rev_acc(As, [], Bs) call to succeed if and only if Bs is the reverse of list As but only later, if ever, develop a more informed view of the behaviour when the second argument is a non-empty list (this can certainly be useful) or perhaps even an arbitrary term.