查看“︁Dropping Hydra”︁的源代码

Dropping Hydra 是 Hypcos 提出的序数记号，使用了 [[Dropping]] 模式。

=== 定义 ===
该符号是一个三色有序树 '''T'''，附加两个正整数作为其“数值参数”。在符号 '''T'''[x, y] 中，红色是根节点的特殊颜色，而白色和黑色用于其他节点。

首先，红根树的数量少于白根树的数量，而白根树的数量又少于黑根树的数量。然后，在所有白根树中，只有白根的树是最小的，而在所有黑根树中，只有黑根的树是最小的。要比较树 '''A''' 和树 '''B'''，遵循以下步骤：

# 假设 <math>A_1,A_2,\cdots,A_k</math> 是通过删除 '''A''' 的根而从 '''A''' 分离的树。<math>B_1,B_2,\cdots,B_l</math> 是通过删除 '''B''' 的根而从 '''B''' 分离的树。
# 令 <math>m(A)=\min\{i\in\{1,2,\cdots,k\}|\forall j\in\{1,2,\cdots,k\}(A_i\geqslant A_j)\}</math>，且 <math>m(B)=\min\{i\in\{1,2,\cdots,l\}|\forall j\in\{1,2,\cdots,l\}(B_i\geqslant B_j)\}</math>。
# 若 <math>A_{m(A)}>B_{m(B)}</math>，则 '''A''' > '''B'''；若 <math>A_{m(A)}<B_{m(B)}</math>，则 '''A''' < '''B'''；若 <math>A_{m(A)}=B_{m(B)}</math>，则按照以下步骤操作。
# 从树 '''A''' 中删除 <math>A_{m(A)}</math>，得到树 '''C'''。从树 '''B''' 中删除 <math>B_{m(B)}</math>，得到树 '''D'''。
# 如果 '''C''' > '''D'''，则 '''A''' > '''B'''；如果 '''C''' < '''D'''，则 '''A''' < '''B'''；如果 '''C''' = '''D'''，则 '''A''' = '''B'''。

根据这些规则，'''T'''[x, y] 将返回一个正整数。

* 如果 '''T''' 是一棵仅根树，则 '''T'''[x, y] = y + 1
* 如果 '''T''' 最右边的叶子节点 c 为白色，且 c 有父节点 b，则：
*# '''T<sub>1</sub>''' 中以 a 为根的子树为 <math>(A_1 A_2 \cdots A_k B)</math>，其中 B 是 '''T<sub>1</sub>''' 中以 b 为根的子树
*# 树 '''T<sub>2</sub>''' 是通过将 '''T<sub>1</sub>''' 中的 <math>(A_1 A_2 \cdots A_k B)</math> 变为 <math>(A_1 A_2 \cdots A_k BB\cdots B)</math>（其中 y 个 '''B''' 为元素）得到的
*# '''T'''[x, y] = '''T<sub>2</sub>'''[x, y]
* 如果 T 最右边的叶子节点 c 为黑色，则：
*# 令节点 c<sub>0</sub> = c<sub>i+1</sub> 为 c<sub>i</sub> 的父节点，直到根节点 c<sub>r</sub>
*# 令树 C<sub>i</sub> 为 '''T''' 的子树，根节点为 c<sub>i</sub>
*# 令 j(0) = 0
*# 重复上述步骤 x 次，n 从 1 到 x
*## 令 <math>j(n)=\min\{i|C_i<C_{j(n-1)}\land i>j(n-1)\}</math>
*## 若 j(1) = r，则：
*### 通过将 C<sub>r−1</sub> 替换为唯一子节点为 C<sub>r−1</sub> 的白色节点，可从 '''T''' 获得树 '''T<sub>1</sub>'''
*### '''T'''[x, y] = '''T<sub>1</sub>'''[x, y]
*## 如果 n > 1，则树 B<sub>n</sub> 可通过将 C<sub>j(n−1)</sub> 中的 C<sub>j(n−2)</sub> 替换为 C<sub>j(n−1)</sub> 得到
*## 如果 n > 1 且 C<sub>j</sub>(n) < B<sub>n</sub>，则
*### 令 <math>k(n)=\max\{i|C_i<C_{j(n-2)}\land i>j(n)\}</math>
*### 树 '''A'''(n) 可通过将 C<sub>j(n−1)</sub> 中的 C<sub>j(n−2)</sub> 替换为 C<sub>k(n)</sub> 得到
*### 将 '''T''' 中的 C<sub>k(n)</sub> 替换为 '''A'''(n)，得到树 '''T<sub>2</sub>'''(n)
*### '''T'''[x, y] = '''T<sub>2</sub>'''(n)[x, y
*## 如果 n = 1 或 C<sub>j</sub>(n) ≥ B<sub>n</sub>，则继续重复
*# 令树 S<sub>0</sub> 为白色仅根树，S<sub>i+1</sub> 是由 C<sub>j(x)</sub> 中用 S<sub>i</sub> 替换 C<sub>j(x−1)</sub> 得到，直到 S<sub>y</sub>
*# 树 '''T<sub>3</sub>''' 是由 '''T''' 中用 S<sub>y</sub> 替换 C<sub>j(x)</sub> 得到
*# '''T'''[x, y] = '''T<sub>3</sub>'''[x, y]

仅根的情况构成了 FGH 的零情况；白 1 和白 3 构成了 FGH 的后继情况；白 1 和白 2 表示白节点树模拟了康托范式。因此，仅根的情况和白情况构成了 FGH，直到 ε<sub>0</sub>，并且它们与 x 无关。黑实际上有 x + 1 个可能的出口，其中一个出口位于步骤黑 4.2.2，x ''−'' 1 个出口位于步骤黑 4.4.4，还有一个出口位于步骤黑 7。在黑中，步骤黑 1 到黑 3 只是准备。步骤黑 4 是 x 次 dropping，因此 x（第一个数值参数）表示我们应该在这里落多少次 dropping。步骤黑 4.1 是实 dropping。每次下降操作后（除了第一次从黑叶子节点下降到白根子树），我们都需要检查下降的结果是否“足够大”。<math>C_{j(n)}</math>的定义小于 <math>C_{j(n-1)}</math>，但只有当它大于“去掉 <math>C_{j(n-2)}</math> 后的 <math>C_{j(n-1)}</math>”时，我们才能进行下一次 dropping 操作。如果 dropping 后的 <math>C_{j(n)}</math>不够“大”，则需要执行步骤黑 4.4。步骤黑 4.4.2 和黑 4.4.3 将<math>C_{j(n-1)}</math>和<math>C_{j(n-2)}</math>之间的部分“插入”到<math>C_{k(n)}</math>，因此这是“加法规则”。步骤黑 4.2 也是一个特殊的“加法规则”。如果 x dropping 完成，且没有遇到步骤黑 4.2 或黑 4.4，我们将进入步骤黑 5 和黑 6。它们将 <math>C_{j(x)}</math> 替换为<math>C_{j(x)}</math>和<math>C_{j(x-1)}</math>之间的 y 个块，并在顶部放置一片白叶，因此这就是“扩展规则”。

为了创建序数符号，使用了白色和黑色节点，但没有使用红色根。公式定义为：

# w(0) 是一个公式
# b(0) 是一个公式
# 如果<math>a1, a2, . . . an</math>是公式，则<math>w (a1 + a2 . . . + an)</math> 是一个公式
# 如果<math>a1, a2, . . . an</math>是公式，则<math>b (a1 + a2 . . . + an)</math>是一个公式

此外，加序公式定义为：

# w(0) 和 b(0) 是加序公式
# 如果<math>a1, a2, . . . an</math>是加序公式，且<math>a1 \geq a2 \geq . . . \geq an</math>，则<math>w (a1 + a2 . . . + an)</math>和 <math>b (a1 + a2 . . . + an)</math>是和序的。

我们需要对如下所示的公式进行比较，其中<math>a1, a2, . . . an</math>以及<math>c1, c2, . . . cn</math> 是和序的。

# <math>w(0) < w (a1 + a2 . . . + an) < b(0) < b (c1 + c2 . . . + cn)</math>
# 如果 <math>a1 > c1</math>，则 <math>w (a1 + a2 . . . + an) > w (c1 + c2 . . . + cn)</math>，且 <math>b (a1 + a2 . . . + an) > b (c1 + c2 . . . + cn)</math>
# 如果 <math>a1 < c1</math>，则 <math>w (a1 + a2 . . . + an) < w (c1 + c2 . . . + cn)</math>，且 <math>b (a1 + a2 . . . + an) < b (c1 + c2 . . . + cn)</math>
# 如果<math>a1 = c1</math>，则
## 如果 <math>w (a2 + a3 . . . + an) > w (c2 + c3 . . . + cn)</math>，则 <math>w (a1 + a2 . . . + an) > w (c1 + c2 . . . + cn)</math>，且 <math>b (a1 + a2 . . . + an) > b (c1 + c2 . . . + cn)</math>
## 如果 <math>w (a2 + a3 . . . + an) < w (c2 + c3 . . . + cn)</math>，则<math>w (a1 + a2 . . . + an) < w (c1 + c2 . . . + cn)</math>，且<math>b (a1 + a2 . . . + an) < b (c1 + c2 . . . + cn)</math>
## 若 <math>w (a2 + a3 . . . + an) = w (c2 + c3 . . . + cn)</math>，则<math>w (a1 + a2 . . . + an) = w (c1 + c2 . . . + cn)</math>，且 <math>b (a1 + a2 . . . + an) = b (c1 + c2 . . . + cn)</math>

这些不是“循环”定义，因为深度为 0 的公式（即 w(0) 和 b(0)）可以直接定义为和序；然后可以进行深度 ≥ 1 之间的比较，进而确定哪种深度为 1 的公式是和序的；然后与深度 ≥ 2 进行比较，依此类推。原序数定义为<math>a1 + a2 . . . + an</math>，其中<math>a1, a2 . . . an</math>是求和公式，<math>a1 \geq a2 \geq \cdots \geq an</math>。

{{默认排序:序数记号}}
[[分类:记号]]