Kirby-Paris Hydra

Kirby-Paris Hydra(KP-Hydra) 是在一棵树上进行的单人游戏，需要很长时间才能终止。由此游戏导出的函数 $H y d r a (n)$ 的增长率超过了皮亚诺公理体系可证明停机的一切递归函数。它与Beklemishev's worm密切相关。

规则

KP-Hydra 游戏的规则如下：

游戏从一棵有根树T开始；
第n回合，选择T的一个叶子节点a，设a的父节点为b，依次执行以下操作(称为一次砍树)：
1. 删除a；
2. 若b不是根节点，取以b为根的子树T'，将其复制n次，连接到b的父节点上。
如果某步操作后只剩下根节点，游戏结束。

我们可以用括号表示树：每一对括号表示一个节点，最外层的括号表示根节点，每个括号内层的括号表示它的子节点。

例如：设 $n = 3$ ，考虑这样的一棵树 $(((())) (() () ()))$ 。

将红色的括号删除后，树的变化如下： $(((())) (() () ())) \to (((())) (() ())) \to (((())) (() ()) (() ()) (() ()) (() ()))$

Kirby 和 Paris 证明了以下定理：无论初始的树T怎样选取，KP-Hydra 游戏总会在有限步内终止。

其证明概要如下：

我们给每一个非空树对应一个序数：

只含根节点的树 $()$ 对应0;
若树 $T_{1}, T_{2}, \dots, T_{n}$ 分别对应序数 $H_{1}, H_{2}, \dots, H_{n}$ ，则 $(T_{1} T_{2} \dots T_{n})$ 对应 $ω^{H_{1}} + ω^{H_{2}} + \dots + ω^{H_{n}}$ 。

例如， $(((())) (() () ())) = ω^{ω^{ω^{0}}} + ω^{ω^{0} + ω^{0} + ω^{0}} = ω^{ω} + ω^{3}$ 。

我们证明：砍树操作后，树对应的序数严格减小。