BRICS RS-03-50 B. Lambov: A Two-Layer Approach to the Computability and Complexity of Real Numbers BRICS

Basic Research in Computer Science

A Two-Layer Approach to the Computability and Complexity of Real Numbers

Branimir Lambov

BRICS Report Series RS-03-50 ISSN 0909-0878 December 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, Branimir Lambov.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/03/50/

A two-layer approach to the computability and complexity of real functions

Branimir Lambov

BRICS^{∗}

Department of Computer Science University of Aarhus DK-8000 Aarhus C Denmark barnie@brics.dk December, 2003

AMS Classification: 03D65, 03D15, 68Q15, 68Q05, 03D80

Abstract

We present a new approach to computability of real numbers in which real functions have type-1 representations, which also includes the ability to reason about the complexity of real numbers and functions. We discuss how this allows efficient implementations of exact real numbers and also present a new real number system that is based on it.

1 Introduction

Most theoretical approaches to the computability of real functions rely on highertype computations, taking a description of a real number into a computation of another description. In practice, creating and maintaining such descriptions is a very complicated process, requiring extra storage along with time-consuming memory management tools such as garbage collection and, if not enough care is applied, also introducing external complexity that may even lead to changing the complexity class of the problem.

∗

Basic Research in Computer Science (www.brics.dk),

funded by the Danish National Research Foundation.

For example, to compute simply a ∗ a, where a is a real number described as some function computing its approximations, and ∗ is a type-2 function that computes multiplication on the reals, the straightforward implementation would require the computation of approximations to a twice. Then, an efficient implementation of a^{n} where n ∈ N using ∗, which on ground types would have complexity of operations O(log n), would inevitably end up being of complexity O(n), because every multiplication would require computing its arguments, leading to at least n requests to compute approximations to a.

The problem in this example can be circumvented by introducing approximation caching. Unfortunately, this leads to other issues and the process of circumventing problems can go on indefinitely.

This paper tries to address this problem from the roots, creating a firm theory on which implementations without such efficiency problems can be devised. The theory presented is a new model of computation, based on representing real functions as objects operating on partial approximations instead of proper real numbers. The novelty of this model is in the introduced second layer that adds the ability to reason about complexity, at the same time separating these concerns from the objects that carry out the computation. No other type-1 model so far has been able to define complexity, and ours manages to do it in a way that is compatible with existing complexity measures for computable analysis.

In the next section we will present the two-layer approach, prove its properties, and compare it to existing models. Following this, we will discuss the usefulness of the ideas presented, along with a short introduction to an actual implementation and the conclusions it allows us to draw. At the end we will take a look at the future plans for this research.

2 Model

2.1 Established notions

First we will introduce two widely accepted notions of computability on real numbers and functions on real numbers, which we will use to justify that the definitions in the model coincide with the established ones.

Let B be a computable base for R that contains the dyadic numbers, and B_{∞} = {x : x ∈ B ∧ x > 0} ∪ {∞} together with operations that respect ∞. To allow us to talk about feasibility, we will use lth(n) = ⌊log_{2} n⌋+1 in the exponents instead of simply n.

Let there exist computable and even poly-time encodings of the elements of B and B_{∞} and of the pairings B × B_{∞}. In some of the proofs we will also need certain basic properties of the encodings:

• a_{1} ≤ a_{2} ∧ b_{1} ≤ b_{2} < ∞ → ⟨(a_{1}, b_{1})⟩ ≤ ⟨(a_{2}, b_{2})⟩

• lth(⟨(a, b)⟩) is polynomial in max(lth(a), lth(b))

• there exists a function rat(n, 2^{d}) that selects a code for the rational number n2^{−d}, such that whenever a, b, c, d are positive integers, a ≤ c ∧ b ≤ d → rat(a, 2^{b}) ≤ rat(c, 2^{d})

• the absolute value operator on the rational codes is such that ⟨b⟩ ≤ ⟨|b|⟩ for any rational b

These properties are satisfied by e.g. the Cantor pairing and the encoding of rational numbers q as pairs (n, d), such that

q = (−1)^{n} \frac{⌊(n + 1)/2⌋}{d}.

Definition 2.1 A Cauchy function representation (CF-representation) of a real number α is a function a : N → B, such that ∀n ∈ N (|a(n) − α| < 2^{−lth(n)})

Definition 2.2 A Cauchy function representation of a partial function ϕ : R → R is a partial functional Φ : (N → B) × N → B, such that

∀α ∈ dom ϕ, ∀a − CF − representations of α

∀n ∈ N ((a, n) ∈ dom Φ ∧ |Φ(a, n) − ϕ(α)| < 2^{−lth(n)})

Definition 2.3 A real number or a real function is computable in a class C of computable functions, resp. functionals, iff there exists a representation in C for it in the sense of Definitions 2.1 or 2.2 respectively.

2.2 Partial approximation representations of real numbers

The inefficiency in these definitions comes from the higher type of the function object Φ in Definition 2.2. To alleviate this, we need to transfer the precision information to the type-0 level. Our approach to this is similar to the domain theoretic and the interval arithmetic ideas, and uses a basic object called a partial approximation.

Definition 2.4 A partial approximation to a real number α is a pair (v, e) of type B × B_{∞}, such that |v − α| < e. We will denote the class of partial approximations to α with A_{α}, and the class of partial approximations to any real with A_{R} = ∪_{α∈R}A_{α}. If a ∈ A_{R} we will use a_{v}, a_{e} to denote respectively the value and error in a.

Definition 2.5 A partial approximation representation, p.a.r., of a real number α is a function A : N → A_{α}, for which ∀k∃n((A(n))_{e} ≤ 2^{−k}).

If a real number is computable, then it certainly has a computable p.a.r.: if B is a representation of α, then λn.(B(n), 2^{−lth(n)}) is one of its p.a.r.’s. Conversely, if a is a p.a.r. of α, then λk.A(μn[A(n)_{e} ≤ 2^{−lth(k)}])_{v} is a valid CF-representation for it.

This equivalence does not hold for restrictions of the notion of computablily. Moreover, it is possible to define all computable reals using p.a.r.’s in subrecursive classes such as primitive recursive, elementary or poly-time functions. For a proof of this, see [12].

In order to be able to speak about different complexity classes of real numbers, a similar equivalence must be available. This gives rise to the following definitions and equivalence property:

Definition 2.6 A modulus for a p.a.r. A of a real number α is a function m : N → N, such that for all k, (A(m(k)))_{e} ≤ 2^{−lth(k)}.

Definition 2.7 We will say that a real number is p.a.r.-computable in a given class C of computable functions, if there exist both a p.a.r. and a modulus for it in C.

Theorem 2.8 A real number is computable in a subrecursive class C that contains the poly-time functions and is closed under composition if and only if it is p.a.r.- computable in C.

Proof Take A := λn.(B(n), 2^{−lth(n)}) and m := λn.n, or for the other direction B := λk.A(m(k)). •

On the level of feasible functions, poly-time p.a.r. computability coincides with Ko’s notion of poly-time computable real numbers [8] (Ko speaks about numbers given in unary notation, which is equivalent to the lth(n) parameter used in our definitions).

2.3 Partial approximation representations of real functions

For real functions, we want to have objects that operate on partial approximations instead of the full representations. They will have to convert approximations to an input to approximations to the result of the application of the function, and also we need to require that the precision of the output approximations gets arbitrarily good as the precision of the input increases. In other words, Definition 2.9 A partial approximation representation of a partial function ϕ : R → R is a partial function F : A_{R} → A_{R}, such that for any choice of α ∈ dom ϕ and a partial approximation representation A of α, λn.F (A(n)) is a partial approximation representation of ϕ(α).

Remark 2.10 This definition implies a ∈ A_{α} → F (a) ∈ A_{ϕ(α)} for α ∈ dom ϕ, because for any p.a.r. A we can create B(n) := \overline{sg}(n) · a + sg(n) · A(n − 1), which is another p.a.r. of α that has B(0) = a, hence F (a) has to be a partial approximation to ϕ(α).

Remark 2.11 Unlike the domain theoretic and interval arithmetic approaches, we do not require the image interval to be described accurately. Our requirement is only that we are able to provide a superset of it, and this superset gets smaller as the input interval gets smaller.

2.3.1 Computability

We have severely restricted the information to which the function object has access; nevertheless, the following theorem proves we have not restricted the class of real functions that are computable:

Theorem 2.12 A partial function ϕ : R → R is computable iff it has a computable p.a.r.

Proof (←) If we have a p.a.r. F of a function ϕ, and α ∈ dom ϕ, then the functional

Φ(B, n) := let (m = μp [(F (B(p), 2^{−lth(p)})_{e} ≤ 2^{−lth(n)}]) in F (B(m), 2^{−lth(m)})

is total in n for any CF-representation B of α since from Definitions 2.9 and 2.5 the minimization will always stop, and Definition 2.4 together with Remark 2.10 ensures |Φ(a, n) − ϕ(α)| < 2^{−lth(n)}. •

Proof (→) We have a fixed α ∈ dom ϕ, and a CF-representation Φ for ϕ.

For any a ∈ A_{α} with a_{e} < 1, we can effectively find the largest natural number m with the property 2^{m}a_{e} < 1. If a_{e} ≥ 1, we take m = 0. Define the function

b := λn.2^{−lth(n)}⌊2^{lth(n)}a_{v} + 1/2⌋.  (1)

For 0 ≤ lth(n) < m we have that

|b(n) − α| ≤ |a_{v} − α| + 2^{−(lth(n)+1)} ≤ 2^{−m} + 2^{−(lth(n)+1)} ≤ 2^{−lth(n)}

Using the fact that exceptions are computable and that given the code of a computable functional Φ, we can construct a parallel one Φ^{†} that honors a new exception x, we can effectively create a function

b⌈m := λn. \{ \begin{matrix}b(n), & if n < m \\ raise x, & otherwise \end{matrix}

and then define

Φ^{‡}(B, n) := try Φ^{†}(B⌈m, n) + 1 catch(x) 0.  (2)

(i.e. Φ^{‡} will return Φ(b, n) + 1 if b restricted to length m was sufficient to compute it, and 0 otherwise)

We will now prove that the function

F (a) := \{ \begin{matrix}(0, ∞), & if l = 0 \\ (Φ^{‡}(b, l − 1) − 1, 2^{−lth(l−1)}), & otherwise \end{matrix}

for

l = μp ≤ m [Φ^{‡}(b, p) = 0]  (3)

is the required p.a.r. of ϕ. To do this, we need to prove that G = λn.F (A(n)) is a p.a.r. of ϕ(α) for any p.a.r. A of α.

The first condition, F (a) ∈ A_{ϕ(α)} for any a ∈ A_{α}, follows from the requirement for Φ and the fact that there is a CF-representation for α that starts with b(0), b(1), …, b(m − 1).

For the second condition, we need to prove the existence of 2^{−k}-approximations to ϕ(α) among G(n) for any k. The sequence defined by

c := λn.2^{−lth(n)}⌊2^{lth(n)}α + 1/2⌋

is a proper CF-name for α. If α is not a dyadic number, then for an arbitrary n, |α − c(n)| < 2^{−(n+1)}. There exists q depending on n, such that |α − c(n)| ≤ 2^{−n}(1/2 − 2^{−(q−n)}), and for all partial approximations a with a_{e} < 2^{−q} we have 2^{i}|a_{v} − c(i)| < 1/2 for all 0 ≤ i ≤ n. But this implies that the sequence obtained by (1) coincides with c on the first n + 1 elements.

Now, since Φ would look at finitely many elements of c to produce a value with any precision 2^{−k}, using that count in the procedure described above, we can come up with a q supplying a long enough sequence. Combining this with a requirement that the minimization (3) reaches the target precision, we have (F (a))_{e} ≤ 2^{−k} for all a’s with a_{e} ≤ 2^{− max(q,k)}, and since A has arbitrarily close approximations, this can be satisfied for a = A(n) for some n.

If α is a dyadic number, i.e. ∃c, n(c(n) = α), then there are only finitely many variations of b that can exists, because they have to coincide after the first n + 1 positions. Then there exists a maximum m for the number of lookups Φ can make to any of these b’s in order to get a 2^{−k}-precise result. Hence a_{e} ≤ 2^{− max(m,k)} suffices to get the required precision for F (a). •

Remark 2.13 The proof of the existence of arbitrarily close approximations in this form is ineffective. There also exists a construction for which this proof can be carried out effectively (by making the choice of b non-deterministic and using a representation generated by A instead of c). The presented proof, however, is much more easily adjustable to the restricted conditions in which it will be used later.

As well as in the case of real numbers, this equivalence does not hold for subclasses of the type-2 computable functions. To define all computable functions, it suffices to use severely restricted type-1 computability subclasses:

Theorem 2.14 A partial real function is computable iff it has a p.a.r. in any subrecursive class C that contains the poly-time functions.

Proof (→) It suffices to change the definition of Φ^{−} to a version bounded in execution time:

Φ^{−}(B, n) := try Φ^{m}(B⌈m, n) + 1 catch(x) 0.

where by Φ^{m} we denote Φ^{†} executed for m steps, which is a basic feasible functional (BFF, [1]).

Since m is of the order of lth(a) for the encoding of a it is possible to do all required steps in time polynomial to lth(a). The proof of the existence of good appoximations can be carried out here as well, the only difference being the need to satisfy a condition in the form a_{e} ≤ 2^{−max(q,k,s)} for s being the number of steps it takes for Φ to complete its evaluation on b of length q.

The p.a.r. is type-1 basic feasible, therefore it is poly-time by a known property of the BFF [2]. •

Proof (←) Follows from the previous theorem. •

2.3.2 Type-2 complexity

Again taking the p.a.r. of a real function we lose all complexity information about that function. To talk about complexity classes again, we define Definition 2.15 A modulus for a p.a.r. F of a partial real function ϕ is a partial functional M : (A_{R} → A_{R}) × (N → N) × N ⟶ N, such that for all α ∈ dom ϕ, p.a.r. A of α, moduli m for A,

∀k((F (A(M(A, m, k))))_{e} ≤ 2^{−lth(k)}).  (4)

Note that even though the actual function object is a type-1 object, we now introduce a type-2 operation to characterize it. However, the strength comes from the separation of these two objects: to have a e.g. a feasible real function you do not have to have a feasible type-2 object, but only need to prove that it exists. Moreover, if a CF-representation of a function needs extra information to be in a certain class (e.g. division needs evidence that the denominator is non-zero to be primitive recursive), it will in general only be needed for the modulus.

Definition 2.16 We will say that a real function is p.a.r.-computable in a given class C of computable type-2 functionals, if both a computable p.a.r. and its modulus can be found in C.

Theorem 2.17 If a function is p.a.r.-computable in a given class C that contains BFF and is closed under functional substitution, then it is computable in the same class.

Proof For ϕ : R → R, α ∈ dom ϕ, F - p.a.r. of ϕ, M-modulus for F, and B - CF-representation of α, take

Φ(B, n) := (F (A(M(A, λp.p, n))))_{v}

where

A := λp.(B(p), 2^{−lth(p)}).

A is a p.a.r. for α with a modulus λp.p, and hence from M being a modulus to F, we have |Φ(B, n) − ϕ(α)| < 2^{−lth(n)}. Φ is a basic feasible functional relative to F and M, therefore it is in C. •

Theorem 2.18 If a partial function ϕ : R → R is computable, then it is p.a.r.- computable.

Proof We’ve already proved in Theorem 2.12 that there exists a computable p.a.r. to every computable real function. If it is F, then

M(A, m, n) := μp[F (A(p))_{e} ≤ 2^{−lth(n)}]

is a modulus for F. •

This modulus does not even use the modulus for the real number. This is true, because in the presence of minimization brute force search makes the moduli redundant.

This is not the case for restricted complexity classes. To prove the equivalence between p.a.r. and CF-computability on some of them, we will introduce the notion of majorizability.

Definition 2.19 (W.A. Howard [5]) We define x^{∗} maj_{ρ} x for a finite type ρ by induction on the type:

x^{∗} maj_{0} x := x^{∗} ≥ x,
x^{∗} maj_{τ→ρ} x := ∀y^{∗}, y (y^{∗} maj_{τ} y → x^{∗}y^{∗} maj_{ρ} xy) .

We will say that a subrecursive class C is majorizable, if for every function f in C there exists f^{∗} ∈ C with f^{∗} maj f, where the majorization operator is of the appropriate type.

Lemma 2.20 The class of primitive recursive type-2 functionals is majorizable.

This lemma is a corollary to the fact that the class of the primitive recursive functionals of finite type (PR^{ω}) are majorizeable, proved in e.g. [9]. We will use the same technique to prove

Lemma 2.21 The class of basic feasible type-2 functionals (BFF) is majorizable.

which is a corollary to

Lemma 2.22 The class of basic feasible functionals of finite type (BFF^{ω}) is majorizable.

Proof We will use the fact [2] that every functional in BFF^{ω} can be written as a term which only contains constants 0_{ρ}, variables y_{ρ}, poly-time functions, Σ_{δ,ρ,τ}, Π_{ρ,τ} and bounded recursion on notation R_{bn}:

R_{bn}(x, y, g, h) = \{ \begin{matrix}y, & if x = 0 \\ min (g(x, R_{bn}(⌊x/2⌋, y, g, h), h(x)) , & otherwise \end{matrix}

0_{ρ}, y_{ρ}, Σ_{δ,ρ,τ} and Π_{ρ,τ} are self majorizable, and for every poly-time function f there exists a polynomial p with coefficients among the natural numbers, such that f(\underline{x}) ≤ 2^{p(lth(\underline{x}))} = f^{∗}(\underline{x}). But the right hand side of this inequality is a polytime function for which ∀\underline{x}∀\underline{y} ≤ \underline{x} (f^{∗}(\underline{x}) ≥ f^{∗}(\underline{y}) ≥ f(\underline{y})), i.e. f^{∗} maj_{1} f. Define

R_{bn}^{∗}(x, y, g, h) := h(x)

If x^{∗}, y^{∗} ≥ x, y, g^{∗} maj_{0→0→0} g and h^{∗} maj_{1} h

R_{bn}^{∗}(x^{∗}, y^{∗}, g^{∗}, h^{∗}) = h^{∗}(x^{∗}) ≥ h(x) ≥ R_{bn}(x, y, g, h),

which proves R_{bn}^{∗} maj_{0→0→(0→0→0)→1→0} R_{bn}.

Now the result follows from the fact that t^{∗} maj_{ρ→τ} t ∧ s^{∗} maj_{ρ} s implies t^{∗}s^{∗} maj_{τ} ts. •

To prove equivalence of the computability classes, we will also need

Lemma 2.23 The following variation of the function b created in (1) along the course of evaluation of F on a p.a.r. A

b(n) := rat(⌊2^{lth(n)}a_{v} + 1/2⌋, 2^{lth(n)})  (5)

can be majorized on partial approximations with error ≤ 1 if there is an upper bound for the absolute value of the real number described by A.

Proof Let a_{0} be a rational number such that |α| < a_{0} for α being the real described by A. Then for any partial approximation a with a_{e} ≤ 1 we have |a_{v}| < a_{0} + 1 and therefore by the properties of the encoding

b^{∗}(n) = rat(1 + ⌊2^{lth(n)}a_{0} + 1/2⌋, 2^{lth(n)}) ≥ b(n)

and also, since when n is increased both the numerator and denominator will not decrease, we have ∀k ≤ n(b^{∗}(n) ≥ b^{∗}(k) ≥ b(k)), which means b^{∗} maj_{1} b. •

Theorem 2.24 If a partial real function is computable in a majorizeable class of type-2 functionals that contains BFF and is closed under functional substitution, then it is p.a.r.-computable in that class.

Proof We will use the proof of Theorem 2.12, substituting the definition of b with (5). All operations used in the generation of F can be done without leaving the class of Φ. Hence F is in the class. We now need to find a modulus for it.

In the class of Φ there exists a functional Ψ that does exactly the same job as Φ, but instead of returning the approximation it gives the largest k to which B was applied. Since the class contains this functional and is majorizable, it also contains a majorizer Ψ^{∗} for it. The modulus for A gives us means to bound the absolute value of the real number described by it, therefore, with the previous lemma, in our class there is a function J that given A and m computes b^{∗} which majorizes all functions b generated by good partial approximations.

Hence Ψ^{∗}(b^{∗}, n) ≥ Ψ(b, n) for all good b’s, in particular for the one (call it b_{0}) generated by a_{0} = A(m(Ψ^{∗}(b^{∗}, n))), which means Φ^{†}(b_{0}, n) will not raise an exception, and F (a_{0}) will give a result with the required precision.

Hence M(A, m, n) = m(Ψ^{∗}(J(A, m), n)) is a modulus for F. • 2.3.3 Real number complexity

In the previous subsection we found correspondence between complexities in this model and type-2 complexity. As this is not the complexity measure normally used for real functions, we also define notions which are more closely related to the latter by defining type-1 moduli on closed subsets of the domain:

Definition 2.25 A uniform modulus on [a, b] ⊆ dom ϕ of a p.a.r. F of a real function ϕ is a function U : N → N, such that

∀α ∈ [a, b]∀A − p.a.r. of α∀k∀n(A(n)_{e} ≤ U(k) → (F (A(n)))_{e} ≤ 2^{−lth(k)})

Theorem 2.26 A partial real function ϕ is computable in a majorizable class of type-2 functionals on [a, b] ⊆ dom ϕ if and only if it has a p.a.r. and a uniform modulus in the same class.

Proof (→) Use a and b to find an upper bound for the absolute value of α, then apply the same reasoning as in the previous proof. •

Proof (←) M(A, m, k) = m(U(k)) is a modulus for all A’s representing reals in the interval, thus ϕ is p.a.r.-computable in the class. •

With this definition we’re back at the type-1 level, and we also have a few important equivalences:

Corollary 2.27 A partial real function ϕ is primitive recursive on [a, b] ⊆ dom ϕ iff it has a primitive recursive p.a.r. and a primitive recursive uniform modulus on [a, b].

Corollary 2.28 A partial real function ϕ is BFF-computable on [a, b] ⊆ dom ϕ iff it has a poly-time p.a.r. and a poly-time uniform modulus on [a, b].

And this combined with the following theorem gives us equivalence with the established notion for feasible real functions.

Theorem 2.29 A partial real function is poly-time computable on [a, b] in the sense of Ko’s defintion [8] iff it is BFF-computable.

Proof A function is poly-time computable in Ko’s sense iff there is an oracle Turing machine computing it in the dyadic representation, which runs in time polynomial to the precision given in 1^{k} notation.

Type-2 complexity theory says a functional is in BFF if and only if there exists an oracle Turing machine computing it running in time which is a second-order polynomial in the length of the inputs [6]. There exist representations of any real number that satisfy lth(B(k)) ≤ p(lth(k)) for a polynomial p (using dyadic representations cut after the lth(k)’th digit), and therefore a second order polynomial in lth(k), lth(B) does not give more power than simply a polynomial in lth(k). •

3 An example: reciprocal of a real number

The task in this section will be to define a suitable p.a.r. of the function 1/α : R → R and to inspect its properties.

Theorem 3.1 The poly-time function F defined as

F (a) = \{ \begin{matrix}(\frac{1}{a_{v}} , \frac{a_{e}}{|a_{v}|(|a_{v}|−a_{e})}), & if a_{e} < |a_{v}| \\ (0, ∞), & if a_{e} ≥ |a_{v}| \end{matrix}  (6)

is a p.a.r. of the reciprocal function on the reals.

Proof Given a fixed α ≠ 0, if a is a partial approximation to α with a_{e} < a_{v}, then

|\frac{1}{α} − \frac{1}{a}| ≤ \frac{1}{|a_{v}| − a_{e}} − \frac{1}{|a_{v}|} ≤ \frac{|a_{v}| − (|a_{v}| − a_{e})}{|a_{v}|(|a_{v}| − a_{e})} = \frac{a_{e}}{|a_{v}|(|a_{v}| − a_{e})},

which means F converts partial approximations to α into partial approximations to 1/α. If a_{0} is a positive rational number smaller than |α|, then to get (F (a))_{e} ≤ ε, it is enough to supply a partial approximation with a_{e} < a_{0}^{2}ε/2 (assuming a_{0}, ε ≤ 1). •

It is a well known fact that the reciprocal function on the reals is not even primitive recursively computable. However, it is poly-time computable on every closed interval that does not contain 0. How does this translate to our framework?

Having a closed interval that does not contain 0 is equivalent to having witness information for the strict positivity of |α|. But this extra information is enough to allow us to define

M(a_{0}, A, m, k) = m(a_{0}#a_{0}#k#2)
U(a_{0}, k) = 2^{−2(lth(a_{0}))^{2}lth(k)}

(with # being the smash function, x#y = 2^{lth(x)lth(y)}) which are, respectively, a modulus for F and an uniform modulus for F on the full real line. Therefore, F defined in (6) is uniformly linear in the error of the approximation a_{e} and the requested precision k, and quadratic in the value of the appriximation a_{v} and the witness a_{0} on the full real interval.

Note that we needed the witness only to define and prove a property of the p.a.r. The representation itself is not changed by whether it can be found or not.

4 Comparison with existing models

During the presentation of the model we made some parallels with existing models. But how do we actually compare to them?

This model has the same expressive power as the type-2 model for Computable Analisys as treated for example in [13]. Important restricted variations and subclasses of the computable real functions and numbers can also be defined in our model with straightforward and natural definitions. The advantage of this model is in its ability to avoid type-2 objects and still define the same notions.

In the setting of feasible real functions, this model complies with Ko’s definition of poly-time computability [8]. Moreover, our model is able to define feasibility of a representation of a function avoiding the use of an oracle Turing machine and any type-2 object at all using the definition of the uniform modulus for a p.a.r. It is an interesting question how it can be extended to arbitrary Polish spaces and what definition of feasibility on type-2 in general that would give.

The core of this model, the p.a.r.’s without their moduli, is very similar to the domain theoretic model for computability on the real line of Edalat and Sünderhauf [3]. The most significant distinction of ours is in dropping the requirement of accurately describing the image interval of a function’s application on an interval, along with freedom to omit unnecessary data from the sequences describing real numbers. With this relaxation we have been able to define complexity in this model using restricted classes of real numbers and functions.

Interval arithmetic [7], can be used as the building block for the p.a.r. computations. However, our model does not have the requirement for accurate descriptions of the image intervals, and it sometimes proves more efficient to use more rough approximation schemes instead of the elaborate algorithms used in interval arithmetic.

5 Implementation

We will try to answer what advantages this model gives for implementations and if there are any visible shortcomings. Most of the discussion in this part is based on observations made during the creation of RealLib^{1}, an exact real number package based on the two-layer model.

We call this model a type-1 model, but when a user writes and executes a program that computes with reals, and ends up with one or several real numbers as results, their program will still be at least a type-2 program in order to successfully extract any property they need (instead of getting it if the current approximation allows). Where is the difference then?

1available at http://www.brics.dk/∼barnie/RealLib

With the classical ideas, implementations (such as XR ^{2}, ICReals [4], CORE [14]) first run through the program to build expression trees, lambda terms or other descriptions of the computation, and start computing only after a request for a property is given, using these descriptions.

But isn’t the description of the computation already present? That is, isn’t the program code already enough description? Why do we need to build those huge expression trees or lambda terms when we already have a compact description of the solution in an elaborate language such as C++ or ML? Moreover, why should we lose the information that the programmer or compiler is giving us about common subexpressions (leading to efficiency problems like the one in the introduction), objects’ lifetime and locality (leading to higher memory requirements and need for garbage collection) and preferred ordering of the operations (leading to complications to both former points)?

In order to put this to practice, one has to be able to allow real functions defined on the type-1 level, and a means to do this is exactly what this model provides. Before that, an implementation of this idea was used in iRRAM [11], but the ideas in this work could not be placed in any theoretical framework. One of our model’s objectives was to fit this system.

The problem with a type-1 implementation is that it is not very easy for the user to request specific properties of a real number which is the result of a computation, and the behaviour of the implementations regarding control flow make it very complicated to display or present the information gathered. iRRAM, which has previously proved to be the most efficient implementation of real number arithmetic, displays both the pros and cons of the type-1 approach. Our implementation, RealLib, aims to diminish the ill effects and preserve the advantages.

This is done by a hybrid approach in which the user’s access to real numbers is implemented on two levels, one that works on partial approximations in order to compute, and one that deals with descriptions of expression terms as full type-1 information of real numbers and is meant to extract and use the results. The execution at the type-2 level is normal and programming for it is easy. There is no history maintenance at the partial approximation level and the computations are fast, especially in the lower precisions where history maintenance dominates the execution time in type-2 approaches. It is the programmer’s choice which part of their application should run where; the system is offering redundant definitions of primitives on both levels to make this possible, and the translation from one to the other is easy, amounting simply to a change of the variable types in many cases.

2K. Briggs, http://members.lycos.co.uk/keithmbriggs/XR.html

More detailed information about our implementation can be found in [10].

6 Future work

A generalization of the ideas presented here to non-locally compact Polish spaces is to be derived. It will possibly provide insight to the still open problem of the right notion of feasibility in the general type-2 setting.

Another interesting question is how to allow intensionality in the type-1 model. The constructions we use in this paper to prove equivalences all break down in the case of intensionally-defined real functions. Figuring whether and how this can be accommodated would help to avoid holes in the domains of functions such as atan2, sqrt on complex numbers, etc.

The implementation has room for improvements, most importantly aiming at making the switch from machine-type precision to exact real numbers as painless as possible, i.e. to reduce the performance gap even more, well beyond the boundary that history maintenance sets for type-2-only systems.

References

[1] Cook, S., Urquart, A., Functional interpretations of feasibly constructive arithmetic. Ann. Pure Applied Logic 63, pp. 103-200 (1993).

[2] Cook, Stephen A. Computability and complexity of higher type functions. Logic from computer science (Berkeley, CA, 1989), 51–72, Math. Sci. Res. Inst. Publ., 21, Springer, New York, 1992.

[3] Edalat, Abbas; Sünderhauf, Philipp A domain-theoretic approach to computability on the real line. Theoret. Comput. Sci. 210 (1999), no. 1, 73–98.

[4] Edalat, A., Exact Real Number Computation Using Linear Fractional Transformations,

    available at http://www.doc.ic.ac.uk/∼ae/exact-computation/

[5] Howard, W.A., Hereditarily majorizable functionals of finite type. In: Troelstra (ed.), Metamathematical investigation of intuitionistic arithmetic and analysis, pp. 454-461. Springer LNM 344 (1973).

[6] Kapron, B. M.; Cook, S. A. A new characterization of type-2 feasibility. SIAM J. Comput. 25 (1996), no. 1, 117–132.

[7] Kearfott, Baker R. Interval computations: introduction, uses, and resources. Euromath Bull. 2 (1996), no. 1, 95–112.

[8] Ko, K.-I., Complexity theory of real functions. Birkhäuser, Boston-Basel-Berlin, x+309 pp., 1991.

[9] Kohlenbach, U. Lecture Notes: Proof Interpretations and the Computational Content of Proofs (Draft, May 2003, ii+165pp.)

available at http://www.brics.dk/∼kohlenb/

[10] Lambov, B., A two-layer approach to the computability and complexity of real functions. Computability and complexity in analysis (Cincinnati, 2003), 279–302, Informatik Berichte, 302 (8/2003), Fernuniversität Hagen, 2003

see also http://www.brics.dk/∼barnie/

[11] Müller, N., The iRRAM: Exact arithmetic in C++. in Computability and complexity in analysis. (Swansea, 2000). Lecture Notes in Computer Science, 2064. Springer-Verlag, Berlin, 2001. viii+395 pp.

see also http://www.informatik.uni-trier.de/iRRAM/

[12] Skordev, D., Characterization of the computable real numbers by means of primitive recursive functions. Computability and complexity in analysis (Swansea, 2000), 296–309, Lecture Notes in Computer Science, 2064, Springer-Verlag, Berlin, 2001. viii+395 pp.

[13] Weihrauch, K., Computable Analysis. Springer, Berlin 2000.

[14] Yap, Chee, Towards Exact Geometric Computation. Computational Geometry : Theory and application, 3-23, Sep 1997.

see also http://www.cs.nyu.edu/exact/core/

Recent BRICS Report Series Publications

RS-03-50 Branimir Lambov. A Two-Layer Approach to the Computability and Complexity of Real Numbers. December 2003. 16 pp.

RS-03-49 Marius Mikucionis, Kim G. Larsen, and Brian Nielsen. Online On-the-Fly Testing of Real-time Systems. December 2003. 14 pp.

RS-03-48 Kim G. Larsen, Ulrik Larsen, Brian Nielsen, Arne Skou, and Andrzej Wasowski. Danfoss EKC Trial Project Deliverables. December 2003. 53 pp.

RS-03-47 Hans Hüttel and Jiří Srba. Recursive Ping-Pong Protocols. December 2003. To appear in the proceedings of 2004 IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS Workshop on Issues in the Theory of Security (WITS’04).

RS-03-46 Philipp Gerhardy. The Role of Quantifier Alternations in Cut Elimination. December 2003. 10 pp. Extends paper appearing in Baaz and Makowsky, editors, European Association for Computer Science Logic: 17th International Workshop, CSL ’03 Proceedings, LNCS 2803, 2003, pages 212-225.

RS-03-45 Peter Bro Miltersen, Jaikumar Radhakrishnan, and Ingo Wegener. On converting CNF to DNF. December 2003. 11 pp. A preliminary version appeared in Rovan and Vojtás, editors, Mathematical Foundations of Computer Science: 28th International Symposium, MFCS ’03 Proceedings, LNCS 2747, 2003, pages 612–621.

RS-03-44 Anna Gál and Peter Bro Miltersen. The Cell Probe Complexity of Succinct Data Structures. December 2003. 17 pp. An early version of this paper appeared in Baeten, Lenstra, Parrow and Woeginger, editors, 30th International Colloquium on Automata, Languages, and Programming, ICALP ’03 Proceedings, LNCS 2719, 2003, pages 332–344.

RS-03-43 Mikkel Nygaard and Glynn Winskel. Domain Theory for Concurrency. December 2003. 45 pp. To appear in a Theoretical Computer Science special issue on Domain Theory.