自然数的初始代数

如何解决自然数的初始代数

我试图确保我使用自然数的基本情况理解初始的代数和同构概念，但我肯定缺少某些东西（而且我的Haskell语法可能很烂）。

稍后进行编辑

我认为我的问题主要与定义Fx和unFix之间同构的函数NatF (Fix NatF) / Fix NatF有关。我的理解是Fix NatF是 N （自然数集），即Nat = 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 ，其中单位转到 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 ⁿ（单位）。这一切我的错误在哪里？

解决方法

代数A由（同构）构成

类型z :: A
一个常量s :: A -> A（您称为“单位”）
函数cata algebra n = s^n(z)（您将其称为“ h”）

然后非正式地h。

在您的示例中，h :: NatF String -> String h ZeroF = "0" h (SuccF x) = x ++ " + 1"是

但这是整个代数（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和代数data class Player( @SerializedName("Position") val position: String,@SerializedName("Name_Full") val name: String ...)来称呼“代数”。

我认为您的困惑与 cata（n）= h ⁿ（单元）有关。这是不正确的-您有一个错误的错误。特别要考虑初始代数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 ^{n + 1}（单位）。