Logic programming: From underspecification to undefinedness
Lee Naish, Harald Søndergaard, Benjamin Horsfall · 2012
The semantics of logic programs was originally de-scribed in terms of two-valued logic. Soon, however, it was realised that three-valued logic had some natural advantages, as it provides distinct values not only for truth and falsehood, but also for “undefined”. The three-valued semantics proposed by Fitting and by Kunen are closely related to what is computed by a logic program, the third truth value being associated with non-termination. A different three-valued se-mantics, proposed by Naish, shared much with those of Fitting and Kunen but incorporated allowances for programmer intent, the third truth value being asso-ciated with underspecification. Naish used an (appar-ently) novel “arrow ” operator to relate the intended meaning of left and right sides of predicate definitions. In this paper we suggest that the additional truth values of Fitting/Kunen and Naish are best viewed as duals. We use Fitting’s later four-valued approach to unify the two three-valued approaches. The addi-tional truth value has very little affect on the Fitting three-valued semantics, though it can be useful when finding approximations to this semantics for program analysis. For the Naish semantics, the extra truth value allows intended interpretations to be more ex-pressive, allowing us to verify and debug a larger class of programs. We also explain that the “arrow ” opera-tor of Naish (and our four-valued extension) is essen-tially the information ordering. This sheds new light on the relationships between specifications and pro-grams, and successive executions states of a program. 1