xxvi
Introduction
operators we discuss. Such sets themselves may be endowed with various, useful structures. In Chapter 3, we illustrate the point just made by studying
various topologies on spaces of interpretations, including the Scott topology
and a topology called the Cantor topology, as already mentioned. The continuity of semantic operators in the Scott topology is examined in Chapter 3,
but the treatment of their continuity in the Cantor topology is deferred until
we reach Chapter 5, where the results are needed. In fact, as noted earlier, it
is convergence in these topologies which is of main interest because it can be
used to find models for logic programs as we show in Chapters 5 and 6, and
thus, convergence is the dominant theme in our development of topology.
We take the theme of structures defined on spaces of interpretations yet
further in Chapter 4 in presenting a detailed account of both various generalized distance functions defined on spaces of interpretations and their associated fixed-point theorems. These tools, some of which depend on level
mappings again, are developed specifically for investigating semantic operators of logic programs with negation, but we believe that Chapter 4 is a
self-contained account of results which are likely to have applications within
computer science outside those areas considered here. In Chapter 5, we combine the developments of Chapters 2, 3, and 4 by applying the fixed-point
theorems of Chapter 4 to the more important semantic operators introduced
in Chapter 2. More specifically, we focus on classes of programs, which we
call unique supported model classes, each of which has the property that all
programs in that class have a unique supported model. An example of such
a class is the class of acceptable programs well-known in termination analysis, but we examine other important unique supported model classes as well.
These classes are interesting because it turns out that for each of the programs
they contain, many of the main semantics studied in the earlier chapters coincide, and hence the meaning of each program in a unique supported model
class is unambiguous relative to the most important semantics. In essence,
we obtain these classes by applying to various semantic operators those fixedpoint theorems of Chapter 4 which guarantee a unique fixed point, if there
is a fixed point at all. The process involves working with successively more
general semantic operators, especially Fitting-style operators, and examining
their properties in relation to single-step operators and convergence of their
iterates in the Cantor topology studied in Chapter 3. Indeed, the process culminates in a very general semantic operator T which subsumes many of those
studied in the earlier chapters, and we estabish many of its important properties in Chapter 5. In particular, we examine in depth the continuity of T in the
Cantor topology, thereby obtaining the corresponding results for single-step
operators and Fitting-style operators. Finally, we note that the work we do
in this chapter consolidates the uniform approach provided in Chapter 2, employing level mappings, to encompass the additional semantics we introduce
in Chapter 5.
Turning now to Chapter 6, our objectives here are twofold. First, we revisit
the stable model semantics and establish a close connection between the well
Introduction
operators we discuss. Such sets themselves may be endowed with various, useful structures. In Chapter 3, we illustrate the point just made by studying
various topologies on spaces of interpretations, including the Scott topology
and a topology called the Cantor topology, as already mentioned. The continuity of semantic operators in the Scott topology is examined in Chapter 3,
but the treatment of their continuity in the Cantor topology is deferred until
we reach Chapter 5, where the results are needed. In fact, as noted earlier, it
is convergence in these topologies which is of main interest because it can be
used to find models for logic programs as we show in Chapters 5 and 6, and
thus, convergence is the dominant theme in our development of topology.
We take the theme of structures defined on spaces of interpretations yet
further in Chapter 4 in presenting a detailed account of both various generalized distance functions defined on spaces of interpretations and their associated fixed-point theorems. These tools, some of which depend on level
mappings again, are developed specifically for investigating semantic operators of logic programs with negation, but we believe that Chapter 4 is a
self-contained account of results which are likely to have applications within
computer science outside those areas considered here. In Chapter 5, we combine the developments of Chapters 2, 3, and 4 by applying the fixed-point
theorems of Chapter 4 to the more important semantic operators introduced
in Chapter 2. More specifically, we focus on classes of programs, which we
call unique supported model classes, each of which has the property that all
programs in that class have a unique supported model. An example of such
a class is the class of acceptable programs well-known in termination analysis, but we examine other important unique supported model classes as well.
These classes are interesting because it turns out that for each of the programs
they contain, many of the main semantics studied in the earlier chapters coincide, and hence the meaning of each program in a unique supported model
class is unambiguous relative to the most important semantics. In essence,
we obtain these classes by applying to various semantic operators those fixedpoint theorems of Chapter 4 which guarantee a unique fixed point, if there
is a fixed point at all. The process involves working with successively more
general semantic operators, especially Fitting-style operators, and examining
their properties in relation to single-step operators and convergence of their
iterates in the Cantor topology studied in Chapter 3. Indeed, the process culminates in a very general semantic operator T which subsumes many of those
studied in the earlier chapters, and we estabish many of its important properties in Chapter 5. In particular, we examine in depth the continuity of T in the
Cantor topology, thereby obtaining the corresponding results for single-step
operators and Fitting-style operators. Finally, we note that the work we do
in this chapter consolidates the uniform approach provided in Chapter 2, employing level mappings, to encompass the additional semantics we introduce
in Chapter 5.
Turning now to Chapter 6, our objectives here are twofold. First, we revisit
the stable model semantics and establish a close connection between the well