Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Ordinals and recursively defined functions on the reals

Gabriel Nivasch, Lior Shiboli

TL;DR

The paper develops the notion of ordinal decreasing functions to certify termination of a broad class of recursive real-valued algorithms, generalizing the classic fusible-number computations. It proves that, for ordinal decreasing $f,g_1,\dots,g_k,s$ with positive outputs, the recursive scheme $M(x)$ halts for all $x\in\mathbb{R}$ and is ordinal decreasing, with explicit bounds on the ordinal height $o(M)$ based on $k$ and the heights of the component functions. The bounds use the finite Veblen hierarchy via $\varphi_{k-1}$ and, in the simpler case, epsilon-number towers, anchoring the results in transfinite ordinal analysis. This work extends prior results on fusible numbers and their generalizations, connects termination to real induction and WPO machinery, and provides a unified framework for proving termination of related recursive constructions with quantitative ordinal-height bounds. The findings have implications for understanding the logical strength required to prove termination and for constructing termination-guaranteed recursive definitions in analysis and computation.

Abstract

We determine sufficient conditions under which certain recursively defined functions are well defined for all real inputs. Given a function $f:\mathbb R\to\mathbb R$, call a decreasing sequence $x_1>x_2>x_3>\cdots$ "$f$-bad" if $f(x_1)>f(x_2)>f(x_3)>\cdots$, and call the function $f$ "ordinal decreasing" if there exist no infinite $f$-bad sequences. We prove the following result: Given ordinal decreasing functions $f,g_1,\ldots,g_k,s$ that are everywhere larger than $0$, define the recursive algorithm "$M(x)$: if $x<0$ return $f(x)$, else return $g_1(-M(x-g_2(-M(x-\cdots-g_k(-M(x-s(x)))\cdots))))$". Then $M(x)$ halts and is ordinal decreasing for all $x \in \mathbb{R}$. The recursive algorithms $M$ and $M_n$ previously studied in the context of fusible numbers by Ericskon et al. (2022) and Bufetov et al. (2024), respectively, are special cases of this scheme. Moreover, given an ordinal decreasing function $f$, denote by $o(f)$ the ordinal height of the root of the tree of $f$-bad sequences. Then we prove that, for $k\ge 2$, the function $M(x)$ defined by the above algorithm satisfies $o(M)\le\varphi_{k-1}(γ+o(s)+1)$, where $γ$ is the smallest ordinal such that $\max\{o(s),o(f),o(g_1), \ldots, o(g_k)\} <\varphi_{k-1}(γ)$.

Ordinals and recursively defined functions on the reals

TL;DR

The paper develops the notion of ordinal decreasing functions to certify termination of a broad class of recursive real-valued algorithms, generalizing the classic fusible-number computations. It proves that, for ordinal decreasing with positive outputs, the recursive scheme halts for all and is ordinal decreasing, with explicit bounds on the ordinal height based on and the heights of the component functions. The bounds use the finite Veblen hierarchy via and, in the simpler case, epsilon-number towers, anchoring the results in transfinite ordinal analysis. This work extends prior results on fusible numbers and their generalizations, connects termination to real induction and WPO machinery, and provides a unified framework for proving termination of related recursive constructions with quantitative ordinal-height bounds. The findings have implications for understanding the logical strength required to prove termination and for constructing termination-guaranteed recursive definitions in analysis and computation.

Abstract

We determine sufficient conditions under which certain recursively defined functions are well defined for all real inputs. Given a function , call a decreasing sequence "-bad" if , and call the function "ordinal decreasing" if there exist no infinite -bad sequences. We prove the following result: Given ordinal decreasing functions that are everywhere larger than , define the recursive algorithm ": if return , else return ". Then halts and is ordinal decreasing for all . The recursive algorithms and previously studied in the context of fusible numbers by Ericskon et al. (2022) and Bufetov et al. (2024), respectively, are special cases of this scheme. Moreover, given an ordinal decreasing function , denote by the ordinal height of the root of the tree of -bad sequences. Then we prove that, for , the function defined by the above algorithm satisfies , where is the smallest ordinal such that .
Paper Structure (15 sections, 20 theorems, 30 equations, 4 figures)

This paper contains 15 sections, 20 theorems, 30 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Ordinal decreasing functions
  3. Our results
  4. Background
  5. Fusible numbers
  6. Real induction
  7. Veblen functions
  8. Natural sum and product of ordinals
  9. Well partial orders
  10. Proof of Theorem \ref{['M halts']}
  11. Proof of Theorem \ref{['thm_o_bound']}
  12. The case $k=1$
  13. The case $k=2$
  14. The general case
  15. Acknowledgements.

Key Result

Theorem 1.5

Consider the recursive algorithm: where the functions $s(x)$, $f(x)$ and $g_i(x)$ for all $i$ are all ordinal decreasing and larger than 0 for every $x$ in the appropriate ranges: $(-\infty, 0)$ for $f,g_i$, and $[0,\infty)$ for $s$. Then $M(x)$ halts and is ordinal decreasing for all $x \in \mathbb{R}$.

Figures (4)

  • Figure 1: The graph of $M(x)$ up to $x=2.1$.
  • Figure 2: Examples of ordinal decreasing functions.
  • Figure 3: Construction of the tame fusible numbers in ENX, which motivate their algorithm $M$.
  • Figure 4: An ordinal decreasing function (solid line) induces a partition of the $x$-axis into a transfinite number of intervals (dotted lines).

Theorems & Definitions (43)

  • Definition 1.1
  • Definition 1.2
  • Definition 1.3
  • Definition 1.4
  • Theorem 1.5
  • Theorem 1.6
  • Lemma 2.1
  • proof
  • Lemma 3.1
  • proof
  • ...and 33 more