Email Gateway (Jun 01 2026 at 14:14): Email Gateway (Jun 01 2026 at 14:14):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce yet another contribution by Ramos et al.:
The Busy Beaver Function
Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto de Queiroz
Abstract
This development formalizes the Busy Beaver upper-bound principle and its computability consequences for AFP Turing machines. The abstract layer works over machine models with finite size classes and unique exact halting times: it defines the time Busy Beaver function and proves that any total upper bound for this function decides zero-input halting. A generic computability interface then yields the usual noncomputability consequence from the absence of computable fixed-input halting deciders; its eventual-domination theorem is proved under an explicit compilation-witness assumption. The development then connects the abstract theory to AFP's Universal Turing Machine formalization by defining exact numeric-result halting times, a finite size measure for Turing programs, a concrete Turing-machine Busy Beaver function, a code-indexed Busy Beaver function whose upper bounds decide AFP's special halting problem (K_1), and a strengthened program/input-pair Busy Beaver function whose upper bounds decide AFP's two-argument halting problem (H_1). Using AFP's Turing-computability interface, it further proves that no upper-bound-induced (H_1) decider set has a Turing-computable total characteristic function, with a specialization to the decider induced by the concrete pair-indexed Busy Beaver function itself.
https://isa-afp.org/entries/Busy_Beaver.html
Last updated: Jun 12 2026 at 04:13 UTC