acyclic
definite
/ / /
/
/ / / / /
locally
T P Scottcovered
acceptable
stratified
continuous
hierarchical
/
/ / / / / / / / /
T P
locally
continuous Φ
∗ -accessible
stratified
in Q
Φ-accessible
uniquely
weakly
determined
stratified
total
well-founded
model
unique
stable
model
160
Mathematical Aspects of Logic Programming Semantics
1
1
1
1
1
1
1
1
1
1
FIGURE 5.1: The main classes of programs discussed in this book. The arrows
indicate class inclusion. See the main text of Section 5.3 for further details.
a program can be locally hierarchical without being acyclic, but still have a
Q-continuous immediate consequence operator, meaning that its immediate
consequence operator is continuous in the topology Q.
Covered programs are defined in Definition 7.5.4. Figure 5.1 indicates that
every acyclic program is covered, but note that this is only the case if we
assume that the underlying language contains at least one function symbol.
Indeed, if this is not the case, then the Herbrand base is finite, and, for example, the program P with the single clause
q(a) ← p(x)
is acyclic
10 but not covered. Q-continuity of the immediate consequence operator for covered programs follows from Corollary 5.4.8. Scott continuity of the
immediate consequence operator for definite programs follows from Theorem
2.2.3 (it was called order continuity there).
The remaining relationships shown in Figure 5.1 follow from results in
Chapter 2 and Section 5.2.
10 For example, assume a is the only constant symbol. Then ground(P ) is q(a) ← p(a),
and so P is obviously acyclic.