七树合一定理 [seven-trees-in-one]
七树合一定理 [seven-trees-in-one]
$\gdef\spaces#1{~ #1 ~}$ 二叉树意味树的每个结点最多两个子树. 其类型由两个构造器归纳给出 叶结点构造器 换言之, 二叉树可定义为某种满足 $B=1+B^2$ 的 (代数) 结构. 回顾 $6$ 次分圆多项式 $$ \Phi_6(x) \spaces= x^2-x+1 $$ 其复根 $\zeta_6$, $\zeta^{-1}_6$ 是所谓的 $6$ 次本原单位根. $\gdef\N{\mathbf{N}}$
$\gdef\Z{\mathbf{Z}}$ 记 $B$ 是二叉树类型, 则存在一个 “极精确的双射” $B \xrightarrow{\sim} B^7$. 显然并非所有 $\zeta_6$ 满足的等式都能提升到 $B$ 之间的同构, 如 $B^6 \ncong 1$. 自然的问题是, 哪些等式能提升到同构? 这个问题由下面的 Fiore–Leinster 定理 回答. $\gdef\N{\mathbf{N}}$
$\gdef\Z{\mathbf{Z}}$ 设 $f,g_1,g_2 \in \N[x]$, 其中 $f$ 有非零常数项且 $\deg f \ge 2$. 若 $f(x) - x$ 整除非常值的 $g_1-g_2$ (在 $\Z[x]$ 中), 则在 $\N[x]/(x=f(x))$ 中, $g_1(x)=g_2(x)$. 特别的, 取 $f(x)=1+x^2$, Fiore–Leinster 定理 表明, 若在 $\N[x]/(x=1+x^2)$ 中成立 $f(x) = g(x)$, 则存在 “极精确的双射” $f(B) \cong g(B)$. 在 $\N[x]/(x=1+x^2)$ 中可以演绎得到 $x=x^7$ 但无法给出 $1=x^6$. 对于前者 $x^7-x = (x^2-x+1)(x^5+x^4-x^2-x) = 0$. 再看 $x^4 + x^2 + 1 = (x^2 + x + 1)(x^2 - x + 1)$, 这给出 $B^4+B^2+1 \ncong 0$, $B^4+B^2+B+1=B$. 这套想法亦可应用于其他树结构, 如有根平面树, 其每个结点有 $0$, $1$ 或 $2$ 个子结点, 即 $T \cong 1+T+T^2$. 由 Fiore–Leinster 定理, 存在 “极精确的双射” $T \cong T^5$.Definition 1. 二叉树类型 [binary-tree]
inductive Tree α
| leaf : Tree α
| node : α → Tree α → Tree α → Tree α
leaf 用于构造出一棵空树, 空树作为某个结点的所有子结点时, 该结点正是叶结点. 相应的, 二叉树的值存储在非叶结点中. 每个 (非空, 无标记) 二叉树类型的值要么是一个单结点 $\{\text{pt}\} = 1$, 要么等价于二叉树的有序配对 $B \times B = B^2$. 即 $B \xrightarrow{\sim} \{\text{pt}\} \sqcup B^2$.
Theorem 2. Blass–Lawvere 定理 [blass-lawvere]
Theorem. Fiore–Leinster [fiore-leinster]