15

一个群扩展了幺半群的想法以允许逆。这允许：

gremove :: (Group a) => a -> a -> a
gremove x y = x `mappend` (invert y)

但是像自然数这样没有逆的结构呢？我在想：

class (Monoid a) => MRemove a where
    mremove :: a -> a -> a

与法律：

x `mremove` x = mempty
x `mremove` mempty = x
(x `mappend` y) `mremove` y = x

另外：

class (MRemove a) => Group a where
    invert :: a -> a
    invert x = mempty `mremove` x

-- | For defining MRemove in terms of Group
defaultMRemove :: (Group a) => a -> a -> a
defaultMRemove x y = x `mappend` (invert y)

所以，我的问题是：什么是MRemove？

4

4 回答 4

9

我能想到的最接近的常见结构是躯干，但它并不真正以明显的方式适用于自然。想想您可以对时间值执行的操作：

  • “减”两次，产生一个时间间隔（不同的类型）
  • 将时间间隔添加到时间以获得另一个时间
  • 添加或减去时间间隔以获得另一个间隔

对时间值对的其他操作很少有意义。你不能加时间，或者乘它们，或者我们在代数中习惯的任何东西。另一方面，区间类型更加灵活，支持加法、减法、反演等。因此，在 Haskell 中，torsor 可以定义为：

class Group (Diff a) => Torsor a where
  type Diff a
  subtract : a -> a -> Diff a
  add      : a -> Diff a -> a

无论如何，这是尝试回答您的直接问题（您可以在 John Baez 的优秀页面上找到更多信息），即使它没有涵盖您的自然示例。

据我所知，唯一接近回答您的问题的另一件事是Coq (semi)ring solver tactic中代码重用的解决方案。他们引入了一个“几乎环”的概念，其公理类似于您所描述的公理，以允许他们将大部分代码重用于自然环和完整环。不过，我不认为这个想法很普遍。

于 2013-02-17T15:20:14.923 回答
6

您正在寻找的名称是抵消幺半群，但严格来说，抵消半群足以捕捉减法的概念。大约一年前，我在想同样的问题，我通过挖掘数学术语找到了答案。查看增量解析器包中的CancellativeMonoid类。我目前正在准备一个只包含 monoid 子类和它们的一些实例的新包，我希望尽快发布它。

于 2013-02-24T04:59:37.623 回答
1

一个类似的问题已经被问到here。给出的答案是与 monus 的可交换幺半群。

于 2018-05-26T16:34:54.487 回答
0

编辑：这个答案是错误的。请参阅下面的评论。我会保留答案以防万一。

看看减法半群。它是一个带有减法运算符的半群，它遵循以下定律：

x - (y - x) = x
x - (x - y) = y - (y - x)
(x - y) - z = (x - z) - y

x <> (y - z) = (x <> y) - (x <> z)
(y - z) <> x = (y <> x) - (z <> x)

可悲的是，我找不到讨论“减法幺半群”的资源，但我认为它需要遵守以下附加定律：

x - x = 0
于 2018-05-26T02:02:12.533 回答