このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

ベックの分配法則とテンソル強度の組み合わせ

ベックの分配法則、テンソル強度の話は何度もしています。

今日気が付いたのですが、ベックの分配法則とテンソル強度は簡単に組み合わせることができて、期待した結果が自然に出ます。

ベックの分配法則とテンソル強度はよく似た概念なので、簡単に組み合わせることができるのは当たり前って言えばそうなんですが、意識したことはありませんでした。付点集合を作るモナド(Maybeモナド)と空集合を除いたベキ集合モナド(全域非決定性のモナド)の複合モナドは、そのクライスリ圏に集合の直積を持ち上げるのですが、その理由がこれで説明できます。

モナドに関する分配法則

Cは圏だとして、モナドとその台関手を同じ文字で表します。つまり、C上のモナドを F = (F, μ, η) のように書きます。ここで、μはモナド乗法、ηはモナド単位です。もうひとつのモナドを F' = (F', μ', η') とします。

関手FとF'の図式順(左から右)の結合を F;F'、反図式順の結合を F'Fと書きます。

  • F;F' = F'F

自然変換 β::F;F'⇒F';F:CC が「とある性質」を持つときベックの分配法則と呼びます。「とある性質」は、次のエントリーに例と共に書いてあります。

http://en.wikipedia.org/wiki/Distributive_law_between_monads には分配法則の味気ない定義だけ書いてあります(現時点では)。http://ncatlab.org/nlab/show/distributive+law は背景も含めて分配法則の一般的な記述がありますが、あまりモナドに言及されてませんね。

(F, F', β) が、モナドに関するベックの分配法則であるとき、FとF'を結合(合成)した関手 F;F':CC は再びモナドになります。より正確に言えば、FとF'のモナド構造とβを利用して、台関手F;F'上にモナド構造を作れる、ということです。

対称モノイド圏上の強モナドとクライスリ圏

Cは単なる圏ではなくて、対称モノイド構造を持つとします。対称じゃなくてもいいのですが、記述が面倒になるんで対称性を仮定します。つまり、C = (C, ×, I, σ) と書けます; ×はモノイド積、Iはモノイド単位、σは対称性です。

F = (F, μ, η) は対称モノイド圏C上のモナドとします。射の族 τA,B:F(A)×B→F(A×B) が「とある性質」を持つとき(モナドFに対する)テンソル強度と呼びます。「とある性質」に関しては次を参照してください。

テンソル強度を持つモナドモナドと呼びます。

対称モノイド圏上の強モナドは、次のような都合の良い性質を持ちます。

  • 対称モノイド圏C上の強モナドFのクライスリ圏は対称モノイド圏である。

モナドFのクライスリ圏 Kl(C, F) をKと置くと、Kに対称モノイド構造が入るのですが、それはもとの圏Cの対称モノイド構造の拡張になっています。強モナドは、圏Cの対称モノイド構造とたいへんうまく協調する、と言えます。

モナドに関する分配法則とテンソル強度の組み合わせ

Cが対称モノイド圏、FとF'はC上のモナドだとします。さらに、(F, F', β) がモナドに関するベックの分配法則で、FもF'も強モナドとします。

分配法則があるので、F;F':CCモナドになります。それだけではなくて、F;F'は強モナドになります。F;F'に対するテンソル強度は、Fのテンソル強度とF'のテンソル強度から自然に構成できます。

言い方を変えると、2つの強モナドの複合モナドは強モナドになる、ということです。その事例のひとつは、冒頭に挙げたMaybeモナドと全域非決定性のモナドの組み合わせです。

この例は、無限走行と非決定性を同時にモデル化するために定義したのですが、強モナドの複合モナドの例になっていたのでした。