On the computational properties of basic mathematical notions
Dag Normann, Sam Sanders
TL;DR
The paper investigates the computational properties of core mathematical notions for $\mathbb{R}\to\mathbb{R}$ and subsets of $\mathbb{R}$ within Kleene's higher-order framework, introducing two robust computation clusters: the $\Omega$-cluster and the $\Omega_1$-cluster. It develops a $\lambda$-calculus formulation that accommodates partial objects, enabling precise analysis of countably based partial functionals and their computability. The authors establish extensive computational equivalences for functionals arising from BV-, regulated-, and AC-related notions, revealing deep connections between mainstream theorems (e.g., Jordan decomposition, FTC, arc length) and higher-order computation. A key finding is that $\Omega$ and $\Omega_1$ are fundamentally partial and not equivalent to any total functional, while both clusters capture a wide array of functionals from BV, Sobolev, and Caccioppoli settings, clarifying the landscape of higher-order computability and its ties to classical analysis.
Abstract
We investigate the computational properties of basic mathematical notions pertaining to $\mathbb{R}\rightarrow \mathbb{R}$-functions and subsets of $\mathbb{R}$, like finiteness, countability, (absolute) continuity, bounded variation, suprema, and regularity. We work in higher-order computability theory based on Kleene's S1-S9 schemes. We show that the aforementioned italicised properties give rise to two huge and robust classes of computationally equivalent operations, the latter based on well-known theorems from the mainstream mathematics literature. As part of this endeavour, we develop an equivalent $λ$-calculus formulation of S1-S9 that accommodates partial objects. We show that the latter are essential to our enterprise via the study of countably based and partial functionals of type $3$.