"Last" 是一个自由幺半群吗？

Question

"Last" 是一个自由幺半群吗？

8

自由幺半群通常被视为“列表幺半群”。但我对可能给我们带来自由幺半群的其他可能结构感兴趣。

首先，让我们回顾一下自由幺半群的定义。我从未完全理解如何将自由幺半群定义为遵循幺半群法则且没有其它规则的结构。我们如何证明某些东西遵循以上所述的没有规则的法则？或者这只是一种直觉？

无论如何，我们将要谈论函子。如果一些幺半群是自由的，那么我们可以使用自由函子获得它。显然，列表在这里非常方便：

free :: Set -> Mon
free a = ([a], (++), [])

然而，我们可能会想到其他几个示例。例如，这里是一个针对Data.Monoid的Last的示例：

freeLast :: Set -> Mon
freeLast a = (Last a, (<>) :: Last a -> Last a -> Last a, Last Nothing)

那么，这个函数对象是否使Last成为一个自由幺半群呢？更一般地说，如果T a的实例遵守定律，那么T是一个自由幺半群吗？

- Zhiltsoff Igor

4

对于任意X，都存在一个自由的X。特别地，对于任意集合S，存在唯一的自由幺半群（而Last S不是它）。但是这并不回答有趣的问题，即“为什么？”，因此我不会将其作为答案。 - Daniel Wagner

1

@ZhiltsoffIgor，你没有引用自由幺半群的实际定义，这似乎是混淆的原因。 - Li-yao Xia

@Li-yaoXia，根据维基百科的定义，它是一个列表，就我所知。但我的问题更多关于自由函子。 - Zhiltsoff Igor

你可以在这里找到自由对象的另一个、更具范畴性的定义：https://en.wikipedia.org/wiki/Free_object。根据这个定义，如果存在两个自由对象 F(A) 和 F'(A)，那么从 F 到 F' 有一个唯一的态射，并且从 F'(A) 到 F(A) 也有一个唯一的态射；由于图表是可交换的，它必须是同构。 - n. m.

2

@ZhiltsoffIgor 问题主体中的那个绝对不是自由箭头，因为首先它不是箭头：它不满足箭头所需的 arr(f >>> g) = arr f >>> arr g 法则。我不确定唯一答案中的那个是否是自由箭头；一旦我确定在那里没有反例支持我的说法，我就变得懒惰了。=P - Daniel Wagner

显示剩余14条评论

5个回答

4

举例说明，我们考虑非负整数，即0,1,2,……。我们可以构造多少个幺半群？

定义mempty = 0和(<>) = (+)。您可以轻松证明这是一个幺半群。

定义mempty = 1和(<>) = (*)。同样，这是一个幺半群（证明它很容易）。

上面定义的两个幺半群分别称为自然数上的“加法”和“乘法”幺半群。它们在结构上是不同的，例如，在乘法幺半群中，元素0的行为与加法幺半群中的任何其他元素完全不同，因此自然数内部存在某些使这些幺半群不同的东西（在下一段中保持这种断言）。

第三个我们可以创建的幺半群称为“串联”幺半群。

定义mempty = no-action和(<>) = glue one integer beside the other。

例如，3 <> mempty = 3和3 <> 2 = 32。请注意，这里元素是自然数并不重要。如果我们取有理数或任何您喜欢的符号，那么幺半群就完全是同一件事。因此，它不依赖于自然数的算术规则，也不依赖于除幺半群规则之外的任何规则，因此该幺半群是自由的。

这是构建幺半群的唯一方法，与底层集的内部规则无关。当然，在Haskell中，串联表示为列表。

注：唯一重要的是它们具有相同数量的元素。例如，具有3个元素a，b和c的自由幺半群将是这三个任意串联，但您可以选择任何符号：1，2，3或α，β，γ......，而幺半群仍然是完全相同的。

- lsmor

听起来你只是在描述参数性，但那不能是“自由性”的唯一条件，因为 Last a 也不依赖于 a 的结构，但它仍然不是 a 上的自由幺半群。（First a 和 Const () a 也不是）。 - Jon Purdy

4

首先，让我们来看看自由幺半群的定义。我从来没有完全理解“如何将自由幺半群定义为遵守幺半群法则而无其他规则的结构”。我们如何证明某个东西只遵循上述法则而不遵循其他规则呢？还是这只是一种直觉？

让我解释一下自由幺半群的目的。

如果我告诉你有一个幺半群，其中一些元素是a、b、c，那么你能从中推断出什么？

1.我们可以通过使用“生成器”a、b、c和幺半群操作（+）和0（也就是（<>）和mempty）编写表达式来找到该幺半群的更多元素。（请参见此答案的后半部分中的定义1。）

2. 我们可以使用幺半群定律来证明一些表达式表示相同的元素：我们可以证明像((a+0)+b)=(a+b)这样的方程式。（定义2。）实际上，我们只需具备这些基础知识所能证明的方程式是对于任何值a、b、c，在任何幺半群中都是成立的。（定理1。）

那么不能仅凭幺半群定律证明的等式怎么办呢？例如，我们无法证明(a+b)=(b+a)。但是如果我们只知道幺半群定律，那么我们也不能证明它的否定(a+b)!=(b+a)。这是什么意思？事实证明，在某些幺半群（例如可交换幺半群）中，该等式成立，而在其他幺半群中则不成立：例如，选择一个幺半群，其中对于几乎所有的x和y均满足x+y=y（这是Haskell中的“Last”幺半群），如果我们选择不同的a和b，则(a+b)!=(b+a)。

但这只是一个例子。那么对于我们无法仅通过幺半群定律证明的等式，我们可以从中得出什么结论呢？自由幺半群提供了一个明确的答案，事实上是一个通用的反例：无法证明的等式在自由幺半群（由a、b、c产生）中是错误的。换句话说，我们可以仅通过幺半群定律证明方程式e=f当且仅当它在自由幺半群中为真（强调“当”）。（定理2。）这对应于自由幺半群“只遵循幺半群定律而不遵循其他规则”的直觉。

所以，这个函子是否使得 Last 成为一个自由幺半群呢？更一般地说，如果 Monoid (T a) 有一个遵守法则的实例，那么 T a 是否是自由幺半群呢？ Last 幺半群不是自由幺半群，因为它使得比单纯从幺半群法则可以证明的等式更多的等式成立。参见其他回答：

forall (t :: Type) (x, y :: t).
  Last (Just x) <> Last (Just y) === Last (Just y)

下面是如何将上述内容形式化的草图。

定义1. 由（一些原子符号）A、B、C生成的单子表达式集合由以下语法规则定义：

e ::=
  | A | B | C   -- generators
  | e + e       -- binary operation (<>)
  | 0           -- identity (mempty)

给定任何“合适的单子”（即带有一些选择元素a，b，c的单子（M，+，0）的单子M，它们不必是不同的），表达式e表示元素eval e在M中。

定义2。方程式是一对表达式，写作e〜f。可证明方程式集是满足以下条件的方程式集（按包含关系排序时最小）：

它包括单子律：可证明e + 0 ~ e，0 + e ~ e和((e + f) + g) 〜 (e + (f + g))。
它是等价关系（将元组视为关系）：例如，对于自反性，e 〜 e是可证明的。
它是一个同余关系：如果可证明e 〜 f，则可证明(g + e) 〜 (g + f)和(e + g) 〜 (f + g)。

（该定义的想法是，如果且仅当可以通过“应用”这些规则来推断它时，断言“e 〜 f可证明”成立。 “最小集合”是形式化该定义的常规方法）

“可证明方程式”的定义可能看起来是随意的。这些是定义“可证性”的正确规则吗？为什么特别是这三个规则？值得注意的是，同余规则在首次尝试给出这样的定义时可能不明显。这就是以下定理，声音和完整性的重点。添加（非冗余）规则，我们会失去声音。删除规则，则会失去完整性。

定理1。（声音）如果可证明e 〜 f，则在任何“合适的单子”M中，eval e = eval f。

定理2。（完整性）如果无法证明e 〜 f，则它们在F中的表示方式不同，eval e≠eval f，在那里F是由A，B，C生成的自由单子。

（相对于完整性，声音要容易得多。读者的练习。）

这个完备性定理是自由幺半群的一个特征：任何其他使定理成立的幺半群 F 都同构于自由幺半群（严格来说，这需要完备性和假设表达式的指称函数 eval : Expr -> M 是满射）。这就是为什么我们可以说“自由幺半群”而不是“列表幺半群”的原因；在表示不重要的上下文中，这种做法最准确（“同构”）。

事实上，如果你将“自由幺半群”定义为幺性表达式通过等价关系 "_ ~ _ 可证明" 的商，那么完备性显然。真正难的工作在于另一个证明，即该幺半群同构于列表幺半群。

- Li-yao Xia

3

以下是 Last 满足的另一条规则：

forall (t :: Type) (x, y :: t).
  Last (Just x) <> Last (Just y) === Last (Just y)

由于它满足另一条法则，所以它不可能是自由幺半群。

- amalloy

我猜这个定律直接来自于(<>)的Last定义。这个定律叫什么？我们怎么确定没有其他法律适用于[]？我写下的freeLast函子有什么问题？ - Zhiltsoff Igor

0

关于自由幺半群符合幺半群定律且没有其他内容的部分仅仅是一种直觉。

自由幺半群的定义是一个满足自由幺半群普遍性质的幺半群。这个性质意味着以下：

给定一个集合

N

关于自由幺半群N

(N, ++, [])

对于该集合上的所有幺半群

(N, (+), 0)

(N, (*), 1)

等等。

必须存在将自由幺半群转换为每个幺半群的函数。在我们的两个示例中，这些函数分别是fold +和fold *。

编程直觉告诉我们，如果您有一堆值，想以多种不同的方式处理它们（求和、相乘等），那么唯一的方法就是将这些值保存在列表、数组或类似的数据结构中。

- Jencel

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Bartosz Milewski · Accepted Answer

这是理解自由幺半群的一种方法：如果有人给你一个值，你能推断出它是如何创建的吗？考虑自然数加法幺半群。我给你一个 7，问你我是怎么得到它的。我可能是将 4+3、3+4、2+5 等相加而得。有很多可能性，这些信息已经丢失了。另一方面，如果我给你一个列表 [4, 3]，你知道它是由单元素列表 [4] 和 [3] 创建的。除非有一个空列表 [] 参与其中，也许它是 [4]<>[3]<>[] 或者 [4]<>[]<>[]<>[3]。但它肯定不是 [3]<>[4]。

对于更长的列表 [1, 2, 3]，你有额外的选择 ([1]<>[2]) <> [3] 或者 [1] <> ([2]<>[3])，以及所有可能的空列表插入。所以你失去的信息遵循单位律和结合律，但没有别的规律。自由幺半群值记住了它是如何创建的，满足单位律和结合律。