126
Mathematical Aspects of Logic Programming Semantics
[Abramsky and Jung, 1994]. First, the Smyth ordering � S defined by X � S Y
if and only if for each y ∈ Y there exists x ∈ X such that x ≤ y. Second, we
define the Hoare ordering � H by X � H Y if and only if for each x ∈ X there
exists y ∈ Y such that x ≤ y. Finally, we define the Egli–Milner ordering � EM
by X � EM Y if and only if X � S Y and X � H Y . Next, we say that T is
Smyth monotonic or simply S-monotonic if, for all x, y ∈ X satisfying x ≤ y,
we have T (x) � S T (y). The notions of Hoare monotonicity and Egli–Milner
monotonicity are defined similarly.
We are now in a position to present the following result of Straccia, OjedaAciego, and Dam´ asio, see [Straccia et al., 2009, Prosposition 3.10].
4.9.1 Proposition Let T : L → P(L) be a multivalued mapping, where L is
a complete lattice.
(a) If T is S-monotonic and for all x ∈ L, T (x) has a least element, then T
has a least fixed point.
(b) If T is H-monotonic and for all x ∈ L, T (x) has a greatest element, then
T has a greatest fixed point.
Straccia et al. also introduce a very general class of logic programs P, a
class much more general than conventional disjunctive logic programs, and
proceed to define a multivalued semantic operator T P associated with each
program P in the class in question. On applying their fixed-point theorems,
they establish a one-to-one correspondence between the models of any program
P and the fixed points of T P . All these results are order-theoretic in nature,
although, in summarizing their conclusions, the question of deriving fixedpoint theorems for multivalued mappings using methods from analysis is raised
by the authors, but not taken up in detail.
Thus, we will focus here mainly on those fixed-point theorems for multivalued mappings which employ analytical methods and results in their formulation or in their proofs, rather than on results which depend primarily on
order theory. This is partly for the reason stated at the end of the previous
paragraph and partly because the results of [Straccia et al., 2009] largely subsume the order-theoretic results derived by several other contributors to this
subject anyway, except that the latter are usually presented in the context
of complete partial orders rather than in the less general context of complete
lattices employed by Straccia and his co-authors. On the other hand, most
other authors require the condition that the multivalued mapping T is nonempty in the sense that, for all x ∈ X, we have T (x) = ∅, a condition that
Straccia et al. do not impose. However, despite the opening sentence of this
paragraph, we do wish to consider a result of our own which gives a form, for
multivalued mappings, of the Rutten-Smyth theorem discussed earlier, Theorem 4.6.3, and its role in unifying the order-theoretic and metric approaches to
the fixed-point theory of multivalued mappings, and this of course necessitates
some discussion of order theory.
Mathematical Aspects of Logic Programming Semantics
[Abramsky and Jung, 1994]. First, the Smyth ordering � S defined by X � S Y
if and only if for each y ∈ Y there exists x ∈ X such that x ≤ y. Second, we
define the Hoare ordering � H by X � H Y if and only if for each x ∈ X there
exists y ∈ Y such that x ≤ y. Finally, we define the Egli–Milner ordering � EM
by X � EM Y if and only if X � S Y and X � H Y . Next, we say that T is
Smyth monotonic or simply S-monotonic if, for all x, y ∈ X satisfying x ≤ y,
we have T (x) � S T (y). The notions of Hoare monotonicity and Egli–Milner
monotonicity are defined similarly.
We are now in a position to present the following result of Straccia, OjedaAciego, and Dam´ asio, see [Straccia et al., 2009, Prosposition 3.10].
4.9.1 Proposition Let T : L → P(L) be a multivalued mapping, where L is
a complete lattice.
(a) If T is S-monotonic and for all x ∈ L, T (x) has a least element, then T
has a least fixed point.
(b) If T is H-monotonic and for all x ∈ L, T (x) has a greatest element, then
T has a greatest fixed point.
Straccia et al. also introduce a very general class of logic programs P, a
class much more general than conventional disjunctive logic programs, and
proceed to define a multivalued semantic operator T P associated with each
program P in the class in question. On applying their fixed-point theorems,
they establish a one-to-one correspondence between the models of any program
P and the fixed points of T P . All these results are order-theoretic in nature,
although, in summarizing their conclusions, the question of deriving fixedpoint theorems for multivalued mappings using methods from analysis is raised
by the authors, but not taken up in detail.
Thus, we will focus here mainly on those fixed-point theorems for multivalued mappings which employ analytical methods and results in their formulation or in their proofs, rather than on results which depend primarily on
order theory. This is partly for the reason stated at the end of the previous
paragraph and partly because the results of [Straccia et al., 2009] largely subsume the order-theoretic results derived by several other contributors to this
subject anyway, except that the latter are usually presented in the context
of complete partial orders rather than in the less general context of complete
lattices employed by Straccia and his co-authors. On the other hand, most
other authors require the condition that the multivalued mapping T is nonempty in the sense that, for all x ∈ X, we have T (x) = ∅, a condition that
Straccia et al. do not impose. However, despite the opening sentence of this
paragraph, we do wish to consider a result of our own which gives a form, for
multivalued mappings, of the Rutten-Smyth theorem discussed earlier, Theorem 4.6.3, and its role in unifying the order-theoretic and metric approaches to
the fixed-point theory of multivalued mappings, and this of course necessitates
some discussion of order theory.