ベクレミシェフの虫

ベクレミシェフの虫 (Beklemishev's worms) は、 Lev D. Beklemishev （ロシア語: Беклемишев Лев Дмитриевич）が記述した終了までに長い時間がかかる1人ゲームである^{[リンク切れ]}。ヒドラゲームにたいへんよく似ている。

説明

虫は非負整数のリストである \([W_0, W_1, \ldots, W_n]\)。ベクレミシェフが「虫の闘い」と呼ぶゲームは、我々のヒーローであるセドリックが、任意の虫 \(W\) とともに登場し、その虫を空のリストにするゲームである。ゲームの \(m\) 番目のステージでは、次の関数 \(\text{next}(W, m)\) によって虫が変化する。

• \(W_n = 0\) であれば、 \(\text{next}(W, m) = [W_0, W_1, \ldots, W_{n-1}]\) となる。（すなわち、セドリックが虫の頭を切り落とす。）
• そうでなければ、数列の良い部分 g と悪い部分 b を、次のように決める。\(i<n, W_i<W_n\) をみたすiが存在するかどうかを考える。
  • i が存在しないときは \(g=[ ], b=[W_0, \ldots, W_{n−1},W_n −1]\) とする。
  • i が存在するときは \(k = \max \{i; i<n, W_i<W_n \}\) とおき、\(g=[W_0,\ldots,W_k], b= [W_{k+1},\ldots,W_n -1]\) とする（\(W_n\) が 1 減っていることに注意）。

そして、 \(\text{next}(W, m) = g + b + b + \cdots + b + b\) （\(m+1\) 個の \(b\)）とする。ここで、 + は数列の連結であり、たとえば [0, 3, 2] + [1, 4, 5] = [0, 3, 2, 1, 4, 5] である。

ベクレミシェフは、彼が虫の法則 (Worm principle) と名付けた定理を証明した。それは、セドリックは \(W\) の初期値に関わらず、常に虫に勝つことができる、というものである。さらに、この事実がペアノ算術では証明不可能であることを証明した。

このことから、増加速度が速い関数を作ることができる。\(\text{Worm}(n)\) を、 \(W = [n]\) から始めて虫に勝つために必要なステップ数とする。すると、 \(\text{Worm}(n)\) は、いかなるペアノ算術による可証全域関数も支配する。この関数の増加速度は \(f_{\varepsilon_0}(n)\) 程度である。

この独立性は可証性論理に基づく\(\varepsilon_0\)の順序数表記と基本列に密接に関係している．

例

• Start: [1]
• Step 1: [0,0]
• Step 2: [0]
• Step 3: []

すなわち \(\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¹³]
• Step 24: [1]
• Step 25: [0²⁶]
• Step 51: []

すなわち \(\text{Worm}(2) = 51\)

計算プログラム

• koteitan, Beklemishev's Worm Simulator in JavaScript, Github page.

亜種

• 原始数列システム
• GoucherのT関数