Introduction
xxiii
esting to observe the behaviour of the sequence of iterates s 0 , T (s 0 ), T
2 (s 0 ),
T
3 (s 0 ), . . . of T on the state s 0 . Suppose, for example, that s 0 is the nowhere
defined partial function on the natural numbers, and T is the operator on
the partial functions determined in the usual way by some well-defined recursive definition on the natural numbers, see [Stoltenberg-Hansen et al., 1994],
for example. Then, typically, the sequence of iterates will form an ω-chain
as defined in Chapter 1 and will converge in the Scott topology (defined in
Chapter 3) to the supremum s of the chain; thus, we have s = lim T
n (s 0 ) in
the Scott topology on the partial functions. Furthermore, T will typically be
Scott continuous (see Chapter 3 again for the definition of Scott continuity) in
the sense that T (s) = T (lim s n ) = lim T (s n ) whenever s n is a sequence converging to s in the Scott topology, that is, a sequence satisfying lim s n = s. If
T is indeed Scott continuous, then it is now easy to deduce that T (s) = s so
that s is a fixed point, in fact, the least fixed point, of T . (These observations
are the heart of the proof of Kleene’s theorem, Theorem 1.1.9, which is sometimes viewed as the fundamental theorem in semantics. They are also quite
close in form to the proof of the Banach contraction mapping theorem, Theorem 4.2.3, except that it is order rather than a contraction property which
determines the convergence.) In such a situation, s is usually taken to be the
meaning or semantics of the original recursive definition. Precisely the same
sort of thing happens in relation to logic programming semantics in the case of
logic programs P which do not contain negation or in other words are definite
programs. Specifically, the iterates of the single-step operator (or immediate
consequence operator)
6 T applied to the empty interpretation converge in the
Scott topology to an interpretation M . This interpretation M is the (least)
fixed point of T , captures well the declarative semantics for P , and relates well
to the procedural semantics for P under SLD-resolution, see Theorem 2.2.3
and the discussion following it.
Following on from the comments just made in the previous paragraph is
the interesting observation from our point of view, or the mathematical point
of view, that the discussion just presented can quite easily be generalized: all
that one needs is an abstract notion of convergence and an abstract notion
of continuity. Such a setting is provided by the notion of convergence space,
and in particular by convergence classes or equivalently by topological spaces,
as defined in Chapter 3. These notions provide a general setting in which one
can study semantics and in particular logic programming semantics for logic
programs P which may or may not contain negation. The classical case of
definite programs corresponds to taking the Scott topology, but we consider
quite extensively another topology, called the Cantor topology by us, defined
in Chapter 3, which is closely connected to negation, has connections with the
Scott topology, and underlies important classes of programs which do involve
negation such as acceptable programs and their generalizations, see Chapter 5. Indeed, a quite elementary property we use is given in Proposition 3.3.2
6 See Chapter 2 for the definitions of these terms.
xxiii
esting to observe the behaviour of the sequence of iterates s 0 , T (s 0 ), T
2 (s 0 ),
T
3 (s 0 ), . . . of T on the state s 0 . Suppose, for example, that s 0 is the nowhere
defined partial function on the natural numbers, and T is the operator on
the partial functions determined in the usual way by some well-defined recursive definition on the natural numbers, see [Stoltenberg-Hansen et al., 1994],
for example. Then, typically, the sequence of iterates will form an ω-chain
as defined in Chapter 1 and will converge in the Scott topology (defined in
Chapter 3) to the supremum s of the chain; thus, we have s = lim T
n (s 0 ) in
the Scott topology on the partial functions. Furthermore, T will typically be
Scott continuous (see Chapter 3 again for the definition of Scott continuity) in
the sense that T (s) = T (lim s n ) = lim T (s n ) whenever s n is a sequence converging to s in the Scott topology, that is, a sequence satisfying lim s n = s. If
T is indeed Scott continuous, then it is now easy to deduce that T (s) = s so
that s is a fixed point, in fact, the least fixed point, of T . (These observations
are the heart of the proof of Kleene’s theorem, Theorem 1.1.9, which is sometimes viewed as the fundamental theorem in semantics. They are also quite
close in form to the proof of the Banach contraction mapping theorem, Theorem 4.2.3, except that it is order rather than a contraction property which
determines the convergence.) In such a situation, s is usually taken to be the
meaning or semantics of the original recursive definition. Precisely the same
sort of thing happens in relation to logic programming semantics in the case of
logic programs P which do not contain negation or in other words are definite
programs. Specifically, the iterates of the single-step operator (or immediate
consequence operator)
6 T applied to the empty interpretation converge in the
Scott topology to an interpretation M . This interpretation M is the (least)
fixed point of T , captures well the declarative semantics for P , and relates well
to the procedural semantics for P under SLD-resolution, see Theorem 2.2.3
and the discussion following it.
Following on from the comments just made in the previous paragraph is
the interesting observation from our point of view, or the mathematical point
of view, that the discussion just presented can quite easily be generalized: all
that one needs is an abstract notion of convergence and an abstract notion
of continuity. Such a setting is provided by the notion of convergence space,
and in particular by convergence classes or equivalently by topological spaces,
as defined in Chapter 3. These notions provide a general setting in which one
can study semantics and in particular logic programming semantics for logic
programs P which may or may not contain negation. The classical case of
definite programs corresponds to taking the Scott topology, but we consider
quite extensively another topology, called the Cantor topology by us, defined
in Chapter 3, which is closely connected to negation, has connections with the
Scott topology, and underlies important classes of programs which do involve
negation such as acceptable programs and their generalizations, see Chapter 5. Indeed, a quite elementary property we use is given in Proposition 3.3.2
6 See Chapter 2 for the definitions of these terms.