Last 是一个自由幺半群吗？
Is Last a free monoid?
自由幺半群通常被视为“列表幺半群”。然而，我对其他可能的结构感兴趣，这些结构可能会给我们 free monoids.
首先，让我们回顾一下自由幺半群的定义。我一直不太明白如何将 自由幺半群 定义为遵守幺半群法则的结构。我们如何证明某事不遵守上述规则？或者这只是一种直觉？
无论如何，我们要讲函子。如果某个幺半群是自由，我们用自由函子得到它。很明显，列表在这里非常方便：
free :: Set -> Mon
free a = ([a], (++), [])
然而，人们可能会想出其他几个。例如，这里是 Last of Data.Monoid:
freeLast :: Set -> Mon
freeLast a = (Last a, (<>) :: Last a -> Last a -> Last a, Last Nothing)
那么，这个仿函数是否使 Last 成为一个 自由幺半群 ？更一般地，如果 Monoid (T a) 存在守法实例，T 是 自由幺半群 吗？
这是 Last 满足的另一个定律：
forall (t :: Type) (x, y :: t).
Last (Just x) <> Last (Just y) === Last (Just y)
因为它满足另一个定律，它一定不是自由的幺半群。
这是理解自由幺半群的一种方法：如果有人给你一个值，你能从中推断出它是如何产生的？考虑自然数的加法幺半群。我给你一个 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])，以及所有可能的空列表插入。因此，您丢失的信息遵循单位定律和结合律，但没有别的。一个自由的幺半群值会记住它是如何创建的，模单位定律和结合性。
Firstly, let us go over the definition of free monoids. I have never quite understood how is it possible to define a free monoid as a structure which abides by monoid laws and nothing else. How do we prove that something abides by no rules but stated above? Or is this just an intuition?
让我来说明一下免费幺半群的用途。
如果我告诉你有一个幺半群，包含一些元素 a、b、c，你能从中推断出什么？
- 我们可以通过编写涉及 生成器
a、b、c 和幺半群运算的表达式来找到该幺半群的更多元素(+) 和 0（又名 (<>) 和 mempty）。 （参见本答案后半部分的定义 1。）
- 我们可以用幺半群法则来证明一些表达式表示相同的元素：我们可以证明方程如
((a + 0) + b) = (a + b)。 （定义2。）事实上，我们仅用知识就可以证明的方程是在任何幺半群中对于任何值a、b、c成立的方程。 （定理 1。）
我们无法仅根据幺半群定律证明的方程怎么办？例如，我们无法证明 (a + b) = (b + a)。但是如果我们只知道幺半群定律，我们也无法证明它的否定，(a + b) /= (b + a)。那是什么意思？事实证明，该等式在某些幺半群（例如，交换幺半群）中成立，但在其他幺半群中不成立：例如，选择一个幺半群，其中 x + y = y 几乎所有 x 和 y（这是 Haskell 中的 Last 幺半群），如果我们选择不同的 a 和 b，则 (a + b) /= (b + a).
但这只是一个例子。对于不能仅从幺半群定律证明的方程，我们一般可以说些什么？自由幺半群提供了一个明确的答案，实际上是一个普遍的反例：在自由幺半群（由 a、b、c 生成）中，无法证明的方程是错误的。换句话说，我们可以仅使用幺半群定律来证明方程 e = f 当且仅当它在自由幺半群中为真（强调“如果”）。 （定理 2.）这对应于自由幺半群“仅遵守幺半群法则而无其他”的直觉。
So, does this functor make Last a free monoid? More generally, if there is a law-abiding instance for Monoid (T a), is T a free monoid?
Last 幺半群不是免费的，因为它使更多的方程为真，而不是你可以纯粹从幺半群定律实际证明的。参见 :
forall (t :: Type) (x, y :: t).
Last (Just x) <> Last (Just y) === Last (Just y)
下面是如何形式化上述内容的草图。
定义1.由（一些原子符号）A、[=41=生成的幺半群表达式的集合], C 由语法定义：
e ::=
| A | B | C -- generators
| e + e -- binary operation (<>)
| 0 -- identity (mempty)
给定任何“合适的幺半群”，也就是说，一个幺半群 (M, (+), 0) 具有一些选定的元素 a、b、c in M（不必不同），表达式 e 表示 M.
中的元素 eval e
定义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 是可证明的”当且仅当它可以通过“应用”这些规则推导出来时才成立。“最小集”是形式化的常规方法那个。)
“可证明的方程式”的定义似乎很武断。这些是定义“可证明性”的正确规则吗？为什么要特别注意这三个规则？值得注意的是，在第一次尝试给出这样的定义时，同余规则可能并不明显。这是以下定理的可靠性和完整性的要点。添加一个 (non-redundant) 规则，我们就失去了稳健性。删除规则，我们将失去完整性。
定理 1.（可靠性）如果 e ~ f 是可证明的，则 eval e = eval f 在任何“合适的幺半群”中 M.
定理 2.（完备性）如果 e ~ f 不可证明，则它们的外延在 F、eval e /= eval f 中有所不同，其中 F 是由 A, B, C.
生成的自由幺半群
（可靠性比完整性更容易证明。reader 的练习。）
这个完备性定理是自由幺半群的特征：任何其他保持定理陈述为真的幺半群 F 与自由幺半群同构（从技术上讲，这需要完整性和假设表示函数 eval : Expr -> M 是满射的）。这就是为什么我们可以说“自由幺半群”而不是“列表的幺半群”；在表示无关紧要的情况下（“直到同构”），这种做法是最准确的。
事实上，如果您将“自由幺半群”定义为等价关系“_ ~ _ 可证明”的幺半群表达式的商，那么完整性是微不足道的。艰苦的工作实际上在于一个单独的证明，即这个幺半群与列表的幺半群同构。
为了举例，我们取 non-negative 个整数，即 0,1,2,...。我们可以制作多少个幺半群？
正在定义 mempty = 0 和 (<>) = (+)。你可以很容易地证明这是一个幺半群。
正在定义 mempty = 1 和 (<>) = (*)。同样，这是一个幺半群（证明它，很容易）
上面定义的两个幺半群，被称为自然数上的加法和乘法幺半群。它们在结构上不同，例如，乘法幺半群中的元素 0 的行为与加法幺半群中的任何其他元素完全不同，因此 自然数中存在一些内在的东西，这使得这个幺半群不同（将此断言保留到下一段）。
我们可以创建第三个幺半群，我们称之为 concatenation 幺半群。
正在定义 mempty = no-action 和 (<>) = glue one integer beside the other。
例如，3 <> mempty = 3 和 3 <> 2 = 32。请注意，元素是自然数这一事实与此处无关。如果我们采用 Rationals 而不是 Natural，或者任何你喜欢的符号，那么幺半群将是完全相同的东西。（*阅读脚注）因此，基础集合中没有任何东西可以构成幺半群与众不同。这就是为什么幺半群是自由的，因为它不依赖于自然数的算术规则，也不依赖于幺半群之外的任何其他规则。
而且这是唯一可以自由构建幺半群的方法，不依赖于底层集合的内部规则。当然，连接表示为 haskell.
中的列表
- 注意：唯一重要的一点是它们共享相同数量的元素。例如，具有 3 个元素
a、b 和 c 的自由幺半群可以是这三个元素的任意串联，但您可以选择任何符号：1、2、3 或 α、β、γ ... 幺半群是完全相同的东西
自由幺半群通常被视为“列表幺半群”。然而，我对其他可能的结构感兴趣，这些结构可能会给我们 free monoids.
首先，让我们回顾一下自由幺半群的定义。我一直不太明白如何将 自由幺半群 定义为遵守幺半群法则的结构。我们如何证明某事不遵守上述规则？或者这只是一种直觉？
无论如何，我们要讲函子。如果某个幺半群是自由，我们用自由函子得到它。很明显，列表在这里非常方便：
free :: Set -> Mon
free a = ([a], (++), [])
然而，人们可能会想出其他几个。例如，这里是 Last of Data.Monoid:
freeLast :: Set -> Mon
freeLast a = (Last a, (<>) :: Last a -> Last a -> Last a, Last Nothing)
那么，这个仿函数是否使 Last 成为一个 自由幺半群 ？更一般地，如果 Monoid (T a) 存在守法实例，T 是 自由幺半群 吗？
这是 Last 满足的另一个定律：
forall (t :: Type) (x, y :: t).
Last (Just x) <> Last (Just y) === Last (Just y)
因为它满足另一个定律，它一定不是自由的幺半群。
这是理解自由幺半群的一种方法：如果有人给你一个值，你能从中推断出它是如何产生的？考虑自然数的加法幺半群。我给你一个 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])，以及所有可能的空列表插入。因此，您丢失的信息遵循单位定律和结合律，但没有别的。一个自由的幺半群值会记住它是如何创建的，模单位定律和结合性。
Firstly, let us go over the definition of free monoids. I have never quite understood how is it possible to define a free monoid as a structure which abides by monoid laws and nothing else. How do we prove that something abides by no rules but stated above? Or is this just an intuition?
让我来说明一下免费幺半群的用途。
如果我告诉你有一个幺半群，包含一些元素 a、b、c，你能从中推断出什么？
- 我们可以通过编写涉及 生成器
a、b、c和幺半群运算的表达式来找到该幺半群的更多元素(+)和0（又名(<>)和mempty）。 （参见本答案后半部分的定义 1。） - 我们可以用幺半群法则来证明一些表达式表示相同的元素：我们可以证明方程如
((a + 0) + b) = (a + b)。 （定义2。）事实上，我们仅用知识就可以证明的方程是在任何幺半群中对于任何值a、b、c成立的方程。 （定理 1。）
我们无法仅根据幺半群定律证明的方程怎么办？例如，我们无法证明 (a + b) = (b + a)。但是如果我们只知道幺半群定律，我们也无法证明它的否定，(a + b) /= (b + a)。那是什么意思？事实证明，该等式在某些幺半群（例如，交换幺半群）中成立，但在其他幺半群中不成立：例如，选择一个幺半群，其中 x + y = y 几乎所有 x 和 y（这是 Haskell 中的 Last 幺半群），如果我们选择不同的 a 和 b，则 (a + b) /= (b + a).
但这只是一个例子。对于不能仅从幺半群定律证明的方程，我们一般可以说些什么？自由幺半群提供了一个明确的答案，实际上是一个普遍的反例：在自由幺半群（由 a、b、c 生成）中，无法证明的方程是错误的。换句话说，我们可以仅使用幺半群定律来证明方程 e = f 当且仅当它在自由幺半群中为真（强调“如果”）。 （定理 2.）这对应于自由幺半群“仅遵守幺半群法则而无其他”的直觉。
So, does this functor make Last a free monoid? More generally, if there is a law-abiding instance for Monoid (T a), is T a free monoid?
Last 幺半群不是免费的，因为它使更多的方程为真，而不是你可以纯粹从幺半群定律实际证明的。参见
forall (t :: Type) (x, y :: t).
Last (Just x) <> Last (Just y) === Last (Just y)
下面是如何形式化上述内容的草图。
定义1.由（一些原子符号）A、[=41=生成的幺半群表达式的集合], C 由语法定义：
e ::=
| A | B | C -- generators
| e + e -- binary operation (<>)
| 0 -- identity (mempty)
给定任何“合适的幺半群”，也就是说，一个幺半群 (M, (+), 0) 具有一些选定的元素 a、b、c in M（不必不同），表达式 e 表示 M.
eval e
定义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 是可证明的”当且仅当它可以通过“应用”这些规则推导出来时才成立。“最小集”是形式化的常规方法那个。)
“可证明的方程式”的定义似乎很武断。这些是定义“可证明性”的正确规则吗？为什么要特别注意这三个规则？值得注意的是，在第一次尝试给出这样的定义时，同余规则可能并不明显。这是以下定理的可靠性和完整性的要点。添加一个 (non-redundant) 规则，我们就失去了稳健性。删除规则，我们将失去完整性。
定理 1.（可靠性）如果 e ~ f 是可证明的，则 eval e = eval f 在任何“合适的幺半群”中 M.
定理 2.（完备性）如果 e ~ f 不可证明，则它们的外延在 F、eval e /= eval f 中有所不同，其中 F 是由 A, B, C.
（可靠性比完整性更容易证明。reader 的练习。）
这个完备性定理是自由幺半群的特征：任何其他保持定理陈述为真的幺半群 F 与自由幺半群同构（从技术上讲，这需要完整性和假设表示函数 eval : Expr -> M 是满射的）。这就是为什么我们可以说“自由幺半群”而不是“列表的幺半群”；在表示无关紧要的情况下（“直到同构”），这种做法是最准确的。
事实上，如果您将“自由幺半群”定义为等价关系“_ ~ _ 可证明”的幺半群表达式的商，那么完整性是微不足道的。艰苦的工作实际上在于一个单独的证明，即这个幺半群与列表的幺半群同构。
为了举例，我们取 non-negative 个整数，即 0,1,2,...。我们可以制作多少个幺半群？
正在定义 mempty = 0 和 (<>) = (+)。你可以很容易地证明这是一个幺半群。
正在定义 mempty = 1 和 (<>) = (*)。同样，这是一个幺半群（证明它，很容易）
上面定义的两个幺半群，被称为自然数上的加法和乘法幺半群。它们在结构上不同，例如，乘法幺半群中的元素 0 的行为与加法幺半群中的任何其他元素完全不同，因此 自然数中存在一些内在的东西，这使得这个幺半群不同（将此断言保留到下一段）。
我们可以创建第三个幺半群，我们称之为 concatenation 幺半群。
正在定义 mempty = no-action 和 (<>) = glue one integer beside the other。
例如，3 <> mempty = 3 和 3 <> 2 = 32。请注意，元素是自然数这一事实与此处无关。如果我们采用 Rationals 而不是 Natural，或者任何你喜欢的符号，那么幺半群将是完全相同的东西。（*阅读脚注）因此，基础集合中没有任何东西可以构成幺半群与众不同。这就是为什么幺半群是自由的，因为它不依赖于自然数的算术规则，也不依赖于幺半群之外的任何其他规则。
而且这是唯一可以自由构建幺半群的方法，不依赖于底层集合的内部规则。当然，连接表示为 haskell.
中的列表- 注意：唯一重要的一点是它们共享相同数量的元素。例如，具有 3 个元素
a、b和c的自由幺半群可以是这三个元素的任意串联，但您可以选择任何符号：1、2、3或α、β、γ... 幺半群是完全相同的东西