自然数的初始代数

Question

我正在尝试使用自然数的基本情况来确保我理解初始代数和变形概念，但我肯定遗漏了一些东西（而且我的 Haskell 语法可能一团糟）。

稍后编辑

我认为我的问题主要与定义 NatF (Fix NatF) 和 Fix NatF 之间同构的函数 Fx / unFix 有关。我的理解是Fix NatF是N（自然数的集合），即Nat = Zero | Succ Nat.

Fx具体是怎么定义的？这是正确的吗？

Fx ZeroF = Zero
Fx (SuccF ZeroF) = Succ (Fx ZeroF) = Succ (Zero)

如果是这样，为什么这与 1 + N -> N 对 [0, succ][ 计算的初始代数不同？ =68=]?

---

原版Post

我知道对于自然数我们有函子 F(U) = 1 + U 和初始代数 F(U) -> U 其中 unit 转到 0 并且 n 转到 succ( n) = n + 1。对于另一个由函数 h 求值的代数，变形 cata 将是 cata(n) = h ⁿ(单位).

所以可以把函子写成data NatF a = ZeroF | SuccF a，不动点写成data Nat = Zero | Succ Nat

我想我们可以定义 Fx :: NatF (Fix NatF) -> Fix NatF 或者说 Fix NatF = Fx (NatF (Fix NatF))

如果我们像这样定义另一个载体类型String的代数

h :: NatF String -> String
h ZeroF  = "0"
h (SuccF x) = x ++ " + 1"

那么我认为我们可以使用 cata h = h . fmap (cata h) . unFix 来表示像 1 这样的自然数，如下所示

(h . fmap (cata h) . unFix) Fx(SuccF Fx(ZeroF)) =
(h . fmap (cata h)) (SuccF Fx(ZeroF)) =
h (SuccF (cata h)(Fx(ZeroF))) =
h(SuccF h(ZeroF)) =
h (SuccF "0") =
"0 + 1"

但这好像不是公式cata(n) = hⁿ(unit)。这一切我的错误在哪里？

Answer 1

代数 NatF A -> A 由（直到同构）

• 类型A
• 一个常量z :: A（你称之为“单位”）
• 一个函数s :: A -> A（你称之为“h”）

然后，非正式地，cata algebra n = s^n(z)。

在您的示例中，h 是

h :: NatF String -> String
h ZeroF  = "0"
h (SuccF x) = x ++ " + 1"

但这是整个代数（z 和 s），而不仅仅是 s 态射。

你上面的h对应的是：

• A = String
• z = "0"
• s x = x ++ " + 1"

确实，（非正式表示法）cata h 1 = s^1(z) = s z = "0" ++ " + 1" = "0 + 1"。

结论：不要使用h同时调用代数和代数“内部”的态射s。

Answer 2

我认为你的困惑与 cata(n)=hⁿ(unit) 有关。这不是真的——你有一个 off-by-one 错误。特别是，考虑初始代数 nat :: 1 + Nat -> Nat:

的定义交换图

          nat
1 + Nat  --->   Nat

  |              |
  | F(cata)      |  cata
  V              V
          h
1 + A    --->    A

这给出了以下内容，Haskell-like 参数的“类型注释”，使我们在做什么更清楚：

cata(0 :: Nat)
-- by definition of nat(unit)
= cata(nat(unit :: 1 + Nat) :: Nat)
-- by diagram
= h(F(cata)(unit :: 1 + Nat) :: 1 + A)
-- as F(cata)(unit) = unit
= h(unit :: 1 + A)

所以，你实际上有cata(0)=h¹(unit) .合适的通式是cata(n)=hⁿ⁺¹(unit).