haskell - 自然数的初代数

Question

我试图确保我使用自然数的基本情况来理解初始代数和变形概念，但我肯定遗漏了一些东西(我的 Haskell 语法也可能是一团糟)。
稍后编辑
我认为我的问题主要与功能有关 Fx/unFix定义 NatF (Fix NatF) 之间的同构和 Fix NatF .我的理解是Fix NatF是 电话 (自然数集)，即 Nat = Zero | Succ Nat .
怎么样Fx确切定义？这样对吗？

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

如果是这样，为什么这与初始代数不一样 1 + N -> N 由对评估 [0, 成功] ?

原帖
我知道对于自然数我们有仿函数 F(U) = 1 + U 和初代数 F(U) -> U 哪里 单位转至 0 和 转至 succ(n) = n + 1 .对于另一个由函数求值的代数 h ，变质 猫 将 cata(n) = hn(单位) .
所以可以把仿函数写成 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) = hn(单位) .在这一切中我的错误在哪里？

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这是代数的“内部”。