zbMATH — the first resource for mathematics

Effective real dynamics. (English) Zbl 0823.03034
Crossley, John N. (ed.) et al., Logical methods. In honor of Anil Nerode’s 60th birthday. Basel: BirkhĂ¤user. Prog. Comput. Sci. Appl. Log. 12, 162-177 (1993).
Traditional constructive mathematics is based on the notion of a constructive real number. Informally, a real number $$x$$ is constructive if there is an algorithm that enables us to compute this number with arbitrary accuracy. In mathematical terms, there exists an algorithm $$\mathcal U$$ that for every integer $$n$$, generates a rational number $$r_ n$$ such that $$| x- r_ n|\leq 2^{- n}$$. Similarly, a constructive function is defined as a function whose values can be computed with any given accuracy.
It is known that in several real-life problems, a real number that is uniquely defined by some system of equations, is not constructive. For example, a fixed point of a constructive mapping or a limit of a constructive monotonic sequence are not necessarily constructive (the first example of such a sequence was proven by Specker in early 50s). Such “limits” are often physically meaningful: e.g., the largest temperature $$T$$ for which superconductivity is possible may not be constructive, but it is a limit (as $$n\to \infty$$) of the monotonic sequence of temperatures that have been achieved by time $$n$$. Another example: if we do not know whether a universal statement $$\forall n A(n)$$ for decidable $$A$$ is true or not, then we cannot say that its truth value is constructive; it is, however, a limit of the monotonic sequence of (computable) truth values of $$\forall n_{\leq N} A(n)$$.
In traditional constructive mathematics, the question is usually whether the real number is constructive or not. Suppose it is not. In many cases when a number $$x$$ is not constructive, but can be represented as a limit of a constructive monotonic sequence $$x_ n$$, there exist reasonably efficient numerical methods that “compute” this number as $$x_ N$$ for some large $$N$$ determined by some heuristic stopping criterion (of course, these heuristic methods are often way off). If $$x$$ cannot be represented as such a limit, then, in some cases, it can be represented as a double limit, e.g., as $$\inf_ n \sup_ m x_{mn}$$, so we can run two iterative procedures to compute $$x$$. Such computations are efficiently used, e.g., in computer graphics to generate Mandelbrot sets, Julia sets, etc. The more complicated this representation, the more difficult it is to compute $$x$$. Therefore, it makes sense to classify constructive and non-constructive real numbers based on the complexity of their representation in terms of constructive numbers (and eventually, in terms of rational numbers).
Such a hierarchical classification is well known for sets of natural numbers: sets $$A$$ from the class $$\Sigma^ 0_ 1$$ can be described as the sets for which $$n\in A$$ can be represented in the form $$\exists m P(m, n)$$ with decidabl for sets from $$\Pi^ 0_ 1$$, the corresponding representation is $$\forall m P(m, n)$$, etc. This idea can be applied to real numbers if we identify a real number $$x$$ with its lower Dedekind set, i.e., with the set of all rational numbers that are $$< x$$. Correspondingly, if we take $$p< x$$, $$q$$ with rational $$p$$ and $$q$$ as a basic statement, we can classify sets of real numbers.
Constructive mathematics has produced a few computability results and lots of negative counterexamples (that something is not computable). The main goal of this paper is, for dynamical systems, to describe the exact levels of computability: e.g., what level of computability of a fixed point corresponds to a given level of computability of a function. Typical examples of results: if a mapping $$F$$ is recursive, and $$a$$ is an attracting point of $$F$$, then $$a$$ is recursive; for every $$\Sigma^ 0_ 2$$ set $$A$$ of integers, there exists a recursive real function $$F$$ for which the set of all attracting points is exactly $$A$$, etc.
For the entire collection see [Zbl 0810.00003].

MSC:
 03F60 Constructive and recursive analysis 03F65 Other constructive mathematics 47H10 Fixed-point theorems