"MonadPlusは単なる自己関手の圏における近半環だよ。何か問題でも" の理解を試みる

それほど数学の素養ない筆者が、論文を斜め読みして「理解を試みてみた」記録です。最低限の雰囲気だけ説明してみるけど、雑だし正確な言い方もしないので、ちゃんと知りたい人は最初から元の論文を読もう。
といういつものような注意書きを書いておきます。


あと、(日本語でなんとなく書いてるので細かい部分はあれとして)もし明らかな重大な間違いとかあったら教えて下さい。


さて、説明に入ります。



"MonadPlusは単なる自己関手の圏における近半環だよ。何か問題でも"


とは、以下のblog(とそこで言及してる論文)のことです。

英語だと

"MonadPlus and Alternative are just near-semirings in the category of endofunctors, what's the problem?"

です。


ちなみに、知らない人がいるかもしれないので念の為に解説しておくと
"モナドは単なる自己関手の圏におけるモノイド対象だよ。何か問題でも"
という有名な文言があるのでそれに合わせた言葉でしょう。


そのblog書いたのは論文の作者です。論文の中には、その言葉出してなかった気がします。論文の中に出てきてるか、出てないか自体はどうでもいいというか、この記事では "MonadPlus" と "近半環" というものの関係をなんとなくでも感じ取ってもらうのが趣旨です。普通の人は


キン ハン カン


といっても聞き慣れないというか、どこかの外国の人の名前か、何かの技みたいな響きを感じますが(?)、数学の用語です。

ここからしばらくは、数学の授業みたいな退屈な(?)解説をしましょう。



"近半環" は、英語では "near semiring" というらしいです。なんか直訳ですね。


ところで何を隠そう、自分も "近半環" という言葉聞いたことありませんでした。ただ "環" と "半環" はかろうじて聞いたことがあります。


つまり "近半環" は


"近" であり "半" である "環" です


なにいってるかわからないですね。自分でも何言ってるかわからないです。というか条件の強さ的には逆(?)なので、上記の言い方だと余計混乱するだけかもしれません、忘れてください。

無理やり話をすすめると、言いたかったこととしては、まず "環" や "半環" のほうがある程度は有名で調べればでてくるので、それらを理解しましょう、という話です。
"環" や "半環" が理解できれば "近半環" はそれらと少し違うだけらしいので、たぶん理解できるでしょう。という流れです。


さて、 "環" は英語で ring、 "半環" は英語で semiring です。


少しだけ寄り道をすると、(Haskellなどに親しんでるプログラマなら) ring よりは馴染み深いであろう、 semigroup は、日本語だと "半群" であり、"半" が付かない "群" も数学用語としてありますね?
"半群" や "群" 自体の説明を入れると寄り道になりすぎるので飛ばします。


さて、話を戻して、 "環" と "半環" です。といっても、このあたりは日本語でも調べれば色々説明があるので、wikipediaなり何なりを見てもらったほうが正確かつわかりやすいでしょう。


wikipedia 環
wikipedia 半環


簡単にまとめておくと

    • 足し算とかけ算が定義できて閉じている*1
    • 足し算が可換
      • a + b と b + a が同じになる
    • 足し算が結合的
      • (a + b) + c と a + (b + c) が同じになる
    • かけ算が結合的
      • (a * b) * c と a * (b * c) が同じになる
    • (左と右両方の)分配法則が成り立つ
      • a ∗ (b + c) と (a ∗ b) + (a ∗ c) が同じ
      • (a + b) ∗ c と (a ∗ c) + (b ∗ c) が同じ
    • 足し算について逆元がある
    • 足し算について単位元が存在
      • (任意のaに対して) a + zero = zero + a = a となるzeroが存在
  • 半環
    • 環から「足し算について逆元」の制約を除いたもの


という感じらしいです。


"可換" というとすごく難しく聞こえるかもしれませんが、別の言葉で言うと"交換法則"です。
"交換法則"や"分配法則"なんて小学校で習いましたね、簡単ですね?


いちいち具体的な環や半環の例はここでは出さないので、具体例知りたい人はググってください。



さて、いよいよ "近半環" ですが、一応日本語のwikipediaの半環のページにも一言だけ記述ありましたね。
(ちなみに英語版には専用のページがあるみたい https://en.wikipedia.org/wiki/Near-semiring )

半環の定義において加法の可換性も右分配律もともに仮定から落とすならば近環 (near-ring) の概念が得られる。先に挙げた意味での基数全体が半環を成すのとまったく同様の意味で、順序数の全体は近環を成す。

ということらしいです(?)わかったようなわからないような感じですね。
今までの記述を元に "近半環" について改めて整理すると以下のようになります。


  • 足し算が結合的
    • (a + b) + c と a + (b + c) が同じになる
  • かけ算が結合的
    • (a * b) * c と a * (b * c) が同じになる
  • 左の分配法則が成り立つ(右は成り立たなくてもよい)
    • (a + b) ∗ c = (a ∗ c) + (b ∗ c) が同じ
  • 足し算について単位元が存在
    • (任意のaに対して) a + zero = zero + a = a となるzeroが存在

数学だけの退屈な(?)話は終わり、やっとMonadPlusが出てきます。

MonadPlusが近半環ということは、とにかくMonadPlusの演算において、まず「足し算」と「かけ算」にあたる操作が定義できるはずです。ここで、ひとまず論文中の関係ある部分のコード丸ごと引用しましょう

m1 ‘mplus‘ (m2 ‘mplus‘ m3) = (m1 ‘mplus‘ m2) ‘mplus‘ m3
m ‘mplus‘ mzero = m
mzero ‘mplus‘ m = m
mzero >>= k = mzero
(m1 ‘mplus‘ m2) >>= k = (m1 >>= k) ‘mplus‘ (m2 >>= k)


さて、MonadPlusにおいてなにが「足し算」でなにが「かけ算」なのか説明してませんでしたが、ここでやっとその説明しましょう。雑にいうと

  • MonadPlusにおけるmplusが足し算
    • なのでmzeroは足し算に関するゼロ元
  • Monadにおけるbindの演算がかけ算

となるようです。さて、上記に上げた "近半環" の条件と、論文から持ってきた5つの法則がそのまま対応するのかと思いきや、よくみるとそうではありませんね?

答えを先にいってしまうと "MonadPlus則" ではなく、 "Monad則" 自体も関係するからです。つまり

  • かけ算が結合的
    • (a * b) * c と a * (b * c) が同じになる

とは、以下のMonad則のことです。

(m >>= f) >>= g  = m >>= (\x -> f x >>= g)

残りは先ほど書いた "近半環" の条件と論文から持ってきた法則はそのまま対応しますね。つまり

-- 足し算が結合的

m1 ‘mplus‘ (m2 ‘mplus‘ m3) = (m1 ‘mplus‘ m2) ‘mplus‘ m3
-- 足し算に関するゼロ元の存在

m ‘mplus‘ mzero = m
-- 足し算に関するゼロ元の存在

mzero ‘mplus‘ m = m
-- かけ算に関するゼロ元の存在

mzero >>= k = mzero
-- 左の分配法則

(m1 ‘mplus‘ m2) >>= k = (m1 >>= k) ‘mplus‘ (m2 >>= k)


MonadPlusが "半環" ではなく "近半環" なのは、すべてのMonadPlusのインスタンスが半環の条件(というか半環と近半環の違い)、すなわち

  • 足し算の可換性
  • 右分配律

を満たさない*2ということなのでしょう。
具体的に
「MonadPlusを"半環"にしようとしても"半環"の条件を満たさない」
というような例は考えるの面倒だったので、各自頑張ってください。



そもそもMonadPlusの法則を真面目に考えると少し奥が深いのですが、そのあたりの話解説するのは長くなるし、うまく解説できる気がしないので、関係ありそうなページを貼って終わりにします

追記:

反例示してくれたり、演算の定義自体が雑というか不正確だったのをちゃんと解説してくれたりした、ありがたいエントリがあるので、みょんさんのコレも読むといいよ(ありがとうございます)

MonadPlusとNearSemiringで反例探し

*1:閉じている、とは、足し算やかけ算をしても、もとの集合の範囲のものになるくらいな感じ

*2:もしくはプログラム上そもそもうまく定義できない?