Intended interpretations are not models!

Figure 1: Merging sorted lists of numbers

The major flaw in this otherwise beautiful picture is that, in practice, the intended interpretation is generally not a model. Consider the following informal predicate description.

merge(As, Bs, Cs): Cs is the sorted list of numbers
which is the multiset union of sorted lists As and Bs

This would make a reasonable comment attached to some code (for example, Figure ) or a specification for a programmer (for example, an exercise in an introductory Prolog course). In addition, it might be helpful to say that As and Bs are intended to be input, though there is no notion of input and output in the conventional declarative semantics. Programmers have little difficulty with such descriptions of the intended behaviour of predicates. It could be surmised that such descriptions correspond to intended interpretations of the model theory and that the primary job of a programmer is to construct programs for which such interpretations are models. However, critical examination reveals this to be false, even for very simple programs.

First, the intended interpretation being a model only guarantees soundness (partial correctness or no wrong answers). In reality, some form of completeness is also necessary: if every predicate always fails then the intended interpretation will be a model but the program will not be very useful! Without considering negation, the most obvious way to avoid missing answers is for the intended interpretation to be the minimum model (which is the same as the success set). We discuss another possibility in section 3.5.

Second, consider the first clause for merge/3 (the same as the base case for the well known append/3 program). It can succeed with non-lists, and precisely which calls to merge/3 containing non-lists succeed is a subtle property of the code and not dealt with at all in the predicate description (from the description we might assume that no such calls should succeed). The description is symmetric with respect to the first two arguments but the code is not, and the set of successful calls with non-lists is not. If the code was changed so the first two arguments of each merge/3 atom were swapped, we would have a different definition with a different success set and minimum model. Similarly, we could swap these two arguments in just recursive calls -- either or both of them. Which (if any) of these is correct according to the (single) intended interpretation?