Abstract and Applied Analysis
Volume 2013, Issue 1 985095
Research Article
Open Access

On 0-Complete Partial Metric Spaces and Quantitative Fixed Point Techniques in Denotational Semantics

N. Shahzad, 

Corresponding Author

N. Shahzad

Department of Mathematics, King Abdulaziz University, P.O. Box 80203, Jeddah 21859, Saudi Arabia kau.edu.sa

Search for more papers by this author
O. Valero, 

O. Valero

Departamento de Ciencias Matemáticas e Informática, Universidad de las Islas Baleares, Carretera de Valldemossa km 7.5, 07122 Palma de Mallorca, Spain uib.es

Search for more papers by this author
First published: 30 December 2013
https://doi.org/10.1155/2013/985095
Citations: 18
Academic Editor: Ngai-Ching Wong

Abstract

In 1994, Matthews introduced the notion of partial metric space with the aim of providing a quantitative mathematical model suitable for program verification. Concretely, Matthews proved a partial metric version of the celebrated Banach fixed point theorem which has become an appropriate quantitative fixed point technique to capture the meaning of recursive denotational specifications in programming languages. In this paper we show that a few assumptions in statement of Matthews fixed point theorem can be relaxed in order to provide a quantitative fixed point technique useful to analyze the meaning of the aforementioned recursive denotational specifications in programming languages. In particular, we prove a new fixed point theorem for self-mappings between partial metric spaces in which the completeness has been replaced by 0-completeness and the contractive condition has been weakened in such a way that the new one best fits the requirements of practical problems in denotational semantics. Moreover, we provide examples that show that the hypothesis in the statement of our new result cannot be weakened. Finally, we show the potential applicability of the developed theory by means of analyzing a few concrete recursive denotational specifications, some of them admitting a unique meaning and others supporting multiple ones.

1. Introduction

1.1. Denotational Semantics for Programing Languages

In denotational semantics one of the aims consists of analyzing the correctness of recursive algorithms by means of mathematical models of the programming languages in which the algorithm has been written. Moreover, in many programming languages one can construct recursive algorithms through procedures in such a way that the meaning of such a procedure is expressed in terms of its own meaning. In order to analyze the meaning of such recursive definitions of procedures, Scott developed what nowadays is known as domain theory (see [1, 2] account of the theory and, also, [3, 4] for recent applications to computer science).

In the spirit of Scott, the meaning of a denotational specification can be obtained as a fixed point of a nonrecursive mapping that is induced by the denotational specification. The fixed point is, at the same time, the supremum and the topological limit of the sequence of successive iterations generated by the nonrecursive mapping acting on a fixed element of the mathematical model. Furthermore, the order relation encodes information so that each step of the procedure computation, modeled by each iteration of the nonrecursive mapping, is identified with a model element that is greater than (or equal to) the elements representing the preceding steps of the procedure computation (the preceding iterations of the nonrecursive mapping), since each iteration gives more information about the meaning of the recursive definition of the procedure than all previous ones. The aforementioned meaning of the recursive procedure denotational specification is modeled as the fixed point of the nonrecursive mapping which corresponds to the supremum and, simultaneously, the topological limit, with respect to the so-called Scott topology, of the increasing successive iterations sequence. As a consequence, the fixed point provides the total information about the meaning yielded by all elements of the increasing sequence of iterations and, in addition, it does not give more information than that which can be deduced from the elements of such a sequence.

A recursive algorithm computing the factorial of a positive integer number typically uses the following recursive denotational specification, where ℕ denotes the set of positive integer numbers:
()
From the preceding illustrative example of denotational specification one deduces the existence of a handicap. Indeed, the meaning of the symbol fact is expressed in terms of itself. Thus the symbol fact cannot be substituted by its meaning in (1), since such a meaning, given by the right-hand side in (1), also contains the symbol. According to Scott theory, the meaning of (1), that is, the entire factorial function, is given by the unique fixed point (which is a total function) of the nonrecursive mapping ϕfact defined, on the set of partial functions ordered by extension (see [5] for a detailed description of the set of partial functions), by
()
where the successive iterations acting over the partial function f1 (domf1 = 1 and f1(1) = 1) hold that if m = 1 and for all m ≤ n. The increasing sequence of iterations models each step of the computation of the factorial of a nonnegative integer number by the recursive algorithm under consideration which follows specification (1) and, besides, the topological limit of such a sequence, taking the Scott topology, is exactly the meaning of the symbol fact which yields the factorial of each nonnegative integer number. Observe that each iteration yields only partial information of the entire factorial function and, thus, each iteration gives more information about the symbol fact (the entire factorial function) than all preceding ones. Finally, the sequence of successive iterations is increasing with respect to the extension order and its supremum matches up with the meaning of the symbol fact.

Of course, the mapping ϕfact has a unique fixed point, which provides the meaning of the denotational specification (1), and such a fixed point matches up with the entire factorial function fact.

It is interesting to stress that, from an information content viewpoint, the Scott model needs to distinguish two kinds of elements: the so-called totally defined objects and the partially defined ones. The former represent elements of the model whose information content cannot be stored in a computer and, therefore, must be approximated (in the preceding example the entire functorial function). The partially defined objects match up with those elements of the model that can be stored in the computer and that approximate the total ones (each partial function in the preceding example).

1.2. Partial Metrics and Denotational Semantics

From the discussion in Section 1.1 we can infer that the Scott model does not incorporate a “metric” tool to measure the information content of the elements that form such a model. Inspired, in part, by the preceding fact, Matthews introduced the notion of partial metric as a mathematical tool to model computational processes in the spirit of Scott in such a way that a quantitative degree of the information content of the involved elements can be provided [6].

Let us recall some notions related to partial metrics in order to explain the significance of this new metric concept in computer science. To this end, we will denote by ℝ+ the set of nonnegative real numbers.

According to [6], a partial metric on a nonempty set X is a function p : X × X → ℝ+ such that for all x, y, z ∈ X
  • (i)

    p(x, x) = p(x, y) = p(y, y)⇔x = y,

  • (ii)

    p(x, x) ≤ p(x, y),

  • (iii)

    p(x, y) = p(y, x),

  • (iv)

    p(x, y) ≤ p(x, z) + p(z, y) − p(z, z).

Clearly a metric on a nonempty set X is a partial metric p on X satisfying, in addition, the following condition for all x ∈ X: (v) p(x, x) = 0.

A partial metric space is a pair (X, p) such that X is a nonempty set and p is a partial metric on X.

Each partial metric p on X generates a T0 topology 𝒯(p) on X which has as a base the family of open p-balls {Bp(x, ɛ) : x ∈ X, ɛ > 0}, where Bp(x, ɛ) = {y ∈ X : p(x, y) < p(x, x) + ɛ} for all x ∈ X and ɛ > 0. From this fact it immediately follows that a sequence (xn) n∈ℕ in a partial metric space (X, p) converges to a point x ∈ X with respect to 𝒯(p)⇔p(x, x) = lim n→∞ p(x, xn). According to [7], a sequence (xn) n∈ℕ in (X, p) is said to be 0-convergent to x ∈ X provided that it converges to x with respect to 𝒯(p) and p(x, x) = 0.

As usual (see [5]) a partial order on a nonempty set X is a reflexive, antisymmetric and transitive binary relation ≤ on X. A partially ordered set is a pair (X,  ≤) such that X is nonempty set and ≤ is a partial order on X. Moreover, given a subset Y⊆X, an upper bound for Y in (X,  ≤) is an element x ∈ X such that y ≤ x for all y ∈ Y. The supremum for Y in (X,  ≤), if exists, is an element z ∈ X which is an upper bound for Y and, in addition, satisfies that z ≤ x provided that x ∈ X is an upper bound for Y. We will denote by ↑x, with x ∈ X, the set {y ∈ X : x ≤ y}. Furthermore, an element x ∈ X is maximal in (X,  ≤) provided that if there exists y ∈ X such that x ≤ y, then y = x.

The success of partial metrics in computer science lies in the fact that every complete partial metric p (see below for the definition of completeness) induces a partial order ≤p on X  (x ≤py⇔p(x, y) = p(x, x)) in such a way that increasing sequences of elements have a supremum with respect to ≤p and converge to it with respect to the partial metric topology 𝒯(p). Inspired by the preceding fact, Matthews named this type of topologies as Scott-like topologies. Moreover, partial metrics can be used as a tool to measure the information content in the spirit of Scott’s models. Indeed, they allow to distinguish between elements in X with totally defined information content and elements with partially defined information content. Specifically, if (X, p) is a partial metric space, then the numerical value p(x, x) allows us to quantify the amount of information contained in x. In particular, according to [6], the smaller p(x, x) is, the more defined x is, x being totally defined whenever p(x, x) = 0.

The preceding facts have led to the widespread acceptance of partial metrics in computer science. A few works on the study of partial metrics spaces and their applications to computer science can be found in [8–19].

On account of [6], a sequence (xn) n∈ℕ in a partial metric space (X, p) is called a Cauchy sequence if lim n,m→∞ p(xn, xm) exists. A partial metric space (X, p) (or simply the partial metric p) is said to be complete if every Cauchy sequence (xn) n∈ℕ in X converges, with respect to 𝒯(p), to a point x ∈ X such that p(x, x) = lim n,m→∞ p(xn, xm). Moreover, every partial metric induces in a natural way a metric. Indeed, given a partial metric space (X, p), then the function ps : X × X → ℝ+ defined by ps(x, y) = 2p(x, y) − p(x, x) − p(y, y) is a metric on X. It is not hard to see that a sequence (xn) n∈ℕ in (X, p) converges to x ∈ X with respect to 𝒯(ps) if and only if lim n→∞ p(x, xn) = lim n→∞ p(xn, xn) = p(x, x). Furthermore, the metric ps plays a crucial role in the study of completeness of partial metric spaces. In particular, it is routine to check that a sequence in (X, p) is Cauchy if and only if it is Cauchy in the metric space (X, ps) and that (X, p) is complete if and only if (X, ps) is complete.

In [6], Matthews extended Banach’s fixed point theorem to the framework of partial metric spaces. Such extension was made in order to provide a quantitative fixed point technique that captures the meaning of recursive denotational specifications as the fixed point of a nonrecursive (contractive) mapping which is at the same time a total defined object of the model, the supremum of the increasing successive iterations sequence, generated by the aforesaid nonrecursive mapping acting on a distinguished element of the model, and the topological limit of such a sequence.

The aforementioned theorem can be stated as follows.

Theorem 1. Let f be a mapping of a complete partial metric space (X, p) into itself such that there is c ∈ [0,1[ satisfying

()
for all x, y ∈ X. Then f has a unique fixed point x* ∈ X which holds:
  • (1)

    the sequence (fn(x0)) n∈ℕ converges to x* with respect to 𝒯(ps) for every x0 ∈ X,

  • (2)

    p(x*, x*) = 0.

Matthews used Theorem 1 to formulate a suitable test to detect lazy data flow deadlock in Kahn’s model of parallel computation (for a fuller treatment of such an application we refer the reader to [20]).

Since Matthews published Theorem 1, an intense research activity on fixed point results in partial metric spaces has been developed. A few recent works in which fixed point results in the metric framework have been extended to the partial metric context can be found in [7, 8, 11, 21–33].

1.3. Statement of the Problem

When the meaning of recursive denotational specifications in programming languages is studied in practical problems, it seems enough to manage the contractive condition (25) only for the chosen distinguished element of the mathematical model and its associated sequence of successive iterations (e.g., f1 and in the discussion of the factorial recursive specification exposed in Section 1.1). Thus, to check contractive condition (25) for all elements of the model is unnecessary. This motivates the natural question of whether the Matthews contractive condition (25) could be relaxed in such a way that the new one is better suited to the demands of the practical problems and, besides, continues to be useful for providing a quantitative fixed point technique to analyze the meaning of recursive denotational specifications. Concretely, we postulate that a new possible contractive condition should require only that
()
for all n ∈ ℕ, where x0 ∈ X is a fixed element which represents the aforementioned distinguished element of the model and f0(x0) = x0.

If the preceding contractive condition, which is required only for a concrete sequence of elements of the model, was appropriate for our purpose, then the completeness that is required for all Cauchy sequences of the partial metric space supporting the mathematical model would be also unnecessary in order to provide the new quantitative fixed point technique.

In the light of the preceding facts, it seems interesting to wonder if it is possible to obtain a fixed point technique, which refines the original Matthews technique, based on the use of a new version of Theorem 1 which simultaneously incorporates the contractive condition (4) and a weaker notion of completeness and, in addition, it allows analyzing the meaning of recursive denotational semantics in the spirit of Scott and maintaining the original ideas of Matthews.

In the remainder of the paper we provide a positive answer to the posed question. In Section 2 we consider the 0-completeness, as introduced in [7], and we show that such a notion of completeness, weaker than the completeness of Matthews, is enough to prove the announced fixed point theorem for self-mappings satisfying the contractive condition (4). Moreover, in the same section, we provide examples that show that the hypothesis in the statement of our new result cannot be weakened. In addition, we discuss the feasibility of using the new fixed point theorem as a mathematical tool for analyzing the meaning of recursive denotational specifications. In Section 3, we show that our new result is appropriate for such a purpose and we illustrate its utility discussing the meaning of a few concrete denotational specifications, among them, the denotational specification of the factorial function and a while-loop.

2. The Fixed Point Theorem

In this section we present our main result which will play a central role in the application to denotational semantics developed in Section 3. To this end, let us recall a few pertinent notions.

Following [34], an element x of a partially ordered set (X,  ≤) is said to be a post-fixed point, with respect to ≤, of a mapping f from (X,  ≤) into itself provided that x ≤ f(x). As usual, a mapping f from a partially ordered set (X,  ≤) into itself will be called monotone if f(x) ≤ f(y) whenever x ≤ y.

On account of [7], a sequence (xn) n∈ℕ in a partial metric space (X, p) is called 0-Cauchy if lim n,m→∞ p(xn, xm) = 0. Moreover, a partial metric space (X, p) is said to be 0-complete if every 0-Cauchy sequence (xn) n∈ℕ in X  0-converges, with respect to 𝒯(p), to a point x ∈ X. Of course, every complete partial metric space is 0-complete, but the converse is not true in general.

In the light of the preceding notions we are in a position to introduce the announced main result.

Theorem 2. Let f be a monotone mapping from a 0-complete partial metric space (X, p) into itself and let x0 ∈ X be a post-fixed point of f with respect to ≤p. If there exists c ∈ [0,1[ such that

()
for all n ∈ ℕ, then f has a fixed point x* ∈ X which satisfies that
  • (1)

    x* is the unique fixed point of f in ↑x0;

  • (2)

    x* is the supremum of (fn(x0)) n∈ℕ in (X,  ≤p); moreover, x* is maximal in (X,  ≤p);

  • (3)

    the sequence (fn(x0)) n∈ℕ converges to x* with respect to 𝒯(ps);

  • (4)

    p(x*, x*) = 0.

Proof. By (5) we have that

()
for all n ∈ ℕ. Whence we obtain that lim n→∞ p(fn(x0), fn(x0)) = 0.

Since x0≤pf(x0) and f is monotone we have that the sequence (fn(x0)) n∈ℕ is increasing in (X,  ≤p). Thus

()
for all n ∈ ℕ. Whence
()
for all k ∈ ℕ. It follows that (fn(x0)) n∈ℕ is a 0-Cauchy sequence in (X, p). Since (X, p) is 0-complete we deduce that the existence of x* ∈ X such that lim n→∞ fn(x0) = x* with respect to   𝒯(p), that is,    p(x*, x*) = lim n→∞ p(fn(x0), x*) = lim n,m→∞ p(fn(x0), fm(x0)) = 0. Therefore, p(x*, x*) = lim n→∞ p(fn(x0), x*) = lim n→∞ p(fn(x0), fn(x0)) = 0 and (fn(x0)) n∈ℕ converges to x* with respect to 𝒯(ps).

Next we show that x* ∈  ↑x0. Since x0≤pfn(x0) for all n ∈ ℕ we have that p(x0, fn(x0)) = p(x0, x0) for all n ∈ ℕ. Now, let ɛ > 0. Then there exists n0 ∈ ℕ such that p(x*, fn(x0)) < ɛ for all n ≥ n0, since lim n→∞ p(fn(x0), x*) = 0. Thus

()
for all n ≥ n0. Whence we obtain that p(x*, x0) − p(x0, x0) = 0 and, hence, that x0 ≤p x*; that is, x* ∈  ↑x0.

Next we show that x* is the supremum of (fn(x0)) n∈ℕ in (X,  ≤p) and that x* is maximal in (X,  ≤p). First of all we prove that x* is an upper bound of (fn(x0)) n∈ℕ. Since

()
for all m, n ∈ ℕ with n ≤ m and lim m→∞ p(fm(x0), x*) = 0, we deduce that p(fn(x0), x*) = p(fn(x0), fn(x0)) = 0 for all n ∈ ℕ. Consequently, fn(x0) ≤p x* for all n ∈ ℕ.

Now assume that there exists y ∈ X such that fn(x0) ≤p y for all n ∈ ℕ. Then p(fn(x0), y) = p(fn(x0), fn(x0)) for all n ∈ ℕ. Hence

()
It follows, from lim n→∞ p(fn(x0), x*) = 0, that p(x*, y) = p(x*, x*) and, hence, that x* ≤p y. Whence x* is the supremum of (fn(x0)) n∈ℕ. Moreover, the fact that p(x*, x*) = 0 provides that y = x* whenever x*≤py. So x* is maximal in (X,  ≤p).

In the following we show that x* is a fixed point of f. We have that fn(x0) ≤p x* for all n ∈ ℕ. Then, by monotonicity of f, we obtain that fn(x0) ≤p f(x*) for all n ∈ ℕ. Since x* is the supremum of (fn(x0)) n∈ℕ we deduce that x* ≤p f(x*). Whence, by maximality of x*, we obtain that x* = f(x*).

It remains to prove that x* is the unique fixed point of f in ↑x0. Indeed, assume that there exists y* ∈  ↑x0 with f(y*) = y*. Then we immediately deduce that fn(x0) ≤p y* for all n ∈ ℕ. So y* is an upper bound of the sequence (fn(x0)) n∈ℕ. Whence we obtain that x*≤py*, since x* is the supremum of (fn(x0)) n∈ℕ. The fact that x* is maximal yields that y* = x*.

The below example shows that the 0-completeness of the partial metric space cannot be relaxed in statement of Theorem 2.

Example 3. Let Σ be a nonempty alphabet. Denote by ΣF the set of finite sequences over Σ. According to [6], consider the partial metric pB : ΣF × ΣF → ℝ+ defined by

()
where l(x, y) denotes the longest common prefix of x and y (of course if x and y have not a common prefix then l(x, y) = 0). It is easy to check that x ≤p y⇔x is a prefix of y.

Observe that, given x ∈ ΣF, l(x, x) is exactly the length of x.

The partial metric space (ΣF, pB) is not 0-complete. Indeed, fix a ∈ Σ and take the sequence (xn) n∈ℕ in ΣF given by for all n ∈ ℕ. It is clear that the sequence is 0-Cauchy but it is not 0-convergent with respect to 𝒯(p).

Define the mapping fa : ΣF → ΣF by fa(x) = ax, where ax denotes the concatenation of a and x. It is evident that f is monotone and that a is a post-fixed point of f. Moreover, we have that

()
for all n ∈ ℕ. Nevertheless, f has no fixed points.

The next examples show that the monotonicity and the contractive condition (5) of the self-mapping cannot be deleted in the statement of Theorem 2 in order to assure the existence of fixed point.

Example 4. Consider the partial metric pmax  : ℝ+ × ℝ+ → ℝ+ given by pmax (x, y) = max {x, y}. Clearly the partial metric space (ℝ+, pmax ) is 0-complete. Moreover, the partial order ≤p satisfies that

()
where ≤ stands for the usual order on ℝ+. Define the function f : ℝ+ → ℝ+ by
()

It is evident that f is not monotone, since and . Moreover, 1 is a post-fixed point of f. Furthermore,

()
for all n ∈ ℕ. Obviously f has no fixed points.

Example 5. Consider the partial metric space (𝒞, p𝒞), where

()
for all f, g ∈ 𝒞. According to [35, 36], the partial metric space (𝒞, p𝒞) is complete and, therefore, is 0-complete. Moreover, it is clear that for  all n ∈ ℕ.

Next consider 𝒞1⊆𝒞 given by 𝒞1 = {f ∈ 𝒞 : f1≤pf} and 𝒟 = 𝒞1∖{f3}, where f1(n) = 1 and f3(n) = 3 for all n ∈ ℕ. It is not hard to check that 𝒟 is 0-complete.

Now define the mapping F : 𝒟 → 𝒟 by

()

It is routine to check that F is monotone and that F is fixed point free. Take f0 ∈ 𝒟 given by f0(n) = 2 for all n ∈ ℕ. Then f0 is a post-fixed point of F. Furthermore, there is no c ∈ [0,1[ such that

()
for any f ∈ 𝒟. Indeed, assume for the purpose of contradiction that that there exists f ∈ 𝒟 satisfying the preceding inequality. Then
()
Whence we obtain that
()
which is impossible.

In the below example we show that the existence of a post-fixed point of the self-mapping cannot be omitted in the statement of Theorem 2 to ensure the existence of fixed point.

Example 6. Let Σ = {0,1}. Denote by ΣF and Σ∞ the set of finite and infinite sequences over Σ, respectively. On account of [6], the partial metric space (Σ∞, pB), known as the Baire partial metric, is complete, where Σ∞ = ΣF ∪ Σ∞ and pB(x, y) = 2−l(x,y) for all x, y ∈ Σ∞ (recall that, similar to Example 3, l(x, y) denotes the longest common prefix of x and y). Hence the partial metric space (Σ∞, pB) is 0-complete. Moreover, it is clear that is a prefix of y.

Consider the monotone mapping f : Σ∞ × Σ∞ defined by

()
where first  (x) denotes the first element of the sequence x. It is clear that
()
for all x ∈ Σ∞, where l(x) denotes the length of the sequence x; that is, l(x) = l(x, x) and, thus, l(x) < ∞ whenever x ∈ ΣF and l(x) = ∞ whenever x ∈ Σ∞.

It is obvious that f is post-fixed point free. Of course, f has no fixed points.

Recently, it has been shown that many fixed point results proved in the partial metric framework can be obtained from the corresponding fixed point results in the metric framework (see [37, 38]). Concretely, in [37], it was proved that every partial metric p on a nonempty set X induces a metric dp on X such that 𝒯(ps)⊆𝒯(dp), where
()
Moreover, (X, dp) is complete if and only if (X, p) is 0-complete.
Taking into account the preceding facts, in [38] it was pointed out that a wide class of generalized contractive mappings in the partial metric context are at the same time generalized contractive mappings in the metric one. So the existence and uniqueness of fixed point results for such mappings can be deduced from those results given for the same kind of mappings in the metric case. Of course, as a particular case of the preceding remark one obtains that if a mapping f : X → X satisfies the below condition
()
for all x, y ∈ X and any c ∈ [0,1[, then f also satisfies the next condition
()
for all x, y ∈ X. Therefore, guaranteed that the partial metric space (X, p) is 0-complete and that a mapping f holds (25), the existence and uniqueness of fixed point of f follow from the classical Banach fixed point and the fact that f holds (26). Observe that in spite of the fact that the existence and uniqueness of fixed point in the statement of Theorem 1 can be deduced directly from the classical Banach fixed point result, Theorem 1 provides a property of such a fixed point that cannot be deduced in the metric context and that is essential in denotational semantics. Specifically, if x* is the fixed point of the mapping, then p(x*, x*) = 0. In consequence, the classical fixed point results do not invalidate totally the new ones in the partial metric framework.
The above discussion motivates one to wonder if our new result, Theorem 2, can be deduced from the corresponding result for metric spaces. However, the answer to the posed question is negative. Indeed, on the one hand, we have that in the statement of Theorem 2 we need the partial order ≤p that induces a partial metric p. Of course such a partial order cannot be induced by the associated metric dp (in fact from any metric), since we have that
()
Nevertheless, the condition x ≤p y⇔p(x, y) = p(x, x) implies that there are in general different elements which can be order-related. An illustrative example of the exposed situation is given by the partial metric pmax  on ℝ+ introduced in Example 4. It is evident that and that . On the other hand, if one preserves all hypotheses in statement of Theorem 2 except inequality (5), then one can wonder if the aforementioned inequality can be replaced by its metric version (with respect to dp or another metric). Again such a question has a negative answer because the metric version of inequality (5) does not provide any information about the behavior of the mapping under consideration. In particular, the next example shows that in this case there are mappings which are fixed point free.

Example 7. Consider the 0-complete partial metric space (𝒟, p𝒞) introduced in Example 5. It is clear that the mapping F : 𝒟 → 𝒟 introduced in the aforesaid example holds all conditions in statement of Theorem 2 except inequality (5). Obviously, it satisfies the metric version of such an inequality; that is,

()
for any f ∈ 𝒟 (in fact for all f ∈ 𝒟). However, F is a fixed point free mapping. Notice that the preceding inequality is satisfied for any metric not only for . So one could consider any metric and still would have an example of a fixed point free mapping.

In the light of Theorem 2, it seems natural to wonder whether the existence of fixed point of the self-mapping could be retrieved from the celebrated Tarski-Kantorovitch’s or Kleene’s fixed point theorem. However, the answer to the posed question is negative such as the below examples show. With the aim of introducing such examples, we recall a few pertinent concepts following [39]. A mapping from a partially ordered set (X,  ≤) into itself is said to be ≤-continuous provided that the supremum of (f(xn)) n∈ℕ is f(x*) for every increasing sequence (xn) n∈ℕ whose supremum exists and is x*. We will say that a partially ordered set (X,  ≤) is countably chain-complete provided that every increasing sequence has a supremum. The aforesaid celebrated fixed point theorem states the following.

Theorem 8. Let (X,  ≤) be a countably chain-complete partially ordered set and let f be a ≤-continuous mapping from (X,  ≤) into itself. If x0 is a post-fixed point of f, then f has a fixed point x* which satisfies that x* ∈  ↑x0.

As announced before, the next examples guarantee that Theorem 2 is not a corollary of Theorem 8. The first of them yields that if (X, p) is a 0-complete partial metric space, then the partially ordered set (X,  ≤p) is not countably chain-complete in general. The second one gives that there exist monotone mappings from 0-complete partially ordered sets into itself which are not ≤p-continuous.

Example 9. Let . Consider the partial metric pmax  introduced in Example 4. It is clear that the partial metric space is 0-complete. Next take the sequence (xn) n∈ℕ in given by xn = 2 + 1/n for all n ∈ ℕ. It is obvious that the sequence (xn) n∈ℕ is increasing in . However, such a sequence has no supremum in . So is not countably chain-complete.

Example 10. Let I(ℝ) be the set of all nonempty compact intervals of the real line. Consider the partial metric pI(ℝ) : I(ℝ) × I(ℝ) → ℝ+ given by

()
According to [6], the partial metric space (I(ℝ), pI(ℝ)) is complete and, thus, 0-complete. Moreover, It is not hard to see that the partial order is defined on I(ℝ) as follows:
()
Next take the sequence ([an, bn]) n∈ℕ in I(ℝ) given by [an, bn] = [1,1 + 1/n] for all n ∈ ℕ. Of course, ([an, bn]) n∈ℕ is an increasing sequence in whose supremum is [1,1]. Define the mapping f : I(ℝ) → I(ℝ) by f([a, b]) = [δ(a), δ(b)], where the function δ : ℝ+ → ℝ+ is defined by
()
It is easy to see that f is monotone. However, f is not ≤p-continuous. Indeed, the sequence (f[an, bn])) n∈ℕ is increasing in and its supremum is [1,2] ≠ f([1,1]) = [1,1].

We end the section discussing the feasibility of using our new fixed point theorem as a mathematical tool for recursive denotational semantics correctness.

Of course, Theorem 2 provides a fixed point technique suitable for analyzing the meaning of recursive denotational specifications in the spirit of Scott and Matthews. Indeed, the computational interpretation of Theorem 2 can be given in the following terms. Fixed an approximation of the meaning of the recursive denotational specification under study, which is given by an element x0 ∈ X such that p(x0, x0) ≠ 0 (x0 is a partial object of the model which is provided by (X, p) and ≤p) then the contractive condition,
()
gives that the sequence of successive iterations (fn(x0)) n∈ℕ represents the progress of the computational recursion process in such a way that the information about the final stage of the process is increased successively in each passage of the same one, since the smaller p(fn(x0), fn(x0)) is, the more defined fn(x0) is and, thus, fn(x0) contains more information about the meaning of the recursive specification than fn−1(x0). Moreover, the final stage of the process, the meaning of the recursive specification, matches up with the fixed point x* of the self-mapping f which satisfies p(x*, x*) = 0 (x* is a total defined object of the model). Hence the computational process is obtaining in each step of the computation an approximation fn(x0) to the final stage of the process x* which is better than the approximations obtained in the preceding steps. Furthermore, the uniqueness of the fixed point ensures that we can find in the model a univocal representative x* of the meaning whose information content, of course, must include the information content of the first approximation; that is, x* ∈  ↑x0. The fact that x* is maximal gives that there is not another element of the model whose information content approximates the recursive denotational specification meaning better than x*. Finally, the convergence of (fn(x0)) n∈ℕ with respect to 𝒯(ps) and the fact that x* is the supremum of (fn(x0)) n∈ℕ yield that x* captures exactly the information content of the meaning and it does not contain more information that can be derived from the elements of the sequence of approximations.

It must be stressed that the point x0 ∈ X can be interpreted as an initial condition which must be satisfied by the denotational specification and, thus, its meaning should depend on such initial condition; that is, for each initial condition x0 there is a meaning of the denotational specification (see Section 3). In this situation, the fact that the unique fixed point x* of the mapping, whose sequence of successive iterations provides the information about the final stage of the process, belongs to ↑x0 yields that, for each initial condition x0, Theorem 2 gives the meaning of the denotational specification associated with such a condition. Observe that Matthews fixed point theorem, Theorem 1 in Section 1, is not able to analyze those denotational specifications whose meaning depends on an initial condition because the fixed point provided by such a result is unique in the whole space (X, p), which provides the mathematical model joint with ≤p. Therefore, Theorem 2 not only relaxes the hypothesis in the statement of Theorem 1, but also expands the sort of denotational specifications that can be treated by means of quantitative fixed point techniques in the spirit of Theorem 1.

3. Testing the New Fixed Point Technique Based on Partial Metric Spaces

The aim of this section is twofold. On the one hand, we show that the developed method in Section 2 (provided by Theorem 2) is useful, as a quantitative alternative to the Scott one, to analyze the meaning of recursive definitions in denotational semantics for programming languages. On the other hand, we want to validate the aforesaid method by means of proving the meaning of a few illustrative examples of recursive denotational specifications.

To this end, we first consider a recursive algorithm computing the factorial of a positive integer number by means of the recursive denotational specification introduced in Section 1.1; that is,
()

The above denotational specification, as we have pointed out in Section 1.1, has the drawback that the meaning of the symbol fact is expressed in terms of itself. Hence the symbol fact cannot be replaced by its meaning in the denotational specification (1), since the meaning, given by the right-hand side in (1), also contains the symbol.

In order to prove that the meaning of specification (33) is the entire factorial function, we take Σ = ℕ and consider the Baire partial metric space (Σ∞, pB) (cf. Example 6). On account of [6], the Baire partial metric space is complete and, therefore, 0-complete.

In what follows, given x ∈ Σ∞, we will write
()
Next we consider, associated with ϕfact, the mapping ψfact : Σ∞ → Σ∞ defined by ψfact(x) = y, where y, is given by
()

Of course, the meaning, the solution to (33), of the recursive denotational specification (33) is a fixed point of the mapping ψfact. Observe that, in fact, the mapping ψfact has only one fixed point and that the mapping ψfact is an adaptation to the Baire partial metric framework of the mapping ϕfact, whose fixed point is the meaning of the denotational specification (33), introduced in Section 1.1.

Clearly the mapping ψfact is monotone. Define x0 ∈ Σ∞ by x0 = 1. Then l(x0) = 1. It is obvious that x0 is a post-fixed point of ψfact; that is, . Moreover, it is easy to check that for all n ∈ ℕ. Consequently,
()
for all n ∈ ℕ.

Since all assumptions in statement of Theorem 2 hold we obtain that ψfact has a unique fixed point x* ∈  ↑x0. It is evident that models the behavior of the recursive program that computes the factorial function when the input is exactly n ∈ ℕ. In fact, provides the factorial of the number n; that is, is a finite approximation to the entire total factorial function which provides the factorial of every number m ∈ ℕ with m ≤ n. Moreover, the sequence is ascending in and this agrees with the fact that each successive iteration contains more information about the entire factorial function, and thus approaches better the entire factorial function, than the preceding ones. In fact, each successive iteration allows computing the factorial of a positive integer number more than the previous one. Furthermore, Theorem 2 ensures that the fixed point x* of ψfact is the supremum of the ascending sequence and that such a sequence converges to x* with respect to . This guarantees that x* does not contain more information that can be derived from the elements of the sequence of successive iterations . So, x* yields the factorial of every number n ∈ ℕ and, in turn, gives no further information. Finally, it must be stressed that Theorem 2 provides that x* is maximal in and that pB(x*, x*) = 0. Notice that the maximal elements in are exactly those that satisfy the condition pB(x*, x*) = 0. Besides, the condition pB(x*, x*) = 0 is equivalent to l(x*) = ∞. The latter agrees with the fact that the entire total factorial function cannot be represented by an element in ΣF. Moreover, observe that in this case the initial conditions x0 ∈ Σ∞ satisfying that x* ∈  ↑x0 and that x* is the meaning of the denotational specification match up with the prefixes x0 of x* such that l(x0) < ∞. So in this case all initial conditions provide the same fixed point of the mapping ψfact, which is the unique meaning of denotational specification (33).

Therefore, Theorem 2 provides the entire factorial function, the meaning of (33), as the unique fixed point of the mapping ψfact with infinite length.

In the light of the preceding example one could think that Theorem 2 provides a quantitative fixed point technique which is only useful to discuss the meaning of very simple denotational specifications such as the factorial denotational specification where the meaning is unique. However, Theorem 2 is able to analyze denotational specifications which admit more than one meaning such as the next example shows. Consider the recursive specification given as follows:
()
Similarly to the preceding example the denotational specification (37) presents the handicap that the meaning of the symbol f is expressed in terms of itself. It is clear that the meaning of (37) is provided by a collection of mappings {fc : c ∈ ℕ} where fc : ℕ → ℕ is given by
()
In order to apply Theorem 2 to obtain the meaning of (37) as the aforesaid collection of mappings {fc : c ∈ ℕ} we define the mapping ψc on Σ∞, with Σ = ℕ, by ψc(x) = y where y is given by
()
It is not hard to see that each with and is a post-fixed point of ψc with respect to ≤p and
()
for all n ∈ ℕ. Therefore, Theorem 2 yields the existence of a unique fixed point xc,* of ψc in which is maximal, the supremum of in (X,  ≤p), and the limit of the sequence with respect to and, in addition, with l(xc,*) = ∞ (i.e., pB(xc,*, xc,*) = 0). Obviously we have that for any x ∈ Σ∞
()
Therefore, we conclude that Theorem 2 provides for any c ∈ ℕ the unique fixed point of ψc which matches up with the meaning of the denotational specification (37) associated with the initial condition c, that is, matches up with the mapping fc defined above. So our result allows obtaining the meaning of the specification under consideration by means of the collection of fixed points of the mapping ψc preserving, as explained in the preceding case, the original Scott spirit and the quantitative one of Matthews.
Finally, we end the paper analyzing the meaning of an additional denotational specification in order to show the power of the developed theory. In particular, we show that Theorem 2 is able to analyze the denotational specification of a while-loop 〈while B  do C〉. Of course, the preceding denotation expressed by means of sequential composition of commands holds the below specification:
()
Similar to the case of the denotational specifications (33) and (37), the denotational specification (42) presents a disadvantage because the meaning of the symbol 〈while B do C〉 is expressed in terms of itself.
An illustrative example of this sort of situations is given by the following while-loop:
()
where the storage variables X and Y take a nonnegative integer value and an integer one, respectively. If ℤ denotes the set of integer numbers and, in addition, x and y stand for the input values of X and Y, respectively, then it is clear that the meaning of the denotational specification (43) is given by a mapping f : ℕ × ℤ → ℕ × ℤ such that f(x, y) = (0, (x!)*y) for all (x, y) ∈ ℕ × ℤ or, equivalently, by a family of mappings {fy : y ∈ ℤ} such that fy : ℕ → ℕ × ℤ is defined by fy(n) = (0, n! *y) for all n ∈ ℕ (see [40]).

In the following we show that Theorem 2 allows analyzing the meaning of the denotation specification (43). To this end, we consider Σ = ℕ × ℤ and given z ∈ Σ∞ we will write each element of the sequence zn as follows zn = (xn, yn) where xn ∈ ℕ and yn ∈ ℤ for all n ≤ l(z).

Next define the mapping ψwhile : Σ∞ → Σ∞ by
()
where w is given by
()
In what follows we show that the mapping ψwhile holds all conditions in the statement of Theorem 2. Clearly, the Baire partial metric space (Σ∞, pB) is complete and, hence, 0-complete. Moreover, fixed y ∈ ℤ, we have that is a post-fixed point of ψwhile such that for all n ∈ ℕ, where with . Furthermore,
()
for all n ∈ ℕ. Consequently, Theorem 2 guarantees the existence of a unique fixed point zy,* of ψwhile in which is maximal, the supremum of in (X,  ≤p), and the limit of the sequence with respect to and, in addition, with l(zy,*) = ∞ (i.e., pB(zy,*, zy,*) = 0). It is clear that for all n ∈ ℕ, since for any z ∈ Σ∞ we have that
()
So, by Theorem 2, for each y ∈ ℤ we obtain a fixed point zy,* of the mapping ψwhile which matches up with the outputs of the mapping fy for each n ∈ ℕ. Whence we obtain that the meaning of the denotational specification (43) is provided by the collection of fixed points of the mapping ψwhile preserving both the original Scott spirit and the quantitative one of Matthews. Hence the provides a finite approximation to the output of the while-loop when the input values of the variables X and Y are n and y, respectively. Since the sequence is ascending in we have that each successive iteration contains more information about the output of while-loop and approaches better such an output than the preceding ones when the input values of the variables X and Y are n and y, respectively. Moreover, zy,* does not contain more information about the final output of the while-loop than can be derived from the elements of the sequence , since the aforementioned sequence converges to its supremum zy,* with respect to . Furthermore, zy,* is maximal (l(zy,*) = ∞) and this agrees with the fact that, provided the input values for X and Y, the meaning of the while-loop cannot be represented by an element in ΣF (in fact such a meaning matches up with the mapping fy defined above).

Acknowledgments

The authors thank the reviewers for their valuable suggestions which have improved the content of the paper. O. Valero thanks the support from the Spanish Ministry of Economy and Competitiveness, under Grant MTM2012-37894-C02. This work was partially funded by the Deanship of Scientific Research (DSR), King Abdulaziz University, Jeddah. N. Shahzad, therefore, acknowledges with thanks DSR for financial support.

      The full text of this article hosted at iucr.org is unavailable due to technical difficulties.