×

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
PDF BibTeX XML Cite