Foundation of Computer (Algebra) ANALYSIS Systems: Semantics, Logic, Programming, Verification

We propose a semantics of operating on real numbers that is sound, Turing-complete, and practical. It modifies the intuitive but super-recursive Blum-Shub-Smale model (formalizing Computer ALGEBRA Systems), to coincide in power with the realistic but inconvenient Type-2 Turing machine underlying Computable Analysis: reconciling both as foundation to a Computer ANALYSIS System. Several examples illustrate the elegance of rigorous numerical coding in this framework, formalized as a simple imperative programming language ERC with denotational semantics for REALIZING a real function $f$: arguments $x$ are given as exact real numbers, while values $y=f(x)$ suffice to be returned approximately up to absolute error $2^p$ with respect to an additionally given integer parameter $p\to-\infty$. Real comparison (necessarily) becomes partial, possibly 'returning' the lazy Kleenean value UNKNOWN (subtly different from $\bot$ for classically undefined expressions like 1/0). This asserts closure under composition, and in fact 'Turing-completeness over the reals': All and only functions computable in the sense of Computable Analysis can be realized in ERC. Programs thus operate on a many-sorted structure involving real numbers and integers, the latter connected via the 'error' embedding $Z\ni p\mapsto 2^p\in R$, whose first-order theory is proven decidable and model-complete. This logic serves for formally specifying and formally verifying correctness of ERC programs.