125
Fixed-Point Theory for Generalized Metric Spaces
Proof: Clearly, � is a d-gum. For spherical completeness, note that every
non-empty ball in (X, �, Γ) contains z, and this suffices.
•
This result will be applied in Section 5.1.4.
4.9 Fixed-Point Theory for Multivalued Mappings
We close this chapter with a discussion of multivalued mappings and some
of the fixed-point theorems which are applicable to them.
Let X be a set. Then a multivalued mapping T defined on X is simply a
mapping T : X → P(X) from X to the power set P(X) of X; thus, for each
x ∈ X, T (x) is a subset of X. Furthermore, a fixed point of a multivalued
mapping T is an element x of X such that x ∈ T (x). Such mappings are
important in studying semantics in the presence of non-determinism because
at any step in the execution of a non-deterministic program, there will in
general be many possible successive states, and therefore the informal meaning
of such a program may be taken to be a multivalued mapping defined on the
set X of states the program may assume. These comments apply in particular
to disjunctive logic programs in which the head of a typical program clause
contains a disjunction of several atoms, rather than a single atom, and in
executing such a program a non-deterministic choice has to be made of an
atom in the head of any clause involved in the execution.
Not surprisingly, given their informal meaning, the formal meaning of disjunctive programs involves fixed points of multivalued mappings. Therefore, it
is of interest to consider fixed-point theorems in this context and the methods
used to establish them. Again, not surprisingly, the methods normally used
to establish such theorems depend either on order theory or on generalized
metrics of one type or another, and we consider both approaches.
We begin by considering an interesting recent paper by Straccia, OjedaAciego, and Dam´ asio, see [Straccia et al., 2009], and relating their work to
ours. In this paper, the authors use methods depending on order theory to
establish a number of results guaranteeing the existence of least and greatest
fixed points of a multivalued mapping T : L → P(L), where L is a complete
lattice. In contrast, the methods we will employ mainly depend on the methods
of analysis. Furthermore, as noted below, the results of [Straccia et al., 2009]
are broadly representative of those obtained by order theory. Therefore, it
will help to state a result of [Straccia et al., 2009], which gives a flavour of
its contents and is typical of results obtained in the field by order theory.
However, to do this requires the statement of some preliminary definitions,
but they will be needed in any case as we proceed.
Given the complete lattice (L, ≤) and its power set P(L), we define three
orderings on P(L) familiar in semantics and domain theory, as follows, see
Fixed-Point Theory for Generalized Metric Spaces
Proof: Clearly, � is a d-gum. For spherical completeness, note that every
non-empty ball in (X, �, Γ) contains z, and this suffices.
•
This result will be applied in Section 5.1.4.
4.9 Fixed-Point Theory for Multivalued Mappings
We close this chapter with a discussion of multivalued mappings and some
of the fixed-point theorems which are applicable to them.
Let X be a set. Then a multivalued mapping T defined on X is simply a
mapping T : X → P(X) from X to the power set P(X) of X; thus, for each
x ∈ X, T (x) is a subset of X. Furthermore, a fixed point of a multivalued
mapping T is an element x of X such that x ∈ T (x). Such mappings are
important in studying semantics in the presence of non-determinism because
at any step in the execution of a non-deterministic program, there will in
general be many possible successive states, and therefore the informal meaning
of such a program may be taken to be a multivalued mapping defined on the
set X of states the program may assume. These comments apply in particular
to disjunctive logic programs in which the head of a typical program clause
contains a disjunction of several atoms, rather than a single atom, and in
executing such a program a non-deterministic choice has to be made of an
atom in the head of any clause involved in the execution.
Not surprisingly, given their informal meaning, the formal meaning of disjunctive programs involves fixed points of multivalued mappings. Therefore, it
is of interest to consider fixed-point theorems in this context and the methods
used to establish them. Again, not surprisingly, the methods normally used
to establish such theorems depend either on order theory or on generalized
metrics of one type or another, and we consider both approaches.
We begin by considering an interesting recent paper by Straccia, OjedaAciego, and Dam´ asio, see [Straccia et al., 2009], and relating their work to
ours. In this paper, the authors use methods depending on order theory to
establish a number of results guaranteeing the existence of least and greatest
fixed points of a multivalued mapping T : L → P(L), where L is a complete
lattice. In contrast, the methods we will employ mainly depend on the methods
of analysis. Furthermore, as noted below, the results of [Straccia et al., 2009]
are broadly representative of those obtained by order theory. Therefore, it
will help to state a result of [Straccia et al., 2009], which gives a flavour of
its contents and is typical of results obtained in the field by order theory.
However, to do this requires the statement of some preliminary definitions,
but they will be needed in any case as we proceed.
Given the complete lattice (L, ≤) and its power set P(L), we define three
orderings on P(L) familiar in semantics and domain theory, as follows, see