102
Mathematical Aspects of Logic Programming Semantics
ordered, we have �(x, z) < �(y, z), and by the strong triangle inequality again
we obtain �(y, z) ≤ max{�(x, y), �(x, z)} < �(y, z), which is impossible.
•
4.3.12 Lemma Let n ≥ 2, and suppose that (x 1 , x 2 , . . . , x n ) is an n-tuple of
elements of X satisfying �(x i+1 , x i+2 ) < �(x i , x i+1 ) for i = 1, . . . , n − 2. Then
�(x 1 , x n ) = �(x 1 , x 2 ).
Proof: We show by induction on n that the identity �(x 1 , x 2 ) = �(x 1 , x n )
holds. This is trivial for n = 2. So assume n > 2 and that the assertion
holds for n − 1. Then �(x 1 , x 2 ) = �(x 1 , x n−1 ), and consequently �(x n−1 , x n ) <
�(x 1 , x 2 ) = �(x 1 , x n−1 ). So Lemma 4.3.11 applies to the points x 1 , x n−1 and
x n and gives �(x 1 , x n ) = �(x 1 , x n−1 ) = �(x 1 , x 2 ), as required.
•
We can now establish the following result.
4.3.13 Proposition Let (X, �, Γ) be a generalized ultrametric space in which
Γ is a linearly ordered set. Furthermore, let f : X → X be strictly contracting,
let x 0 ∈ X, and let x i = f
i (x 0 ) for all i < ω. Then the sequence (x i ) i<ω is
pseudo-convergent.
Proof: Let α < β < γ < ω, and note then that (x α , x α+1 , . . . , x β , . . . , x γ )
satisfies the hypothesis of Lemma 4.3.12 because f is strictly contracting.
So we obtain �(x α , x β ) = �(x α , x α+1 ) and �(x β , x γ ) = �(x β , x β+1 ). Thus,
�(x β , x γ ) = �(x β , x β+1 ) < �(x α , x α+1 ) = �(x α , x β ), as desired.
•
4.4 Dislocated Metrics
Dislocated metrics were first studied by S.G. Matthews under the name of
metric domains in the context of Kahn’s dataflow model.
15 We proceed now
with the definitions needed for stating the main theorem of Matthews, which,
in fact, is the form of the Banach contraction mapping theorem applicable to
these spaces. Thus, we will define the notions of convergence, Cauchy sequence,
and completeness for dislocated metrics. As it turns out, these notions can be
carried over directly from the corresponding conventional ones.
15 The contents of Section 4.4, including Theorem 4.4.6, can be found in [Matthews, 1986].
Matthews and other authors have argued that the slightly less general notion of (weak )
partial metric is more appropriate than that of dislocated metric from a domain-theoretic
point of view. We refer the reader to [Matthews, 1994, Heckmann, 1999, Waszkiewicz, 2002]
for an account of this, since we have no direct need of it, and indeed dislocated metrics are
well-suited to our purposes.
Mathematical Aspects of Logic Programming Semantics
ordered, we have �(x, z) < �(y, z), and by the strong triangle inequality again
we obtain �(y, z) ≤ max{�(x, y), �(x, z)} < �(y, z), which is impossible.
•
4.3.12 Lemma Let n ≥ 2, and suppose that (x 1 , x 2 , . . . , x n ) is an n-tuple of
elements of X satisfying �(x i+1 , x i+2 ) < �(x i , x i+1 ) for i = 1, . . . , n − 2. Then
�(x 1 , x n ) = �(x 1 , x 2 ).
Proof: We show by induction on n that the identity �(x 1 , x 2 ) = �(x 1 , x n )
holds. This is trivial for n = 2. So assume n > 2 and that the assertion
holds for n − 1. Then �(x 1 , x 2 ) = �(x 1 , x n−1 ), and consequently �(x n−1 , x n ) <
�(x 1 , x 2 ) = �(x 1 , x n−1 ). So Lemma 4.3.11 applies to the points x 1 , x n−1 and
x n and gives �(x 1 , x n ) = �(x 1 , x n−1 ) = �(x 1 , x 2 ), as required.
•
We can now establish the following result.
4.3.13 Proposition Let (X, �, Γ) be a generalized ultrametric space in which
Γ is a linearly ordered set. Furthermore, let f : X → X be strictly contracting,
let x 0 ∈ X, and let x i = f
i (x 0 ) for all i < ω. Then the sequence (x i ) i<ω is
pseudo-convergent.
Proof: Let α < β < γ < ω, and note then that (x α , x α+1 , . . . , x β , . . . , x γ )
satisfies the hypothesis of Lemma 4.3.12 because f is strictly contracting.
So we obtain �(x α , x β ) = �(x α , x α+1 ) and �(x β , x γ ) = �(x β , x β+1 ). Thus,
�(x β , x γ ) = �(x β , x β+1 ) < �(x α , x α+1 ) = �(x α , x β ), as desired.
•
4.4 Dislocated Metrics
Dislocated metrics were first studied by S.G. Matthews under the name of
metric domains in the context of Kahn’s dataflow model.
15 We proceed now
with the definitions needed for stating the main theorem of Matthews, which,
in fact, is the form of the Banach contraction mapping theorem applicable to
these spaces. Thus, we will define the notions of convergence, Cauchy sequence,
and completeness for dislocated metrics. As it turns out, these notions can be
carried over directly from the corresponding conventional ones.
15 The contents of Section 4.4, including Theorem 4.4.6, can be found in [Matthews, 1986].
Matthews and other authors have argued that the slightly less general notion of (weak )
partial metric is more appropriate than that of dislocated metric from a domain-theoretic
point of view. We refer the reader to [Matthews, 1994, Heckmann, 1999, Waszkiewicz, 2002]
for an account of this, since we have no direct need of it, and indeed dislocated metrics are
well-suited to our purposes.