29
The Semantics of Logic Programs
conditions. This selection is often most conveniently described by an operator,
mapping interpretations to interpretations, whose fixed points are exactly the
models being sought. In this section, we will introduce the first of a number of
operators we study in the context of declarative semantics, namely, the singlestep or immediate consequence operator due to Kowalski and van Emden,
see [van Emden and Kowalski, 1976]. The single-step operator was historically
the first to be studied in relation to logic programming semantics and in
many ways is the most natural. Indeed, it turns out that for definite programs
the single-step operator is order continuous and that its least fixed point, as
given by Kleene’s theorem, Theorem 1.1.9, accords well with a programmer’s
expectations of what a declarative semantics should be and how it should
relate to the procedural semantics.
5
For the remainder of this section and for the next, we will work in classical
two-valued logic. Hence, I P or I P,J means I P,J,2 here and in the subsequent
section, where J is a given preinterpretation, and we will on occasions remind
the reader of this notational convenience.
The following is an important definition.
2.2.1 Definition Let P be a normal logic program, and let J be a preinterpretation for L P . The single-step operator or immediate consequence operator
T P,J : I P,J → I P,J is defined, for I ∈ I P,J , by setting T P,J (I) to be the set
of all A ∈ B P,J for which there is a clause A ← L 1 , . . . , L n in ground J (P )
satisfying I |= L 1 ∧ . . . ∧ L n , that is, satisfying I(L 1 ∧ . . . ∧ L n ) = t.
Consistent with our earlier remarks concerning notation, we will usually
denote T P,J simply by T P when J is understood. Furthermore, we will sometimes find it convenient to refer to T P as the T P -operator .
The importance of the immediate consequence operator is clear from the
following proposition.
2.2.2 Proposition The models for P are exactly the pre-fixed points of T P .
Proof: Let I ∈ I P be a model for P , and let A ∈ T P (I). Then there is a
clause A ← L 1 , . . . , L n in ground(P ) with I(L 1 ∧ . . . ∧ L n ) = t; let us denote
this clause by C. Since I is a model for P , we have I(C) = t. Hence, I(A) = t,
and so A ∈ I, giving T P (I) ⊆ I, as required.
Conversely, suppose T P (I) ⊆ I, and let A ← L 1 , . . . , L n be a clause C in
ground(P ) with I(L 1 ∧ . . . ∧ L n ) = t. Then A ∈ T P (I) ⊆ I. Hence, I(A) = t,
and in consequence I(C) = t, as required.
•
The notion of model is far too general to capture the declarative semantics
of logic programs without some restrictions being imposed upon it. Indeed, B P
itself is always a model for P , but in general B P fails by far to give a reasonable “intended meaning” for a program. Standard approaches to declarative
5 As already noted, we will not consider procedural aspects in depth and instead refer
the reader to [Apt, 1997, Lloyd, 1987] for details of procedural semantics.
Précédent

- 60/305

Suivant