On the computational properties of basic mathematical notions

TL;DR

This paper explores the computational aspects of fundamental mathematical concepts related to real functions and sets, revealing two large classes of computationally equivalent operations grounded in classical theorems.

Contribution

It introduces a higher-order computability framework for basic mathematical notions and develops a lambda-calculus formulation accommodating partial objects.

Findings

Identifies two large classes of computationally equivalent operations

Develops a lambda-calculus formulation for S1-S9 schemes

Shows the importance of partial objects in higher-order computability

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 $\lambda$-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$.