xxii
Introduction
sociate with the program one or more of a number of operators called semantic
operators
4 defined on spaces of interpretations (or valuations) determined by
the program. One then studies the fixed points of these operators, leading to
the fixed-point semantics of the program in question. This latter semantics
can roughly be equated with the denotational semantics of imperative and
functional programs associated with the names of Dana Scott and Christopher Strachey because some, but not all, of the important semantic operators
which have been introduced are Scott continuous in the sense of domain theory, or at least are monotonic. Moreover, fixed points play a fundamental role
also in denotational semantics. Finally, there is a general requirement that
all the semantics described previously should coincide or at least be closely
related in some sense.
5
Taking the observations just made a little further forward, we note that
there are several interconnected strands to the programme of analyzing the
fixed points of semantic operators, but three of the main ones are as follows.
First, we consider a number of operators already well-known in the theory, in
addition to introducing several more. In this step, we focus on ensuring that
the operators we study, and their fixed points, correctly reflect the meaning
of programs and their properties. Second, we investigate the properties of the
operators themselves, especially in relation to whether or not they are Scott
continuous and, if not, what properties they do possess. Scott continuity is a
desirable feature for a semantic operator to have because it implies that the
operator has a least fixed point. Furthermore, this least fixed point is often
taken to be the fixed-point semantics of the program in question, and indeed,
operators which are not Scott continuous may in general fail to have any fixed
points at all. Third, we study the fixed-point theory of semantic operators in
considerable generality. In fact, the failure of certain apparently reasonable
semantic operators (already known to capture declarative semantics) to be
Scott continuous often results from the introduction of negation, because the
introduction of negation may render the operators in question to be nonmonotonic and hence to fail to be Scott continuous, as we will see in Chapter 2.
The point just made is important because it is one of the reasons for
introducing alternatives to order theory in studying fixed-point theory in relation to semantics and in establishing fixed-point theorems applicable to nonmonotonic operators, see Chapter 4. Therefore, it will help to give some insight next into the non-traditional methods we introduce and develop, how
they work in the context of negation, and especially how they work in finding models for logic programs with negation. Our point of view is to regard
programs, and logic programs in particular, as (abstract) dynamical systems
whose states change under program execution and whose state changes can be
modelled by an operator T . Starting with some initial state, s 0 , say, it is inter4 This is a generic term which we use to cover all of a number of specific operators we
will study, such as the T P -operator, see Definition 2.2.1.
5 See Theorem 2.2.3, for example, and [Lloyd, 1987] for details of how procedural semantics relates to declarative semantics.
Introduction
sociate with the program one or more of a number of operators called semantic
operators
4 defined on spaces of interpretations (or valuations) determined by
the program. One then studies the fixed points of these operators, leading to
the fixed-point semantics of the program in question. This latter semantics
can roughly be equated with the denotational semantics of imperative and
functional programs associated with the names of Dana Scott and Christopher Strachey because some, but not all, of the important semantic operators
which have been introduced are Scott continuous in the sense of domain theory, or at least are monotonic. Moreover, fixed points play a fundamental role
also in denotational semantics. Finally, there is a general requirement that
all the semantics described previously should coincide or at least be closely
related in some sense.
5
Taking the observations just made a little further forward, we note that
there are several interconnected strands to the programme of analyzing the
fixed points of semantic operators, but three of the main ones are as follows.
First, we consider a number of operators already well-known in the theory, in
addition to introducing several more. In this step, we focus on ensuring that
the operators we study, and their fixed points, correctly reflect the meaning
of programs and their properties. Second, we investigate the properties of the
operators themselves, especially in relation to whether or not they are Scott
continuous and, if not, what properties they do possess. Scott continuity is a
desirable feature for a semantic operator to have because it implies that the
operator has a least fixed point. Furthermore, this least fixed point is often
taken to be the fixed-point semantics of the program in question, and indeed,
operators which are not Scott continuous may in general fail to have any fixed
points at all. Third, we study the fixed-point theory of semantic operators in
considerable generality. In fact, the failure of certain apparently reasonable
semantic operators (already known to capture declarative semantics) to be
Scott continuous often results from the introduction of negation, because the
introduction of negation may render the operators in question to be nonmonotonic and hence to fail to be Scott continuous, as we will see in Chapter 2.
The point just made is important because it is one of the reasons for
introducing alternatives to order theory in studying fixed-point theory in relation to semantics and in establishing fixed-point theorems applicable to nonmonotonic operators, see Chapter 4. Therefore, it will help to give some insight next into the non-traditional methods we introduce and develop, how
they work in the context of negation, and especially how they work in finding models for logic programs with negation. Our point of view is to regard
programs, and logic programs in particular, as (abstract) dynamical systems
whose states change under program execution and whose state changes can be
modelled by an operator T . Starting with some initial state, s 0 , say, it is inter4 This is a generic term which we use to cover all of a number of specific operators we
will study, such as the T P -operator, see Definition 2.2.1.
5 See Theorem 2.2.3, for example, and [Lloyd, 1987] for details of how procedural semantics relates to declarative semantics.