222
Mathematical Aspects of Logic Programming Semantics
is encountered in the logic programming paradigm in the case of the stable
model semantics, for example, and indeed our analysis in Section 6.2 is limited in this respect. Multiple fixed points also arise naturally in the context of
disjunctive logic programs, that is, logic programs where additionally disjunctions of atoms are allowed in rule heads as discussed briefly in Section 4.9. The
application of fixed-point theorems for multivalued mappings as provided, for
example, in Sections 4.9 to 4.13 may provide a remedy when this line of work
has been fully worked out. In particular, an approach to this problem based on
the Rutten-Smyth theorem and a careful analysis and choice of quasimetrics
(perhaps based on level mappings) holds out considerable prospects in this
respect, see [Seda, 1997]. In addition, approaches such as the one mentioned
in Section 4.14 also overcome this problem to a considerable extent.
1
8.2 Quantitative Domain Theory
Domain theory,
2 based on order continuity of semantic operators, is the
dominant theory underlying the denotational semantics of programming languages. However, an alternative tradition in the semantics of programming
languages to that using domains is an approach based on the use of metric
spaces, as already mentioned in Chapter 4.
3 A reconciliation of these two approaches is of obvious interest for the theory of programming semantics, and a
considerable body of work has been done on this very topic,
4 resulting in the
area of quantitative domain theory. Indeed, the Rutten-Smyth theorem arose
out of precisely these considerations.
In contrast to mainstream work on this reconciliation, which is driven by
a mainly conceptual motivation to unite two theories, the work presented
in this book is driven by a clear application, namely, the semantic analysis
of logic programming. In pursuing this application, we have developed several results which provide conceptual insights into the relationships between
domain-theoretic semantics and metric semantics. A key role is played by the
Scott and Cantor topologies (Chapter 3) as the underlying spaces. Another
key role is played by the relationship between ordered spaces and (generalized)
metric spaces (Section 4.8) and by the various fixed-point theorems which can
be provided for these spaces (Chapter 4), some of which have been taken
directly from work on quantitative domain theory.
A theme which has not been taken up in this book in detail and which provides scope for further work is to investigate more closely how the application1 See also [Hitzler and Seda, 1999c, Straccia et al., 2009] for some more investigations
into these matters.
2 See [Scott, 1982a].
3 See [de Bakker, 2002].
4 Initiated by work such as [Smyth, 1987].
Mathematical Aspects of Logic Programming Semantics
is encountered in the logic programming paradigm in the case of the stable
model semantics, for example, and indeed our analysis in Section 6.2 is limited in this respect. Multiple fixed points also arise naturally in the context of
disjunctive logic programs, that is, logic programs where additionally disjunctions of atoms are allowed in rule heads as discussed briefly in Section 4.9. The
application of fixed-point theorems for multivalued mappings as provided, for
example, in Sections 4.9 to 4.13 may provide a remedy when this line of work
has been fully worked out. In particular, an approach to this problem based on
the Rutten-Smyth theorem and a careful analysis and choice of quasimetrics
(perhaps based on level mappings) holds out considerable prospects in this
respect, see [Seda, 1997]. In addition, approaches such as the one mentioned
in Section 4.14 also overcome this problem to a considerable extent.
1
8.2 Quantitative Domain Theory
Domain theory,
2 based on order continuity of semantic operators, is the
dominant theory underlying the denotational semantics of programming languages. However, an alternative tradition in the semantics of programming
languages to that using domains is an approach based on the use of metric
spaces, as already mentioned in Chapter 4.
3 A reconciliation of these two approaches is of obvious interest for the theory of programming semantics, and a
considerable body of work has been done on this very topic,
4 resulting in the
area of quantitative domain theory. Indeed, the Rutten-Smyth theorem arose
out of precisely these considerations.
In contrast to mainstream work on this reconciliation, which is driven by
a mainly conceptual motivation to unite two theories, the work presented
in this book is driven by a clear application, namely, the semantic analysis
of logic programming. In pursuing this application, we have developed several results which provide conceptual insights into the relationships between
domain-theoretic semantics and metric semantics. A key role is played by the
Scott and Cantor topologies (Chapter 3) as the underlying spaces. Another
key role is played by the relationship between ordered spaces and (generalized)
metric spaces (Section 4.8) and by the various fixed-point theorems which can
be provided for these spaces (Chapter 4), some of which have been taken
directly from work on quantitative domain theory.
A theme which has not been taken up in this book in detail and which provides scope for further work is to investigate more closely how the application1 See also [Hitzler and Seda, 1999c, Straccia et al., 2009] for some more investigations
into these matters.
2 See [Scott, 1982a].
3 See [de Bakker, 2002].
4 Initiated by work such as [Smyth, 1987].