Beklemishev's worms

Beklemishev's worms are a construction described by Lev D. Beklemishev (Russian: Беклемишев Лев Дмитриевич) that result in a one-player game that takes a long time to terminate.Beklemishev, L. (2006). The Worm principle. In Z. Chatzidakis, P. Koepke, & W. Pohlers (Eds.), Logic Colloquium '02 (Lecture Notes in Logic, pp. 75-95). Cambridge: Cambridge University Press. 
It is closely related to Kirby-Paris hydras.
== Description ==
A worm is simply a list of nonnegative integers \([W_0, W_1, \ldots, W_n]\). In a game Beklemishev calls "the Worm battle," our hero Cedric is presented with an arbitrary worm \(W\), and his task is to reduce it to an empty list. On turn \(m\) of the game, the worm is altered by the function \(\text{next}(W, m)\):
* If \(W_n = 0\), then \(\text{next}(W, m) = [W_0, W_1, \ldots, W_{n-1}]\). (That is, Cedric chops off the worm's head.)
* Otherwise, define \(k = \max_{i < n} W_i < W_n\). We define the good part of the sequence to be \(g = [W_0, \ldots, W_k]\) and the bad part to be \(b = [W_{k+1}, \ldots, W_{n-1}, W_n - 1]\). (Note that \(W_n\) is decremented by 1.) If \(k\) is nonexistent, define \(g\) to be an empty list and \(b = [W_0, \ldots, W_{n-1}, W_n - 1]\). We then define \(\text{next}(W, m) = g + b + b + \cdots + b + b\) with \(m+1\) copies of \(b\). (Here + means sequence concatenation, so for example [0, 3, 2] + [1, 4, 5] = [0, 3, 2, 1, 4, 5].)
Beklemishev proved, in a theorem he calls the Worm principle, that Cedric can always defeat the worm regardless of the initial value of \(W\). He further showed that this fact is unprovable in Peano arithmetic.
The Worm's expansion rule is almost identical to Primitive Sequence System's expansion system.
From this, we can create a specific fast-growing function. Define \(\text{Worm}(n)\) to be the number of steps required to defeat a worm starting with \(W = [n]\). Then \(\text{Worm}(n)\) is a function that dominates all functions provably recursive in Peano arithmetic, giving the function a growth rate comparable to \(f_{\varepsilon_0}(n)\).
== Examples ==
A Japanese Googology Wiki user koteitan created a simulator for Beklemishev's worms (cf. #Computer programs). Here are examples of small inputs:
* Start: [1]
* Step 1: [0,0]
* Step 2: [0]
* Step 3: []
So \(\text{Worm}(1) = 3\).
* Start: [2]
* Step 1: [1,1]
* Step 2: [1,0,1,0,1,0]
* Step 3: [1,0,1,0,1]
* Step 4: [1,0,1,0,0,0,0,0,0]
* Step 10: [1,0,1]
* Step 11: [\(1,0^{13}\)]
* Step 24: [1]
* Step 25: [\(0^{26}\)]
* Step 51: []
So \(\text{Worm}(2) = 51\).
== Computer programs ==
* koteitan, Beklemishev's Worm Simulator in JavaScript, Github page.
== Variants ==
* Primitive sequence system
* Goucher's T(n) function (External link)
== Sources ==
== See also ==
ja:ベクレミシェフの虫
ru:Червь Беклемишева
Category:Functions
Category:Eponymous functions