haskell - 自然数的初始代数

Question

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

稍后编辑

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

具体是如何Fx定义的？这个对吗？

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

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

---

原帖

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

所以可以把函子写成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)有关。这不是真的 - 你有一个错误。特别是，考虑初始代数的定义交换图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 ¹ (unit)。适当的通式是cata(n)=h ⁿ⁺¹ (unit)。