128
Mathematical Aspects of Logic Programming Semantics
Suppose that (x i ) i∈I is an increasing orbit of T and that j ∈ I is a limit
ordinal. Then x j+1 is an element of T (x j ) such that x i ≤ x j+1 for all i < j, and
of course {x i | i < j} ≤ x j ≤ x j+1 if the supremum exists. In particular,
any increasing orbit (x i ) i∈I which is tight (if such exists) must satisfy the
following condition: for any limit ordinal j, there exists x = x j+1 such that
x ∈ T ( {x i | i < j}) and
{x i | i < j} ≤ x.
(4.1)
This condition is a slight variant of a condition which was identified by Khamsi
and Misane as a sufficient condition for the existence of fixed points of Hoare
monotonic multivalued mappings. In fact, the following result was established
by them, see [Khamsi and Misane, 1998], except that it was formulated for
decreasing orbits and infima, and we have chosen to work with the dual notions
instead to be consistent with the form of Kleene’s theorem we give later.
4.10.3 Theorem (Knaster-Tarski multivalued) Suppose that X is a
complete partial order and that T : X → P(X) is a multivalued mapping
which is non-empty, Hoare monotonic, and satisfies condition (4.1). Then T
has a fixed point.
We omit details of the proof of this result except to observe that, starting with the bottom element x 0 = ⊥ of X, the condition (4.1) permits the
construction, transfinitely, of a tight orbit (x i ) of T . Since this can be carried
out for ordinals whose underlying cardinal is greater than that of X, we are
forced to conclude that (x i ) is eventually constant and therefore that T has a
fixed point.
Noting that {x i | i < j} = {x i+1 | i < j}, one can view condition (4.1)
schematically as the statement “ {T (x i ) | i < j} ≤ T ( {x i | i < j})”, and it
can therefore be thought of as a rather natural, weak continuity condition on
T which is automatically satisfied by any monotonic single-valued mapping T
on a complete partial order. The question of when the orbit constructed in the
previous paragraph becomes constant in not more than ω steps is a question
of continuity, as in the single-valued version, and will be taken up in Section
4.13.
Theorem 4.10.3 was established by Khamsi and Misane in order to
show the existence of (consistent) answer sets for a class of disjunctive
logic programs called signed programs. We have shown elsewhere, see
[Hitzler and Seda, 1999c], that it sometimes is necessary to work transfinitely
in practice, a point which justifies the name “Knaster-Tarski theorem” applied
to Theorem 4.10.3.
Thus, in summary, Hoare monotonicity of T together with (4.1) gives,
for multivalued mappings, an exact analogue of the fixed-point theory for
monotonic single-valued mappings due to Knaster-Tarski. Moreover, there are
applications of it to the semantics of disjunctive logic programs which parallel
those made in the standard, non-disjunctive case.
Mathematical Aspects of Logic Programming Semantics
Suppose that (x i ) i∈I is an increasing orbit of T and that j ∈ I is a limit
ordinal. Then x j+1 is an element of T (x j ) such that x i ≤ x j+1 for all i < j, and
of course {x i | i < j} ≤ x j ≤ x j+1 if the supremum exists. In particular,
any increasing orbit (x i ) i∈I which is tight (if such exists) must satisfy the
following condition: for any limit ordinal j, there exists x = x j+1 such that
x ∈ T ( {x i | i < j}) and
{x i | i < j} ≤ x.
(4.1)
This condition is a slight variant of a condition which was identified by Khamsi
and Misane as a sufficient condition for the existence of fixed points of Hoare
monotonic multivalued mappings. In fact, the following result was established
by them, see [Khamsi and Misane, 1998], except that it was formulated for
decreasing orbits and infima, and we have chosen to work with the dual notions
instead to be consistent with the form of Kleene’s theorem we give later.
4.10.3 Theorem (Knaster-Tarski multivalued) Suppose that X is a
complete partial order and that T : X → P(X) is a multivalued mapping
which is non-empty, Hoare monotonic, and satisfies condition (4.1). Then T
has a fixed point.
We omit details of the proof of this result except to observe that, starting with the bottom element x 0 = ⊥ of X, the condition (4.1) permits the
construction, transfinitely, of a tight orbit (x i ) of T . Since this can be carried
out for ordinals whose underlying cardinal is greater than that of X, we are
forced to conclude that (x i ) is eventually constant and therefore that T has a
fixed point.
Noting that {x i | i < j} = {x i+1 | i < j}, one can view condition (4.1)
schematically as the statement “ {T (x i ) | i < j} ≤ T ( {x i | i < j})”, and it
can therefore be thought of as a rather natural, weak continuity condition on
T which is automatically satisfied by any monotonic single-valued mapping T
on a complete partial order. The question of when the orbit constructed in the
previous paragraph becomes constant in not more than ω steps is a question
of continuity, as in the single-valued version, and will be taken up in Section
4.13.
Theorem 4.10.3 was established by Khamsi and Misane in order to
show the existence of (consistent) answer sets for a class of disjunctive
logic programs called signed programs. We have shown elsewhere, see
[Hitzler and Seda, 1999c], that it sometimes is necessary to work transfinitely
in practice, a point which justifies the name “Knaster-Tarski theorem” applied
to Theorem 4.10.3.
Thus, in summary, Hoare monotonicity of T together with (4.1) gives,
for multivalued mappings, an exact analogue of the fixed-point theory for
monotonic single-valued mappings due to Knaster-Tarski. Moreover, there are
applications of it to the semantics of disjunctive logic programs which parallel
those made in the standard, non-disjunctive case.