next up previous contents
Next: Functional approaches Up: Introduction to EXACT NUMERICAL Previous: Order normalization

   
Inequality tests in real number computation

In all effective approaches to exact real number computation via concrete representations, the (in)equality relations are undecidable. This is not surprising, because an infinite amount of information must be checked in order to decide that two given numbers are equal. In particular, this means that it is not possible to obtain exact algorithms from finite-precision algorithms by simply changing the underlying representation of numbers. The reason is that (in)equality tests are the basic ingredient for branching and looping.

Nevertheless, many definitions by cases consisting of inequalities, such as

90#90

do produce computable functions--but they don't produce algorithms, because such functions cannot be computed by first evaluating the condition and then computing the corresponding branch. As an application of the order-normalization Theorem 9.1, we obtain.

Theorem 10.1   There is a computable partial function

91#91

such that

92#92

with domain of definition 93#93

Notice that, given this domain of definition, an equivalent specification is

94#94


95#95

Although the operator is partial, it can be used to define total functions. For example,

96#96

which shows that 97#97 is indeed computable. If 98#98 are computable functions that agree at a computable number x0, then the function 99#99 defined by

100#100

is also computable, because

101#101

Also, some partial functions such as

102#102

can be defined by

103#103

and hence are computable.

Notice that the case-analysis operator is a continuous map, defined on a subset of [-1,1]4, which cannot be extended to a continuous map on any larger subset. In other words, the points (x,t,y,z) with x = t but 104#104 are singularities of the case-analysis operator. This means that the partial character of the case-analysis operator is due to topological rather than recursion-theoretic reasons.


next up previous contents
Next: Functional approaches Up: Introduction to EXACT NUMERICAL Previous: Order normalization
Martin Escardo
2000-10-02