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

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 maximization of functions and then recursively defining integration from maximization. In both cases we have an 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, which implies that it is also fully abstract.

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 [3]. However, such “correct” programs do not produce correct results in practice, due to the presence of roundoff 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. [4, 5, 25] on the practical side and e.g. [2, 20, 21, 24, 26, 27, 28] 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 [6] and [16]. Such programming languages do allow for correctness proofs based on analytical methods.

Real PCF [16] is an extension of the programming language PCF [23] 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.

Based on previous work on domain theory and integration [11, 8], we show how to handle integration in Real PCF. In domain-theoretic integration, one obtains increasingly better approximations to the value of the integral of a real-valued function. This has led to exact computations of integrals in various fields such as statistical physics [7], neural nets [9], stochastic processes [10], and fractal geometry [12].

In order to handle integration in Real PCF, we generalize Riemann integration of real-valued 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 [22].

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

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 define interval Riemann integrals. In Section 4 we extend Real PCF with a primitive for integration. In Section 5 we define a function maximization operator. In Section 6 we extend Real PCF with a primitive for maximization. In Section 7 we show how to recursively define integration from maximization. In Section 8 we define multiple integrals and show how to define them from interval Riemann integration. In Section 9 we show that Real PCF extended with maximization is universal.

Several proofs have been omitted due to lack of space. For a full version of this paper containing all proofs see [13].

2. Real PCF

In this section we summarize the results of [16, 14] needed in this paper. We assume familiarity with PCF [23, 19]. We are deliberately informal concerning syntax. For simplicity and without essential loss of generality, we restrict ourselves to the unit interval [0, 1].

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

Let us consider binary expansions of numbers in the unit interval. 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 [21], 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 [15]. □

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 linear 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.2 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 shrinking chain of intervals. Conversely, any shrinking chain of intervals gives rise to an interval expansion, as shown at the end of the next subsection.

2.2. The unit 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. Therefore, we sometimes notationally identify singleton intervals and real numbers.

We let I be the set of closed subintervals of [0, 1] ordered by reverse inclusion, denoted by ⊑. The letters x, y, z, a, b, c in bold font range over I, and we put

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

(I, ⊑) is a continuous Scott domain (bounded complete ω-continuous dcpo) [1] with bottom element ⊥ = [0, 1]. Its way-below relation is given by

x ≪ y iff the interior of x contains y.

The set Max(I) of maximal elements (singleton intervals) with the subspace topology of the Scott topology of I is homeomorphic to the Euclidean unit interval. More generally, we can consider the domain I[a, b] of all closed subintervals of [a, b].

Definition 2.3 Given intervals x, y ∈ I, 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.4 1. The map cons_{a} : I → I is continuous for every a ∈ I.

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

3. The information order of (I, ⊑) coincides with the prefix preorder of (I, □, ⊥), in the sense that

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

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

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

If x ⊑ z and x is non-maximal then we denote the unique 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, if

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

is a chain of non-singleton intervals with join x then the sequence

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

is an interval expansion of x.

2.3. Real PCF

The linear maps cons_{a} for a ≠ ⊥ with distinct rational end-points will play a rôle analogous to the rôle played by the successor map on natural numbers.

The predecessor map, undefined or arbitrarily defined at zero, is a left inverse of the successor map. Similarly, we now look for 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}, first consider cons_{[a,b]} as a map [0, 1] → [0, 1]. The co-restriction of cons_{[a,b]} to its range [a, b] is invertible. Hence the continuous map

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

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]. We thus let tail_{[a,b]} : I → I be defined by

tail_{[a,b]}([x, y]) = [tail_{[a,b]}(x), tail_{[a,b]}(y)].

This map is clearly a left inverse of cons_{[a,b]} : I → I and is continuous. The left-inverses of s_{0}, s_{\frac{1}{2}} and s_{1} corresponding to tail_{[0, \frac{1}{2} ]}, tail_{[ \frac{1}{4} , \frac{3}{4} ]}, and tail_{[ \frac{1}{2} , 1]} respectively are

p_{0}(x) = min(2x, 1)
p_{\frac{1}{2}} (x) = max(0, min(2x − \frac{1}{2}, 1))
p_{1}(x) = max(0, 2x − 1).

We need two more primitives, in addition to the linear maps cons_{a} and their left inverses tail_{a}.

The first is 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.5 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 [21] (see Subsection 2.4 below). The map x ↦ (x <_{⊥} r) can be regarded as the best continuous approximation to the monotone function x ↦ (x <′_{⊥} r). □

The second primitive is a stronger version of the conditional, called the parallel conditional:

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.6 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}], and R = [\frac{1}{2}, 1]. By means of the primitives that we have introduced, this recursive definition can be rewritten as

x ⊕ y = pif x <_{⊥} \frac{1}{2}

then pif y <_{⊥} \frac{1}{2} then cons_{L}(tail_{L}(x) ⊕ tail_{L}(y))

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

else pif y <_{⊥} \frac{1}{2} then cons_{C}(tail_{R}(x) ⊕ tail_{L}(y)) else cons_{R}(tail_{R}(x) ⊕ tail_{R}(y)). □

For recursive definitions of the complement map x ↦ 1−x, multiplication, and logarithm see [16].

Definition 2.7 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. □

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

2.4. 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.8 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 not 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 f(x) = g(x) for all maximal x with p(x) = ⊥. This is the case, for instance, in the recursive definition of average given in Example 2.6. 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. Adequacy

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

1. cons_{a}(cons_{b}(x)) → cons_{cons_{a}(b)}(x)

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

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

4. tail_{a}(cons_{b}(x)) → cons_{tail_{a}(b)}(x)

if a ⊑ b and a ≠ b

5. tail_{a}(cons_{b}(x)) → cons_{tail_{a}(b)}(tail_{tail_{b}(a)}(x))

if tail_{a}(b) and tail_{b}(a) are non-maximal

6. cons_{a}(x) <_{⊥} r → true if \overline{a} < r

7. cons_{a}(x) <_{⊥} r → false if \underline{a} > r

8. pif true then x else y → x

9. pif false then x else y → y

10. pif p then cons_{a}(x) else cons_{b}(y) →

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

if a ⊓ b ≠ ⊥.

Roughly, these rules

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

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 range a.

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

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.11 below.

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

A Real PCF program X denoting a generalized real number x is computable if for every nonbottom interval y ≪ x, as close to x as we please, X produces a partial result a with

y ⊑ a ⊑ x.

Theorem 2.11 (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}.

3. Interval Riemann integrals

A generalization of the Riemann theory of integration based on domain theory was introduced in [8]. Essentially, a domain-theoretic framework for the integration of realvalued 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 paper we will only be concerned with integration w.r.t. to the Lebesgue measure (uniform distribution) in ℝ^{n}. Other measures in ℝ^{n} will be dealt with in a future paper.

In order to extend Real PCF with integration, we embark on a novel approach compared to [8] for integration w.r.t. the Lebesgue measure in ℝ. We work with the continuous dcpo R = I ℝ of compact intervals of the real line ordered by reverse inclusion, and we consider integration of maps of type R^{n} → R rather than ℝ^{n} → ℝ, and we deduce various properties which are interesting in their own right as well.

Addition in the continuous dcpo R is defined by

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

The map (x, y) ↦ x + y : R × R → R is continuous. Given a real number α and an interval x, we put

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

The map x ↦ xα : R → R is continuous too. We also put

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.

Lemma 3.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 3.2 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 3.3 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.

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

∫_{a}^{b} f = ⨆_{P ∈P[a,b]} ∑_{x∈P} f(x)dx.

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

Proposition 3.5 For all monotone 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.

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

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

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

is continuous.

Proof Let F be a directed subset of [I[a, b] → R]. Then

∫_{a}^{b} ⨆ F = ⨆_{P} ∑_{x∈P} (⨆ F) (x)dx

= ⨆_{P} ∑_{x∈P} ( ⨆_{f∈F} f(x)) dx
= ⨆_{P} ∑_{x∈P} ⨆_{f∈F} f(x)dx
= ⨆_{P} ⨆_{f∈F} ∑_{x∈P} f(x)dx
= ⨆_{f∈F} ⨆_{P} ∑_{x∈P} f(x)dx

= ⨆_{f∈F} ∫_{a}^{b} f. □

Lemma 3.7 Let [a, b] be an interval, let B be any basis of I[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 = ⨆_{Q∈P_{B}[a,b]} ∑_{x∈Q} f(x)dx.

Remark 3.8 Moore [22] 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 [17, 18]. Therefore Lemma 3.7 above and Theorem 3.12 below show that our definition generalizes that of Moore to all Scott continuous functions. □

Given any continuous function f : ℝ → ℝ, the function If : R → R defined by

If(x) = f(x)

is also continuous. Since continuous maps preserve connectedness and compactness,

If(x) = [inf f(x), sup f(x)].

Hence 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\} .

The map If is an extension of the map f, in the sense that

If({x}) = {f(x)}.

Any continuous map f : ℝ → ℝ has infinitely many distinct continuous extensions to R → R. The extension If is characterized as the greatest one. Theorem 3.12 below shows that If can be replaced by any continuous extension f in the above equation.

Lemma 3.9 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) = [inf_{x∈x} \underline{f(\{x\})}, sup_{x∈x} \overline{f(\{x\})}] .

Lemma 3.10 For any continuous f : R → R,

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

Theorem 3.11 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 3.9, f_{| Max(R)} = g_{| Max(R)} implies f̂ = ĝ. Therefore the result follows from Lemma 3.10. □

Theorem 3.12 If f : ℝ → ℝ is continuous and f : R → R is a continuous extension of f then

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

Proof We know that this is true for f = If. If f is any extension then Lemma 3.9 implies that f̂ = If. Therefore the result follows from Theorem 3.11. □

The significance of Theorems 3.11 and 3.12 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 greatest continuous 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 [22].

4. Integration in Real PCF

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 ∫.

In this section we add ∫ : [I → I] → I as a primitive operation to Real PCF.

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

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

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

Proof (Outline) 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}. □

Notation 4.2 1. ∫ Y dx stands for ∫ λxY.

2. ∫ F (x)dx stands for ∫ F if F is a primitive operation of type I → I. □

This notation is ambiguous. For instance, ∫ cons_{a}(x)dx can stand for both ∫ cons_{a} and ∫ λx cons_{a}(x). However, his ambiguity does not introduce inconsistencies, because both terms have the same meaning.

Lemma 4.1 gives rise to the following reduction rules:

1. ∫ cons_{a}(Y)dx → cons_{a} (∫ Y dx)

2. ∫ Y [x]dx → ∫ Y [cons_{L}(x)]dx ⊕ ∫ Y [cons_{R}(x)]dx

3. ∫ Y dx → ∫ Y′dx if Y → Y′.

Here Y [x] is a term of type I with some free occurrences of x, and Y [X] denotes the term Y with all free occurrences of x replaced by the term X.

We call these rules the output, input, and production rules respectively. 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).

In order to establish adequacy we need some lemmas.

Lemma 4.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 = ⨆_{n≥0} ∫ ^{(n)} f,

where the join is directed.

Lemma 4.4 For every natural number n,

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

Corollary 4.5 For every n there is a program in Real PCF (without the integration primitive) defining ∫^{(n)}.

Lemma 4.6 If F : I → I is a closed computable term then every partial result produced by the program ∫^{(n)} F is also produced by the program ∫ F.

Proof By induction on n. For the base case use the production rule, the output rule, and the fact that F is computable. For the inductive step use the input rule 2^{n} times, the fact that ⊕ and ∫^{(n)} are computable, and the fact that Y [cons_{a}(x)] is computable if Y [x] is computable. □

Lemma 4.7 ∫ is a computable primitive operation.

Proof Let F be any closed computable program denoting a function f : I → I, and let y ≪ ∫ f. Since ∫ f is the join of the chain {∫^{(n)} f}_{n≥0}, there is an n such that y ≪ ∫^{(n)} f, by a basic property of the way-below relation in continuous dcpos. Now, ∫^{(n)} F is computable because ∫^{(n)} and F are computable. Hence there is some a with y ⊑ a ⊑ ∫^{(n)} f such that ∫^{(n)} F partially evaluates to a program of the form cons_{a}(X), by definition of computability. But

y ⊑ a ⊑ ∫ ^{(n)} f ⊑ ∫ f

and ∫ F partially evaluates to a program of the form cons_{a}(X′), by virtue of Lemma 4.6. Therefore ∫ is computable. □

Theorem 4.8 (Adequacy) Every term in Real PCF extended with integration is computable.

Proof Extend the proof of adequacy of Real PCF given in [16] by including Lemma 4.7 as one of the inductive steps. □

5. A supremum operator

In this section we define a supremum operator. The presentation follows the same pattern as Section 3.

Recall that an extension If : R → R of any continuous function f : ℝ → ℝ was defined in Section 3. This construction clearly generalizes to real valued continuous of several real variables. For example, we have that

I max(x, y) = [max(\underline{x}, \underline{y}), max(\overline{x}, \overline{y})].

When there is not danger of ambiguity, we write f instead of If.

Lemma 5.1 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 5.2 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 = ⨆_{P ∈P[a,b]} max_{x∈P} f(x). □

Proposition 5.3 For all monotone 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 5.4 For every interval [a, b], the supremum map

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

is continuous.

Lemma 5.5 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 = ⨆_{Q∈P_{B}[a,b]} 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 5.6 For any continuous f : R → R,

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

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

Theorem 5.8 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.

6. Real PCF extended with supremum

This section follows the same pattern as Section 4. 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.

In this section we add sup : [I → I] → I as a primitive operation to Real PCF.

Lemma 6.1 max and min (in curried form I → I → I) are definable in Real PCF.

Proof max can be recursively defined by

max(x, y) = pif x <_{⊥} \frac{1}{2} then pif y <_{⊥} \frac{1}{2} then cons_{L}(max(tail_{L}(x), tail_{L}(y)))

else y

else pif y <_{⊥} \frac{1}{2} then x else cons_{R}(max(tail_{R}(x), tail_{R}(y))),

and min can be defined by

min(x, y) = 1 − max(1 − x, 1 − y). □

Lemma 6.2 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}) .

Notation 6.3 1. sup_{x} Y stands for sup λxY.

2. sup_{x} F (x) stands for sup F if F is a primitive operation of type I → I. □

Lemma 6.2 gives rise to the following reduction rules:

1. sup_{x} cons_{a}(Y) → cons_{a} (sup_{x} Y )

2. sup_{x} Y [x] → max (sup_{x} Y [cons_{L}(x)])
(sup_{x} Y [cons_{R}(x)])

3. sup_{x} Y → sup_{x} Y′ if Y → Y′.

Notice that these are the reduction rules for ∫ with ∫ and ⊕ replaced by sup and max respectively. We obtain the following similar results:

Lemma 6.4 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 = ⨆_{n≥0} sup^{(n)}f,

where the join is directed.

Lemma 6.5 For every natural number n,

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

Corollary 6.6 For every n there is a Real PCF program defining sup^{(n)}.

Lemma 6.7 If F : I → I is a closed computable term then every partial result produced by the program sup^{(n)}F is also produced by the program sup F.

Lemma 6.8 sup is a computable primitive operation.

Theorem 6.9 (Adequacy) Every term in Real PCF extended with sup 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.

7. A Recursive definition of integration

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

Let D = [[I → I] → I]. Then the second equation of Lemma 4.1 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 p : ℝ^{3} → ℝ by

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

Then, given a ≤ b, the map

r(x) = p(a, x, b)

is idempotent,

a ≤ r(x) ≤ b,

and

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

Define a function H : D → D by

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

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

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

where f̂ is defined as in Lemma 3.9.

Proof By induction on n. For the base case use the fact that f̂(⊥) = p(inf f, ⊥, sup f). □

Proposition 7.2 ∫ is the least fixed point of H.

Proof Immediate consequence of Lemmas 4.3 and 7.1. □

Corollary 7.3 The integration operator is definable in Real PCF extended with sup.

Proof We clearly have that

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

Therefore H is definable. □

8. Multiple 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 8.1 Let f : R^{n} → R be a map and a⃗ be an ndimensional 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 8.2 The multiple interval Riemann integral of a monotone map f : R^{n} → R on a hyper-cube a⃗ is defined by

∫a⃗ f = ⨆_{P⃗ ∈Pa⃗} ∑_{x⃗∈P⃗} f(x⃗)dx⃗. □

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

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

Theorem 8.3 (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:

∫_{(a,b)} f = ⨆_{P ×Q∈P(a,b)} ∑_{(x,y)∈P ×Q} f(x, y)d(x, y)
= ⨆_{P ∈Pa} ⨆_{Q∈Pb} ∑_{x∈P} ∑_{y∈Q} f(x, y)dxdy

= ⨆_{P ∈Pa} ∑_{x∈P} ( ⨆_{Q∈Pb} ∑_{y∈Q} f(x, y)dy) dx

= ∫_{(a)} λx ∫_{(b)} λyf(x, y). □

Corollary 8.4 For every n there is a program in Real PCF extended with either integration or sup 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. The equation of the above theorem can be read as a definition of a program for the case n + 1 from a program for the case n. By the adequacy theorems, these programs indeed compute multiple integrals of order n. □

This application of the adequacy theorems shows that adequacy is a powerful result. In fact, it allows us to derive correct programs from analytical results, in a representationindependent fashion. This is precisely the idea behind denotational semantics.

9. Universality of Real PCF extended with the supremum operator

Definition 9.1 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 [23]. Real PCF with no extensions is not universal, because ∃ is not definable [14]. If we extend Real PCF with ∃ and the computation rules given in loc. cit., then the adequacy property remains true. The following universality result is proved in [14]:

Theorem 9.2 Real PCF extended with ∃ is universal.

Corollary 9.3 Real PCF extended with ∃ is fully abstract.

The reader is referred to [23] for the definition of full abstraction.

Although Theorem 9.2 implies that sup is definable in Real PCF extended with ∃, we do not know a neat fixedpoint definition of sup.

Proposition 9.4 . 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 with D as a retract, in the sense that

r_{D} ∘ s_{D} = id_{D}

and s_{D} ∘ r_{D} is an idempotent on I with image isomorphic to D. 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. □

Corollary 9.5 Real PCF extended with sup is universal and hence fully abstract.

We do not know whether Real PCF extended with integration is universal. Moreover, we do not know whether integration is definable in Real PCF with no extensions.

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.

Remark 9.6 Notice that the section-retraction pairs defined in the proof of Proposition 9.4 are expressed in terms of sequential primitives only, and that the maximum operation on I represents the “parallel or” operation ∨ on T defined in [23], in the sense that the following diagram commutes:

I × I ⟶^{max} I
s_{T} ×s_{T} ↑  ↓^{r_{T}}
T × T ⟶_{∨} T

Acknowledgements

We would like to thank Peter Freyd for his suggestion about the recursive definition of the integration operator. 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” and “Foundational Structures in Computer Science”, 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. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, Oxford, 1994.

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

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

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

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

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

[7] 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, Moler Centre, Cambridge, 11-14 September 1995. IC Press.

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

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

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

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

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

[13] A. Edalat and M. Escardó. Integration in Real PCF. Available by ftp (theory.doc.ic.ac.uk:papers/Escardo/papers) and WWW (http://theory.doc.ic.ac.uk/∼mhe/), December 1995.

[14] M. Escardó. Real PCF extended with ∃ is universal. Available by anonymous ftp at theory. doc. ic. ac. uk: papers/ Escardo/ papers and also by WWW at http:// theory. doc. ic. ac. uk/ ∼mhe/ Imperial College, London.

[15] M. 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.

[16] M. Escardó. PCF extended with real numbers. Theoretical Computer Science, 162, July 1996.

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

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

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

[20] K.-I. Ko. Complexitity Theory of Real Functions. Birkhauser, Boston, 1991.

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

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

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

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

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

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

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

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