自然数的初始代数

Question

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

如果是这样，为什么这和由对[0,succ]求值的初始代数1+n->N不一样呢？

原帖

我知道对于自然数，我们有函子F(U)=1+U和初始代数F(U)->U，其中单位为0，n为succ(n)=n+1。对于另一个由函数h求值的代数，其成体性cata为cata(n)=hⁿ（单位）。

h :: NatF String -> String
h ZeroF  = "0"
h (SuccF x) = x ++ " + 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ⁿ（单位）。在这一切中，我的错误在哪里？

Answer 1

我想你的困惑与cata(n)=hⁿ（单位）有关。这不是真的--您有一个Off by-One错误。特别是，考虑初始代数Nat::1+nat->Nat:

          nat
1 + Nat  --->   Nat

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

它给出了以下内容，并对参数进行了类似Haskell的“类型注释”，以使我们更清楚地了解我们在做什么：

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¹（单位）。合适的通式为cata(n)=hⁿ⁺¹（单位）。