General Recursive Function

General recursive functions (GRFs), also called µ-recursive functions or partial recursive functions, are the collection of partial functions ${\mathbb{\mathbb{N}}}^k\rightharpoonup \mathbb{\mathbb{N}}$ that are computable. This definition is equivalent using any Turing complete system of computation. See Wikipedia:general recursive function for background.

Historically it was defined as the smallest class of partial functions ${\mathbb{\mathbb{N}}}^k\rightharpoonup \mathbb{\mathbb{N}}$ that is closed under composition, recursion, and minimization, and includes zero, successor, and all projections (see formal definitions below). In the rest of this article, this is the formulation that we focus on exclusively. In this way, it can be considered to be a Turing complete model of computation. In fact, it is one of the oldest Turing complete models, first formalized by Kurt Gödel and Jacques Herbrand in 1933, 3 years before λ-calculus and Turing machines.

BBµ(n) is a Busy Beaver function for GRFs:$$BB\mu (n)=\max \{f()|f\in {\text{GRF}}_0,|f|=n\}$$

where $f\in GR{F}_k$ means that $f:{\mathbb{\mathbb{N}}}^k\rightharpoonup \mathbb{\mathbb{N}}$ is a k-ary GRF and $|f|$ is the "structural size" of f (defined below). In other words, it is the largest number computable via a 0-ary function (a constant) with a limited "program" size. It is more akin to the traditional Sigma score for a Turing machine rather than the Step function in the sense that it maximizes over the produced value, not the number of steps needed to reach that value.

Definition

Primitive Recursive Functions

TODO

Minimization

TODO

Macros

In order to improve readability we define the following macros:

	Macro	arity	Definition	Size	Function
Plus constant	$Plus[n]$	1	$\begin{array}{lcl}Plus[1]& :=& S\\ Plus[n+1]& :=& C(S,Plus[n])\end{array}$	$2n-1$	$\lambda x.x+n$
Constant	$K^k[n]$	k	$\begin{array}{lcl}{K}^k[0]& :=& Z^k\\ K^k[n]& :=& C(Plus[n],Z^k)\end{array}$	$2n+1$	$\lambda x_1\dots x_k.n$
Iteration	$Rep[f,n]$	1	$Rep[f,n]:=R(K^0[n],C(f,P_2^2))$	$|f|+2n+4$	$\lambda x.f^x(n)$
Ackermann iteration	$Ack[n,f]$	1	$\begin{array}{lcl}Ack[0,f]& :=& f\\ Ack[n+1,f]& :=& Rep[Ack[n,f],1]\end{array}$	$6n+|f|$
Knuth base 2 up-arrows	$Knuth2[n]$	1	$\begin{array}{lcl}Knuth2[0]& :=& Rep[Plus[2],0]\\ Knuth2[n+1]& :=& Rep[Knuth2[n],1]\end{array}$	$6n+7$	$\lambda x.2{\uparrow }^{n}x$
Polygonal	$Poly[n]$	1	$Poly[n]:=R(Z^0,R(S,C(Plus[n],P_2^3)))$	$2n+5$	$\lambda x.\frac{n}{2}x(x-1)+x$
	$Tri$	1	$Tri:=Poly[1]$	$7$	$\lambda x.\frac{x(x+1)}{2}$
	$Square$	1	$Square:=Poly[2]$	$9$	$\lambda x.x^2$

Champions

n	BBµ(n)	Champion	Champion Found	Holdouts Proven
2k+1	≥ k	$K^0[k]$	Trivial
15	≥ 7	$K^0[7]$	Trivial
17	≥ 10	$C(Tri,K^0[4])$	Shawn Ligocki 9 Dec 2025
19	≥ 16	$C(Square,K^0[4])$	Shawn Ligocki 9 Dec 2025
21	≥ 25	$C(Square,K^0[5])$	Shawn Ligocki 9 Dec 2025
23	≥ 36	$C(Square,K^0[6])$	Shawn Ligocki 9 Dec 2025
25	≥ 256	$C(Rep[Square,2],K^0[3])$	Shawn Ligocki 9 Dec 2025
27	$\ge 2^{16}$	$C(Rep[Square,2],K^0[4])$	Shawn Ligocki 9 Dec 2025
29	$\ge 2\uparrow \uparrow 5$	$C(Rep[Rep[Square,2],0],K^0[3])$	Shawn Ligocki 9 Dec 2025
31	$\ge 2\uparrow \uparrow 7$	$C(Rep[Rep[Square,2],0],K^0[4])$	Shawn Ligocki 9 Dec 2025
33	$\ge 2\uparrow \uparrow 9$	$C(Rep[Rep[Square,2],0],K^0[5])$	Shawn Ligocki 9 Dec 2025
35	$\ge 2\uparrow \uparrow \uparrow 4$	$C(Knuth2[3],K^0[4])$	Shawn Ligocki 8 Dec 2025
37	$\ge 2\uparrow \uparrow \uparrow 5$	$C(Knuth2[3],K^0[5])$	Shawn Ligocki 8 Dec 2025
39	$\ge 2\uparrow \uparrow \uparrow 6$	$C(Knuth2[3],K^0[6])$	Shawn Ligocki 8 Dec 2025
6k+17	$\ge 2{\uparrow }^{k}4$	$C(Knuth2[k],K^0[4])$	Shawn Ligocki 8 Dec 2025
6k+19	$\ge 2{\uparrow }^{k}5$	$C(Knuth2[k],K^0[5])$	Shawn Ligocki 8 Dec 2025
6k+21	$\ge 2{\uparrow }^{k}6$	$C(Knuth2[k],K^0[6])$	Shawn Ligocki 8 Dec 2025