MonadPlusとNearSemiringで反例探し

d.hatena.ne.jp

上の記事を読んでちょっと考えたこととかをまとめる.

NearSemiringとは和についてモノイド, 積について半群で, 0が左吸収元である左分配的集合.(wikipedia流儀; 関係ないけど以下に出てくる例はHaskellのMonadで, Monad則からreturnが積の単位元になるのでNearSemiringより少し強い)
まず元の記事にあるように, MonadPlus mに対し演算mplus及び>>=によってNearSemiringの構造が入るらしい.

当然最初の疑問として, そもそもbind>>=は左右で要求する型が違うので, そもそもどこ上の演算と見てるんだよという話である.
これはmplusや>>=をa -> m a上などに拡張してやると定義自体は普通にできる.

class NearSemiring m where
  (<+>) :: m a -> m a -> m a
  zero :: m a
  (<*>) :: m a -> m a -> m a
  one :: m a

newtype S m a = S { unS :: a -> m a }

instance MonadPlus m => NearSemiring (S m) where
  (S ma) <+> (S mb) = S $ \x -> ma x `mplus` mb x
  zero = S $ const mzero
  (S m) <*> (S k) = S $ \x -> m x >>= k
  one = S return

上の定義によって, MonadPlus mのもとでS m *上に演算<+>と<*>が定まる.
これが実際にNearSemiringの構造を与えることは適当に式を変形すればできると思う.
例えば右分配則だけやると以下(ただし以下ではS xとxを自然に同一視する).

(m1 <+> m2) <*> k = \x -> (m1 x `mplus` m2 x) >>= k  (<+>と<*>の定義)
  = \x -> (m1 x >>= k) `mplus` (m2 x >>= k)  (MonadPlusの右分配則)
  = (\x -> m1 x >>= k) <+> (\x -> m2 x >>= k)  (<+>の定義)
  = (m1 <*> k) <+> (m2 <*> k)  (<*>の定義)

さてこれでまともな演算が定義できた.
あとはQuickCheck辺りを使えば, 具体的なmに対して左分配則が成り立たないような反例を見つけてくれる.

実際に動かして発見できた反例は以下.

[0,0] <*> ([0] <+> [1]) ≠ ([0,0] <*> [0]) <+> ([0,0] <*> [1])

---> [0,1,0,1] /= [0,0,1,1]

---

ところで, 記事で紹介されている論文には上のようなことはざっと見た限り載っていなさそうだった.(ちゃんと読んでないので書いてあったらすいません)

論文で扱っているNearSermiringはもう少し違う感じのやつで, 例えば以下のようにして定めたDCはMonadPlusになり, よってNearSemiringの構造が入る. (コードは論文より引用)

newtype Ran f g x = Ran { unRan :: forall y. (x -> f y) -> g y }
newtype Exp f g x = Exp { unExp :: forall y. (x -> y) -> (f y -> g y) }
newtype DC f x = DC { unDC :: Ran (Exp f f) (Exp f f) x }

instance Monad (DC f) where
  return x = DC $ Ran $ \f -> f x
  DC (Ran m) >>= f = DC $ Ran $ \g -> m (\a -> unRan (unDC $ f a) g)

instance MonadPlus (DC f) where
  mzero = DC $ Ran $ \k -> Exp $ \c x -> x
  mplus (DC (Ran a)) (DC (Ran b)) = DC $ Ran $ \sk -> Exp $ \f fk -> unExp (a sk) f $ unExp (b sk) f fk

rep :: Monad m => m a -> DC m a
rep x = DC $ Ran $ \g -> Exp $ \h m -> x >>= \a -> unExp (g a) h m

abs :: MonadPlus m => DC m a -> m a
abs (DC (Ran f)) = unExp (f $ \x -> Exp $ \h m -> return (h x) `mplus` m) id mzero

さてせっかくなのでこうして定義されたDCに対しても, 前述の仕方でNearSemiring型クラスのインスタンスにし, 右分配則が成り立たない反例を探してみよう.
QuickCheckで探した所以下の例が見つかった. (ただし以下の例ではabsとrepを用いてm aとDC m aを同一視している)

[0,0] <*> ([0] <+> [0]) ≠ ([0,0] <*> [0]) <+> ([0,0] <*> [0])

--> [0,0,0,0] /= [0,0,0,0,0,0]

というわけでQuickCheck様様という話でした. おしまい.

参考文献

• "MonadPlusは単なる自己関手の圏における近半環だよ。何か問題でも" の理解を試みる - scalaとか・・・ 元の記事
• http://www.fceia.unr.edu.ar/~mauro/pubs/FromMonoidstoNearsemirings.pdf 論文
• Near-semiring - Wikipedia, the free encyclopedia NearSemiringの定義確認用

コード