114
Mathematical Aspects of Logic Programming Semantics
4.8 Relationships Between the Various Spaces
We move on next to study the relationships which exist between the various different spaces we have introduced in this chapter. In particular, we
focus on the representation of certain relationships in terms of others. This
will in some cases lead to alternative proofs of fixed-point theorems we have
already considered. The one exception to this comment is the interplay between quasimetrics and partial orders. It is clear from the results of Section 4.6
that this interplay is strong. But we will not consider it again other than in
the context of multivalued mappings, see Sections 4.10 and 4.13; see also
[Smyth, 1987, Smyth, 1991, Bonsangue et al., 1996, Rutten, 1996] for further
details.
4.8.1 Metrics and Dislocated Metrics
Our intention here is to establish relationships between metrics and dislocated metrics. Furthermore, we will examine several methods of obtaining
dislocated metrics from metrics, some of which will be applied later, and we
will show how Matthews’ theorem can be derived from the Banach contraction
mapping theorem.
We begin by noting that if f is a contraction with contractivity factor λ on
a d-metric space (X, �), then we have �(f (x), f (x)) ≤ λ�(x, x) for all x ∈ X.
Furthermore, the property �(x, x) = 0 for all x ∈ X, if � happens to satisfy
this, simply means that the d-metric � is actually a metric. It follows, therefore,
that we are interested in studying the function u 1 : X → R associated with
any d-metric �.
4.8.1 Definition Let (X, �) be a d-metric space. We define the function u 1 :
X → R by u 1 (x) = �(x, x), for all x ∈ X, and call it the dislocation function
of �.
Depending on the context, dislocation functions are sometimes also called
weight functions, see, for example, [Matthews, 1994, Waszkiewicz, 2002].
The following result gives a rather general method by which d-metrics can
be obtained from metrics.
4.8.2 Proposition Let (X, d) be a metric space, let u : X → R
+
0 be a function, and let T : R
+
0 × R
+
0 → R
+
0 be a symmetric function which satisfies the
triangle inequality. Then (X, �), where
�(x, y) = d(x, y) + T (u(x), u(y))
for all x, y ∈ X is a d-metric space, and u 1 (x) = T (u(x), u(x)) for all x ∈ X.
In particular, if T (x, x) = x for all x ∈ R
+
0 , then u 1 = u.
Mathematical Aspects of Logic Programming Semantics
4.8 Relationships Between the Various Spaces
We move on next to study the relationships which exist between the various different spaces we have introduced in this chapter. In particular, we
focus on the representation of certain relationships in terms of others. This
will in some cases lead to alternative proofs of fixed-point theorems we have
already considered. The one exception to this comment is the interplay between quasimetrics and partial orders. It is clear from the results of Section 4.6
that this interplay is strong. But we will not consider it again other than in
the context of multivalued mappings, see Sections 4.10 and 4.13; see also
[Smyth, 1987, Smyth, 1991, Bonsangue et al., 1996, Rutten, 1996] for further
details.
4.8.1 Metrics and Dislocated Metrics
Our intention here is to establish relationships between metrics and dislocated metrics. Furthermore, we will examine several methods of obtaining
dislocated metrics from metrics, some of which will be applied later, and we
will show how Matthews’ theorem can be derived from the Banach contraction
mapping theorem.
We begin by noting that if f is a contraction with contractivity factor λ on
a d-metric space (X, �), then we have �(f (x), f (x)) ≤ λ�(x, x) for all x ∈ X.
Furthermore, the property �(x, x) = 0 for all x ∈ X, if � happens to satisfy
this, simply means that the d-metric � is actually a metric. It follows, therefore,
that we are interested in studying the function u 1 : X → R associated with
any d-metric �.
4.8.1 Definition Let (X, �) be a d-metric space. We define the function u 1 :
X → R by u 1 (x) = �(x, x), for all x ∈ X, and call it the dislocation function
of �.
Depending on the context, dislocation functions are sometimes also called
weight functions, see, for example, [Matthews, 1994, Waszkiewicz, 2002].
The following result gives a rather general method by which d-metrics can
be obtained from metrics.
4.8.2 Proposition Let (X, d) be a metric space, let u : X → R
+
0 be a function, and let T : R
+
0 × R
+
0 → R
+
0 be a symmetric function which satisfies the
triangle inequality. Then (X, �), where
�(x, y) = d(x, y) + T (u(x), u(y))
for all x, y ∈ X is a d-metric space, and u 1 (x) = T (u(x), u(x)) for all x ∈ X.
In particular, if T (x, x) = x for all x ∈ R
+
0 , then u 1 = u.
