CPDT非正式习题中nat_tree无穷树数据类型定义疑问

关于nat_tree定义的解释 #

你给出的归纳定义本身完全符合习题要求，产生误解的核心原因是对Node构造子的参数类型理解有误：

• Node的参数是nat -> nat_tree类型，本质是以自然数为下标的无穷序列，每一个自然数k都对应唯一的子树，刚好满足「每个内部节点有可数无穷个子节点」的要求。你误以为该定义下每个树只有一个叶子，是错误把这个函数类型当成了单个子树：你可以构造任意的映射，比如Node (fun k => Leaf k)就代表一个内部节点，它的第k个子节点就是值为k的叶子，仅这一个节点就包含可数无穷个叶子，完全符合树的结构，不是列表。
• 列表每个节点仅存在唯一的后继子节点，而该定义下的内部节点可以通过任意自然数下标访问任意子节点，属于标准的ω-分支无穷树定义，也是形式化验证领域定义这类无穷分支树的常用写法。

对应的increment函数可以按照如下逻辑实现，刚好满足所有叶子节点数值加1的需求：

Fixpoint increment (nt : nat_tree) : nat_tree :=
  match nt with
  | Leaf n => Leaf (S n)
  | Node childs => Node (fun k => increment (childs k))
  end

内容的提问来源于stack exchange，提问作者Andrey