148
Mathematical Aspects of Logic Programming Semantics
are disjoint and do not contain success. Now define I = I 1 ∪ I 2 ∪ {success}
and define l : B P → ω + 1 by l(A) = l i (A), if A ∈ B Pi , and l(success) = ω.
Then P is easily seen to be Φ
∗ -accessible with respect to I and l.
We continue to carry over the approach of Section 5.1.2; again, we follow
[Seda and Hitzler, 2010]. So let P be a program which is Φ
∗ -accessible with
respect to a level mapping l : B P → γ and an interpretation I. For any
'
K ∈ I P , we again denote by K the set K restricted to the predicate symbols
in Neg
∗ . Again, we define a function f on I P , this time taking values in Γ l ,
P
'
'
by setting f (K) = 0 if K \ K ⊆ I and, if K \ K ⊆ I, by setting f (K) = 2
−α ,
where α is the smallest ordinal such that there is an atom A ∈ B P with
'
l(A) = α, A ∈ K \ K and A ∈ I. Now define a function u : I P → Γ l by again
setting u(K) = max{f (K), d l (K
' , I
' )}, where d l is the generalized ultrametric
from Definition 5.1.3.
Finally, for all J, K ∈ I P , we set
�(J, K) = max{d l (J \ J
' , K \ K
' ), u(J), u(K)}
as before. Thus, for all J, K ∈ I P , we have
�(J, K) = max{d l (J \ J
' , K \ K
' ), f (J), d l (J
' , I
' ), f (K), d l (K
' , I
' )}.
In fact, the details of the proof of the main result below will be simplified
by introducing the functions d 1 and d 2 , where, for all J, K ∈ I P , we set
d 1 (J, K) = d l (J
' , K
' ) and d 2 (J, K) = d l (J \ J
' , K \ K
' ). Indeed, in these terms
we have
�(J, K) = max{d 1 (J, I), d 1 (K, I), d 2 (J, K), f (J), f (K)}
for all J, K ∈ I P .
5.1.14 Theorem Let P be a Φ
∗ -accessible normal logic program. Then the
space (I P , �) is a spherically complete, dislocated generalized ultrametric
space, and T P is strictly contracting with respect to �. In particular, P has a
unique supported model.
Proof: It follows from Proposition 4.8.22 that � is a dislocated generalized
ultrametric. For spherical completeness, let (B α ) be a (decreasing) chain of
balls in I P with centres I α . Let K be the set of all atoms which are eventually
in I α , that is, the set of all A ∈ B P such that there exists some ordinal β with
A ∈ I α for all α ≥ β. We show that for each ball B 2 −α (I α ) in the chain, we
have d l (I α , I) ≤ 2
−α , which suffices to show that K is in the intersection of
the chain. Indeed, it is easy to see by the definition of � that all I β with β > α
agree on all atoms of level less than α. Hence, by definition of K we obtain
that K and I α agree on all atoms of level less than α, as required.
It remains to show that T P is strictly contracting with respect to �, for it
will then follow from Theorem 4.5.1 that the operator T P has a unique fixed
Mathematical Aspects of Logic Programming Semantics
are disjoint and do not contain success. Now define I = I 1 ∪ I 2 ∪ {success}
and define l : B P → ω + 1 by l(A) = l i (A), if A ∈ B Pi , and l(success) = ω.
Then P is easily seen to be Φ
∗ -accessible with respect to I and l.
We continue to carry over the approach of Section 5.1.2; again, we follow
[Seda and Hitzler, 2010]. So let P be a program which is Φ
∗ -accessible with
respect to a level mapping l : B P → γ and an interpretation I. For any
'
K ∈ I P , we again denote by K the set K restricted to the predicate symbols
in Neg
∗ . Again, we define a function f on I P , this time taking values in Γ l ,
P
'
'
by setting f (K) = 0 if K \ K ⊆ I and, if K \ K ⊆ I, by setting f (K) = 2
−α ,
where α is the smallest ordinal such that there is an atom A ∈ B P with
'
l(A) = α, A ∈ K \ K and A ∈ I. Now define a function u : I P → Γ l by again
setting u(K) = max{f (K), d l (K
' , I
' )}, where d l is the generalized ultrametric
from Definition 5.1.3.
Finally, for all J, K ∈ I P , we set
�(J, K) = max{d l (J \ J
' , K \ K
' ), u(J), u(K)}
as before. Thus, for all J, K ∈ I P , we have
�(J, K) = max{d l (J \ J
' , K \ K
' ), f (J), d l (J
' , I
' ), f (K), d l (K
' , I
' )}.
In fact, the details of the proof of the main result below will be simplified
by introducing the functions d 1 and d 2 , where, for all J, K ∈ I P , we set
d 1 (J, K) = d l (J
' , K
' ) and d 2 (J, K) = d l (J \ J
' , K \ K
' ). Indeed, in these terms
we have
�(J, K) = max{d 1 (J, I), d 1 (K, I), d 2 (J, K), f (J), f (K)}
for all J, K ∈ I P .
5.1.14 Theorem Let P be a Φ
∗ -accessible normal logic program. Then the
space (I P , �) is a spherically complete, dislocated generalized ultrametric
space, and T P is strictly contracting with respect to �. In particular, P has a
unique supported model.
Proof: It follows from Proposition 4.8.22 that � is a dislocated generalized
ultrametric. For spherical completeness, let (B α ) be a (decreasing) chain of
balls in I P with centres I α . Let K be the set of all atoms which are eventually
in I α , that is, the set of all A ∈ B P such that there exists some ordinal β with
A ∈ I α for all α ≥ β. We show that for each ball B 2 −α (I α ) in the chain, we
have d l (I α , I) ≤ 2
−α , which suffices to show that K is in the intersection of
the chain. Indeed, it is easy to see by the definition of � that all I β with β > α
agree on all atoms of level less than α. Hence, by definition of K we obtain
that K and I α agree on all atoms of level less than α, as required.
It remains to show that T P is strictly contracting with respect to �, for it
will then follow from Theorem 4.5.1 that the operator T P has a unique fixed