Integration in Real PCF

Abbas Edalat Martín Hötzel Escardó

Department of Computing, Imperial College 180 Queen’s Gate, London SW7 2BZ, UK {ae,mhe}@doc.ic.ac.uk

Wednesday 11 \underline{th} December 1996

Abstract

Real PCF is an extension of the programming language PCF with a data type for real numbers. Although a Real PCF definable real number cannot be computed in finitely many steps, it is possible to compute an arbitrarily small rational interval containing the real number in a sufficiently large number of steps. Based on a domain-theoretic approach to integration, we show how to define integration in Real PCF. We propose two approaches to integration in Real PCF. One consists in adding integration as primitive. The other consists in adding a primitive for function maximization and then recursively defining integration from maximization. In both cases we have a computational adequacy theorem for the corresponding extension of Real PCF. Moreover, based on previous work on Real PCF definability, we show that Real PCF extended with the maximization operator is universal.

1 Introduction

Traditionally, in computing science one represents real numbers by floating-point approximations. If we assume that these approximations are “exact” then we can prove correctness of numerical programs by analytical methods. Such an idealization is the idea behind the so-called BSS model [6]. However, such “correct” programs do not produce correct results in practice, due to the presence of round-off errors. Moreover, they are inappropriate for problems whose solution is sensitive to small variations on the input.

As a consequence, “exact real number computation” has been advocated as an alternative solution (see e.g. [7, 8, 42] on the practical side and e.g. [5, 31, 32, 36, 43, 44, 45] on the foundational side). However, work on exact real number computation has focused on representations of real numbers and has neglected the issue of data types for real numbers. In particular, programming languages for exact real number computation with an explicit distinction between operational semantics, which is representation-dependent, and denotational semantics, which is representation-independent, have hardly been investigated. Two exceptions are [25, 26, 27] and [21]. Such programming languages do allow for correctness proofs based on analytical methods.

Real PCF [21] is an extension of the programming language PCF [34] with a data type for real numbers, with operational and denotational semantics. Of course, the operational semantics cannot evaluate a program denoting a real number in finitely many steps. However, it can compute an arbitrarily small rational interval containing the real number in a sufficiently large number of steps.

There have been a number of applications of domain theory to the construction of computational models for classical spaces, including locally compact Hausdorff spaces [14] and metric spaces [17]. These models have resulted in new techniques in real number computation. In particular, the computational measure and integration theory [11, 14, 16, 18] has had various applications, including exact computation of integrals, fractal geometry [15], statistical physics [10], stochastic processes [13] and neural networks [12, 35]. In domain-theoretic integration, one obtains increasingly better approximations to the value of the integral of a real-valued function.

In order to handle integration in Real PCF, we generalize Riemann integration of realvalued maps of a real variable to interval-valued maps of an interval variable. This also extends the results in the interval analysis approach to integration [33]. Based on our approach, M. Alvarez-Manilla [2] has recently developed a similar generalization of Riemann-Stieltjes integration.

We propose two approaches to integration in Real PCF. One consists in adding integration as primitive. The other consists in adding a primitive for function maximization and then recursively defining integration from maximization. In both cases we have a computational adequacy theorem for the corresponding extension of Real PCF. Moreover, based on previous work on Real PCF definability [23], we show that Real PCF extended with the maximization operator is universal.

The fact that we are able to handle integration in Real PCF shows the strength of such a denotational approach to exact real number computation and makes explicit the effective content of domain-theoretic integration.

Since numerical solution to differential equations is invariably based on integration of functions, Real PCF with integration also provides a framework for solving differential equations up to any precision.

Organization

In Section 2 we briefly introduce Real PCF. In Section 3 we relate (not necessarily continuous) real valued functions of real variables to Scott continuous interval valued functions of interval variables. In Section 4 we define interval Riemann integrals. In Section 5 we extend Real PCF with a primitive for integration.

2 Real PCF

In this section we summarize the results of [21, 23, 22] needed in this paper. We assume familiarity with PCF [34, 29]. We are deliberately informal concerning syntax. For simplicity and without essential loss of generality, in this paper we consider Real PCF restricted to the unit interval. For a formal account of syntax and a general treatment of real numbers see [21].

2.1 Interval expansions

It is well-known that decimal expansions of real numbers are not appropriate for real number computation, if we read infinite expansions from left to right. For example, multiplication by 3 is not computable w.r.t. decimal representation. In fact, any base has essentially the same problem [45].

Let us consider binary expansions of numbers in the unit interval [0, 1]. In this case, a solution for the above problem is to allow the digit \frac{1}{2} in addition to the digits 0 and 1. According to Martin-Löf [32], this kind of solution goes back to Brouwer.

For a_{n} ∈ \{0, \frac{1}{2}, 1\}, the sequence

a_{1}a_{2} ⋯ a_{n} ⋯

represents the number

∑_{n≥1} a_{n}2^{−n}.

Therefore the operations

a_{1}a_{2} ⋯ a_{n} ⋯ ↦ 0 a_{1}a_{2} ⋯ a_{n} ⋯
a_{1}a_{2} ⋯ a_{n} ⋯ ↦ \frac{1}{2} a_{1}a_{2} ⋯ a_{n} ⋯
a_{1}a_{2} ⋯ a_{n} ⋯ ↦ 1 a_{1}a_{2} ⋯ a_{n} ⋯

correspond to the following maps of the unit interval into itself:

s_{0}(x) = (x + 0)/2
s_{\frac{1}{2}} (x) = (x + \frac{1}{2})/2
s_{1}(x) = (x + 1)/2.

Thus, a binary expansion represents an intersection of a shrinking chain of intervals:

a_{1}a_{2} ⋯ a_{n} ⋯

represents

⋂_{n≥1} s_{a_{1}} ∘ ⋯ ∘ s_{a_{n}}([0, 1]).

Example 2.1 Routine algebra shows that the average operation

x ⊕ y = (x + y)/2

satisfies the equations

s_{0}(x) ⊕ s_{0}(y) = s_{0}(x ⊕ y)
s_{0}(x) ⊕ s_{1}(y) = s_{\frac{1}{2}} (x ⊕ y)
s_{1}(x) ⊕ s_{0}(y) = s_{\frac{1}{2}} (x ⊕ y)
s_{1}(x) ⊕ s_{1}(y) = s_{1}(x ⊕ y),

which can be considered as a recursive definition of the average map [19]. □

There is no reason to commit ourselves to the particular operations s_{0}, s_{\frac{1}{2}} and s_{1}. These operations are uniquely determined by their images [0, \frac{1}{2}], [\frac{1}{4}, \frac{3}{4}], and [\frac{1}{2}, 1] respectively, in the following sense. Given any interval [a, b] ⊆ [0, 1], there is a unique increasing affine map

cons_{[a,b]} : [0, 1] → [0, 1]

with range [a, b], namely

cons_{[a,b]}(x) = (b − a)x + a.

That is, cons_{[a,b]} rescales and translates the unit interval so that it becomes [a, b]. Therefore the maps s_{0}, s_{\frac{1}{2}} and s_{1} are equal to the maps cons_{[0, \frac{1}{2} ]}, cons_{[ \frac{1}{4} , \frac{3}{4} ]}, and cons_{[ \frac{1}{2} , 1]} respectively.

Definition 2.1 A sequence of intervals

[a_{1}, b_{1}], [a_{2}, b_{2}], …, [a_{n}, b_{n}], …

is said to be an interval expansion of the interval

⋂_{n≥1} cons_{[a_{1},b_{1}]} ∘ cons_{[a_{2},b_{2}]} ∘ ⋯ ∘ cons_{[a_{n},b_{n}]}([0, 1]).  □

For example, interval expansions formed from the intervals

[0, 1/10], [1/10, 2/10], …, [9/10, 1]

are essentially decimal expansions of real numbers contained in the unit interval.

Interval expansions denote iterated selections of subintervals. For example, the interval expansion

[0, \frac{1}{2}], [\frac{1}{4}, \frac{3}{4}], [\frac{1}{2}, 1], [0, \frac{1}{2}], …,

which corresponds to the binary expansion 0\frac{1}{2}10 ⋯, can be interpreted as the following sequence of instructions: select the two middle quarter parts of the interval [0, \frac{1}{2}], select the second half of the resulting interval, select the first half of the resulting interval, and so on. Thus, an interval expansion denotes an intersection of a shrinking chain of intervals. Conversely, any shrinking chain of intervals gives rise to an interval expansion, as shown in Section 2.4.

2.2 The interval domain

We think of intervals as approximations of real numbers, the singleton intervals being “exact” approximations. We consider these approximations as generalized real numbers, which we refer to as partial real numbers. Therefore, we sometimes notationally identify singleton intervals and real numbers.

We let R be the set of real compact intervals ordered by reverse inclusion, denoted by ⊑. The letters x, y, z, a, b, c in bold font range over R, and we write

x = [\underline{x}, \overline{x}].

The poset R is a bounded complete domain [1]. Its way-below relation is given by

x ≪ y iff the interior of x contains y.

The set Max(R) of maximal elements (singleton intervals) with the subspace topology induced by the Scott topology of R is homeomorphic to the Euclidean real line.

We also consider the domain I[a, b] of all closed subintervals of [a, b] and the domain R^{⋆} = Iℝ^{⋆} of compact intervals of the extended real line ℝ^{⋆} = ℝ ∪ {−∞, +∞}. The domain I[0, 1] is denoted by I. Notice that R lacks a bottom element, and that the bottom elements of I and R^{⋆} are [0, 1] and [−∞, +∞] respectively.

2.3 Canonical extensions of continuous real valued maps of real variables

In this subsection we consider the domain R of compact real intervals ordered by reverse inclusion. The results stated for R also hold for I.

Every continuous map f : ℝ^{n} → ℝ extends to a Scott continuous function If : R^{n} → R defined by

If(x_{1}, …, x_{n}) = {f(r_{1}, …, r_{n})|r_{1} ∈ x_{1}, …, r_{n} ∈ x_{n}},

called its canonical extension. For n = 1 we reason as follows. Since f is continuous, it maps connected sets to connected sets, and compact sets to compact sets. Hence it maps compact intervals to compact intervals. Therefore If is well-defined. But extensions of maps to powersets preserve intersections of ⊇-directed sets. Therefore If is Scott continuous. For n arbitrary the argument is analogous. It is easy to see that the canonical extension is the greatest monotone extension. Since it is continuous and every continuous function is monotone, it is also the greatest continuous extension.

If the function f is increasing in each argument, with respect to the natural order of ℝ, then If is given pointwise:

If(x_{1}, …, x_{n}) = [f(\underline{x_{1}}, …, \underline{x_{n}}), f(\overline{x_{1}}, …, \overline{x_{n}})].

If f is decreasing in each argument, then If is given “antipointwise”:

If(x_{1}, …, x_{n}) = [f(\overline{x_{1}}, …, \overline{x_{n}}), f(\underline{x_{1}}, …, \underline{x_{n}})].

Convention 2.1 We often notationally identify the function f with its extension If, and a real number r with the singleton interval {r}. The same convention applies to functions denoted by operator symbols, such as addition denoted by +. □

Two important examples are

x + y = [\underline{x} + \underline{y}, \overline{x} + \overline{y}],
px + q = [p\underline{x} + q, p\overline{x} + q],

for p ≥ 0 and q arbitrary.

2.4 Real PCF

In this subsection we introduce the primitive operations of Real PCF and then we define Real PCF to be PCF extended with constants and reduction rules for these operations.

The cons map

Definition 2.2 We define a binary operation □ on I by

x □ y = cons_{x}(y).
□

Recall that a monoid is a set together with an associative binary operation and a neutral element.

Theorem 2.2

1. (I, □, ⊥) is a monoid.

2. The information order of the domain I coincides with the prefix preorder of the monoid (I, □, ⊥), in the sense that

x ⊑ z iff x □ y = z for some y.

Moreover, such a suffix y is unique iff x is non-maximal.

Item 1 is the basis for the operational semantics of Real PCF and item 2 is the fundamental link between the denotational and the operational semantics.

If x ⊑ z and x is non-maximal then we denote the unique suffix y such that x □ y = z by z ⧄ x. Now it is easy to see that a shrinking a chain of intervals can be represented by an interval expansion. In fact,

a_{1} ⊑ a_{2} ⊑ ⋯ ⊑ a_{n} ⊑ …

is a chain of non-maximal intervals with join x iff the sequence

a_{1}, (a_{2} ⧄ a_{1}), …, (a_{n+1} ⧄ a_{n}), …

is an interval expansion of x.

The (canonical extensions of the) affine maps cons_{a} for a ≠ ⊥ with distinct rational endpoints will play a rôle analogous to the rôle played by the successor map on natural numbers.

The tail map

The predecessor map, undefined or arbitrarily defined at zero, is a left inverse of the successor map. Similarly, we now consider a continuous left inverse of cons_{a}; that is, a map tail_{a} such that

tail_{a}(cons_{a}(x)) = x.

Since this equation is equivalent to

tail_{a}(a □ x) = x,

we see that tail_{a} removes the prefix a from its argument, if such a prefix exists.

In order to define tail_{a} : I → I, we first define tail_{a} : [0, 1] → [0, 1] and then we take its canonical extension. The co-restriction of cons_{[a,b]} : [0, 1] → [0, 1] to its image [a, b] is invertible. Hence the continuous map defined by

tail_{[a,b]}(x) = \{ \begin{matrix}cons[a,b]^{−1}(a) & if x ≤ a \\ cons[a,b]^{−1}(x) & if x ∈ [a, b] \\ cons[a,b]^{−1}(b) & if x ≥ b \end{matrix}

= \{ \begin{matrix}0 & if x ≤ a \\ (x − a)/(b − a) & if x ∈ [a, b] \\ 1 & if x ≥ b \end{matrix}

= max(0, min((x − a)/(b − a), 1))

is a left inverse of cons_{[a,b]} : [0, 1] → [0, 1], and its canonical extension is a left inverse of the canonical extension of cons_{a}.

The head map

Here we consider a counterpart of the equality test for zero on natural numbers. For each r ∈ (0, 1) define a continuous map x ↦ (x <_{⊥} r) : I → T , where T = {true, false}_{⊥}, by

x <_{⊥} r = \{ \begin{matrix}true & if \overline{x} < r \\ false & if \underline{x} > r \\ ⊥ & otherwise. \end{matrix}

We are interested in the case that r is rational.

Remark 2.3 The function x ↦ (x <′_{⊥} r) : I → T , defined by

x <′_{⊥} r = \{ \begin{matrix}true & if \overline{x} < r \\ false & if \underline{x} ≥ r \\ ⊥ & otherwise. \end{matrix}

is monotone but not continuous, and hence not computable. In fact, equality of real numbers is not decidable [32] (but see below). The map x ↦ (x <_{⊥} r) can be regarded as the best continuous approximation to the monotone function x ↦ (x <′_{⊥} r). □

We write

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

Again, we are interested in the case that r is rational.

The parallel conditional

Finally we need the parallel conditional, defined by:

pif p then x else y = \{ \begin{matrix}x & if p = true \\ y & if p = false \\ x ⊓ y & if p = ⊥. \end{matrix}

This map is also continuous. The idea is that x ⊓ y is the best information compatible with both x and y. Therefore, if the condition is undefined then this information can be safely produced anyway (see Subsection 2.4 below).

Example 2.2 The recursive definition of average of real numbers given in Example 2.1 generalizes to a recursive definition of average of intervals:

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),

where

L = [0, \frac{1}{2}],  C = [\frac{1}{4}, \frac{3}{4}],  R = [\frac{1}{2}, 1].

By means of the primitives that we have introduced, this recursive definition can be rewritten as

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)). □

For more recursive definitions of real functions such as the complement map x ↦ 1−x, binary maximum, multiplication, and logarithm see [21, 22].

A note on the parallel conditional

Recall that the sequential conditional is defined by

if p then x else y = \{ \begin{matrix}x & if p = true \\ y & if p = false \\ ⊥ & if p = ⊥. \end{matrix}

Proposition 2.4 Let R be a domain with Max(R) homeomorphic to the real line or the unit interval, let D be any domain, let p : R → T be a continuous predicate, let g, h : R → D be continuous functions, and define a function f : R → D by

f(x) = if p(x) then g(x) else h(x).

If p is non-trivial, in the sense that there are maximal elements x and y such that p(x) = true and p(y) = false, then f is non-total, in the sense that f(z) = ⊥ for some maximal element z. Proof The non-empty disjoint sets U = p^{−1}(true) ∩ Max(R) and V = p^{−1}(false) ∩ Max(R) are open in Max(R), because p is continuous, and {true} and {false} are open in T . Hence U ∪ V ≠ Max(R), because Max(R) is connected. Therefore there is some maximal element z such that p(z) = ⊥. □

Thus, the sequential conditional is not appropriate for definition by cases of total functions on R, because it produces non-total functions in non-trivial cases.

In most definitions by cases of the form

f(x) = pif p(x) then g(x) else h(x)

which occur in practice, one has that g(x) = h(x) for all maximal x with p(x) = ⊥. This is the case, for instance, in the recursive definition of average given in Example 2.2. Another example is given by the following definition of the absolute value function:

|x| = pif x <_{⊥} 0 then − x else x.

For the case x = 0 one has

|0| = pif ⊥ then − 0 else 0 = 0 ⊓ 0 = 0.

Hence, the parallel conditional is also useful to overcome the fact that equality of real numbers is not decidable.

2.5 Operational semantics of Real PCF

Definition 2.3 Real PCF consists of PCF extended with a ground type I for the unit interval and constants for the primitive operations introduced in this subsection, restricted to rational parameters. □

An extension of PCF with a further type for the real line is introduced in [21].

The operational semantics of Real PCF is given by the following immediate reduction rules:

  1. cons_{a}(cons_{b}M) → cons_{a□b} M

2. tail_{a}(cons_{b}M) → fix cons_{L} if \overline{b} ≤ \underline{a}

3. tail_{a}(cons_{b}M) → fix cons_{R} if \underline{b} ≥ \overline{a}

4. tail_{a}(cons_{b}M) → cons_{b⧄a} M if a ⊑ b and a ≠ b

5. tail_{a}(cons_{b}M) → cons_{(a⊔b)⧄a}(tail_{(a⊔b)⧄b} M)

if a ⋢ b ⋢ a and a ⊔ b exists and is not a singleton

6. head_{r}(cons_{a}M) → true if \overline{a} < r

7. head_{r}(cons_{a}M) → false if \underline{a} > r

8. pif true MN → M

9. pif false MN → N

10. 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 ≠ ⊥ 11. \frac{N → N′}{MN → MN′} if M is cons_{a}, tail_{a}, head_{r} or pif

12. \frac{M → M′}{pif LM → pif LM′} \frac{N → N′}{pif LMN → pif LMN′}.

Notice that the first reduction rule is associativity of the operation □ expressed in a different way.

Roughly, these rules

1. reduce computations on partial real numbers to computations on intervals with rational end-points, namely the subscripts of cons and tail, and

2. “factor out” as many cons primitives as possible.

The underlying idea is that if we have a program X of the form

cons_{a}(X′) with X′ unevaluated,

then we know that the result of X is contained in the interval a, because by definition cons_{a} is a map with image a.

Definition 2.4 A Real PCF program of the form cons_{a}(X) is said to be a partially evaluated program with partial result a. □

2.6 Computational adequacy of Real PCF

The above reduction rules allow us to partially evaluate any program, producing better and better partial results converging to its actual result, in the sense of Theorem 2.5 below.

We extend the notion of computable PCF term to Real PCF by adding the following clause to the inductive definition given in [34]:

Definition 2.5 A Real PCF program X denoting a partial real number x is computable if for every non-bottom x′ ≪ x, as close to x as we please, the program X produces a partial result a with x′ ⊑ a, in finitely many reduction steps. □

Theorem 2.5 (Computational adequacy) Every Real PCF term is computable.

It follows that a program has some partial evaluation iff it does not denote bottom; it is important here that a cannot be bottom in a primitive operation cons_{a}.

2.7 Universality of Real PCF

Definition 2.6 A programming language L is universal if every computable element in the universe of discourse of L is L-definable. □

PCF is not universal. However, PCF extended with the parallel conditional and the existential quantification operator ∃ : (N → T ) → T defined by

∃(p) = \{ \begin{matrix}true & if p(n) = true for for some n \\ false & if p(⊥) = false \\ ⊥ & otherwise. \end{matrix}

is universal [34]. Real PCF with no extensions is not universal, because ∃ is not definable. If we extend Real PCF with ∃ and the computation rules given in loc. cit., then the adequacy property remains true.

Theorem 2.6 Real PCF extended with ∃ is universal.

3 Scott continuous functions R → R

In this section we include unpublished results from [22], which relate (not necessarily continuous) functions ℝ → ℝ to Scott continuous functions R → R. Subsection 3.1 considers the continuous case in a generalized setting, and Subsection 3.2 considers the general case.

3.1 Partial real valued functions

In this subsection we consider continuous functions defined on any space with values on the extended partial real line R^{⋆}.

The projections \underline{π}, \overline{π} : R^{⋆} → ℝ^{⋆} defined by

\underline{π}(x) = \underline{x}  and  \overline{π}(x) = \overline{x}

are not continuous because they don’t preserve the specialization order, as the specialization order of ℝ^{⋆} is discrete.

The set of extended real numbers endowed with its natural order ≤ is a continuous lattice, and so is its opposite [28]. Moreover, for any space X, a function f : X → ℝ^{⋆} is lower semicontinuous iff it is continuous with respect to the Scott topology on ℝ^{⋆} induced by ≤, and it is upper semicontinuous iff it is continuous with respect to the Scott topology on ℝ^{⋆} induced by ≥. It is clear from this observation that the above projections are respectively lower and upper semicontinuous.

In order to avoid the rather long terms “lower semicontinuous” and “upper semicontinuous”, we denote by \underline{ℝ} and \overline{ℝ} the set of extended real numbers endowed with the Scott topologies induced by ≤ and ≥ respectively, and we refer to the points of these topological spaces as respectively lower and upper real numbers. Thus, the above projections are continuous functions \underline{π} : R^{⋆} → \underline{ℝ} and \overline{π} : R^{⋆} → \overline{ℝ}.

The projections satisfy

\underline{π} ≤ \overline{π}

pointwise. Thus, given any continuous function f : X → R^{⋆}, we can define continuous functions \underline{f} : X → \underline{ℝ} and \overline{f} : X → \overline{ℝ} by composition with the projections, and we have that \underline{f} ≤ \overline{f} pointwise. Conversely, Lemma 3.1 For any space X and all continuous maps \underline{f} : X → \underline{ℝ} and \overline{f} : X → \overline{ℝ} with

\underline{f} ≤ \overline{f}

pointwise, there is a unique continuous map f : X → R^{⋆} such that

\underline{f} = \underline{π} ∘ f  and  \overline{f} = \overline{π} ∘ f,

namely [\underline{f}, \overline{f}] defined by

[\underline{f}, \overline{f}](x) = [\underline{f}(x), \overline{f}(x)].

Proof It suffices to show that [\underline{f}, \overline{f}] is continuous. Given a basic open set ↑ ↑y in R^{⋆}, we have that

[\underline{f}, \overline{f}]^{−1}(↑ ↑y) = \{x ∈ X|y ≪ [\underline{f}, \overline{f}](x)\}
= \{x ∈ X|\underline{y} ≪\underline{ℝ} \underline{f}(x) and \overline{y} ≪\overline{ℝ} \overline{f}(x)\}
= \{x ∈ X|\underline{y} ≪\underline{ℝ} \underline{f}(x)\} ∩ \{x ∈ X|\overline{y} ≪\overline{ℝ} \overline{f}(x)\}
= \underline{f}^{−1}(↑ ↑\underline{ℝ} \underline{y}) ∩ \overline{f}^{−1}(↑ ↑\overline{ℝ} \overline{y})

is an open set, because ↑ ↑\underline{ℝ} \underline{y} and ↑ ↑\overline{ℝ} \overline{y} are open sets in \underline{ℝ} and \overline{ℝ} respectively. Therefore [\underline{f}, \overline{f}] is continuous. □ Thus, for any space X, a continuous function f : X → R^{⋆} is essentially the same as a pair of continuous maps ⟨\underline{f} : X → \underline{ℝ}, \overline{f} : X → \overline{ℝ}⟩ with \underline{f} ≤ \overline{f} pointwise.

We can thus say that an extended partial real number is given by a pair ⟨\underline{x}, \overline{x}⟩ of respectively lower and upper real numbers with \underline{x} ≤ \overline{x}.

Corollary 3.2 R^{⋆} is homeomorphic to the subspace of \underline{ℝ} × \overline{ℝ} consisting of pairs of extended real numbers ⟨\underline{x}, \overline{x}⟩ with \underline{x} ≤ \overline{x}.

Since R^{⋆} is a bounded complete domain with bottom, it is a densely injective space [28], which means that for any dense subspace inclusion X ⊆ Y, every continuous map f : X → R^{⋆} extends to a continuous map f̂ : Y → R^{⋆}. In fact, there is always a greatest continuous extension, given by the equation

f̂(y) =\begin{matrix}⨆ & ↑ \\ y∈V \end{matrix} ⨅_{x∈V ∩X} f(x),

where V ranges over the open sets of Y, which is a particular case of the equation given in [28, 39].

Proposition 3.3 Let X be a dense subspace of a metric space Y and f : X → R^{⋆} be a continuous map. Then the greatest continuous extension f̂ : Y → R^{⋆} of f is given by

f̂(y) = [lim inf_{x→y} \underline{f}(x), lim sup_{x→y} \overline{f}(x)] .

Here x → y is a short-hand for x ∈ X and x → y.

Proof

f̂(y) = \begin{matrix}⨆ & ↑ \\ y∈V \end{matrix} ⨅_{x∈X∩V} f(x)
= \begin{matrix}⨆ & ↑ \\ ϵ>0 \end{matrix} ⨅_{x∈X,d(x,y)<ϵ} [\underline{f}(x), \overline{f}(x)]

= \begin{matrix}⨆ & ↑ \\ ϵ>0 \end{matrix} [ inf_{x∈X,d(x,y)<ϵ} \underline{f}(x), sup_{x∈X,d(x,y)<ϵ} \overline{f}(x)]

= [sup_{ϵ>0} inf_{x∈X,d(x,y)<ϵ} \underline{f}(x), inf_{ϵ>0} sup_{x∈X,d(x,y)<ϵ} \overline{f}(x)]

= [lim inf_{x→y} \underline{f}(x), lim sup_{x→y} \overline{f}(x)] . □

In particular, if f : X → ℝ^{⋆} is a continuous map, then the above proposition applied to the coextension s ∘ f : X → R^{⋆} of f to R^{⋆}, where s : ℝ^{⋆} → R^{⋆} is the singleton embedding, produces a greatest extension f̂: Y → R^{⋆} of f, given by

f̂(y) = [lim inf_{x→y} f(x), lim sup_{x→y} f(x)] .

Let f : ℝ → ℝ be continuous. By the above remark, if f has a limit at ∞, then f̂(∞) = lim_{x→∞} f(x). For a pathological example, consider f : (ℝ − {0}) → ℝ defined by f(x) = sin(1/x). Then f̂(0) = [−1, 1] and f̂(∞) = 0, so that f̂ behaves as the so-called topologist’s sine curve [30].

Lemma 3.4 Every continuous map f : ℝ → R has a greatest continuous extension f̂: R → R, given by

f̂(x) = ⨅ f(x).

Proof Since this is clearly the greatest monotone extension, it suffices to show that it is continuous. In this proof we make use of the upper power space construction [38, 40, 41, 14]. Let U be the endofunctor on the category of topological spaces which assigns to a space X its upper space, whose points are the non-empty compact saturated sets of X, and which assigns to a continuous map f : X → Y the continuous map Uf : UX → UY defined by Uf(Q) = ↑ ↑f(Q). Then for any space X the map x ↦ ↑ ↑x : X → UX is continuous, and for any continuous ⊓-semilattice D, the meet map ⨅ : UD → D is well-defined and continuous. Since R is a continuous ⊓-semilattice and a subspace of Uℝ, the map f̂ is continuous, because it can be expressed as the following composition of continuous maps:

[figure: R; ⊂; Uℝ; Uf; UR; ⨅; R]
x ↦ x ↦ ↑ ↑f(x) ↦ ⨅ ↑ ↑f(x) = ⨅ f(x).

(Note: This also shows that the assignment f ↦ f̂ is Scott continuous, and is a particular case of a much more general fact about injectivity established in [20]). □

3.2 Discontinuous functions in real analysis versus Scott continuous functions in domain theory

This subsection contains results about extensions of arbitrary real valued functions to continuous partial real valued functions.

In real analysis one often considers discontinuous functions f : ℝ → ℝ, but in many cases only the points of continuity of f are interesting. For instance, a function f : ℝ → ℝ is Riemann integrable on any compact interval iff it is bounded on compact intervals and continuous almost everywhere [37]. Moreover, the integral of f depends only on its points of continuity. The following theorem shows that such uses of ad hoc discontinuity can be avoided in domain theory.

Lemma 3.5 For any function f : X → ℝ^{⋆} defined on a metric space X there is a greatest continuous map f̃: X → R^{⋆} agreeing with f at every point of continuity of f, given by

f̃(x) = [lim inf_{y→x} f(y), lim sup_{y→x} f(y)] .

Proof We know from classical topology and analysis that

\underline{g}(y) = lim inf_{x→y} f(x)

is the greatest lower semicontinuous function below f, and that

\overline{g}(y) = lim sup_{x→y} f(x)

is the least upper semicontinuous function above f (see e.g. [9, 37]). Since f̃ is [\underline{g}, \overline{g}], it is continuous by Lemma 3.1. Since f is continuous at y iff lim_{x→y} g(x) exists iff lim inf_{x→y} f(x) = lim sup_{x→y} g(x), f̃ agrees with f at every point of continuity of f. □

Theorem 3.6 For any function f : ℝ → ℝ bounded on compact intervals there is a greatest continuous map f̂: R → R agreeing with f at every point of continuity of f, given by

f̂(x) = [inf \underline{g}(x), sup \overline{g}(x)],

where \underline{g} : ℝ → \underline{ℝ} and \overline{g} : ℝ → \overline{ℝ} are continuous maps defined by

\underline{g}(y) = lim inf_{x→y} f(x)  and  \overline{g}(y) = lim sup_{x→y} f(x).

Proof Since f is bounded on compact intervals, the function f̃ : ℝ → R^{⋆} defined in Lemma 3.5 corestricts to R. By Lemma 3.4, the corestriction can be extended to a function f̂: R → R, given by

f̂(x) = ⨅ f̃(x) = [inf \underline{g}(x), sup \overline{g}(x)].  □

4 Interval Riemann integrals

A generalization of the Riemann theory of integration based on domain theory was introduced in [11]. Essentially, a domain-theoretic framework for the integration of real-valued functions w.r.t. any finite measure on a compact metric space was constructed using the probabilistic power domain of the upper space of the metric space. In this work we are only be concerned with integration w.r.t. the Lebesgue measure (uniform distribution) in ℝ^{n}.

In order to extend Real PCF with integration, we embark on a novel approach compared to [11] for integration w.r.t. the Lebesgue measure in ℝ, in that we consider integration of maps of type R^{n} → R rather than ℝ^{n} → ℝ. We deduce various properties of integration defined in this way, which are interesting in their own right as well.

In Subsection 4.1 we introduce simple interval Riemann integration. In Subsection 4.2 we introduce multiple Riemann integration, which is related to simple interval Riemann integration via an extension of the so-called Fubini’s rule. In Subsection 4.3 we introduce a supremum operator, which is used in Section 5 to obtain a fixed-point definition of Riemann integration.

4.1 Simple interval Riemann Integrals

Recall that (the canonical extension of) addition in R is defined by

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

and that given a real number α ≥ 0 and a partial real number x, we have that

xα = αx = [\underline{x}α, \overline{x}α].

We denote the diameter of an interval x ∈ R by dx:

dx = \overline{x} − \underline{x}.

A partition of an interval [a, b] is a finite set of the form

P = {[a, x_{1}], [x_{1}, x_{2}], …, [x_{n−1}, x_{n}], [x_{n}, b]}.

We denote by P[a, b] the set of all partitions of [a, b]. A partition Q refines a partition P if Q is obtained by partitioning some elements of P, in the sense that there is a (necessarily unique) family {Q_{x}}_{x∈P} such that Q is its disjoint union and Q_{x} is a partition of x for each x ∈ P. Such a family is called the refinement witness. The following lemma is immediate:

Lemma 4.1 P[a, b] is directed by the refinement order. That is, for any two partitions of [a, b] there is a third partition refining both.

Definition 4.1 Let f : R → R be a map and [a, b] be an interval. An interval Riemann sum of f on [a, b] is a sum of the form

∑_{x∈P} f(x)dx  for P ∈ P[a, b]. □

Lemma 4.2 Let f : R → R be a monotone map (w.r.t. the information order). If a partition Q of an interval [a, b] refines a partition P then

∑_{x∈P} f(x)dx ⊑ ∑_{x∈Q} f(x)dx.

Therefore, the set of interval Riemann sums of f on [a, b] is directed. Proof If two compact intervals x_{1} and x_{2} just touch then

f(x_{1} ⊓ x_{2})d(x_{1} ⊓ x_{2}) = f(x_{1} ⊓ x_{2})(dx_{1} + dx_{2})
= f(x_{1} ⊓ x_{2})dx_{1} + f(x_{1} ⊓ x_{2})dx_{2}
⊑ f(x_{1})dx_{1} + f(x_{2})dx_{2}.

By induction, if successive elements of the sequence x_{1}, …, x_{n} just touch then

f( ⨅_{k=1}^{n} x_{k})d( ⨅_{k=1}^{n} x_{k}) ⊑ ∑_{k=1}^{n} f(x_{k})dx_{k}.

Hence, if {Q_{x}}_{x∈P} is the refinement witness, then for any x ∈ P,

f(x)dx ⊑ ∑_{y∈Q_{x}} f(y)dy,

because x = ⨅ Q_{x}. By monotonicity of addition and induction on the size of P,

∑_{x∈P} f(x)dx ⊑ ∑_{x∈P} ∑_{y∈Q_{x}} f(y)dy.

Since Q is the disjoint union of the sets Q_{x} and addition is associative,

∑_{x∈P} ∑_{y∈Q_{x}} f(y)dy = ∑_{y∈Q} f(y)dy. □

Definition 4.2 The interval Riemann integral of a monotone map f : R → R on an interval [a, b] is defined by

∫_{a}^{b} f =\begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} ∑_{x∈P} f(x)dx.

We sometimes denote ∫_{a}^{b} f by ∫_{a}^{b} f(x)dx. □

Proposition 4.3 For all continuous maps f, g : R → R and all real numbers α and β,

∫_{a}^{a} f = 0,
∫_{a}^{b} f + ∫_{b}^{c} f = ∫_{a}^{c} f,
∫_{a}^{b}(αf + βg) = α ∫_{a}^{b} f + β ∫_{a}^{b} g.

Proof The first equation follows from the fact that {[a, a]} is the essentially the only partition of [a, a]. If P and Q are partitions of [a, b] and [b, c] respectively, then P ∪ Q is a partition of [a, c]. Conversely, if R is partition of [a, c], then there are partitions P and Q of [a, b] and [b, c] respectively such that P ∪ Q refines R. Therefore

∫_{a}^{b} f + ∫_{b}^{c} f = \begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} ∑_{x∈P} f(x)dx +\begin{matrix}⨆ & ↑ \\ Q∈P[b,c] \end{matrix} ∑_{y∈Q} f(y)dy
= \begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} \begin{matrix}⨆ & ↑ \\ Q∈P[b,c] \end{matrix} ∑_{x∈P} f(x)dx + ∑_{y∈Q} f(y)dy
= \begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} \begin{matrix}⨆ & ↑ \\ Q∈P[b,c] \end{matrix} ∑_{z∈P ∪Q} f(z)dz
= \begin{matrix}⨆ & ↑ \\ R∈P[a,c] \end{matrix} ∑_{z∈R} f(z)dz

= ∫_{a}^{c} f.

We omit the routine proof of the third equation. □ Clearly, ∫_{a}^{b} f depends only on the values that f assumes on I[a, b].

Theorem 4.4 For every interval [a, b], the integration map

f ↦ ∫_{a}^{b} f : [I[a, b] → R] → R

is Scott continuous. Proof Let F be a directed subset of the domain [I[a, b] → R]. Then

∫_{a}^{b} ^{⨆↑} F = \begin{matrix}⨆ & ↑ \\ P \end{matrix} ∑_{x∈P} (^{⨆↑} F) (x)dx

= \begin{matrix}⨆ & ↑ \\ P \end{matrix} ∑_{x∈P} ( \begin{matrix}⨆ & ↑ \\ f∈F \end{matrix} f(x)) dx
= \begin{matrix}⨆ & ↑ \\ P \end{matrix} ∑_{x∈P} \begin{matrix}⨆ & ↑ \\ f∈F \end{matrix} f(x)dx
= \begin{matrix}⨆ & ↑ \\ P \end{matrix}\begin{matrix}⨆ & ↑ \\ f∈F \end{matrix} ∑_{x∈P} f(x)dx
= \begin{matrix}⨆ & ↑ \\ f∈F \end{matrix} \begin{matrix}⨆ & ↑ \\ P \end{matrix} ∑_{x∈P} f(x)dx

= \begin{matrix}⨆ & ↑ \\ f∈F \end{matrix} ∫_{a}^{b} f. □

Any dense subset A of [a, b] clearly induces a basis

B = {[x, y]|x ≤ y in A}

of I[a, b].

Lemma 4.5 Let [a, b] be an interval, let B be any basis of I[a, b] induced by a dense subset of [a, b], and denote by P_{B}[a, b] the partitions of [a, b] consisting of basis elements. Then for any continuous function f : I[a, b] → R,

∫_{a}^{b} f =\begin{matrix}⨆ & ↑ \\ Q∈P_{B}[a,b] \end{matrix} ∑_{x∈Q} f(x)dx.

Proof Let u ≪ ∫_{a}^{b} f. It suffices to conclude that

u ⊑\begin{matrix}⨆ & ↑ \\ P ∈P_{B}[a,b] \end{matrix} ∑_{x∈P} f(x)dx.

Let P = {x_{1}, …, x_{n}} ∈ P[a, b] such that u ≪ ∑_{x∈P} f(x)dx. W.l.o.g., we can assume that [a, b] has non-zero diameter and that P consists of intervals of non-zero diameter. Then for each x ∈ P there is some x′ ≪ x in B such that already

u ≪ ∑_{x∈P} f(x′)dx

because f, addition, and scalar multiplication are continuous. Wlog we can assume that only successive elements of the sequence x′_{1}, …, x′_{n} don’t overlap, because otherwise we can shrink the intervals x′_{i} in such a way that that the above inequality still holds. Then the unique partition Q of [a, b] consisting of intervals of non-zero diameter with the end-points of the intervals x′_{1}, …, x′_{n} is of the form {y_{1}, z_{1}, y_{2}, …, z_{n−1}, y_{n}} with

1. z_{i} = x′_{i} ⊔ x′_{i+1} for 1 ≤ i ≤ n

2. (a) y_{1} ⊓ z_{1} = x′_{1} and z_{n−1} ⊓ y_{n} = x′_{n} (b) z_{i−1} ⊓ y_{i} ⊓ z_{i} = x′_{i} for 1 < i < n.

We claim that

∑_{x∈P} f(x)dx ⊑ ∑_{y∈Q} f(y)dy,

which implies that

u ≪\begin{matrix}⨆ & ↑ \\ Q∈P_{B}[a,b] \end{matrix} ∑_{x∈Q} f(x)dx,

by transitivity, and concludes the proof. For notational simplicity and w.l.o.g., we prove the claim for the case P = {x_{1}, x_{2}}. In this case the claim reduces to

f(x′_{1})dx_{1} + f(x′_{2})dx_{2} ⊑ f(y_{1})dy_{1} + f(z_{1})dz_{1} + f(y_{2})dy_{2},

and is proved by

f(x′_{1})dx_{1} + f(x′_{2})dx_{2}
= f(x′_{1})(dy_{1} + dx_{1} − dy_{1}) + f(x′_{2})(dx_{2} − dy_{2} + dy_{2})
= f(x′_{1})dy_{1} + f(x′_{1})(dx_{1} − dy_{1}) + f(x′_{2})(dx_{2} − dy_{2}) + f(x′_{2})dy_{2}
⊑ f(y_{1})dy_{1} + f(z_{1})(dx_{1} − dy_{1}) + f(z_{1})(dx_{2} − dy_{2}) + f(y_{2})dy_{2}
= f(y_{1})dy_{1} + f(z_{1})dz_{1} + f(y_{2})dy_{2}. □

Remark 4.6 Moore [33] handles integration by considering sums which are essentially interval Riemann sums for partitions consisting of n intervals of the same length, but he restricts his definition to rational functions. The integrand is assumed to be monotone w.r.t. inclusion and continuous w.r.t. the Hausdorff metric on intervals. Since the Hausdorff metric induces the Lawson topology on R, the integrand is Scott continuous [24, 28]. Therefore Lemma 4.5 above and Theorem 4.11 below show that our definition generalizes that of Moore to all Scott continuous functions, and Theorem 4.7 below shows that our definition captures all Riemann integrable functions. □

Since If(x) = [inf f(x), sup f(x)], the end-points of an interval Riemann sum are given by lower and upper Darboux sums respectively:

∑_{x∈P} If(x)dx = [ ∑_{x∈P} inf f(x)dx, ∑_{x∈P} sup f(x)dx] .

Therefore

∫_{a}^{b} If = [\underline{∫{b \atop a}}f, \overline{∫{b \atop a}}f] = \{∫_{a}^{b} f\} ,

where the symbols \underline{∫{b \atop a}} and \overline{∫{b \atop a}} denote lower and upper Riemann integrals respectively. Any continuous map f : ℝ → ℝ has infinitely many continuous extensions to R → R. Recall that the extension If is characterized as the greatest one. Theorem 4.7 below shows that the above equation generalizes to any Riemann integrable function. This entails that interval Riemann integration, even when restricted to Scott continuous functions, captures all Riemann integrable functions.

Theorem 4.7 Let f : ℝ → ℝ be Riemann integrable on compact intervals [a, b], and let f̂: R → R be the Scott continuous function defined in Theorem 3.6. Then

∫_{a}^{b} f̂ = {∫_{a}^{b} f} .

Proof Let \underline{g} and \overline{g} be defined as in Theorem 3.6. Then

∫_{a}^{b} f̂ = \begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} ∑_{x∈P} f̂(x)dx
= \begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} ∑_{x∈P}[inf \underline{g}(x), sup \overline{g}(x)]dx

= \begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} [ ∑_{x∈P} inf \underline{g}(x)dx, ∑_{x∈P} sup \overline{g}(x)dx]

= [ sup_{P ∈P[a,b]} ∑_{x∈P} inf \underline{g}(x)dx, inf_{P ∈P[a,b]} ∑_{x∈P} sup \overline{g}(x)dx]

= [\underline{∫{b \atop a}}\underline{g}, \overline{∫{b \atop a}}\overline{g}]

= {∫_{a}^{b} f} ,

because \underline{g} and \overline{g} agree with f at every point of continuity of f and hence are Riemann integrable, with the same (lower and upper) integrals as f. □

We now show that the above theorem holds with the greatest continuous extension f̂ of f replaced by any continuous extension f̃ whatsoever.

Lemma 4.8 For every continuous function f : R → R there is a greatest continuous function f̂ : R → R such that

f_{| Max R} = f̂_{| Max R},

given by

f̂(x) = ⨅ f(↑ ↑x ∩ Max R)

Proof We first restrict f to Max R ≅ ℝ, and then we find the greatest continuous extension to R by an application of Lemma 3.4, obtained by a formula which is essentially the same as the above one. □

Lemma 4.9 For any continuous f : R → R,

∫_{a}^{b} f = ∫_{a}^{b} f̂.

Proof ∫_{a}^{b} f ⊑ ∫_{a}^{b} f̂ because f ⊑ f̂. For the other direction, we first prove that

f̂(x)dx ⊑ ∫ \overline{x} \underline{x} f

for all x ∈ R. Let b ≪ f̂(x)dx. It suffices to conclude that

b ⊑ ∫ \overline{x} \underline{x} f.

Since f̂(x) = ⨅_{r∈x}f({r}), by Lemma 4.8, we have that b ≪ f({r})dx for all r ∈ x. By continuity of f, for each r ∈ x there is a w_{r} ≪ {r} such that already b ≪ f(w_{r})dx. Since the interiors of the intervals w_{r} form an open cover of the compact interval x, there is a finite subset C of {w_{r}}_{r∈x} such that the interiors of the members of C already cover x. Since the way-below order of R is multiplicative, b ≪ ⨅_{y∈C} f(y)dx . Now, there is a unique partition P of x, consisting of non-singleton intervals, such that the set of end-points of elements of P is the set of end-points of elements of C belonging to x, together with the two points \underline{x} and \overline{x}. Since

f(z) ⊑ ⨅_{y∈P,z⊑y} f(y),

we have that

⨅_{z∈C} f(z) ⊑ ⨅_{z∈C} ⨅_{y∈P,z⊑y} f(y) = ⨅_{y∈P} f(y).

Hence b ≪ ⨅_{y∈P} f(y)dx. But

⨅_{y∈P} f(y)dx ⊑ ∑_{z∈P} f(z)dz,

because

⨅_{y∈P} f(y)dx = [min_{y∈P} f(y)dx, max_{y∈P} f(y)dx] ,

and hence the weighted average ∑_{z∈P} f(z)dz has to be contained in the latter interval. Therefore b ≪ ∑_{z∈P} f(z)dz ⊑ ∫ \overline{x} \underline{x} f, which yields b ⊑ ∫ \overline{x} \underline{x} f, as desired. Finally, we have that

∫_{a}^{b} f̂ = \begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} ∑_{x∈P} f̂(x)dx ⊑\begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} ∑_{x∈P} ∫ \overline{x} ; \underline{x} f

= \begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} ∫_{a}^{b} f = ∫_{a}^{b} f,

which concludes the proof. □

Theorem 4.10 The interval Riemann integral of a continuous function f : R → R depends only on the value that f assumes at maximal elements, in the sense that for any continuous function g : R → R,

f_{| Max(R)} = g_{| Max(R)} implies ∫_{a}^{b} f = ∫_{a}^{b} g.

Proof By Lemma 4.8, f_{| Max(R)} = g_{| Max(R)} implies f̂ = ĝ. Therefore the result follows from Lemma 4.9. □

Corollary 4.11 If f : ℝ → ℝ is Riemann integrable on compact intervals and f̃: R → R is any Scott continuous map agreeing with f at points of continuity of f, then

∫_{a}^{b} f̃ = {∫_{a}^{b} f} .

Proof By Theorem 4.7, we know that this is true for the greatest such f̃, namely f̂. Therefore the result follows from Theorem 4.10. □ The significance of Theorems 4.10 and Corollary 4.11 is that sometimes it is easy to obtain a Real PCF program for an extension of a function f but it is difficult or undesirable to obtain a program for its greatest continuous extension. For instance, the distributive law does not hold for the canonical extensions of addition and multiplication, so that two different definitions of the same function can give rise to two different extensions and two different programs [33].

Finally, we have the following characterization of interval Riemann integration via ordinary lower and upper Riemann integration:

Theorem 4.12 Let s : ℝ → R be the singleton embedding and f : R → R be any Scott continuous map. Then

∫_{a}^{b} f = [\underline{∫{b \atop a}}\underline{f ∘ s}, \overline{∫{b \atop a}}\overline{f ∘ s}] .

Proof The proof of Theorem 4.7, with \underline{g} = \underline{f ∘ s} and \overline{g} = \overline{f ∘ s} shows that this is the case if f is the greatest extension of its restriction f ∘s. Then the result follows from Theorem 4.10. □

4.2 Multiple interval Riemann integrals

A partition of a hyper-cube

a⃗ = (a_{1}, …, a_{n}) ∈ R^{n}

is a cartesian product

P⃗ = P_{1} × ⋯ × P_{n}

of partitions of a_{1}, …, a_{n} respectively. We denote the set of partitions of a⃗ by Pa⃗. Refinements are defined coordinatewise. The volume of an n-dimensional hyper-cube x⃗ is

dx⃗ = dx_{1} ⋯ dx_{n}.

Definition 4.3 Let f : R^{n} → R be a map and a⃗ be an n-dimensional hyper-cube. A multiple interval Riemann sum of f on a⃗ is a sum of the form

∑_{x⃗∈P⃗} f(x⃗)dx⃗  for P⃗ ∈ Pa⃗. □

Definition 4.4 The multiple interval Riemann integral of a monotone map f : R^{n} → R on a hyper-cube a⃗ is defined by

∫a⃗ f =\begin{matrix}⨆ & ↑ \\ P⃗ ∈Pa⃗ \end{matrix} ∑_{x⃗∈P⃗} f(x⃗)dx⃗.  □

For n = 1 this definition reduces to our previous definition:

∫_{(a)} f = ∫ \overline{a} \underline{a} f.

Theorem 4.13 (Fubini’s Rule) For every natural number n > 1, every continuous function f : R^{n} → R, and every n-dimensional hyper-cube a⃗,

∫a⃗ f = ∫_{(a_{1})} (∫a⃗′ f(x)dx⃗′) dx_{1},

where a⃗′ = (a_{2}, …, a_{n}) and x⃗′ = (x_{2}, …, x_{n}). Proof For notational simplicity and without essential loss of generality, we prove the claim for n = 2, which corresponds to the inductive step of the claim for arbitrary n by induction on n:

∫_{(a,b)} f = \begin{matrix}⨆ & ↑ \\ P ×Q∈P(a,b) \end{matrix} ∑_{(x,y)∈P ×Q} f(x, y)d(x, y)
= \begin{matrix}⨆ & ↑ \\ P ∈Pa \end{matrix}\begin{matrix}⨆ & ↑ \\ Q∈Pb \end{matrix} ∑_{x∈P} ∑_{y∈Q} f(x, y)dxdy

= \begin{matrix}⨆ & ↑ \\ P ∈Pa \end{matrix} ∑_{x∈P} (\begin{matrix}⨆ & ↑ \\ Q∈Pb \end{matrix} ∑_{y∈Q} f(x, y)dy) dx
= ∫_{(a)} λx ∫_{(b)} λyf(x, y). □

4.3 A supremum operator

In this section we define a supremum operator, which is used in Section 5.2 to obtain a fixedpoint definition of interval Riemann integration. The presentation follows the same pattern as Section 4.1, and therefore we omit the proofs which are reworkings of previous proofs.

Lemma 4.14 Let f : R → R be a monotone map (w.r.t. the information order). If a partition Q of an interval [a, b] refines a partition P then

max_{x∈P} f(x) ⊑ max_{x∈Q} f(x).

Definition 4.5 For a function f : ℝ → ℝ we write

sup_{[a,b]} f = sup_{x∈[a,b]} f(x).

The supremum of a monotone map f : R → R on an interval [a, b] is defined by

sup_{[a,b]} f =\begin{matrix}⨆ & ↑ \\ P ∈P[a,b] \end{matrix} max_{x∈P} f(x).  □

Proposition 4.15 For all continuous maps f, g : R → R and all real numbers α and β,

sup_{[a,a]} f = f(a),
max(sup_{[a,b]} f, sup_{[b,c]} f) = sup_{[a,c]} f,
sup_{[a,b]} max(αf, βg) = max(α sup_{[a,b]} f, β sup_{[a,b]} g).

Clearly, sup_{[a,b]} f depends only on the values that f assumes on I[a, b].

Theorem 4.16 For every interval [a, b], the supremum map

f ↦ sup_{[a,b]} f : [I[a, b] → R] → R

is continuous.

Lemma 4.17 Let [a, b] be an interval, and let B be any basis of I[a, b]. Then for any continuous function f : I[a, b] → R,

sup_{[a,b]} f =\begin{matrix}⨆ & ↑ \\ Q∈P_{B}[a,b] \end{matrix} max_{x∈Q} f(x).

Clearly, for f : ℝ → ℝ continuous we have that

max_{x∈P} If(x) = [max_{x∈P} inf f(x), max_{x∈P} sup f(x)] .

Therefore

sup_{[a,b]} If = {sup_{[a,b]} f} .

Lemma 4.18 For any continuous f : R → R,

sup_{[a,b]} f = sup_{[a,b]} f̂.

Theorem 4.19 The supremum of a continuous function f : R → R depends only on the value that f assumes at maximal elements.

Corollary 4.20 If f : ℝ → ℝ is continuous and f : R → R is a continuous extension of f then

sup_{[a,b]} f = {sup_{[a,b]} f} .

An infimum operator inf is defined similarly, by replacing max by min.

5 Integration in Real PCF

In Subsection 5.1 we extend Real PCF with a primitive for interval Riemann integration, and we establish computational adequacy for the extension. In Subsection 5.2 we show how to recursively define integration from the supremum operator. In Subsection 5.3 we extend Real PCF with a primitive for supremum, and we establish computational adequacy for the extension. Finally, in Subsection 5.4 we discuss universality of Real PCF extended with integration or supremum.

5.1 Real PCF extended with interval Riemann integration

Again, for simplicity and without essential loss of generality, we restrict ourselves to the unit interval. Clearly, the map ∫_{0}^{1} : [I → R] → R restricts to [I → I] → I. We denote the restriction by ∫.

The programming language Real PCF∫

Instead of introducing integration as a constant, we introduce it as a construction. This treatment of primitive operations is taken from Gunter [29]. We could treat all primitive operations in this way, as he does, but we treat only integration in this way, for simplicity.

Definition 5.1

1. Real PCF∫ is Real PCF extended by the following term-formation rule:

If Y : I is a term and x : I is a variable, then ∫ Y dx : I is a term, with the same free variables as Y, except for x, which becomes bound. Terms of this form are called integrals, whereas Y is called the integrand.

2. The meaning of the term ∫ Y dx in an environment ρ is ∫ f, where f is the meaning of λx.Y in ρ. □

Convention 5.1 We denote α-congruence by ≡. Following Barendregt [4], we identify αcongruent terms, and we adopt the inductive definition of substitution given in loc. cit., extended by the rules • c[α := M] ≡ c for any constant c.

• (∫ Y dx)[α := M] ≡ (∫ Y [α := M]dx) provided α ≢ x.

• (∫ Y dx)[x := M] ≡ (∫ Y dx). Notice that this definition assumes the so-called “[bound] variable convention” in order to omit the cumbersome proviso which prevents the capture of free variables [3]. □ Operational semantics Recall that ⊕ denotes binary average, which is a Real PCF definable operation. Lemma 5.2 For any continuous map f : I → I,

∫ cons_{a} ∘ f = cons_{a} (∫ f) ,

∫ f = ∫ f ∘ cons_{L} ⊕ ∫ f ∘ cons_{R}.

Proof The first equation is linearity. For the second equation we have

∫ f = ∫_{0}^{1} f
= ∫0^{\frac{1}{2}} f + ∫ 1_{\frac{1}{2}} f
= ∫_{0}^{1} f (\frac{x}{2}) \frac{1}{2}dx + ∫_{0}^{1} f (\frac{x+1}{2}) \frac{1}{2}dx
= ∫ f ∘ cons_{L} ⊕ ∫ f ∘ cons_{R}. □

Definition 5.2 The immediate reduction rules for integration are:

1. (Production) ∫ Y dx → ∫ Zdx if Y → Z,

2. (Output) ∫ cons_{a}Y dx → cons_{a} (∫ Y dx),

3. (Input) ∫ Y dx → ∫ Y_{L}dx ⊕ ∫ Y_{R}dx, where

Y_{a} ≡ Y [x := cons_{a}x].  □

Intuitively, the output rule produces partial output, the input rule supplies partial input, and the production rule partially evaluates the integrand (with no input or with the partial input supplied by the input rule in previous reduction steps).

Computational adequacy

Lemma 5.3 For every natural number n define a map ∫^{(n)} : [I → I] → I by

∫ ^{(n)} f = ∑_{k=1}^{2^{n}} f ([\frac{k − 1}{2^{n}}, \frac{k}{2^{n}} ]) \frac{1}{2^{n}} .

Then ∫^{(n)} is continuous, and

∫ f =\begin{matrix}⨆ & ↑ \\ n≥0 \end{matrix} ∫ ^{(n)} f.

Proof The right-hand side of the equation can be expressed as

\begin{matrix}⨆ & ↑ \\ n≥0 \end{matrix} ∑_{y∈Q_{n}} f(y)dy,

where

Q_{n} = \{[\frac{k − 1}{2^{n}}, \frac{k}{2^{n}} ]| 1 ≤ k ≤ 2^{n}\} .

Let D_{n} = {k/2^{n}|0 ≤ k ≤ 2^{n}}. Then ⋃_{n≥0} D_{n} is the set of dyadic numbers, which is dense in [0, 1]. Hence intervals with distinct dyadic end-points form a basis of I[0, 1], say B. Moreover, the end-points of the intervals in Q_{n} are contained in D_{n}. Hence for every partition P ∈ P_{B}[0, 1] there is some n such that Q_{n} refines P. Therefore the result follows from Lemma 4.5.

□

Lemma 5.4 For every natural number n,

∫ ^{(0)} f = f(⊥),
∫ ^{(n+1)} f = ∫ ^{(n)} f ∘ cons_{L} ⊕ ∫ ^{(n)} f ∘ cons_{R}.

Proof For the first equation we have

∫ ^{(0)} f = ∑_{k=1}^{2^{0}} f ([\frac{k − 1}{2^{0}}, \frac{k}{2^{0}} ]) \frac{1}{2^{0}} = f([0, 1]) = f(⊥).

For the second equation we have

∫ ^{(n+1)} f = ∑_{k=1}^{2^{n+1}} f ([\frac{k − 1}{2^{n+1}}, \frac{k}{2^{n+1}} ]) \frac{1}{2^{n+1}}
= ∑_{k=1}^{2^{n}} f ([\frac{k − 1}{2^{n+1}}, \frac{k}{2^{n+1}} ]) \frac{1}{2^{n+1}} + ∑_{k=2^{n}+1}^{2^{n+1}} f ([\frac{k − 1}{2^{n+1}}, \frac{k}{2^{n+1}} ]) \frac{1}{2^{n+1}}
= \frac{1}{2} ∑_{k=1}^{2^{n}} f ([\frac{k − 1}{2^{n+1}}, \frac{k}{2^{n+1}} ]) \frac{1}{2^{n}} + \frac{1}{2} ∑_{k=1}^{2^{n}} f ([\frac{(k + 2^{n}) − 1}{2^{n+1}}, \frac{k + 2^{n}}{2^{n+1}} ]) \frac{1}{2^{n}}
= ∑_{k=1}^{2^{n}} f (\frac{[\frac{k−1}{2^{n}}, \frac{k}{2^{n}} ]}{2}) \frac{1}{2^{n}} ⊕ ∑_{k=1}^{2^{n}} f (\frac{[\frac{k−1}{2^{n}}, \frac{k}{2^{n}} ] + 1}{2}) \frac{1}{2^{n}}
= ∫ ^{(n)} f (\frac{x}{2}) dx ⊕ ∫ ^{(n)} f (\frac{x + 1}{2}) dx
= ∫ ^{(n)} f ∘ cons_{L} ⊕ ∫ ^{(n)} f ∘ cons_{R}. □

As a corollary, we have that for every n there is a program in Real PCF (without the integration primitive) defining ∫^{(n)}. But, in order to establish computational adequacy, it will prove simpler to introduce ∫^{(n)} as a primitive construction. Definition 5.3

1. Real PCF^{∫^{(n)}} is Real PCF∫ extended with a constant Ω_{σ} : σ for each type σ and the

following term-formation rule for each natural number n: If Y : I is a term and x : I is a variable, then ∫^{(n)} Y dx : I is a term, with the same free variables as Y, except for x, which becomes bound.

2. The meaning of Ω_{σ} is the bottom element of the domain of interpretation of σ.

3. The meaning of ∫^{(n)} Y dx in an environment ρ is ∫^{(n)} f, where f is the meaning of λx.Y in ρ.

4. There is no reduction rule for Ω_{σ}.

5. The immediate reduction rules for ∫^{(n)} are:

(a) (Production) ∫^{(0)} Y dx → ∫^{(0)} Zdx if Y → Z,

(b) (Output) ∫^{(0)} cons_{a}Y dx → cons_{a} (∫^{(0)} Y dx),

(c) (Input) ∫^{(n+1)} Y dx → ∫^{(n)} Y_{L}dx ⊕ ∫^{(n)} Y_{R}dx. □ Definition 5.4 A sublanguage of a language L is a subset of L-terms which is closed under reduction. □ The following lemma is immediate: Lemma 5.5 If every L-term is computable, so is every term of any sublanguage of L.

Thus, in order to prove that every term of Real PCF∫ is computable it suffices to prove that every term of Real PCF^{∫^{(n)}} is computable.

Definition 5.5 Let ≼ be the least relation on terms such that:

1. If M : σ then Ω_{σ} ≼ M.

2. If Y ≼ Y′ : I then ∫^{(n)} Y dx ≼ ∫ Y′dx and also ∫ Y dx ≼ ∫ Y′dx.

3. M ≼ M.

4. If M ≼ M′ : σ → τ and N ≼ N′ : σ, then (MN) ≼ (M′N′).

5. If M ≼ M′ are terms (of the same type) then λα.M ≼ λα.M′. □

This relation turns out to be reflexive and transitive, which justifies the notation, but we don’t need this fact.

The following lemma is analogous to Lemma 3.2 of [34].

Lemma 5.6 If M ≼ N and M → M′ then M′ ≼ N′ and N → N′ for some N′.

This situation is summarized by the diagram below:

\begin{matrix}M & ≼ & N \\ M′ & & ≼ & N′ & ^{. . . . .} \end{matrix}

Proof By structural induction on M, according to why M → M′. □

Corollary 5.7 If M ≼ N and M →^{∗} M′ then M′ ≼ N′ and N →^{∗} N′ for some N′. Proof By induction on the length of the reduction. □

Corollary 5.8 For each natural number n and all Y : I and x : I,

Eval (∫ ^{(n)} Y dx) ⊆ Eval (∫ Y dx) .

Proof Immediate consequence of Corollary 5.7, noticing that, by definition of ≼, if one has that cons_{a}Z ≼ Z′ then Z′ has to be of the form cons_{a}Z′′. □

The term Ω_{σ} is trivially computable.

Lemma 5.9 For every n, if Y : I is computable so is ∫^{(n)} Y dx for all x : I. Proof By induction on n.

Base: Since the terms ∫^{(0)} Y dx and Y [x := Ω_{I}] have the same meaning in any environment, namely ∫^{(0)} f = f(⊥) where f is the meaning of λx.Y, and since Y [x := Ω_{I}] is computable as it is an instantiation of a computable term by computable terms, it suffices to conclude that Eval(Y [x := Ω_{I}]) ⊆ Eval(∫^{(0)} Y dx). Assume that Y [x := Ω_{I}] →^{∗} cons_{a}Z. One easily checks by structural induction that Y [x := Ω_{I}] ≼ Y. Hence, by Corollary 5.7 we conclude that Y →^{∗} Z′ for some Z′ with cons_{a}Z ≼ Z′. By definition of ≼, Z′ has to be of the form cons_{a}Z′′. Hence, by some applications of the production rule followed by an application of the output rule, ∫^{(0)} Y dx →^{∗} ∫^{(0)} cons_{a}Z′′dx → cons_{a}(∫^{(0)} Z′′dx).

Induction step: If Y is computable so is Y_{a} for any a. Hence, by the induction hypothesis, ∫^{(n)} Y_{a}dx is computable. Since ⊕ is a Real PCF term, it is computable. By definition of computability, it follows that ∫^{(n)} Y_{L}dx ⊕ ∫^{(n)} Y_{R}dx is computable. Therefore ∫^{(n+1)} Y dx is computable, because every reduction from ∫^{(n+1)} Y dx factors through ∫^{(n)} Y_{L}dx ⊕ ∫^{(n)} Y_{R}dx via the input rule, and ∫^{(n+1)} Y dx has the same meaning as ∫^{(n)} Y_{L}dx ⊕ ∫^{(n)} Y_{R}dx, in any environment. □

Lemma 5.10 Every Real PCF^{∫^{(n)}} term is computable. Proof Extend the proof of Lemma 35 of [21, page 109] by including Lemma 5.9 as one of the inductive steps. □

Theorem 5.11 (Computational Adequacy) Every Real PCF∫ term is computable. Proof Lemmas 5.3, Corollary 5.8, and Lemmas 5.10 and 5.5. □

5.2 A fixed-point definition of integration

It is natural to ask whether the integration operator, added in Section 5.1 as primitive, is already recursively definable in Real PCF.

Let D = [[I → I] → I]. Then the second equation of Lemma 5.2 leads one to consider the map G : D → D defined by

G(F)(f) = F (f ∘ cons_{L}) ⊕ F (f ∘ cons_{R}).

Thus the integration operator ∫ is a fixed point of G. However, the least fixed point is the bottom element of D.

Peter Freyd suggested that if we restrict ourselves to the subspace D′ ⊆ D of functions F ∈ D such that

inf f ≤ F (f) ≤ sup f,

then G restricts to a map G′ : D′ → D′, and ∫ is the least fixed point of G′. We use this idea in a modified form, obtaining ∫ directly as the least fixed point of a function H : D → D.

Define a map j : [0, 1]^{3} → [0, 1] by

j(x, y, z) = max(x, min(y, z)).

Then, given a ≤ b, the map g : [0, 1] → [0, 1] defined by

g(x) = j(a, x, b)

is idempotent,

a ≤ f(x) ≤ b,

and

g(x) = x iff a ≤ x ≤ b.

Also, define a function H : D → D by

H(F)(f) = j (inf f, F (f ∘ cons_{L}) ⊕ F (f ∘ cons_{R}), sup f) .

Lemma 5.12 For every continuous function f : I → I,

H^{n}(⊥)(f) = ∫ ^{(n)} f̂,

where f̂ is defined as in Lemma 4.8. Proof By induction on n. For the base case use the fact that f̂(⊥) = j(inf f, ⊥, sup f). □

Proposition 5.13 ∫ is the least fixed point of H. Proof Immediate consequence of Lemmas 5.3 and 5.12. □

Thus, if the supremum operator is definable, so is the integration operator. But the supremum operator is not definable. The proof is postponed to Subsection 5.4.

5.3 Real PCF extended with supremum

This subsection follows the same pattern as Subsection 5.1. Due to this reason, we omit the proofs which are reworking of proofs given earlier. Again, for simplicity and without essential loss of generality, we restrict ourselves to the unit interval. Clearly, the map sup_{[0,1]} : [I → R] → R restricts to [I → I) → I. We denote the restriction by sup.

Definition 5.6 Real PCF^{sup} is Real PCF extended with a construction sup_{x} Y, as in Definition 5.1, denoting the operation sup : [I → I] → I. □

Lemma 5.14 For any continuous map f : I → I,

sup cons_{a} ∘ f = cons_{a} (sup f) ,
sup f = max (sup f ∘ cons_{L}, sup f ∘ cons_{R}) .

Definition 5.7 The immediate reduction rules for supremum are:

1. (Production) sup_{x} Y → sup_{x} Z if Y → Z,

2. (Output) sup_{x} cons_{a}Y → cons_{a} (sup_{x} Y),

3. (Input) sup_{x} Y → max (sup_{x} Y_{L}, sup_{x} Y_{R}),

where

Y_{a} ≡ Y [x := cons_{a}x].  □

Notice that these are the reduction rules for ∫ with ∫ and ⊕ replaced by sup and max respectively. We obtain the following similar results, whose proofs are omitted because they are similar too:

Lemma 5.15 For every natural number n define a map sup^{(n)} : [I → I] → I by

sup^{(n)}f = max_{k=1}^{2^{n}} f ([\frac{k − 1}{2^{n}}, \frac{k}{2^{n}} ]) .

Then sup^{(n)} is continuous, and

sup f =\begin{matrix}⨆ & ↑ \\ n≥0 \end{matrix} sup^{(n)}f.

Lemma 5.16 For every natural number n,

sup^{(0)}f = f(⊥),
sup^{(n+1)}f = max (sup^{(n)}f ∘ cons_{L}, sup^{(n)}f ∘ cons_{R}) .

As a corollary, we have that for every n there is a Real PCF program defining sup^{(n)}. But, as we did for integration, we add the partial supremum operators sup^{(n)} as primitive, and we conclude that:

Theorem 5.17 (Computational Adequacy) Every Real PCF^{sup} term is computable.

The operation inf is definable from sup by

inf f = 1 − sup_{x}(1 − f(x)),

so there is no need to include it as primitive too.

Corollary 5.18 The integration operator is definable in Real PCF^{sup}. Proof The function H of Lemma 5.12 is Real PCF^{sup} definable. □

Corollary 5.19 For every natural number n there is a program in Real PCF extended with either integration or supremum which computes the multiple integration operator ∫ : [I^{n} → I] → I of order n. Proof (Since PCF does not have cartesian products, we have to use curried maps.) Our primitive or program for integration takes care of the case n = 1. Fubini’s Rule (Theorem 4.13) can be read as a definition of a program for the case n + 1 from a program for the case n. By the computational adequacy theorems, these programs indeed compute multiple integrals of order n. □ This application of the computational adequacy theorems shows that computational adequacy is a powerful property. In fact, it allows us to derive correct programs from analytical results, in a representation-independent fashion. Of course, this is precisely the idea behind denotational semantics.

5.4 Universality of Real PCF extended with integration or supremum

Although Theorem 2.6 implies that sup is definable in Real PCF extended with ∃, we don’t know a neat fixed-point definition of sup.

Proposition 5.20 The existential quantification operator ∃ is definable in Real PCF extended with sup. Proof For D ∈ {N , T }, define continuous maps

D ⇆_{s_{D}}^{r_{D}} I

by

s_{N} (n) = if n = 0 then 0 else cons_{R}(s_{N} (n − 1))
r_{N} (x) = if x <_{⊥} 1/4 then 0 else r_{N} (tail_{R}(x)) + 1,
s_{T} (t) = if t then 1 else 0
r_{T} (x) = if x <_{⊥} 1/2 then false else true

Then (s_{D}, r_{D}) is a section-retraction pair. This is immediate for D = T . For D = N, we prove by induction on n that r_{N} ∘ s_{N} (n) = n. If n = ⊥ or n = 0 this is immediate. For the inductive step we have that

r_{N} ∘ s_{N} (n + 1) = r_{N} (cons_{R}(s_{N} (n))
= r_{N} (tail_{R} ∘ cons_{R}(s_{N} (n))) + 1
= r_{N} (s_{N} (n)) + 1
= n + 1 by the induction hypothesis.

It follows that the diagram below commutes:

[I → I] ⟶^{sup} I
r_{N} →s_{T} ↑  ↓^{r_{T}}
[N → T ] ⟶_{∃} T

In fact, let p ∈ [N → T ] and define f : I → I by

f = (r_{N} → s_{T})(p) = s_{T} ∘ p ∘ r_{N} .

If there is some n such that p(n) = true, then there is some x such that f(x) = 1, namely x = s_{N} (n), and in this case we have that sup f = 1. If p(⊥) = false, then f(⊥) = 0, and in this case we have that sup f = 0. Therefore ∃ is definable in Real PCF extended with sup. □

Corollary 5.21 Real PCF extended with sup is universal.

This shows that sup is not Real PCF definable, because ∃ is not Real PCF definable. We don’t know whether Real PCF extended with integration is universal. Moreover, we don’t know whether integration is definable in Real PCF with no extensions, but we conjecture that this is not the case.

For applications of Real PCF to real analysis, it seems more natural to include the supremum operator as a primitive operation than to include the existential quantification operator.

Acknowledgements

We would like to thank Peter Freyd for his suggestion about the fixed-point definition of the integration operator, based on our reduction rules, Klaus Keimel for many discussions about this paper, and Reinhold Heckmann for having spotted some mistakes in the preliminary versions. The second author has been supervised by Mike Smyth and has benefited from endless discussions with him.

This work has been supported by EPSRC projects “Constructive Approximation Using Domain Theory”, “Foundational Structures in Computer Science” and “Programming Languages for Real Number Computation: Theory and Implementation”, and by an ARC project “A Computational Approach to Measure and Integration Theory”. The second author has also been supported by the Brazilian agency CNPq.

References

[1] 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.

[2] M. Alvarez-Manilla. A generalization of the Riemann-Stieltjes integral using domain theory. Master’s thesis, Department of Computing, Imperial College, 1996.

[3] H.P. Barendregt. The Lambda-Calculus: its Syntax and Semantics. North-Holland, Amsterdam, 1984.

[4] H.P. Barendregt. Lambda calculi with types. In S. Abramsky, D.M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 2, pages 117–309. Clarendon Press, Oxford, 1992.

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

[6] 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.

[7] H.J. Boehm and R. Cartwright. Exact real arithmetic: Formulating real numbers as functions. In Turner. D., editor, Research Topics in Functional Programming, pages 43–64. Addison-Wesley, 1990.

[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] N. Bourbaki. General Topology, volume 1. Addison-Wesley, London, 1966.

[10] A. Edalat. Domain of computation of a random field in statistical physics. 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, Møller Centre, Cambridge, 11-14 September 1995. IC Press.

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

[12] A. Edalat. Domain theory in learning processes. In S. Brookes, M. Main, A. Melton, and M. Mislove, editors, Proceedings of MFPS, volume one of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.

[13] A. Edalat. Domain theory in stochastic processes. In Proceedings of Logic in Computer Science (LICS), Tenth Annual IEEE Symposium, 26-19 June, 1995, San Diego. IEEE Computer Society Press, 1995.

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

[15] A. Edalat. Power domains and iterated function systems. Information and Computation, 124:182–197, 1996.

[16] A. Edalat. The Scott topology induces the weak topology. Mathematical Structures in Computer Science, 1996. To appear.

[17] A. Edalat and R. Heckmann. A computational model for metric spaces. Theoretical Computer Science, 1996. To appear.

[18] A. Edalat and S. Negri. Generalised Riemann integral on locally compact spaces. In A. Edalat, S. Jourdan, and G. McCusker, editors, Advanced in theory and formal methods of computing: Proceedings of the third Imperial College workshop April 1996. Imperial College Press, 1996.

[19] 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, 11–14 September 1994. IC Press. 1995.

[20] M.H. Escardó. Injective spaces revisited. Submitted for publication, July 1996.

[21] M.H. Escardó. PCF extended with real numbers. Theoretical Computer Science, 162(1):79–115, August 1996.

[22] M.H. Escardó. PCF extended with real numbers: A domain-theoretic approach to higherorder exact real number computation. PhD thesis, Imperial College, Department of Computing, November 1996.

[23] M.H. Escardó. Real PCF extended with ∃ is universal. In A. Edalat, S. Jourdan, and G. McCusker, editors, Advances in Theory and Formal Methods of Computing: Proceedings of the Third Imperial College Workshop, April 1996, pages 13–24, Christ Church, Oxford, 1996. IC Press.

[24] 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.

[25] P. Di Gianantonio. A functional approach to computability on real numbers. PhD thesis, University of Pisa, 1993. Technical Report TD 6/93.

[26] P. Di Gianantonio. Real number computability and domain theory. In 18th symposioum on Mathematical Foundation of Compueter Science, number 711 in LNCS, pages 413– 422. Springer-Verlag, 1993.

[27] P. Di Gianantonio. Real number computability and domain theory. Information and Computation, 127(1):11–25, 1996.

[28] 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.

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

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

[31] Ker-I Ko. Complexitity Theory of Real Functions. Birkhauser, Boston, 1991.

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

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

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

[35] P. J. Potts. The storage capacity of forgetful neural networks. Master’s thesis, Department of Computing, Imperial College, 1995.

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

[37] H.L. Royden. Real Analysis. Collier Macmillan Publishing, third edition, 1988.

[38] A. Schalk. Algebras for Generalized Power Constructions. PhD thesis, Technische Hochschule Darmstadt, July 1993. http://hypatia.dcs.qmw.ac.uk.

[39] D. S. Scott. Continuous lattices. In F.W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lectures Notes in Mathematics, pages 97–136. Springer-Verlag, 1972.

[40] 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.

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

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

[43] K. Weihrauch. Computability. Springer-Verlag, Berlin, 1987.

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

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

Contents

1 Introduction 1

2 Real PCF 3 2.1 Interval expansions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 The interval domain . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.3 Canonical extensions of continuous real valued maps of real variables . . . . . 5 2.4 Real PCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.5 Operational semantics of Real PCF . . . . . . . . . . . . . . . . . . . . . . . . 9 2.6 Computational adequacy of Real PCF . . . . . . . . . . . . . . . . . . . . . . 10 2.7 Universality of Real PCF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

3 Scott continuous functions R → R 11 3.1 Partial real valued functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 Discontinuous functions in real analysis versus Scott continuous functions in

domain theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

4 Interval Riemann integrals 15 4.1 Simple interval Riemann Integrals . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2 Multiple interval Riemann integrals . . . . . . . . . . . . . . . . . . . . . . . . 22 4.3 A supremum operator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

5 Integration in Real PCF 24 5.1 Real PCF extended with interval Riemann integration . . . . . . . . . . . . . 24 5.2 A fixed-point definition of integration . . . . . . . . . . . . . . . . . . . . . . 29 5.3 Real PCF extended with supremum . . . . . . . . . . . . . . . . . . . . . . . 30 5.4 Universality of Real PCF extended with integration or supremum . . . . . . . 31