146
Mathematical Aspects of Logic Programming Semantics
Finally, let
I = {move(a, b) | (a, b) ∈ G} ∪ {win(a) | g(a) = 1}.
It is straightforward to verify that Game is acceptable with respect to I and
l.
We will now show how to construct a complete dislocated metric for any
given acceptable program with respect to which the immediate consequence
operator associated with the program is a contraction. For this purpose, let
P be a program which is acceptable with respect to a level mapping l and
an interpretation I. For any K ∈ I P , we denote by K
' the set K restricted
to the predicate symbols in Neg
∗
P . Next, we define a function f : I P → R by
n
'
setting f (K) = 0 if K \ K ⊆ I and, if K \ K
' ⊆ I, by setting f (K) = 2
− ,
where n ≥ 0 is the smallest integer such that there is an atom A ∈ B P with
'
l(A) = n, A ∈ K \ K and A ∈ I. Now define a function u : I P → R by 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
5
�(J, K) = max{d l (J \ J
' , K \ K
' ), u(J), u(K)}.
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
' )}.
We apply Proposition 4.8.7 in order to show that � is a complete dislocated
ultrametric. We will need the following lemma.
5.1.10 Lemma Let u(K) = max{f (K), d l (K
' , I
' )} for K ∈ I P . Then u is
continuous as a function from (I P , d l ) to R.
Proof: Let K m be a sequence in I P which converges in d l to some K ∈ I P .
'
We need to show that d l (K , I
' ) converges to d l (K
' , I
' ) and that f (K m )
m
converges to f (K) as m → ∞. Since (K m ) converges to K with respect to
the metric d l , it follows that for each n ∈ N there is m n ∈ N such that, for
all m ≥ m n , K and K m agree on all atoms of level less than or equal to n.
Suppose that f (K) = 2
−n0 , say, and that m ≥ m n0 . Then K m and K agree
'
'
on all atoms of level less than or equal to n 0 , and it follows that K and K m
'
agree on all atoms of level less than or equal to n 0 and, hence, that K \ K
'
and K m \ K agree on all atoms of level less than or equal to n 0 . Therefore,
m
we have f (K m ) = 2
−n0 = f (K) for all m ≥ m n0 . Also, if d l (K
' , I
' ) = 2
−n0 ,
'
say, then d l (K , I
' ) = 2
−n0 = d l (K
' , I
' ) for all m ≥ m n0 .
m
The result now follows.
•
It remains to show that T P is a contraction with respect to �.
5 This approach was inspired by [Fitting, 1994b]. The function u is usually called a weight
function if it is used for constructing dislocated metrics from metrics, see [Matthews, 1992,
Waszkiewicz, 2002]. Here, and in Section 5.1.3, we follow [Seda and Hitzler, 2010].