PCF extended with real numbers

Martín Hötzel Escardó

Department of Computing, Imperial College, 180 Queen’s Gate, London SW7 2BZ, United Kingdom, E-mail: mhe@doc.ic.ac.uk

Abstract

We extend the programming language PCF with a type for (total and partial) real numbers. By a partial real number we mean an element of a cpo of intervals, whose subspace of maximal elements (single-point intervals) is homeomorphic to the Euclidean real line. We show that partial real numbers can be considered as “continuous words”. Concatenation of continuous words corresponds to refinement of partial information. The usual basic operations cons, head and tail used to explicitly or recursively define functions on words generalize to partial real numbers. We use this fact to give an operational semantics to the above referred extension of PCF. We prove that the operational semantics is sound and complete with respect to the denotational semantics. A program of real number type evaluates to a head-normal form iff its value is different from ⊥; if its value is different from ⊥ then it successively evaluates to head-normal forms giving better and better partial results converging to its value.

Keywords: Exact real number computation. Domain Theory and Interval Analysis. Denotational and operational semantics.

1 Introduction

There are several practical and theoretical approaches to exact real number computation (see eg. [7–9,18,21,24,26,30,31,37,39,40,42]). However, the author is not aware of any attempt to give denotational and operational semantics to an implementable programming language with a data type for exact real numbers. Most approaches to exact real number computation are based on representation of real numbers in other data types, such as streams of digits or rational numbers. P. di Gianantonio [9] discusses an extension of PCF with streams and shows how to represent real numbers in this extension (see below).

In this paper we extend the programming language PCF [28] with a type for real numbers. This type is interpreted as the cpo of intervals introduced independently by R.M. Moore in the 60’s [25] and by D.S. Scott in the

To appear in Theoretical Computer Science, July 1996

early 70’s [32]. In fact, such an extension was one of the problems left open by G.D Plotkin [28]. It is straight-forward to give a denotational semantics to such an extension, but it is not immediate how to give an operational semantics to it. P. di Gianantonio also presents an extension of PCF with a ground type interpreted as an algebraic cpo of real numbers, but he does not give an operational semantics to it.

An important feature of our approach to exact real number computation is that the programmer does not have access to representations within the programming language and can think of real numbers as abstract entities in the usual mathematical sense. Of course, the PCF interpreter has access only to concrete representations. The correct interaction between the abstract level and the concrete level is usually referred to as the Adequacy Property (of the operational semantics with respect to the denotational semantics). At the denotational level, a PCF program is just a mathematical expression denoting a number or a function. The task of the programmer is to find a mathematical expression denoting the entity that he or she has in mind. This entity is usually given by unrestricted mathematical means. In this case the programmer has to find an equivalent PCF expression. The Adequacy Property ensures that the entity denoted by the program will actually be computed by the PCF interpreter, and this is why the programmer is not concerned with representations.

We refer to the elements of the cpo of intervals as “partial real numbers”. The domain of partial numbers is a non-algebraic continuous cpo. Its subspace of maximal elements (single-point intervals) is homeomorphic to the Euclidean real line, so that real numbers are special cases of partial real numbers. Notice that no algebraic cpo can have this property.

We show that partial real numbers can be considered as “continuous words”, in the sense that they can be given the structure of a monoid, in such a way that it has a submonoid isomorphic to the monoid of words over any finite alphabet. Moreover, as it is the case for words, the prefix preorder of the monoid of continuous words coincides with its information order. This coincidence is the basis for the successful interaction between the operational and denotational semantics of PCF extended with real numbers.

Concatenation of continuous words have intuitive geometrical and computational interpretations. Geometrically, a concatenation of continuous words corresponds to a rescaling of an interval followed by a translation (an affine transformation). Computationally, a concatenation of continuous words corresponds to refinement of partial information; in a concatenation xy the partial real number y refines the information given by x, by selecting a subinterval of x.

The notion of length of words generalizes to partial real numbers. The length of a partial real number is an extended non-negative real number, being infinity iff the partial number is maximal, and zero iff the partial number is bottom. Roughly speaking, the length of a partial number x considered as a partial realization of an unknown real number y gives the number of digits of an expansion of y that x is able to give correctly. The concatenation operation “adds lengths”, in the sense that the length function is a monoid homomorphism from the monoid of partial real numbers to the additive monoid of non-negative extended real numbers.

The usual basic operations cons, head and tail used to explicitly or recursively define functions on words generalize to partial real numbers. Geometrically, the operation cons is an affine transformation (in analytic terms, a linear map) on the unit interval, tail reverses the effect of cons, and head decides in which half of the real line its argument lies, telling us nothing in ambiguous cases.

Concatenation of partial numbers can be infinitely iterated. This fact gives a notion of meaningful infinite computation. The concatenation of finite initial segments of infinite computations gives more and more information about the final result, in such a way that every piece of information about the (ideal) result is eventually produced in a finite amount of steps. In practice, the terms of a computation can be taken as the partial numbers with distinct rational end-points.

The interpretation of partial real numbers as continuous words is related to a well-known approach to real number computation. Usual binary expansions are not appropriate representations for real number computation; for instance, multiplication by three is not computable if we read the expansions from left to right [42]. But binary expansions of numbers in the signed unit interval [−1, 1] allowing a digit −1 turn out to be effective [8,9,17,40–42]. In the domain of partial numbers contained in the signed unit interval, infinite concatenations of the partial numbers [−1, 0], [−\frac{1}{2}, \frac{1}{2}] and [0, 1] correspond to binary expansions of numbers in the signed unit interval using the digits −1, 0 and 1 respectively.

We use the fact that partial real numbers can be considered as continuous words to obtain an operational semantics for the extension of PCF referred above. We prove that the operational semantics enjoys the following Adequacy Property: a program of real number type evaluates to a head-normal form iff its value is different from ⊥; if its value is different from ⊥ then it successively evaluates to head-normal forms giving better and better partial results converging to its value.

To be accurate, the interpretation of partial numbers as continuous words holds only for the domain of partial real numbers contained in the unit interval (or any other compact interval). The domain of partial number contained in the unit interval is referred to as the lazy unit interval, and the domain of all partial real numbers is referred to as the lazy real line. The above results are extended from the lazy unit interval to the lazy real line via an action of the lazy unit interval on the lazy real line.

Organization

In Section 2 we briefly introduce the domain-theoretic and topological aspects of partial real numbers which are relevant to this paper. In Section 3 we develop the idea that “partial real numbers are continuous words”. In Section 4 we extend PCF with partial real numbers. Finally, in Section 5 we present some concluding remarks and directions for further work.

2 The domain of partial real numbers

2.1 Domains

Our main references to Domain Theory are [3] and [16]. The widely circulated notes [29] are an excellent introduction, but they do not cover (non-algebraic) continuous cpos. The book [19] contains all the domain-theoretic material needed to understand PCF (without real numbers) as well as a detailed account to PCF. In this paper a (continuous Scott) domain is defined to be a bounded complete ω-continuous cpo; notice that a Scott domain is usually defined to be a bounded complete ω-algebraic cpo. In Section 3 we make use of elementary domain theory only, and therefore the reader can think of a domain just as a bounded complete cpo. But in Section 4 we make essential use of continuity, implicitly in the use of function spaces and explicitly in the proof of the Adequacy Theorem 34.

When we refer to a dcpo as a topological space we mean its set of elements under its Scott topology [3,16,35].

2.2 The lazy real line

We denote by R the set of non-empty compact subintervals of the real line ordered by x ⊑ y iff x ⊇ y; see Moore [25] and Scott [32]. If we add a bottom element to the continuous dcpo R, which can be concretely taken as the interval (−∞, +∞), then R becomes a domain, referred to as the lazy real line.

For the topological connections between Domain Theory and Interval Analysis [25] see [15]. In particular, it is shown that the Scott open sets are the Moore open upper sets. Since Moore restricts himself to monotone functions, the results presented in [25] go through if we replace the Moore topology by the Scott topology. See also [4] for more connections between Domain Theory and Interval Analysis.

Following the points of view of both Moore and Scott, we do not consider the elements of R as intervals. We instead consider them as generalized real numbers, in a similar way that complex numbers are considered as generalized real numbers, and we call them partial real numbers. The maximal partial real numbers (that is, the singleton intervals) are identified with the real numbers. This identification makes sense from a topological view, because the subspace of maximal elements of R is homeomorphic to the Euclidean real line. Nonmaximal partial real numbers can be considered as partial realizations of real numbers. For example, [3.14, 3.15] can be considered as a partial realization of π (and of several other numbers). Hence the designation partial real number.

A subset of the lazy real line has a join iff it has an upper bound; when the join exists, it is the intersection of the subset. Every subset of the lazy real line has a meet, namely the least interval (most defined partial number) containing the union of the set.

We denote the left and right end-points of a partial number x by \underline{x} and \overline{x} respectively, so that x = [\underline{x}, \overline{x}].

Two partial numbers x and y have an upper bound iff they overlap. In this case their join is the overlapping part; that is, x ⊔ y = [max(\underline{x}, \underline{y}), min(\overline{x}, \overline{y})]. Dually, we have that their meet is given by x ⊓ y = [min(\underline{x}, \underline{y}), max(\overline{x}, \overline{y})].

The way-below relation on the lazy real line is given by x ≪ y iff x = ⊥, or \underline{x} < \underline{y} and \overline{y} < \overline{x}. Therefore, a basis for the lazy real line is given by the set containing ⊥ and the non-maximal partial numbers with rational (respectively dyadic) end-points. Recall that a dyadic number is a rational of the form m/2^{n}.

2.3 Order of magnitude on the lazy real line

We define a strict order < on partial numbers (not to be confused with the strict version ⊏ of the information order or with the way-below order ≪) by x < y iff \overline{x} < \underline{y}. This relation is clearly irreflexive, transitive, and asymmetric, in the sense that x < y together with x > y is impossible.

We say that two elements x and y of a domain are consistent, written x ≃ y, if they have a common upper bound. The consistency relation is always reflexive and symmetric, but not transitive, and it is preserved by monotone maps.

The following proposition is immediate:

Proposition 1 For all partial real numbers x and y, exactly one of the relations x < y, x ≃ y and x > y holds.

We define a relation ≤ on partial numbers (not to be confused with the information order ⊑) by x ≤ y iff \overline{x} ≤ \underline{y}. This relation does not enjoy any of the properties that an order relation should satisfy, and therefore the notation can be misleading. We introduce it only for notational convenience.

2.4 The lazy unit interval

The set I of all partial numbers contained in the unit interval [0, 1] is a domain, referred to as the lazy unit interval. The bottom element of I is the partial number [0, 1]. Its way-below order is given by x ≪ y iff \underline{x} = 0 or \underline{x} < \underline{y}, and \overline{y} < \overline{x} or \overline{y} = 1.

The lazy unit interval can be presented in a geometrically more convenient form as follows. The unit square [0, 1] × [0, 1] under the componentwise order induced by the usual order ≤ on [0, 1] is a continuous lattice, whose Lawson topology coincides with the Euclidean topology on the unit square; see [16] for a proof of these facts. If we consider the points below (equivalently, on the left of) the diagonal which goes from (0, 1) to (1, 0), that is, the points (x, y) with x + y ≤ 1, we get a triangle, which we refer to as the unit triangle. The unit triangle is easily seen to be a domain. Its maximal elements are the points (x, y) with x + y = 1, that is, the points on the diagonal.

It turns out that the unit triangle is isomorphic to the lazy unit interval. The isomorphisms can be taken as (x, y) ↦ [1 − y, x] and [x, y] ↦ (y, 1 − x). We can think of the unit triangle as a coordinate system for the lazy unit interval.

We have a similar fact for the lazy real line; a coordinate system for R is given by the half-plane consisting of the points (x, y) with x + y ≤ 0. A coordinate system for R_{⊥} is obtained by adding a point (−∞, −∞) to the half-plane.

3 Partial real numbers considered as continuous words

Subsections 3.1–3.7 are restricted to the lazy unit interval and Subsection 3.8 extends the results of these sections to the lazy real line.

3.1 The prefix preorder of a monoid

Recall that a monoid is a set together with a binary associative operation and a neutral element for this operation. It is customary to refer to this operation as multiplication, but in this paper it is convenient to refer to it as concatenation.

By a word over an alphabet Σ we mean either a finite word in Σ^{∗} or an infinite word in Σ^{ω}. We denote the set of all words by Σ^{∞}. Usual concatenation of words, with the convention that xy = x if x is infinite, makes Σ^{∞} into a monoid with neutral element the empty word ε.

In any monoid (M, ·, e) we can define a preorder, called its prefix preorder, by x ≤ z iff xy = z for some y. In this case x is called a prefix of z and y is called a suffix. This relation is reflexive because e is right neutral, and it is transitive because the concatenation operation is associative. It has e as its least element because e is left neutral. Monoid homomorphisms preserve the least element and the prefix preorder, by the very definition of monoid homomorphism. An element x is maximal iff it is left dominant, in the sense that xy = x for every y. The meet of a set, when it exists, is the greatest common prefix of the elements of the set.

The prefix preorder of the monoid Σ^{∞} makes the set Σ^{∞} into a Scott domain [35]. In particular, the prefix preorder is a partial order; that is, it is antisymmetric. An element of Σ^{∞} is maximal iff it is an infinite word, and it is finite in the domain-theoretic sense iff it is a finite word. The concatenation operation seen as a function Σ^{∞} × Σ^{∞} → Σ^{∞} is not continuous, because it is not even monotone. But it is continuous on its second argument. This can be expressed by saying that left translations x ↦ ax are continuous for all words a.

3.2 Left translations of a monoid

We denote a left translation x ↦ ax of a monoid (M, ·, e) by cons_{a}. Left translations are monotone and cons_{a}(M) = ↑ ↑a, where ↑ ↑a = {x ∈ M|a ≤ x}. An element a is left cancelable iff the translation cons_{a} is injective.

If x is left cancelable and x ≤ z, we denote the unique y such that xy = z by z/x, so that x(z/x) = z. The basic properties of this (partially defined) quotient operation are:

x/e = x
x/x = e

(y/x)(z/y) = z/x
(xy)/z = (x/z)y

when the quotients are defined.

Let a be a left cancelable element of a monoid M. Then the co-restriction of cons_{a} to its image is a bijection between the sets M and ↑ ↑a, with inverse x ↦ x/a. Therefore M is a preordered set isomorphic to the set ↑ ↑a under the inherited order, because cons_{a} is monotone.

The left cancelable elements of Σ^{∞} are the finite words. It follows that ↑ ↑a is a domain isomorphic to Σ^{∞} for every finite word a. The subsection below shows that the lazy unit interval has the same property for every non-maximal partial number a, for a suitable concatenation operation on partial numbers.

3.3 Concatenation of partial real numbers

Define a binary operation (x, y) ↦ xy on I by

xy = [(\overline{x} − \underline{x})\underline{y} + \underline{x}, (\overline{x} − \underline{x})\overline{y} + \underline{x}]

That is, given x, y ∈ I, rescale and translate the unit interval so that it becomes x, and define xy to be the interval which results from applying the same rescaling and translation to y. Then it is immediate that xy is a subinterval of x. The rescaling factor is the diameter of x, namely \overline{x} − \underline{x}, and the translation constant is the left end-point of x. If x is maximal, then its diameter is zero, so that xy = x. In order to simplify notation, we let κ_{x} stand for the diameter of x and μ_{x} stand for the left end-point of x. This is the notation of [23] for affine transformations. Notice that x = [μ_{x}, μ_{x} + κ_{x}]. Then we can write

xy = κ_{x}y + μ_{x}

Theorem 2 (I, ·, ⊥) is a monoid with the following properties:

(i) Its prefix preorder coincides with the information order of the domain I. (ii) Its left cancelable elements are the non-maximal ones. (iii) Its left translations preserve all meets and all existing joins.

Proof. Let x, y, z ∈ I. Then

xy = κ_{x}y + μ_{x} = κ_{x}[μ_{y}, μ_{y} + κ_{y}] + μ_{x} = [κ_{x}μ_{y} + μ_{x}, κ_{x}(μ_{y} + κ_{y}) + μ_{x}] Hence μ_{xy} = κ_{x}μ_{y} + μ_{x} and κ_{xy} = κ_{x}κ_{y}. Therefore

(xy)z = κ_{xy}z + μ_{xy} = κ_{x}κ_{y}z + κ_{x}μ_{y} + μ_{x} = κ_{x}(κ_{y}z + μ_{y}) + μ_{x} = x(yz)

Now, clearly x⊥ = x, because by definition ⊥ = [0, 1] is rescaled and translated so that it becomes x. Also, ⊥x = x because by definition ⊥ = [0, 1] is rescaled and translated so that it becomes itself; hence ⊥x is the application of the identity to x. Therefore (I, ·, ⊥) is a monoid.

(i) By construction, x ⊑ xy. If x ⊑ z and x is maximal, then xy = x = z for every y. The proof of item (ii) shows that if x ⊑ z and x is non-maximal then there is a (unique) y such that xy = z.

(ii) A rescaling is reversible iff the rescaling factor is non-zero, a translation is always reversible, and an element has diameter zero iff it is maximal.

(iii) The linear maps p ↦ κ_{x}p + μ_{x} are either increasing order isomorphisms between the real line and itself (if κ_{x} > 0) or else constant maps (if κ_{x} = 0). □

The above proof shows that the concatenation operation on partial numbers “multiplies diameters”, in the sense that κ_{xy} = κ_{x}κ_{y}. Therefore κ_{xy} ≤ κ_{x} and κ_{xy} ≤ κ_{y}, the equalities holding iff x = ⊥ or y = ⊥.

Concatenation of partial numbers has the following geometrical and computational interpretations. In a concatenation xy, the interval y refines the information given by x by selecting a subinterval of x. For example, the partial numbers [0, 1], [0, \frac{1}{2}], [\frac{1}{2}, 1], and [\frac{1}{3}, \frac{2}{3}] respectively select the whole interval, the first half, the second half, and the middle third part. Thus, concatenation of partial numbers allows for incremental computation on partial real numbers, also known as lazy evaluation (cf. Proposition 4). Hence the denomination lazy unit interval.

There is yet another geometrical interpretation of concatenation, induced by the isomorphism between the lazy unit interval and the unit triangle. The upper set of any non-maximal element x of the unit triangle is clearly a triangle, isomorphic to the unit triangle via a rescaling of the unit triangle followed by a translation. Thus, any element y can be interpreted either as an absolute address of a point in the unit triangle or else as a relative address of a point in the smaller triangle generated by x, namely the point xy, obtained by applying the same rescaling and translation to y.

We finish this subsection with the following lemma:

Lemma 3 The bases of the lazy unit interval consisting of respectively all nonmaximal partial numbers and all non-maximal partial numbers with rational end-points are submonoids of (I, ·, ⊥) closed under existing quotients, in the sense that if b and c are basis elements with b ⊑ c then c/b is a basis element too.

Proof. Existing quotients are given by

y/x = (y − μ_{x})/κ_{x} =_{def} [(\underline{y} − μ_{x})/κ_{x}, (\overline{y} − μ_{x})/κ_{x})]

Therefore, if x and y have distinct (rational) end-points, so does y/x. □

The basis consisting of all non-maximal partial numbers with dyadic endpoints is a submonoid, but it is not closed under existing quotients.

3.4 Infinitely iterated concatenations

Let M be a monoid with a partial prefix order and joins of non-decreasing ω-chains, and let ⟨x_{n}⟩_{n≥1} be a sequence of elements of M. Then we have that

x_{1} ≤ x_{1}x_{2} ≤ ⋯ ≤ x_{1}x_{2} ⋯ x_{n} ≤ ⋯

The infinitely iterated concatenation of ⟨x_{n}⟩_{n≥1} is defined to be the join of these partial concatenations, informally denoted by x_{1}x_{2} ⋯ x_{n} · · ·. It is also convenient to use the informal notation y_{1} ⊔ y_{2} ⊔ ⋯ ⊔ y_{n} ⊔ ⋯ for the join of a chain y_{1} ≤ y_{2} ≤ ⋯ ≤ y_{n} ≤ · · ·.

An interval expansion of a partial real number x is a sequence of intervals ⟨x_{n}⟩_{n≥1} such that x = x_{1}x_{2} ⋯ x_{n} · · ·. For example, interval expansions formed from the intervals

[0, \frac{1}{10}] , [\frac{1}{10}, \frac{2}{10}] , …, [\frac{8}{10}, \frac{9}{10}] , [\frac{9}{10}, 1]

are essentially decimal expansions.

If we think of an infinitely iterated concatenation as a computation, the following proposition shows that we can compute in an incremental fashion if left translations are continuous:

Proposition 4 (Infinite associativity) Let M be a monoid with infinitely iterated concatenations. Then M satisfies the ω-associativity law

x_{1}(x_{2} ⋯ x_{n} ⋯) = x_{1}x_{2} ⋯ x_{n} ⋯

iff left translations preserve joins of non-decreasing ω-chains.

Proof. (⇒) Assume that the ω-associativity law holds, let ⟨y_{n}⟩_{n≥1} be a nondecreasing ω-chain of elements of M, and let ⟨x_{n}⟩_{n≥1} be a sequence of elements of M such that y_{n}x_{n} = y_{n+1}. Then the join of the chain is the same as the infinitely iterated concatenation of the sequence ⟨x_{n}⟩_{n≥1} with y_{1} added as a new first element, because y_{1}x_{1}x_{2} ⋯ x_{n} = y_{n}, as an inductive argument shows. Therefore

a(y_{1} ⊔ y_{2} ⊔ ⋯ ⊔ y_{n} ⊔ ⋯) = a(y_{1}x_{1}x_{2} ⋯ x_{n} ⋯)
= ay_{1}x_{1}x_{2} ⋯ x_{n} ⋯
= a ⊔ ay_{1} ⊔ ay_{1}x_{1} ⊔ ⋯ ⊔ ay_{1}x_{1} ⋯ x_{n} ⊔ ⋯
= a ⊔ ay_{1} ⊔ ay_{2} ⊔ ⋯ ⊔ ay_{n} ⊔ ⋯
= ay_{1} ⊔ ay_{2} ⊔ ⋯ ⊔ ay_{n} ⊔ ⋯

(⇐) Assume that left translations preserve joins of non-decreasing ω-chains. Then we have that

x_{1}(x_{2} ⋯ x_{n} ⋯) = x_{1}(x_{2} ⊔ x_{2}x_{3} ⊔ ⋯ ⊔ x_{2}x_{3} ⋯ x_{n} ⊔ ⋯)
= x_{1}x_{2} ⊔ x_{1}x_{2}x_{3} ⊔ ⋯ ⊔ x_{1}x_{2}x_{3} ⋯ x_{n} ⊔ ⋯
= x_{1} ⊔ x_{1}x_{2} ⊔ x_{1}x_{2}x_{3} ⊔ ⋯ ⊔ x_{1}x_{2}x_{3} ⋯ x_{n} ⊔ ⋯
= x_{1}x_{2} ⋯ x_{n} ⋯  □

We denote the infinitely iterated concatenation xx ⋯ x ⋯ of a constant sequence with range x by x^{ω}. An immediate consequence of the above proposition is that x^{ω} is the least fixed point of cons_{x} for any monoid with infinite concatenations.

Now let y_{1} ≤ y_{2} ≤ ⋯ ≤ y_{n} ≤ ⋯ be a chain of left cancelable elements. Then the sequence y_{1}, y_{2}/y_{1}, y_{3}/y_{2}, …, y_{n+1}/y_{n}, … has the elements of the chain as partial concatenations. Therefore the join of the chain is the same as the infinite concatenation of the induced sequence.

Proposition 5 Consider the bases of I consisting of respectively all nonmaximal partial numbers and all non-maximal partial numbers with rational end-points. Then there is a bijection between ω-chains of basis elements and sequences of basis elements, taking any chain to a sequence whose infinitely interated concatenation is the join of the chain. □

Therefore we can replace ω-chains of basis elements by (arbitrary) sequences of basis elements and work with infinitely iterated concatenations instead of joins.

For monoids with infinitely interated concatenations, it is natural to ask homomorphisms to preserve them.

Proposition 6 A monoid homomorphism preserves infinitely iterated concatenations iff it preserves joins of increasing ω-chains

Proof. Let h : L → M be a monoid homomorphism between monoids L and M.

(⇒) Let ⟨y_{n}⟩_{n≥1} be an non-decreasing ω-chain of elements of L having a join and let ⟨x_{n}⟩_{n≥1} be a sequence of elements of L such that y_{n}x_{n} = y_{n+1}. Then we have that

h(y_{1} ⊔ ⋯ ⊔ y_{n} ⊔ ⋯)
= h(y_{1}x_{1} ⋯ x_{n} ⋯)
= h(y_{1})h(x_{1}) ⋯ h(x_{n}) ⋯
= h(y_{1}) ⊔ h(y_{1})h(x_{1}) ⊔ ⋯ ⊔ h(y_{1})h(x_{1}) ⋯ h(x_{n}) ⊔ ⋯
= h(y_{1}) ⊔ ⋯ ⊔ h(y_{n}) ⊔ ⋯

because h(y_{n})h(x_{n}) = h(y_{n+1}).

(⇐) Let ⟨x_{i}⟩_{i≥1} be a sequence of elements of L having an infinitely iterated concatenation. Then we have that

h (x_{1}x_{2} ⋯ x_{n} ⋯) = h (x_{1} ⊔ x_{1}x_{2} ⊔ ⋯ ⊔ x_{1}x_{2} ⋯ x_{n} ⊔ ⋯)
= h(x_{1}) ⊔ h(x_{1}x_{2}) ⊔ ⋯ ⊔ h(x_{1}x_{2} ⋯ x_{n}) ⊔ ⋯
= h(x_{1}) ⊔ h(x_{1})h(x_{2}) ⊔ ⋯ ⊔ h(x_{1})h(x_{2}) ⋯ h(x_{n}) ⊔ ⋯
= h(x_{1})h(x_{2}) ⋯ h(x_{n}) ⋯  □

3.5 Continuous words

Concatenation of partial numbers in the lazy unit interval generalizes concatenation of words over any finite alphabet, in the following sense:

Proposition 7 For every finite n-letter alphabet Σ, the monoid Σ^{∞} is isomorphic to a submonoid of I. Moreover, the induced embedding of Σ^{∞} into I is a continuous monoid homomorphism.

Proof. Without essential loss of generality, we prove the claim for the twoletter case Σ = {0, 2}. Let C be the submonoid of I finitely generated by the partial numbers [0, 1/3] and [2/3, 1]. Then C clearly contains the partial numbers corresponding to the intervals successively produced in the construction of the Cantor set. Hence the joins of strictly increasing ω-chains of elements of C are the elements of the Cantor set. But these joins are the infinitely iterated concatenations of the generators. The set C of finite and infinite concatenations of the generators is also a submonoid of I, which can be considered as the monoid of partial Cantor numbers. It is easy to see that {0, 2}^{∞} is isomorphic to C. We know that {0, 2}^{∗} is the free monoid over {0, 2}. Hence there is a unique monoid homomorphism h : {0, 2}^{∗} → C such that h(0) = [0, 1/3] and h(2) = [2/3, 1]. But h has a unique continuous extension to {0, 2}^{∞}, because monoid homomorphisms are monotone and {0, 2}^{∗} consists of the finite elements (in the domain-theoretic sense) of {0, 2}^{∞}. The resulting extension is a monoid homomorphism. Since it takes an infinite word x to the element of the Cantor set whose ternary expansion is x, it follows that h is a bijection, and therefore a monoid isomorphism. □

Therefore, the elements of the lazy unit interval can be considered as “continuous words”. For any word x ∈ Σ^{∞} let length(x) ∈ [0, ∞] denote the length of x defined in the usual way. For any continuous word x ∈ I and any real number b > 1 we define length_{b}(x) ∈ [0, ∞] to be − log_{b}(κ_{x}). Thus, length_{b}(x) = ∞ iff x is maximal, and length_{b}(x) = 0 iff x is bottom.

If a continuous word x is a partial realization of an unknown real number y, then length_{b}(x) is the number of correct digits of an expansion to base b of y that x allows us to know. For example, if we consider x = [0.143, 0.145] as a partial realization of an unknown real number y then length_{10}(x) is roughly 2.7, meaning that x allows us to know two decimal digits of y.

Proposition 8 Consider [0, ∞] as a monoid under addition and as a domain under its prefix preorder (which coincides with its natural order).

(i) For every real number b > 1, length_{b} : I → [0, ∞] is a continuous monoid homomorphism.

(ii) Let h be the embedding of the monoid of words over a finite n-letter alphabet into I defined in Proposition 7. Then length = length_{n+1} ∘ h.

Proof. Routine verification. The first part follows from the fact that the concatenation operation multiplies diameters and that logarithms take multiplication to addition. □

Corollary 9 The infinitely iterated concatenation of a sequence of continuous words is maximal iff the sum of the lengths of the continuous words is ∞.

Proof. The length function is a continuous monoid homomorphism and a partial number has infinite length iff it is maximal. □

The following proposition allows us to prove some properties of real number programs. We say that a map f : I → I is guarded if there is a real number δ > 0 such that length(f(x)) ≥ length(x) + δ, called a guarding constant for f. Clearly, left translations cons_{a} with a ≠ ⊥ are guarded, with guarding constant length(a).

Proposition 10 Any continuous guarded map f : I → I has a maximal partial number as its unique fixed point.

Proof. Since length(f^{n}(⊥)) ≥ nδ for every n and length is a continuous homomorphism, length (⨆_{n} f^{n}(⊥)) ≥ sup_{n} nδ = ∞. This means that the least fixed point of f is maximal. Therefore it is the unique fixed point of f. □

3.6 Heads and tails of continuous words

We begin by considering the head and tail maps on words over the alphabet Σ = {0, 1}.

Let σ range over Σ, and define maps tail : Σ^{∞} → Σ^{∞} and head : Σ^{∞} → Σ_{⊥}

tail(ϵ) = ϵ
tail(σx) = x
head(ϵ) = ⊥
head(σx) = σ

These maps are continuous, and we have that

tail(cons_{σ}(x)) = x
head(cons_{σ}(x)) = σ

Recall that a pair of continuous maps s : D → E and r : E → D between dcpos D and E with the property that

r ∘ s = id

is called a section-retraction pair [3]. In this case s preserves all existing meets and joins, and s ∘ r is an idempotent.

By definition, tail is a retraction and cons_{σ} is a section. Recall also that if in addition the induced idempotent has

s ∘ r ⊑ id

then the pair of maps s and r are said to be an embedding-projection pair. The pair of maps tail and cons_{σ} are not an embedding-projection pair, because for example

cons_{0}(tail(ϵ)) = 0 ⋢ ϵ = id(ϵ)

Now define a continuous equality map (x, y) ↦ (x =_{⊥} y) : Σ_{⊥}×Σ_{⊥} → {tt, ff}_{⊥} by

(x =_{⊥} y) = \{ \begin{matrix}tt & if x, y ∈ Σ and x = y \\ ⊥ & if ⊥ ∈ \{x, y\} \\ ff & if x, y ∈ Σ and x ≠ y \end{matrix}

and a continuous conditional map

(p, x, y) ↦ (if p then x else y) : {tt, ff}_{⊥} × Σ^{∞} × Σ^{∞} → Σ^{∞}

by

if p then x else y = \{ \begin{matrix}x & if p = tt \\ ϵ & if p = ⊥ \\ y & if p = ff \end{matrix}

Then we have that

x = if head(x) =_{⊥} 0 then cons_{0}(tail(x)) else cons_{1}(tail(x))  (1)

Manipulations of this equation lead to usual explicit and recursive definitions of several functions. For example, it follows from (1) that the identity function satisfies the equation

id(x) = if head(x) =_{⊥} 0 then cons_{0}(id(tail(x))) else cons_{1}(id(tail(x)))

In fact, the identity function is the unique continuous map which satisfies the functional equation

f(x) = if head(x) =_{⊥} 0 then cons_{0}(f(tail(x))) else cons_{1}(f(tail(x)))

The function that switches the rôles of the letters 0 and 1 can be given by the the recursive definition

g(x) = if head(x) =_{⊥} 0 then cons_{1}(g(tail(x))) else cons_{0}(g(tail(x)))

In this subsection we look for a generalization of this theme for partial numbers. The first problem to be overcome is that continuous words have nonintegral lengths and in particular non-zero lengths < 1. Moreover, a continuous word of length > 1 has infinitely many prefixes of length 1. Since the head map on words extracts a prefix of length 1, it is not immediately clear what the head map on continuous words should be for words of length < 1.

Under the embedding of Σ^{∞} into I defined in Proposition 7, if we put

l = [0, 1/3] and r = [2/3, 1]

then Equation (1) becomes

x = if x <_{⊥} \frac{1}{2} then cons_{l}(x/l) else cons_{r}(x/r)  (1′)

where the conditional map is defined in the same way for partial numbers and the continuous comparison map (x, y) ↦ (x <_{⊥} y) : I × I → {tt, ff}_{⊥} is defined by

(x <_{⊥} y) = \{ \begin{matrix}tt & if x < y \\ ⊥ & if x ≃ y \\ ff & if x > y \end{matrix}

Remark 11 If we had x <_{⊥} x = ff then this map would not be continuous. □

Then we need a continuous map tail_{a} : I → I, for any left cancelable partial number a, with the property that

tail_{a}(x) = x/a for every x with x ⊑ a, that is, with the property that tail_{a} is a left-inverse of cons_{a}. A naïve attempt to obtain such a map would be to put tail_{a}(x) = ⊥ if x ⋢ a. But then tail_{a} would not be continuous.

Lemma 12 Let a ∈ I be a non-maximal element, let tail_{a} : I → I be any continuous left inverse of cons_{a}, and let f_{a} be the induced idempotent. Then for every x ∈ I,

(i) a ⊑ f_{a}(x) (ii) f_{a}(x) = x iff a ⊑ x (iii) tail_{a}(x) = f_{a}(x)/a

Proof. (1) a ⊑ cons_{a}(tail_{a}(x)) = f_{a}(x).

(2) (⇒) Immediate consequence of (1) above. (⇐) If a ⊑ x then x = a(x/a) and f_{a}(x) = cons_{a}(tail_{a}(a(x/a))) = cons_{a}(x/a) = x.

(3) tail_{a}(x) = cons_{a}(tail_{a}(x))/a = f_{a}(x)/a. □

Thus, in order to obtain a continuous left inverse of cons_{a} we first look for a continuous map f_{a} enjoying properties (1) and (2) above. Assume that x ≃ a. Then f_{a}(x) ⊑ f_{a}(x ⊔ a) = x ⊔ a, because x ⊑ x ⊔ a. Since a ⊑ x ⊔ a, by (1) and (2) it is natural to let f_{a}(x) be x ⊔ a. Then f_{a}(x) can be thought as the truncation of x to a, because x ⊔ a is the greatest subinterval of x contained in a.

Lemma 13 Let a be an element of I. If join_{a} : I → I is a monotone map such that

join_{a}(x) = x ⊔ a for all x ≃ a.

then join_{a}(x) = \underline{a} for all x < a and join_{a}(x) = \overline{a} for all x > a.

Proof. Here we write \underline{a} to mean [\underline{a}, \underline{a}], of course. Assume that x < a. This means that \overline{x} < \underline{a}. Then [\underline{x}, \underline{a}] ⊑ x. Hence \underline{a} = join_{a}([\underline{x}, \underline{a}]) ⊑ join_{a}(x). Therefore \underline{a} = join_{a}(x), because \underline{a} is maximal. The other case is similar. □

Lemma 14 For all non-maximal a ∈ I define maps join_{a}, tail_{a} : I → I by

join_{a}(x) = \{ \begin{matrix}\underline{a} & if x < a \\ x ⊔ a & if x ≃ a \\ \overline{a} & if x > a \end{matrix}

tail_{a}(x) = join_{a}(x)/a

Then join_{a} and tail_{a} are continuous.

Proof.

join_{a}(x) = max(\underline{a}, min(x, \overline{a})) =_{def} [max(\underline{a}, min(\underline{x}, \overline{a})), max(\underline{a}, min(\overline{x}, \overline{a}))]

Hence

tail_{a}(x) = max(\underline{a}, min(x, \overline{a}))/a = (max(\underline{a}, min(x, \overline{a})) − μ_{a})/κ_{a}
= max(0, min((x − μ_{a})/κ_{a}, 1))

Since join_{a} and tail_{a} are the pointwise extensions of the non-decreasing continuous maps

r ↦ max(\underline{a}, min(r, \overline{a})) : [0, 1] → [0, 1]
r ↦ max(0, min((r − μ_{a})/κ_{a}, 1)) : [0, 1] → [0, 1]

respectively, it follows that they are continuous (see Moore [25]). □

Proposition 15 For all non-maximal a ∈ I, the maps cons_{a} and tail_{a} form a section-retraction pair, with join_{a} as the induced idempotent.

Proof. Immediate consequences of Lemmas 12 and 14. □

Notice that the definition of join_{a} makes sense even for maximal partial numbers a; in this case join_{a} is a constant map with range a. If we define x □ y = join_{x}(y), then (I, □, ⊥) is a monoid whose prefix preorder coincides with the information order on I. Of course, this monoid is not isomorphic to the monoid (I, ·, ⊥) This shows that there are several essentially different ways of making I into a monoid inducing the information order of I.

The second problem to be overcome is that Equation (1′) is true only for a restricted set of partial numbers x. This problem is partially solved by replacing l and r by

L = [0, \frac{1}{2}] and R = [\frac{1}{2}, 1]

respectively. By replacing the (sequential) conditional by the parallel one, namely (p, x, y) ↦ (pif p then x else y) : {tt, ff}_{⊥} × I × I → I defined by

pif p then x else y = \{ \begin{matrix}x & if p = tt \\ x ⊓ y & if p = ⊥ \\ y & if p = ff \end{matrix}

(cf. [28] and Subsection 4.5), the problem is completely solved. Recall that the meet x ⊓ y is the greatest common prefix of the continuous words x and y.

Finally, for each r ∈ [0, 1] define head_{r} : I → {tt, ff}_{⊥} by

head_{r}(x) = (x <_{⊥} r)

Theorem 16 For any partial number x ∈ I,

x = pif head_{\frac{1}{2}} (x) then cons_{L}(tail_{L}(x)) else cons_{R}(tail_{R}(x))  (1′′)

Proof. By virtue of Proposition 15, it suffices to check the crucial case x ≃ \frac{1}{2}. Equation (1′′) is true in this case because

join_{L}(x) = [\underline{x}, \frac{1}{2}] join_{R}(x) = [\frac{1}{2}, \overline{x}]

and therefore join_{L}(x) ⊓ join_{R}(x) = x. □

Of course, there is nothing special about the number \frac{1}{2} and the partial numbers [0, \frac{1}{2}] and [\frac{1}{2}, 1]; the above theorem works for any binary partition of the unit interval, and can be extended to any finite n-ary partition with n ≥ 2.

The idea behind the above theorem is strongly related to the ideas presented in [14]; see Examples 18, 19, and 25. See also Smyth’s constructions of the unit interval as inverse limits of finite topological structures [36].

Example 17 (Path composition) The parallel conditional can be used to overcome the fact that x <_{⊥} x is ⊥ instead of ff.

Let E be any domain, and let f, g : I → E be continuous maps. Then f and g are (generalized) paths in the domain E. (The restrictions of f and g to the singleton intervals are paths in the usual sense [20].) If f(1) = g(0) the paths are said to be composable. Now define a continuous map h : I → E by

h(x) = pif x <_{⊥} \frac{1}{2} then f(2x) else g(2x − 1)

If the paths are composable, then h is a (generalized) composite path. Let us check the crucial case x = \frac{1}{2}:

h(\frac{1}{2}) = pif \frac{1}{2} <_{⊥} \frac{1}{2} then f(2\frac{1}{2}) else g(2\frac{1}{2} − 1) = pif ⊥ then f(1) else g(0)
= f(1) ⊓ g(0) = f(1) = g(0)

Notice that the sequential conditional would produce ⊥ instead of f(1) ⊓ g(0), and therefore h would be undefined at \frac{1}{2}.

If f and g are not composable, then h is a generalized composite path with a jump at \frac{1}{2}, namely f(1)⊓g(0). For instance, if E = I and f and g are constant maps with range 0 and 1, then h can be thought as a switch which turns on at time \frac{1}{2}. In this case, the switch is in the transition state [0, 1] = 0⊓1 at time \frac{1}{2}. Notice that even in this case h is Scott continuous, because it is a composition of continuous maps. □

The following recursive definitions generalize the recursive definition for real numbers presented in [14] to partial real numbers.

Example 18 (Complement) We now derive a recursive definition of the extension of the complement map r ↦ 1 − r on [0, 1] to I given by

1 − x = [1 − \overline{x}, 1 − \underline{x}]

Of course, for maximal partial numbers, this indeed coincides with the original map, up to the identification of real numbers and maximal partial numbers.

We begin with the following observation:

(i) If x ⊆ L then 1 − x ⊆ R. (ii) If x ⊆ R then 1 − x ⊆ L.

This leads one to write down the following set of incomplete equations:

1 − cons_{L}(x) = 1 − cons_{R}(⋯)
1 − cons_{R}(x) = 1 − cons_{L}(⋯)

If we can fill the gaps with expressions depending on 1 − x then we are almost done. Routine algebra shows that the gaps can be filled in an essentially unique way:

1 − cons_{L}(x) = 1 − cons_{R}(1 − x)
1 − cons_{R}(x) = 1 − cons_{L}(1 − x)

Now we reduce this two equations to a single equation, by means of the primitive operations that we have introduced:

1 − x = pif head_{\frac{1}{2}} (x) then cons_{R}(1 − tail_{L}(x)) else cons_{L}(1 − tail_{R}(x))

This can be considered as a recursive definition of complement, because if we eliminate recursion by means of the least fixed point operator then it is possible to prove by fixed point induction [3] that complement is the least (in fact, the unique) fixed point of the induced functional. We use fixed point induction in conjunction with an induction principle for partial real numbers generalizing the one introduced in [14].

It is illustrative to unfold 1 − [a, b] for [a, b] ∈ I with 1/2 ∈ [a, b]:

1 − [a, b] = pif ⊥ then cons_{R}(1 − [2a, 1]) else cons_{L}(1 − [0, 2b − 1])
= cons_{R}([0, 1 − 2a]) ⊓ cons_{L}([2 − 2b, 1])
= [\frac{1}{2}, 1 − a] ⊓ [1 − b, \frac{1}{2}] = [1 − b, 1 − a]

Notice that the above recursive definition resembles a recursive definition with respect to binary representation, with L and R corresponding to the digits 0 and 1 respectively. □

Example 19 (Average) We now derive a recursive definition of the extension of the average operation

r ⊕ s = \frac{r + s}{2}

given by

x ⊕ y = [\underline{x} ⊕ \underline{y}, \overline{x} ⊕ \overline{y}]

The derivation follows the same pattern as the derivation of the recursive definition of complement given in the above example.

Initial observation:

(i) If x, y ⊆ L then x + y ⊆ L. (ii) If x ⊆ L and y ⊆ R then x + y ⊆ C. (iii) If x, y ⊆ R then x + y ⊆ R. where C = [1/4, 3/4]. Incomplete equations:

cons_{L}(x) ⊕ cons_{L}(y) = cons_{L}(⋯)
cons_{L}(x) ⊕ cons_{R}(y) = cons_{C}(⋯)
cons_{R}(x) ⊕ cons_{L}(y) = cons_{C}(⋯)
cons_{R}(x) ⊕ cons_{R}(y) = cons_{R}(⋯)

Gaps filled:

cons_{L}(x) ⊕ cons_{L}(y) = cons_{L}(x ⊕ y)
cons_{L}(x) ⊕ cons_{R}(y) = cons_{C}(x ⊕ y)
cons_{R}(x) ⊕ cons_{L}(y) = cons_{C}(x ⊕ y)
cons_{R}(x) ⊕ cons_{R}(y) = cons_{R}(x ⊕ y)

Reduction to a single equation: x ⊕ y = pif head_{\frac{1}{2}} (x) then pif head_{\frac{1}{2}} (y) then cons_{L}(tail_{L}(x) ⊕ tail_{L}(y))

else cons_{C}(tail_{L}(x) ⊕ tail_{R}(y))

else pif head_{\frac{1}{2}} (y) then cons_{C}(tail_{R}(x) ⊕ tail_{L}(y)) else cons_{R}(tail_{R}(x) ⊕ tail_{R}(y)),

In practice it may be convenient to use the more familiar notations

x < \frac{1}{2}, x/2, x/2 + 1/4, x/2 + \frac{1}{2}, min(2x, 1), and max(0, 2x − 1) instead of

head_{\frac{1}{2}} (x), cons_{L}(x), cons_{C}(x), cons_{R}(x), tail_{L}(x), and tail_{R}(x) respectively, and even write 2x and 2x − 1 for the last two cases by an abuse of notation. With this notation the above recursive definition becomes x ⊕ y = pif x < \frac{1}{2} then pif y < \frac{1}{2} then (2x ⊕ 2y)/2

else (2x ⊕ (2y − 1))/2 + 1/4

else pif y < \frac{1}{2} then ((2x − 1) ⊕ 2y)/2 + 1/4

else ((2x − 1) ⊕ (2y − 1))/2 + \frac{1}{2} □

Example 20 (Multiplication) We now derive a recursive definition of multiplication, which is extended in the same way as average. During this example juxtaposition means multiplication instead of concatenation. Again, the derivation follows the same pattern.

Initial observation:

(i) If x, y ⊆ L then xy ⊆ [0, 1/4]. (ii) If x ⊆ L and y ⊆ R then xy ⊆ [0, 1/2]. (iii) If x, y ⊆ R then xy ⊆ [1/4, 1].

Incomplete equations:

cons_{L}(x) × cons_{L}(y) = cons_{[0, 1/4]}(⋯)
cons_{L}(x) × cons_{R}(y) = cons_{[0, 1/2]}(⋯)
cons_{R}(x) × cons_{L}(y) = cons_{[0, 1/2]}(⋯)
cons_{R}(x) × cons_{R}(y) = cons_{[1/4, 1]}(⋯)

Gaps filled with expressions depending on x, y and xy:

cons_{L}(x) × cons_{L}(y) = cons_{[0, 1/4]}(xy)
cons_{L}(x) × cons_{R}(y) = cons_{[0, 1/2]} (\frac{x + xy}{2} )
cons_{R}(x) × cons_{L}(y) = cons_{[0, 1/2]} (\frac{xy + y}{2} )
cons_{R}(x) × cons_{R}(y) = cons_{[1/4, 1]} (\frac{x + xy + y}{3} )

Now we have to find a recursive definition of ternary average. In this case there are eight cases to consider, but since the operation is permutative (permutativity is the generalization of commutativity to n-ary operations), there are really only four cases to consider. We omit the routine derivation and the reduction to a single equation. □

3.7 Computation rules for continuous words

The following lemma shows how to reduce expressions e denoting non-bottom partial numbers to expressions of the form cons_{a}(e′) with a ≠ ⊥. Such an expression is called a head-normal form. The idea is that if an expression e has a head-normal form cons_{a}(e′) then we know that its value is contained in a.

Thus, a head-normal form is a partially evaluated expression. A better partial evaluation of e is obtained by partially evaluating e′, obtaining a head-normal form cons_{b}(e′′), and applying rule (i) below to cons_{a}(cons_{b}(e′′)) in order to obtain the more informative head-normal form cons_{ab}(e′′) of e, and so on.

Lemma 21 For all non-maximal a, b ∈ I and all x ∈ I,

(i) cons_{a}(cons_{b}(x)) = cons_{ab}(x) (ii) tail_{a}(cons_{b}(x)) = L^{ω} if b ≤ a (iii) tail_{a}(cons_{b}(x)) = R^{ω} if b ≥ a (iv) tail_{a}(cons_{b}(x)) = cons_{b/a}(x) if a ⊑ b

(v) tail_{a}(cons_{b}(x)) = cons_{(a⊔b)/a}(tail_{(a⊔b)/b}(x)) if a ≃ b (vi) head_{r}(cons_{a}(x)) = tt if a < r (vii) head_{r}(cons_{a}(x)) = ff if a > r (viii) pif tt then x else y = x (ix) pif ff then x else y = y

(x) pif p then cons_{a}(x) else cons_{b}(y) =

cons_{a⊓b}(pif p then cons_{a/(a⊓b)}(x)

else cons_{b/(a⊓b)}(y))

Proof. (i) This is the associativity law expressed in terms of left translations. (ii) If b ≤ a then tail_{a}(bx) = 0 = [0, \frac{1}{2}]^{ω}. (iii) Similar.

(iv) Equivalent to the fact that (bx)/a = (b/a)x.

(v) For all c ≃ x, cons_{b}(join_{c}(x)) = cons_{b}(c ⊔ x) = cons_{b}(c) ⊔ cons_{b}(x) = join_{bc}(cons_{b}(x)), because left-translations preserve existing joins. Hence

tail_{a}(cons_{b}(x)) = join_{a}(cons_{b}(x))/a = join_{a⊔b}(cons_{b}(x))/a
= join_{b((a⊔b)/b)}(cons_{b}(x))/a = cons_{b}(join_{(a⊔b)/b}(x))/a
= cons_{b}(cons_{(a⊔b)/b}(tail_{(a⊔b)/b}(x)))/a
= cons_{a⊔b}(tail_{(a⊔b)/b}(x))/a = cons_{(a⊔b)/a}(tail_{(a⊔b)/b}(x))

The second step follows from the fact that join_{a}(y) = join_{a⊔b}(y) if a ≃ b and b ⊑ y. The last step follows from the fact that (cy)/a = (c/a)y.

(vi–ix) Immediate. (x) It suffices to show that

cons_{a}(x) ⊓ cons_{b}(y) = cons_{a⊓b}(cons_{a/(a⊓b)}(x) ⊓ cons_{b/(a⊓b)}(y))

Since left translations preserve meets and a = c(a/c) for all c, the result follows by taking c = a ⊓ b. □

3.8 The lazy unit interval acting on the lazy real line

In this subsection we extend the results of the previous subsections from the lazy unit interval to the lazy real line.

The concatenation operation

xy = κ_{x}y + μ_{x}

originally defined for x and y in the lazy unit interval makes sense for x and y ranging over the lazy real line. With this extension, R becomes a monoid too. But its prefix preorder does not coincide with its information order, and it is due to this reason that we initially restricted ourselves to the lazy unit interval. In fact, if y = ax this does not mean that y is contained in a. However, if we know that x is in the lazy unit interval then y = ax do imply that y is contained in a, even if y is not in the lazy unit interval. This is the content of the following theorem.

Theorem 22 The map (x, y) ↦ xy : R × I → R is a (right) action of the monoid (I, ·, ⊥) on the monoid (R, ·, [0, 1]), inducing the information order of R:

(i) For all x ∈ R and all y, z ∈ I, x⊥ = x and (xy)z = x(yz). (ii) For all x, z ∈ R, x ⊑ z iff xy = z for some y ∈ I, such a y being unique

iff x is non-maximal.

Moreover, for all a ∈ R, the map ricons_{a} : I → R_{⊥} defined by ricons_{a}(x) = ax preserves all meets and all existing joins. □

Given x, z ∈ R with x ⊑ z and x non-maximal, denote the unique y ∈ I such that xy = z by z/x.

For each non-maximal a ∈ R, define a strict continuous map irtail_{a} : R_{⊥} → I and a continuous non-strict map rrjoin_{a} : R_{⊥} → R_{⊥} by extending Lemma 14 in the obvious way, so that

irtail_{a}(x) = x/a if x ⊑ a

Finally, for each non-maximal a ∈ R define a strict continuous map rrcons_{a} : R_{⊥} → R_{⊥} by

rrcons_{a}(x) = ax

Proposition 23 For all non-maximal a ∈ R, the maps ricons_{a} and irtail_{a} form a section-retraction pair, with rrjoin_{a} as the induced idempotent. □

Thus, I is a retract of R_{⊥}, in many ways. In particular,

(i) ricons_{[0,1]} : I → R_{⊥} is the inclusion, (ii) irtail_{[0,1]} : R_{⊥} → I is a “truncated projection”, and (iii) rrjoin_{[0,1]} : R_{⊥} → R_{⊥} is the co-extension of the truncated projection.

Example 24 (Addition) We obtain a recursive definition of addition in R_{⊥} by reducing addition to the average operation on I defined in Example 19. First notice that

x + y = pif x < 0 ∨ y < 0 then 2 (\frac{x+1}{2} + \frac{y+1}{2}) − 2

else pif x > 1 ∨ y > 1 then 2 (\frac{x}{2} + \frac{y}{2} ) else 2 (\frac{x+y}{2} )

where ∨ is “parallel or” [28]. Hence

x + y = pif x < 0 ∨ y < 0 then 2 (\frac{x+1}{2} + \frac{y+1}{2}) − 2

else pif x > 1 ∨ y > 1 then 2 (\frac{x}{2} + \frac{y}{2} ) else 2 out(in(x) ⊕ in(y))

where in = irtail_{[0,1]} : R_{⊥} → I and out = ricons_{[0,1]} : I → R_{⊥}.

The operation out is of fundamental importance in this recursive definition; it is this operation that makes the above recursive definition “get off the ground”. More formally, this is a non-strict operation, and some non-strict operation is needed if the fixed point operator (used to solve the above equation) is to produce a non-bottom solution. If we want to avoid using intermediate maps on the unit interval in recursive definitions of maps on the real line, we can use the non-strict operation rrjoin to get off the ground. See example below. □

Multiplication on R_{⊥} can be obtained in a similar way from multiplication on I.

Example 25 (Logarithm) The following recursive definition of the logarithm function log_{b}, with b > 1, is based on [14]. We first reduce the calculation of log_{b}(x) for x arbitrary to a calculation of log_{b}(x) for x ⊆ [1, b], so that log_{b}(x) ⊆ [0, 1], and then recursively consider the cases x = \sqrt{x′} and x = \sqrt{bx′′}. Notice that such x′ and x′′ are again contained in [1, b], and that both cases hold iff x = \sqrt{b} iff x^{2} = b. Also, the reduction process diverges if x contains non-positive numbers.

log_{b}(x) = pif x > b then log_{b}(x/b) + 1 else pif x < 1 then log_{b}(bx) − 1

else rrjoin_{[0,1]} (pif x^{2} < b then \frac{log_{b}(x^{2})}{2} else \frac{log_{b}(x^{2}/b)+1}{2})

Recall that rrjoin_{[0,1]}(x) = max(0, min(x, 1)). The application of the map rrjoin therefore seems redundant, because the tests preceding the recursive call of the logarithm function in the argument of rrjoin would ensure that the result is contained in [0, 1]. But the logarithm function is what the recursive definition is defining and therefore it has to ensure that this is indeed the case. As explained in Example 24, such a map is needed to “get off the ground”. □

The head-normal forms for R_{⊥} are taken as the expressions of the form ricons_{a}(e).

Lemma 26 For all non-maximal a ∈ R and b ∈ I, and all x ∈ I,

(i) (a) rrcons_{a}(rrcons_{b}(x)) = rrcons_{ab}(x) (b) rrcons_{a}(ricons_{b}(x)) = ricons_{ab}(x)

(c) ricons_{a}(cons_{b}(x)) = ricons_{ab}(x) (ii) irtail_{a}(ricons_{b}(x)) = L^{ω} if b ≤ a (iii) irtail_{a}(ricons_{b}(x)) = R^{ω} if b ≥ a (iv) irtail_{a}(ricons_{b}(x)) = cons_{b/a}(x) if a ⊑ b

(v) irtail_{a}(ricons_{b}(x)) = cons_{(a⊔b)/a}(tail_{(a⊔b)/b}(x)) if a ≃ b (vi) rhead_{r}(ricons_{a}(x)) = tt if a < r (vii) rhead_{r}(ricons_{a}(x)) = ff if a > r (viii) pif tt then x else y = x (ix) pif ff then x else y = y

(x) pif p then ricons_{a}(x) else ricons_{b}(y) =

ricons_{a⊓b}(pif p then ricons_{a/(a⊓b)}(x)

else ricons_{b/(a⊓b)}(y)

where the parallel conditional, the comparison map, and the head map for R_{⊥} are defined in the same way as for I. Notice that the above lemma is Lemma 21 with “r” and “i” inserted in appropriate places.

4 PCF extended with real numbers

We introduce two successive extensions of PCF, first with a type for the lazy unit interval (Subsection 4.2) and then with a further type for the lazy real line (Subsection 4.3). We also discuss the issues of canonical evaluation and of deterministic evaluation of PCF programs containing parallel features (Subsections 4.4 and 4.5 respectively).

For the reader’s convenience we introduce the basic notions of PCF needed in this paper (Subsection 4.1). See [19] for an excellent textbook account to PCF.

4.1 The programming language PCF

This section is based on [28], with minor adaptations and simplifications convenient to our needs, and can be safely skipped and used as a reference.

Given a collection of symbols called ground types, the set of types is the least set containing the ground types and containing the formal expression (σ → τ) whenever it contains σ and τ. The greek letters σ and τ range over types. We let (σ_{1}, …, σ_{n}, τ) stand for (σ_{1} → (σ_{2} → ⋯ (σ_{n} → τ) ⋯)).

Given a collection L of formal constants, each having a fixed type, and a family of formal variables {α_{i}^{σ}} (i ≥ 0) for each type σ, the L-terms are given by the following inductive rules:

(i) Every variable α_{i}^{σ} is an L-term of type σ. (ii) Every constant of type σ is an L-term of type σ. (iii) If M and N are L-terms of types (σ → τ) and σ respectively then (MN)

is an L-term of type τ. (iv) If M is an L-term of type τ then (λα_{i}^{σ}M) is an L-term of type σ → τ.

When L is understood from the context it need not be used as a prefix. The letters L, M, and N range over terms. The letter c range over constants. We denote the fact that a term M has type σ by M : σ. Notice that every term has a unique type. Terms of the form (MN) are called combinations. Terms of the form (λαM) are called abstractions. Parentheses around combinations and abstractions are sometimes omitted with the convention that juxtaposition associates to the left. We also omit parentheses in type expressions with the convention that → associates to the right.

The set of free variables of a term M is FV(M), inductively defined by

(i) FV(α_{i}^{σ}) = {α_{i}^{σ}} (ii) FV(c) = ∅ (iii) FV(MN) = FV(M) ∪ FV(N) (iv) FV(λα_{i}^{σ}M) = FV(M) − {α_{i}^{σ}}

A term M is closed if FV(M) = ∅ and open otherwise. Programs are closed terms of ground type. The idea is that the ground types are the data types and programs produce data, via the operational semantics. The remaining terms are significant as subprograms.

[N/α]M is the result of replacing all free occurrences of the variable α in M by N, making the appropriate changes in the bound variables of M so that no free variables of N become bound.

4.1.1 The languages L_{DA}, L_{PA} and L_{PA+∃}

The ground types for the language L_{DA} are N and T, and its constants are

tt : T ff : T

if_{σ} : (T, σ, σ, σ) for σ ground Y_{σ} : (σ → σ) → σ for each σ k_{n} : N for each natural number n (+1) : N → N, (−1) : N → N, (= 0) : N → T

The language L_{PA} is the language L_{DA} extended by the constants

pif_{σ} : (T, σ, σ, σ) for σ ground

The language L_{PA+∃} is the language L_{PA} extended with the constant

∃ : (N → T) → T

4.1.2 Denotational semantics

A collection of domains for PCF is a family {D_{σ}}_{σ} of domains, one for each type σ, such that D_{σ→τ} = [D_{σ} → D_{τ}]. It is standard if D_{T} is the flat domain of truth values and D_{N} is the flat domain of natural numbers.

An interpretation of a language L is a collection {D_{σ}}_{σ} of domains for PCF together with a mapping

c ↦ A⟦c⟧ : L → ⋃_{σ}{D_{σ}}

which is type-respecting, in the sense that if c : σ then A⟦c⟧ ∈ D_{σ}.

An interpretation is standard if it interprets the constants tt, ff, if_{σ}, Y_{σ}, k_{n}, (+1), (−1), (= 0), pif_{σ} and ∃ respectively as tt, ff, the sequential conditional, the fixed point operator, the natural number n, the successor function, the predecessor function, the test for zero, the parallel conditional and the continuous existential quantifier (whose definition is deliberately omitted).

An interpretation ⟨{D_{σ}}_{σ}, A⟩ induces a denotational semantics Â for L.

First, the set Env of environments is the set of type-respecting functions from the set of variables to ⋃_{σ}{D_{σ}}. It is ranged over by ρ. If α : σ and x ∈ D_{σ} then ρ[x/α] is the environment which maps α to x and any other variable α′ to ρ(α′). The undefined environment ⊥ maps each variable of type σ to the bottom element of the domain D_{σ}.

The denotational semantics

M ↦ (ρ ↦ Â⟦M⟧(ρ)) : Terms → (Env → ⋃_{σ}{D_{σ}})

is inductively defined by:

(i) Â⟦α⟧(ρ) = ρ(α) (ii) Â⟦c⟧(ρ) = A⟦c⟧ (iii) Â⟦MN⟧(ρ) = Â⟦M⟧(ρ) (Â⟦N⟧(ρ)) (iv) Â⟦λαM⟧(ρ)(x) = Â⟦M⟧(ρ[x/α]) (with x ∈ D_{σ} if α : σ)

Informally,

(i) A variable denotes what the environment assigns to it. (ii) A constant denotes what the interpretation assigns to it. (iii) If a term M denotes the function f : D → E and a term N denotes the

value x ∈ D then the combination MN denotes the value f(x) ∈ E. (iv) If a term M denotes the value y_{x} ∈ E in an environment which assigns

the value x ∈ D to the variable α, then the abstraction λαM denotes the function f : D → E defined by f(x) = y_{x}.

If M is closed then its denotation does not depend on the environment, in the sense that Â⟦M⟧(ρ) = Â⟦M⟧(ρ′) for all ρ and ρ′.

In order to simplify notation, we let ⟦M⟧ stand for the denotation Â⟦M⟧(⊥) of a closed term M with respect to an implicit semantics Â. Also, for any term M, we let ⟦M⟧(ρ) stand for Â⟦M⟧(ρ).

4.1.3 Operational semantics

The operational semantics of L_{DA} is given by an immediate reduction relation, defined by the following rules:

(i) (λαM)N → [N/α]M (ii) YM → M(YM) (iii) (+1)k_{n} → k_{n+1}, (−1)k_{n+1} → k_{n} (iv) (= 0)k_{0} → tt, (= 0)k_{n+1} → ff

(v) if ttMN → M, if ffMN → N

(vi) \frac{M → M′}{MN → M′N}, \frac{N → N′}{MN → MN′} if M is if, (+1), (−1) or (= 0)

We omit the reduction rules of the languages L_{PA} and L_{PA+∃}. The reduction relation preserves types, in the sense that if M → M′ and M has type σ, so does M′.

Evaluation is given by a partial function Eval from programs to constants, defined by

Eval(M) = c iff M →^{∗} c

It is well-defined because if M →^{∗} c and M →^{∗} c′ then c = c′.

The following theorem is often referred to as the Adequacy Property of PCF. It asserts that the operational and denotational semantics coincide.

Theorem 27 (Plotkin [28], Theorem 3.1) For any L_{DA} program M and constant c,

Eval(M) = c iff ⟦M⟧ = ⟦c⟧.

Proof. Lemma 29 below. □

The following definitions are introduced to formulate and prove Lemma 29.

The predicates Comp_{σ} are defined by induction on types by:

(i) If M : σ is a program then M has property Comp_{σ} iff ⟦M⟧ = ⟦c⟧ implies Eval(M) = c.

(ii) If M : σ → τ is a closed term it has property Comp_{σ→τ} iff whenever N : σ is a closed term with property Comp_{σ} then MN is a term with property Comp_{τ}.

(iii) If M : σ is an open term with free variables α_{1} : σ_{1}, …, α_{n} : σ_{n} then it has property Comp_{σ} iff [N_{1}/α_{1}] ⋯ [N_{2}/α_{n}]M has property Comp_{σ} whenever N_{1}, …, N_{n} are closed terms having properties Comp_{σ_{1}}, …, Comp_{σ_{n}} respectively.

A term of type σ is computable if it has property Comp_{σ}.

If M : σ → τ and N : σ are closed computable terms, so is MN and also a term M : (σ_{1}, …, σ_{n}, τ) is computable iff M̃N_{1} … N_{n} is computable whenever the terms N_{1} : σ_{1}, …, N_{n} : σ_{n} are closed computable terms and M̃ is a closed instantiation of M by computable terms.

In the following definitions α has to be chosen as some variable of appropriate type in each instance. Define terms Ω_{σ} by Ω_{σ} = Y_{σ}(λαα) for σ ground and Ω_{σ→τ} = λαΩ_{τ}, and define terms Y_{σ}^{(n)} by Y_{σ}^{(0)} = Ω_{σ} and Y_{σ}^{(n+1)} = λα(Y_{σ}^{(n)}α). Then ⟦Y_{σ}⟧ = ⨆_{n}⟦Y_{σ}^{n}⟧ for any standard interpretation.

Now define the syntactic information order ≼ as the least relation between terms such that

(i) Ω_{σ} ≼ M : σ and Y_{σ}^{(n)} ≼ Y_{σ}, (ii) M ≼ M, and (iii) if M ≼ M′ : σ → τ and N ≼ N′ : σ then λαN ≼ λαN′ and also

MN ≼ M′N′.

Lemma 28 (Plotkin [28], Lemma 3.2) If M ≼ N and M → M′ then either M′ ≼ N or else for some N′, N → N′ and M′ ≼ N′.

Proof. By structural induction on M and cases according to why the immediate reduction M → M′ takes place. □

We include the proof of the following lemma since we are going to extend it to PCF with real numbers:

Lemma 29 (Plotkin [28], Lemma 3.3) Every L_{DA}-term is computable.

Proof. By structural induction on the formation rules of terms:

(1) Every variable is computable since any closed instantiation of it by a computable term is computable.

(2) Every constant other than the Y_{σ}’s is computable. This is clear for constants of ground type. Out of +1, −1, = 0, and if we only consider −1 as an example. It is enough to show (−1)M computable when M is a closed computable term of type N. Suppose ⟦(−1)M⟧ = ⟦c⟧. Then c = k_{m} for some m and so ⟦M⟧ = m + 1. Therefore as M is computable, M →^{∗} k_{m+1} and so (−1)M →^{∗} k_{m} = c.

(3) If M : σ → τ and N : σ are computable, so is the combination MN. If MN is closed so are M and N and its computability follows from clause ii of the definition of computability. If it is open, any closed instantiation L of it by computable terms has the form M̃Ñ where M̃ and Ñ are closed instantiations of M and N respectively and therefore themselves computable which in turn implies the computability of L and hence of MN.

(4) If M : τ is computable, so is the abstraction λαM. It is enough to show that the ground term LN_{1} ⋯ N_{n} is computable when N_{1}, ⋯, N_{n} are closed computable terms and L is a closed instantiation of λαM by computable terms. Here L must have the form λαM̃ where M̃ is an instantiation of all free variables of M, except α, by closed computable terms. If ⟦LN_{1} ⋯ N_{n}⟧ = ⟦c⟧, then we have ⟦[N_{1}/α]M̃N_{2} ⋯ N_{n}⟧ = ⟦LN_{1} ⋯ N_{n}⟧ = ⟦c⟧. But [N_{1}/α]M̃ is computable and so too therefore is M̃N_{2} ⋯ N_{n}. Therefore LN_{1} ⋯ N_{n} → [N_{1}/α]M̃N_{2} ⋯ N_{n} →^{∗} c, as required.

(5) Each Y_{σ} is computable. It is enough to prove Y_{σ}N_{1} ⋯ N_{k} is computable when N_{1}, ⋯, N_{k} are closed computable terms and Y_{σ}N_{1} ⋯ N_{k} is ground. Suppose ⟦YN_{1} ⋯ N_{k}⟧ = ⟦c⟧. Since ⟦Y_{σ}⟧ = ⨆_{n}⟦Y_{σ}^{n}⟧, ⟦Y^{(n)}N_{1} ⋯ N_{k}⟧ = ⟦c⟧ for some n. Since ⟦Ω_{σ}⟧ = ⊥ for σ ground, Ω_{σ} is computable for σ ground. From this and (1), (3), and (4) proved above it follows that every Ω_{σ} and Y_{σ}^{(n)} is computable. Therefore Y^{(n)}N_{1} ⋯ N_{k} →^{∗} c and so by Lemma 28, YN_{1} ⋯ N_{k} →^{∗} c, concluding the proof. □

This lemma extends to the languages L_{PA} and L_{PA+∃}. It suffices to show that pif and ∃ are computable, with respect to appropriate reduction rules.

4.2 The programming language PCF^{I}

We let L range over the languages L_{DA}, L_{PA} and L_{PA+∃}, and L^{I} denote the extension of L with a new ground type I and the following new constants:

(i) cons_{a} : I → I (ii) tail_{a} : I → I (iii) head_{r} : I → T (iv) pif_{I} : (T, I, I, I)

for each non-bottom a ∈ I with distinct rational end-points and each rational r ∈ (0, 1). We refer to the ground type I as the real number type, and to programs of real number type as real programs.

4.2.1 Denotational semantics

We let D_{I} = I and we extend the standard interpretation A of L to L^{I} by

(i) A⟦cons_{a}⟧ = cons_{a} (ii) A⟦tail_{a}⟧ = tail_{a} (iii) A⟦head_{r}⟧ = head_{r} (iv) A⟦pif_{I}⟧pxy = pif p then x else y 4.2.2 Operational semantics

We extend the immediate reduction relation → of L to L^{I} by the following rules:

(i) cons_{a}(cons_{b}M) → cons_{ab} M (ii) tail_{a}(cons_{b}M) → Ycons_{L} if b ≤ a (iii) tail_{a}(cons_{b}M) → Ycons_{R} if b ≥ a (iv) tail_{a}(cons_{b}M) → cons_{b/a} M if a ⊑ b and a ≠ b

(v) tail_{a}(cons_{b}M) → cons_{(a⊔b)/a}(tail_{(a⊔b)/b} M) if a ≃ b, a ⋢ b, b ⋢ a, b ≰ a, and a ≰ b

(vi) head_{r}(cons_{a}M) → tt if a < r (vii) head_{r}(cons_{a}M) → ff if a > r (viii) pif ttMN → M, pif ffMN → N

(ix) pif L (cons_{a}M) (cons_{b}N) →
cons_{a⊓b}(pif L (cons_{a/(a⊓b)} M) (cons_{b/(a⊓b)} N))

if a ⊓ b ≠ ⊥

(x) \frac{N → N′}{MN → MN′} if M is cons_{a}, tail_{a}, head_{r} or pif

(xi) \frac{M → M′}{pifLM → pifLM′}  \frac{N → N′}{pifLMN → pifLMN′}

These rules are well-defined by virtue of Lemma 3 and because the extra conditions on them which are not present in Lemma 21 ensure that no bottom elements and no maximal elements are produced as subscripts of cons or tail. It may seem that there is a missing self-evident reduction rule for tail_{a}, namely the rule tail_{a}(cons_{a}M) → M; see remark after Lemma 35.

Notice that the immediate reduction rules for the parallel conditional are nondeterministic. The following lemma shows that this non-determinism does not produce inconsistencies:

Lemma 30 M → N implies ⟦M⟧(ρ) = ⟦N⟧(ρ) for all terms M and N and any environment ρ.

Proof. This is true for the language L, and remains true for the extended language L^{I} by virtue of Lemma 21. □

The partial map Eval on programs M of truth-value and natural number type is defined in the same way as for L. It is well-defined by virtue of Lemma 30, because no two different constants have the same interpretation. We extend Eval to a multi-valued map on real programs M by

Eval(M) = {a ∈ I|M →^{∗} cons_{a}M′ for some M′};

that is, a ∈ Eval(M) iff M has a head-normal form cons_{a}M′.

4.2.3 Soundness of the operational semantics

Lemma 31 For all real programs M, a ∈ Eval(M) implies a ⊑ ⟦M⟧.

Proof. By Lemma 30, if M →^{∗} cons_{a}M′ then ⟦M⟧ = ⟦cons_{a}M′⟧ = a⟦M′⟧. Therefore a ⊑ ⟦M⟧, because the information order on partial numbers coincides with the prefix preorder. □

Theorem 32 (Soundness) For any real program M,

⨆ Eval(M) ⊑ ⟦M⟧

Proof. The join exists because ⟦M⟧ is an upper bound of the set Eval(M). Therefore the result follows from Lemma 31. □

4.2.4 Completeness of the operational semantics

By virtue of Lemma 31, for any real program M we have that Eval(M) is empty if ⟦M⟧ = ⊥. The following theorem states a stronger form of the converse:

Theorem 33 (Completeness) For any real program M,

⨆ Eval(M) ⊒ ⟦M⟧

Proof. Lemma 35 below. □

The soundness and completeness properties in the senses of Theorems 32 and 33 can be referred together as the Adequacy Property.

Theorem 34 PCF extended with real numbers enjoys the Adequacy Property.

The recursive definitions given in Examples 18, 19, 20, 24, and 25 give rise to PCF programs in the obvious way. It would be a formidable task to syntactically prove the correctness of the resulting programs by appealing to the operational semantics given by the reduction rules. However, a mathematical proof of the correctness of a recursive definition allows us to conclude that the induced programs indeed produce correct results, via an application of the Adequacy Theorem. In fact, this is the point of denotational semantics.

We extend the inductive definition of the predicates Comp_{σ} by the following clause:

A real program M has property Comp_{I} if for every non-bottom partial number x ≪ ⟦M⟧ (as close to ⟦M⟧ as we please) there is some a ∈ Eval(M) with x ⊑ a.

If we read the relation x ≪ y as “x is a piece of information about y” then the above definition says that a real program is computable if every piece of information about its value can be produced in a finite number of reduction steps.

The domain-theoretic justificative for continuity of computable functions is that it is a finiteness condition [29,32,34,35]; a function f is continuous if a finite amount of information about f(x) depends only on a finite amount of information about x. The continuity of a domain, which amounts to its waybelow relation being well-behaved, gives us a general and abstract framework for consistently talking about “pieces of information”. Then it should come as no surprise that Lemma 35 makes essential use of the way-below relation and of the continuity of the primitive functions.

The following lemma, which extends Lemma 29, establishes the Completeness Theorem:

Lemma 35 Every term is computable.

Proof. It suffices to extend the inductive proof of Lemma 29. We have to:

(i) slightly modify the proof for the case of abstractions, because it mentions constants and we have added new constants;

(ii) extend the proof of computability of the terms Y_{σ} to the new types; and (iii) show that the new constants are computable.

(i) If M is computable so is λαM:

It is enough to show that the ground term LN_{1} ⋯ N_{n} is computable when N_{1}, ⋯, N_{n} are closed computable terms and L is a closed instantiation of λαM by computable terms. Here L must have the form λαM̃ where M̃ is an instantiation of all free variables of M, except α, by closed computable terms. Since [N_{1}/α]M̃ is computable, so is [N_{1}/α]M̃N_{2} ⋯ N_{n}. Since LN_{1} ⋯ N_{n} → [N_{1}/α]M̃N_{2} ⋯ N_{n} and the reduction relation preserves meaning, in order to evaluate LN_{1} ⋯ N_{n} it suffices to evaluate [N_{1}/α]M̃N_{2} ⋯ N_{n}.

(ii) Y_{σ} is computable for all new types:

In order to prove that Y_{σ} is computable for all new types it suffices to show that the term Y_{(σ_{1},...,σ_{k},I)}N_{1} ⋯ N_{k} is computable whenever N_{1} : σ_{1}, …, N_{k} : σ_{k} are closed computable terms.

It follows from (i) above that the terms Y_{σ}^{(n)} are computable for all new types, because the proof of computability of Y_{σ}^{(n)} for old types depends only on the fact that variables are computable and that the combination and abstraction formation rules preserve computability.

The syntactic information order ≼ on L extends to L^{I}, and Lemma 28 is easily seen to remain true by a routine extension of its inductive proof.

Let x ≪ ⟦YN_{1} ⋯ N_{k}⟧ be a non-bottom partial number. By a basic property of the way-below relation of any continuous dcpo, there is some n such that x ≪ ⟦Y^{(n)}N_{1} ⋯ N_{k}⟧, because ⟦Y⟧ = ⨆_{n}⟦Y^{(n)}⟧. Since Y^{(n)} is computable, there is a c ∈ Eval(Y^{(n)}N_{1} ⋯ N_{k}) with x ⊑ c. Since there is a term M with Y^{(n)}N_{1} ⋯ N_{k} →^{∗} cons_{c}M and Y^{(n)} ≼ Y, it follows from Lemma 28 that YN_{1} ⋯ N_{k} →^{∗} cons_{c}M for some M and therefore c ∈ Eval(YN_{1} ⋯ N_{k}).

(iii) The new constants are computable:

In order to prove that one of the new constants c is computable it suffices to show that if M_{1}, …, M_{n} are closed computable terms such that cM_{1} … M_{n} has real number type, then cM_{1} … M_{n} is computable.

(iii)(a) cons_{a} is computable:

Let M be a computable real program and let x ≪ ⟦cons_{a}M⟧ = a⟦M⟧ be a non-bottom partial number. We have to produce c ∈ Eval(cons_{a}M) with x ⊑ c. Let b ≪ ⟦M⟧ with x ≪ ab. If b = ⊥ then we can take c = a. Otherwise let b′ ∈ Eval(M) with b ⊑ b′. Then we can take c = ab′, because cons_{a}M →^{∗} cons_{a}(cons_{b′}M′) → cons_{ab′}M′ for some M′.

(iii)(b) tail_{a} is computable:

Let M be a computable real program and let y ≪ ⟦tail_{a}M⟧ = tail_{a}(⟦M⟧) be a non-bottom partial number. We have to produce c ∈ Eval(tail_{a}M) with y ⊑ c. Since tail_{a} is continuous, there is some x ≪ ⟦M⟧ such that y ≪ tail_{a}(x). Let b ∈ Eval(M) with x ⊑ b. It follows that b ⋢ a, because y ≠ ⊥ and if b ⊑ a then y ≪ tail_{a}(x) ⊑ tail_{a}(b) ⊑ tail_{a}(a) = ⊥. Then exactly one of the following four cases holds:

(t1) b ≤ a (t2) a ≤ b (t3) a ⊑ b (t4) a ≃ b, a ⋢ b, b ≰ a, and a ≰ b

which have the following proofs:

(t1) In this case tail_{a}M →^{∗} tail_{a}(cons_{b}M′) → Ycons_{L} for some M′. Hence y ≪ ⟦tail_{a}M⟧ = ⟦Ycons_{L}⟧. Since Ycons_{L} is a computable term, there is some c ∈ Eval(Ycons_{L}) ⊆ Eval(tail_{a}M) with y ⊑ c.

(t2) This case is handled similarly. (t3) Since x ⊑ b, we have that tail_{a}(x) ⊑ tail_{a}(b) = b/a, and since y ⊑ tail_{a}(x),

we have that y ⊑ b/a. Therefore we can take c = b/a, because tail_{a}M →^{∗} tail_{a}(cons_{b}M′) → cons_{b/a}M′ for some M′.

(t4) Since x ⊑ b, we have that tail_{a}(x) ⊑ tail_{a}(b) = (a ⊔ b)/a, and since y ⊑ tail_{a}(x), we have that y ⊑ (a ⊔ b)/a. Therefore we can take c = (a ⊔ b)/a, because tail_{a}M →^{∗} tail_{a}(cons_{b}M′)) → cons_{(a⊔b)/a}(tail_{(a⊔b)/b}M′) for some M′.

(iii)(c) head_{r} is computable:

Assume that ⟦head_{r}M⟧ = head_{r}(⟦M⟧) ≠ ⊥ for a computable real program M. Then there is an x ≪ ⟦M⟧ such that either x < r or else x > r, because head_{r} is continuous. Let c ∈ Eval(M) with x ⊑ c. Then either c < r or else c > r. Hence there is some M′ such that either head_{r}M →^{∗} head_{r}(cons_{c}M′) → tt or else head_{r}M →^{∗} head_{r}(cons_{c}M′) → ff respectively. Therefore if x < r then Eval(head_{r}M) = tt and if x > r then Eval(head_{r}M) = ff.

(iii)(d) pif is computable:

It suffices to show that pifLMN is computable whenever ⟦L⟧ = ⊥ and M and N are computable programs, because the case ⟦L⟧ ≠ ⊥ is immediate. Let x ≪ ⟦pifLMN⟧. Then x ≪ ⟦M⟧ ⊓ ⟦N⟧. Hence x ≪ ⟦M⟧ and x ≪ ⟦N⟧. Let a ∈ Eval(M) and b ∈ Eval(N) with x ⊑ a and x ⊑ b. Then x ⊑ a ⊓ b and a ⊓ b ∈ Eval(pifLMN), because pifLMN →^{∗} pifL(cons_{a}M)(cons_{b}N) → cons_{a⊓b}(pifL(cons_{a/(a⊓b)}M)(cons_{b/(a⊓b)}N)).

This concludes the proof of Lemma 35. □

The proof for tail_{a} implicitly shows that a reduction rule tail_{a}(cons_{a}M) → M would be useless. This can be explicitly explained as follows. If M denotes ⊥, so does tail_{a}(cons_{a}M). Hence there is no point in reducing tail_{a}(cons_{a}M) before reducing M to a head-normal form. If M has a head-normal form cons_{c}M′, then tail_{a}(cons_{a}M) reduces to tail_{a}(cons_{ac}M′), which in turn reduces to cons_{c}M′. In practice, However, this rule (and possibly more rules) can be included for efficiency reasons.

4.3 The programming language PCF^{R}

We let L^{R} denote the extension of L^{I} with a new ground type R and the following new constants:

(i) rrcons_{a} : R → R (ii) ricons_{a} : I → R (iii) irtail_{a} : R → I (iv) rhead_{r} : R → T

(v) pif_{R} : (T, R, R, R)

for each a ∈ R with distinct rational end-points and each rational number r.

We let D_{R} = R_{⊥} and we extend the standard interpretation A of L^{I} to L^{R} in the obvious way:

(i) A⟦rrcons_{a}⟧ = rrcons_{a} (ii) A⟦ricons_{a}⟧ = ricons_{a} (iii) A⟦irtail_{a}⟧ = irtail_{a} (iv) A⟦rhead_{r}⟧x = rhead_{r}

(v) A⟦pif_{R}⟧pxy = pif p then x else y

The reduction rules for L^{R} are given by Lemma 26, with the same restrictions as for the reduction rules for L^{I}. The Computability Lemma 35 and the Adequacy Theorem 34 routinely generalize to L^{R}.

4.4 Canonical evaluation

Although we have that for all real programs M and N,

⟦M⟧ = ⟦N⟧ iff ⨆ Eval(M) = ⨆ Eval(N),

it is not the case that ⟦M⟧ = ⟦N⟧ iff Eval(M) = Eval(N). (But ⟦M⟧ = ⟦N⟧ iff Eval(M) and Eval(N) are cofinal.) Moreover, Eval(M) may contain some intentional information. For example, suppose that a program M : I denotes 1/2. Then it can be the case that Eval(M) contains L (take M = cons_{L}(Ycons_{R})). In this case we can observe that ⟦M⟧ ≤ 1/2, which is certainly not an observable property of 1/2 [1,34,35,38]. In fact, this property is not observable in the evaluation of all programs denoting 1/2 (the program M = Ycons_{C} is a counter-example).

Both problems can be solved by hiding the intensional information contained in Eval(M) as follows. Add an immediate reduction rule

cons_{a}M → cons_{b}(cons_{a/b}M) if b ⊑ a and b ≠ a,

and define a strong head-normal form to be a real program of the form cons_{a}(cons_{b}M) with 0 < b < 1. It follows that a real program M has a strong head-normal form cons_{a}(cons_{b}M′) iff a ≪ ⟦M⟧, because a ≪ x iff there is some b such that 0 < b < 1 and ab ⊑ x. Now, for all real programs M, define

Eval′(M) = {a ∈ I|M has a strong head-normal form cons_{a}(cons_{b}M′)}.

With this definition it is immediate that ⨆ Eval′(M) = ⨆ Eval(M) and

⟦M⟧ = ⟦N⟧ iff Eval′(M) = Eval′(N),

because

Eval′(M) = {a ∈ I|a ≪ ⟦M⟧ and a has distinct rational end-points}.

It is also possible to show that, for any standard enumeration of the rational numbers, the set Eval′(M) is recursively enumerable. Recall that an enumeration r_{0}, r_{1}, …, r_{n}, … of the rational numbers is standard if there are recursive maps s, p, q : ℕ → ℕ such that

r_{n} = (−1)^{s(n)} \frac{p(n)}{q(n)},

and recall that the basic operations and predicates on rational numbers are recursive with respect to any standard enumeration. In order to prove that Eval′(M) is recursively enumerable it is necessary to assign Gödel numbers to terms and show that the reflexive and transitive closure of the immediate reduction relation is recursively enumerable with respect to the Gödel numbering.

In practice we do not need this modification, because the intensional information present in Eval(M) is not accessible within the language. In fact, it is even desirable to shorten the set Eval(M); see the subsection below.

4.5 Deterministic evaluation

By imposing a strategy on the application of the reduction rules, it is possible to eliminate the non-determinism and turn Eval(M) into a finite or infinite sequence with the partial number ⟦M⟧ as its iterated concatenation, for any real program M. We omit the details; but see below. For efficiency reasons, any practical functional programming language for exact real number computation based on the above ideas should have its evaluation implemented in this way.

The papers [8] and [22] give practical and theoretical explanations for the need of non-deterministic or parallel features in real number computation when we do not allow intensional operations. Notice that Bishop and Bridges [6] need an intensional operation in order to do constructive analysis, even for defining the basic operations on real numbers.

The above strategy eliminates the non-determinism of evaluation at the cost of simulating the parallel evaluation of the condition and the branches of the parallel conditional, until either the condition becomes true or false, or else both branches become a head-normal form. Perhaps it is possible to make use of abstract interpretation [2] in order to eliminate some instances of the parallelism.

5 Concluding remarks and further work

A useful extension of PCF with real numbers should be fully abstract and have all computable elements and functions definable. We are currently investigating the definability credentials of our extension. Our notion of computability is taken from [33]. We already know that the computable real numbers, the basic arithmetic operations, some trigonometric functions, and the logarithmic functions are definable. We conjecture that L_{P A+∃}^{R} has all computable elements and functions definable (and therefore it is fully abstract).

Such an extension would be useful to mechanize the ideas presented in [10– 12]. In an ongoing joint work with A. Edalat [13], we have shown that it is relatively easy to extend the language presented in this paper with a primitive for Riemann integration, by using the methods presented in [11]. We are also investigating methods for handling the more general theory of integration presented in loc. cit. within the language introduced in this paper.

Although such an approach to exact real number computation may seem to produce inefficient programs, it nevertheless provides a theoretical tool to prove computability without resorting to awkward indexings or representations. Recall that we do not need to know the operational semantics of the language in order to program in it, although it may be desirable to know it in order to obtain efficient programs. Once we know how to solve a problem theoretically, we can proceed to translate the solution to a real-life programming imperative language. Moreover, we do think that it is possible to extend real-life functional programming languages such as Haskell, Miranda, ML [5,27] with a relatively efficient treatment of real numbers based on continuous words, so that the theoretical solution can be readily used in practice. In such an approach it is desirable to include the basic arithmetic operations and other usual functions occurring in analysis as primitive.

In an even more practical approach, we can restrict ourselves to the partial real numbers with floating-point end-points. But we cannot hope Theorem 33 to hold, due to the presence of round-off errors (equivalently, due to the fact that there are finitely many floating-point numbers). Nevertheless, any produced result is guaranteed to be a correct partial realization of the ideal result. We emphasize that the best produced result can be worse than the best machine representable partial realization, this time due to round-off errors alone. Moreover, two distinct programs with the same value can concretely evaluate to distinct partial realizations of their ideal value, again due to round-off errors. In fact, the (correct) restriction of the concatenation operation to floating-point partial numbers does not satisfy the associativity property; it only satisfies the subassociativity law (xy)z ⊑ x(yz), in such a way that the fundamental computation rule cons_{a}(cons_{b}(x)) → cons_{ab}(x) introduces information loss. Such an implementation of PCF extended with real numbers is close to the ideas presented in [25]. Notice that Interval Analysis as introduced in loc. cit. remains an active area of research.

Since Automata Theory is based on monoids of words, it seems plausible that the monoid of continuous words could also be used to generalize automata to real numbers in a natural way.

Acknowledgement

This work has been carried out under the supervision of Mike Smyth. I have benefited from endless discussions with him and Abbas Edalat. Several useful comments by Abbas Edalat on the draft versions of this paper have allowed me to improve the presentation. The author has been supported by the Brazilian agency CNPq.

References

[1] S. Abramsky. Domain Theory and the Logic of Observable Properties. PhD thesis, University of London, Queen’s College, 1987.

[2] S. Abramsky. Abtract interpretation, logical relations and Kan extensions. Journal of Logic and Computation, 1(1):5–40, 1990.

[3] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D.M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, Oxford, 1994.

[4] B.M. Acióly. A Computational Foundation of Interval Mathematics. PhD thesis, Universidade Federal do Rio Grande do Sul, Instituto de Informatica, Porto Alegre, Brazil, 1991. (In Portuguese).

[5] R. Bird and P. Wadler. Introduction to Functional Programming. Prentice-Hall, New York, 1988.

[6] E. Bishop and D. Bridges. Constructive Analysis. Springer-Verlag, Berlin, 1985.

[7] L. Blum, M. Shub, and S. Smale. On a theory of computation and complexity over the real numbers. Bull. Amer. Math. Soc., 21:1–46, 1989.

[8] H.J. Boehm, R. Cartwright, M. Riggle, and M.J. O’Donnel. Exact real arithmetic: A case study in higher order programming. In ACM Symposium on Lisp and Functional Programming, 1986.

[9] P. di Gianantonio. A Functional Approach to Computability on Real Numbers. PhD thesis, Università Degli Studi di Pisa, Dipartamento di Informatica, 1993.

[10] A. Edalat. Power domains and iterated function systems. Technical Report Doc 94/13, Department of Computing, Imperial College, 1994. Submitted to Information and Computation.

[11] A. Edalat. Domain theory and integration. Theoretical Computer Science, 151:163–193, 1995.

[12] A. Edalat. Dynamical systems, measures and fractals via domain theory. Information and Computation, 120(1):32–48, July 1995.

[13] A. Edalat and M.H. Escardó. Real PCF extended with integration. Unpublished draft presented in the Computational Measure and Integration Theory Workshop, Imperial College, London (available by anonymous ftp at theory@doc.ic.ac.uk:papers/Escardo/drafts), October 1995.

[14] M.H. Escardó. Induction and recursion on the real line. In C. Hankin, I. Mackie, and R. Nagarajan, editors, Theory and Formal Methods 1994: Proceedings of the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, pages 259–282, Møller Centre, Cambridge, UK, 11–14 September 1994. IC Press. 1995.

[15] M.H. Escardó and D.M. Claudio. Scott domain theory as a foundation for interval analysis. Technical Report 218, UFRGS/II, Porto Alegre, Brazil, 1993.

[16] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, New York, 1980.

[17] K. Grue. Unrestricted lazy numerical algorithms. Unpublished manuscript.

[18] A. Grzegorczyk. On the definition of computable real continuous functions. Fund. Math., 44:61–77, 1957.

[19] C. A. Gunter. Semantics of Programming Languages – Structures and Techniques. The MIT Press, London, 1992.

[20] J.G. Hocking and G.S. Young. Topology. Dover Publications, 1988.

[21] S.C. Kleene and R.E Vesley. The Foundations of Intuitionistic Mathematics: Especially in Relation to Recursive Functions. North-Holland, Amsterdam, 1965.

[22] H. Luckhardt. A fundamental effect in computations on real numbers. Theoretical Computer Science, 5:321–324, 1977.

[23] S. MacLane and G. Birkhoff. Algebra. Macmillan, New York, 1st edition, 1967.

[24] P. Martin-Lof. Notes on Constructive Mathematics. Almqvist & Wiksell, Stockholm, 1970.

[25] R.E. Moore. Interval Analysis. Prentice-Hall, Englewood Cliffs, 1966.

[26] J. Myhill. Criteria of constructivity of real numbers. J. Symbolic Logic, 18:7–10, 1953.

[27] L.C. Paulson. ML for the working programmer. Cambridge University Press, Cambridge, 1991.

[28] G. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(1):223–255, 1977.

[29] G. Plotkin. Domains. Post-graduate Lectures in advanced domain theory, University of Edinburgh, Department of Computer Science, 1980.

[30] M.B. Pour-el and I. Richards. Computability and non-computability in classical analysis. Trans. Am. Math. Soc., pages 539–560, 1983.

[31] H.G. Rice. Recursive real numbers. Proc. Amer. Math. Soc., pages 784–791, 1954.

[32] D. S. Scott. Lattice theory, data types and semantics. In Formal semantics of programming languages, pages 66–106, Englewood Cliffs, 1972. Prentice-Hall.

[33] M.B. Smyth. Effectively given domains. Theoretical Computer Science, 5(1):256–274, 1977.

[34] M.B. Smyth. Power domains and predicate transformers: a topological view. In J. Diaz, editor, Automata, Languages and Programming, pages 662–675. Springer-Verlag, 1983. LNCS 154.

[35] M.B. Smyth. Topology. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, pages 641–761. Clarendon Press, Oxford, 1992.

[36] M.B. Smyth. Semi-metrics, closure spaces, and digital topology. Theoretical Computer Science, 151:257–276, 1995.

[37] A. Turing. On computable numbers, with an application to the Entscheindungproblem. The London Mathematical Society, 42:230–265, 1936.

[38] S. Vickers. Topology via Logic. Cambridge University Press, Cambridge, 1989.

[39] J. Vuillemin. Exact real arithmetic with continued fractions. In Proc. ACM Conference on Lisp and Functional Programming, pages 14–27, 1988.

[40] Klaus Weihrauch. Computability. Springer-Verlag, Berlin, 1987.

[41] Klaus Weihrauch. A simple introduction to computable analysis. Technical Report 171 – 7/1995, FernUniversitat, 1995.

[42] E. Wiedmer. Computing with infinite objects. Theoretical Computer Science, 10:133–155, 1980.

Contents

1 Introduction 1 2 The domain of partial real numbers 4

2.1 Domains 4 2.2 The lazy real line 4 2.3 Order of magnitude on the lazy real line 5 2.4 The lazy unit interval 6

3 Partial real numbers considered as continuous words 6 3.1 The prefix preorder of a monoid 7 3.2 Left translations of a monoid 7 3.3 Concatenation of partial real numbers 8 3.4 Infinitely iterated concatenations 10 3.5 Continuous words 12 3.6 Heads and tails of continuous words 14 3.7 Computation rules for continuous words 23 3.8 The lazy unit interval acting on the lazy real line 25

4 PCF extended with real numbers 27 4.1 The programming language PCF 28 4.2 The programming language PCF^{I} 33 4.3 The programming language PCF^{R} 39 4.4 Canonical evaluation 39 4.5 Deterministic evaluation 40

5 Concluding remarks and further work 41 Acknowledgement 42 References 43

47