147
Supported Model Semantics
5.1.11 Theorem Let P be a program which is acceptable with respect to
some level mapping l and interpretation I. Then � is a complete dislocated
ultrametric, and T P is a contraction with respect to �. In particular, P has a
unique supported model M and M = lim T
n (I 0 ) for any I 0 ∈ I P .
P
Proof: The mapping � is a complete dislocated ultrametric by Lemma 5.1.10
and Proposition 4.8.7. By Matthews’ theorem, Theorem 4.4.6, it remains to
show that T P is a contraction with respect to �. The argument for this is
essentially the same as the slightly more general one in the proof of Theorem
5.1.14, to be given in the next section, so we omit it here.
•
5.1.3 Φ ∗ -Accessible Programs
We have seen in Section 5.1.2 that application of the Banach contraction
mapping theorem can be replaced by application of Matthews’ theorem when
passing from acyclic to acceptable programs. Likewise, the Priess-Crampe and
Ribenboim theorem can be used in place of Banach’s theorem when passing
from acyclic to locally hierarchical programs. Naturally, the question arises
as to whether or not a class of programs can be described which generalizes
both the acceptable and the locally hierarchical programs such that Theorem
4.5.1, which generalizes both Matthews’ theorem and the Priess-Crampe and
Ribenboim theorem, can be applied. We will describe such a class of programs
in this section.
5.1.12 Definition A program P is called Φ
∗ -accessible
6 if and only if there
exists a level mapping l for P and a model I for P whose restriction to Neg
∗
P
is a supported model for P
− such that the following condition holds. For each
clause A ← L 1 , . . . , L n in ground(P ), either we have I |= L 1 ∧ · · · ∧ L n and
l(A) > l(L i ) for all i = 1, . . . , n or there exists i ∈ {1, . . . , n} such that I |= L i
and l(A) > l(L i ).
As an example, we refer again to the generate-and-test scheme described
in Program 5.1.2.
5.1.13 Program Assume that the unary predicate symbols generate and
test are defined via acceptable programs P 1 and P 2 , and consider the program
P which is the union of P 1 , P 2 and the following clause.
success ← generate(X), test(X).
It is easy to see that P is Φ
∗ -accessible: first note that P 1 and P 2 are Φ
∗
accessible with respect to models I 1 and I 2 and level mappings l 1 and l 2 , say,
with codomain ω. We can assume without loss of generality that B P1 and B P2
6 It was shown in [Hitzler and Seda, 2003] that it is possible to compute all partial recursive functions with definite Φ ∗ -accessible programs using SLD-resolution.
Supported Model Semantics
5.1.11 Theorem Let P be a program which is acceptable with respect to
some level mapping l and interpretation I. Then � is a complete dislocated
ultrametric, and T P is a contraction with respect to �. In particular, P has a
unique supported model M and M = lim T
n (I 0 ) for any I 0 ∈ I P .
P
Proof: The mapping � is a complete dislocated ultrametric by Lemma 5.1.10
and Proposition 4.8.7. By Matthews’ theorem, Theorem 4.4.6, it remains to
show that T P is a contraction with respect to �. The argument for this is
essentially the same as the slightly more general one in the proof of Theorem
5.1.14, to be given in the next section, so we omit it here.
•
5.1.3 Φ ∗ -Accessible Programs
We have seen in Section 5.1.2 that application of the Banach contraction
mapping theorem can be replaced by application of Matthews’ theorem when
passing from acyclic to acceptable programs. Likewise, the Priess-Crampe and
Ribenboim theorem can be used in place of Banach’s theorem when passing
from acyclic to locally hierarchical programs. Naturally, the question arises
as to whether or not a class of programs can be described which generalizes
both the acceptable and the locally hierarchical programs such that Theorem
4.5.1, which generalizes both Matthews’ theorem and the Priess-Crampe and
Ribenboim theorem, can be applied. We will describe such a class of programs
in this section.
5.1.12 Definition A program P is called Φ
∗ -accessible
6 if and only if there
exists a level mapping l for P and a model I for P whose restriction to Neg
∗
P
is a supported model for P
− such that the following condition holds. For each
clause A ← L 1 , . . . , L n in ground(P ), either we have I |= L 1 ∧ · · · ∧ L n and
l(A) > l(L i ) for all i = 1, . . . , n or there exists i ∈ {1, . . . , n} such that I |= L i
and l(A) > l(L i ).
As an example, we refer again to the generate-and-test scheme described
in Program 5.1.2.
5.1.13 Program Assume that the unary predicate symbols generate and
test are defined via acceptable programs P 1 and P 2 , and consider the program
P which is the union of P 1 , P 2 and the following clause.
success ← generate(X), test(X).
It is easy to see that P is Φ
∗ -accessible: first note that P 1 and P 2 are Φ
∗
accessible with respect to models I 1 and I 2 and level mappings l 1 and l 2 , say,
with codomain ω. We can assume without loss of generality that B P1 and B P2
6 It was shown in [Hitzler and Seda, 2003] that it is possible to compute all partial recursive functions with definite Φ ∗ -accessible programs using SLD-resolution.