查看“︁Kirby-Paris Hydra”︁的源代码

'''Kirby-Paris Hydra(KP-Hydra)''' 是在一棵树上进行的单人游戏，需要很长时间才能终止。由此游戏导出的函数<math>\rm{Hydra(n)}</math>的增长率超过了[[皮亚诺公理体系]]可证明停机的一切递归函数。它与[[Beklemishev's Worm|Beklemishev's worm]]密切相关。

== 规则 ==
KP-Hydra 游戏的规则如下：

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

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

例如：设<math>n=3</math>，考虑这样的一棵树<math>(((()))(()(){\color{red}()}))</math>。

将红色的括号删除后，树的变化如下：<math>(((())){\color{blue}(()(){\color{red}()})})\rightarrow
(((())){\color{blue}(()())})\rightarrow
(((())){\color{blue}(()())}{\color{green}(()())}{\color{green}(()())}{\color{green}(()())})</math>

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

其证明概要如下：

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

* 只含根节点的树<math>()</math>对应0;
* 若树<math>T_1,T_2,\cdots,T_n</math>分别对应序数<math>H_1,H_2,\cdots,H_n</math>，则<math>(T_1T_2\cdots T_n)</math>对应<math>\omega^{H_1}+\omega^{H_2}+\cdots+\omega^{H_n}</math>。


例如，<math>(((()))(()()()))
=\omega^{\omega^{\omega^0}}+\omega^{\omega^0+\omega^0+\omega^0}
=\omega^\omega+\omega^3</math>。

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