140
Mathematical Aspects of Logic Programming Semantics
again in Section 5.2, but this time from the point of view of three-valued supported models (more precisely by studying variants of Fitting’s Φ-operator).
By analogy with Chapter 2, we will establish a correspondence between semantics defined, on the one hand, by means of monotonic operators, and
characterizations given by means of level mappings, on the other hand. As a
result, we obtain a hierarchy of program classes which extends observations
from Chapter 2. All this will be carried out in this chapter in Section 5.3.
Finally, in Section 5.4, we make some brief observations concerning how
one may approach the results of this chapter from a much more general point
of view.
5.1 Two-Valued Supported Models
We know from Proposition 2.2.6 that the (two-valued) supported models for a given program P are exactly the fixed points of the corresponding
single-step operator T P . From Program 2.2.4, we know that T P is in general
not monotonic. This fact has the particular consequence that the fixed-point
theorems from Section 1.1 for monotonic operators are not applicable to T P
in this case. The alternative suggested by our development in Chapter 4 is to
apply, to non-monotonic single-step operators, fixed-point theorems utilizing
generalized metrics. In particular, it suggests in our current context the application of those theorems which directly generalize the Banach contraction
mapping theorem to the extent that they ensure uniqueness of the resulting
fixed points, if any. Of course, if we successfully apply any of these particular theorems to a single-step operator, the corresponding program will clearly
be uniquely determined. It follows, therefore, that any approach of this type
employing fixed-point theorems which guarantee uniqueness of the resulting
fixed points cannot, when applied to single-step operators, encompass all (definite) programs. Program 2.3.1, for example, is definite, but has two supported
models and, hence, cannot be uniquely determined.
Throughout the present section, it will be convenient to let I P denote I P,2 .
5.1.1 Acyclic and Locally Hierarchical Programs
Let us first recall the program Even (Program 2.1.3). Iterates of the corresponding immediate consequence operator T Even are easily computed and are
as follows, for all n ∈ N, see Example 3.3.6.
A
b
T
2n = even s
2k (0) | 0 ≤ k < n ,
Even
A
b
T
2n+1
Even = B Even \ even s
2k+1 (0) | 0 ≤ k < n
Mathematical Aspects of Logic Programming Semantics
again in Section 5.2, but this time from the point of view of three-valued supported models (more precisely by studying variants of Fitting’s Φ-operator).
By analogy with Chapter 2, we will establish a correspondence between semantics defined, on the one hand, by means of monotonic operators, and
characterizations given by means of level mappings, on the other hand. As a
result, we obtain a hierarchy of program classes which extends observations
from Chapter 2. All this will be carried out in this chapter in Section 5.3.
Finally, in Section 5.4, we make some brief observations concerning how
one may approach the results of this chapter from a much more general point
of view.
5.1 Two-Valued Supported Models
We know from Proposition 2.2.6 that the (two-valued) supported models for a given program P are exactly the fixed points of the corresponding
single-step operator T P . From Program 2.2.4, we know that T P is in general
not monotonic. This fact has the particular consequence that the fixed-point
theorems from Section 1.1 for monotonic operators are not applicable to T P
in this case. The alternative suggested by our development in Chapter 4 is to
apply, to non-monotonic single-step operators, fixed-point theorems utilizing
generalized metrics. In particular, it suggests in our current context the application of those theorems which directly generalize the Banach contraction
mapping theorem to the extent that they ensure uniqueness of the resulting
fixed points, if any. Of course, if we successfully apply any of these particular theorems to a single-step operator, the corresponding program will clearly
be uniquely determined. It follows, therefore, that any approach of this type
employing fixed-point theorems which guarantee uniqueness of the resulting
fixed points cannot, when applied to single-step operators, encompass all (definite) programs. Program 2.3.1, for example, is definite, but has two supported
models and, hence, cannot be uniquely determined.
Throughout the present section, it will be convenient to let I P denote I P,2 .
5.1.1 Acyclic and Locally Hierarchical Programs
Let us first recall the program Even (Program 2.1.3). Iterates of the corresponding immediate consequence operator T Even are easily computed and are
as follows, for all n ∈ N, see Example 3.3.6.
A
b
T
2n = even s
2k (0) | 0 ≤ k < n ,
Even
A
b
T
2n+1
Even = B Even \ even s
2k+1 (0) | 0 ≤ k < n