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

私が考えることができる最も近い一般的な構造はトーサーですが、それは明白な方法で自然に実際には適用されません。時間値に対して実行できる操作について考えてみてください。

  • 2回「減算」して、時間間隔を算出します（別のタイプ）
  • 別の時間を取得するには、時間に時間間隔を追加します
  • 時間の間隔を加算または減算して、別の間隔を取得します

時間値のペアに対する他の操作はほとんど意味がありません。時間を追加したり、乗算したりすることはできません。また、代数で慣れているものは何でもできません。一方、間隔タイプははるかに柔軟性があり、加算、減算、反転などをサポートします。したがって、torsorはHaskellで次のように定義できます。

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

とにかく、それはあなたの直接の質問に答える試みです（あなたはそれらのジョン・バエズの素晴らしいページでもっと見つけることができます）、それはあなたの自然な例をカバーしていませんが。

私の知る限り、あなたの質問に答えるのに近い他の唯一のことは、Coqの（半）リングソルバー戦術でコードを再利用するためのソリューションです。彼らは、あなたが説明するものと同様の公理を持つ「概数」の概念を導入し、コードのほとんどを自然界と完全なリングに再利用できるようにします。しかし、そのアイデアはあまり普及していないと思います。

于 2013-02-17T15:20:14.923 に答える
6

あなたが探している名前は相殺モノイドですが、厳密に言えば、相殺半群は減算の概念を捉えるのに十分です。私は 1 年ほど前にまったく同じ質問について疑問に思っていましたが、数学の専門用語を掘り下げることで答えを見つけました。incremental-parser パッケージのCancellativeMonoidクラスを見てください。私は現在、モノイド サブクラスとそのインスタンスのいくつかのみを含む新しいパッケージを準備しており、すぐにリリースしたいと考えています。

于 2013-02-24T04:59:37.623 に答える