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

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

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

参照用 記事

モナドとテンソル強度の楽しいお絵描き

「モナドとテンソル強度のサンプル」にて:

テンソル強度(tensorial strength)関連の絵算が楽しいので説明しようと思ってるんですが、テンソル強度自体の定義や実例なしで計算方法を示しても面食らっちゃいますよね。で、実例を挙げます。今日は典型的な例を2つ。もっと面白い例を後日紹介するつもりです(つもり、ね)。

追加の例について書いてないけど、まーいいや、楽しい(?)絵算いってみましょう。

内容:

前置き

圏の対象はa, bなどの英小文字で表します。(C, +, 0)がモノイド圏、F:C→C はCの自己関手、(F, μ, η)がC上のモナドになっているとします。「モノイド圏を自己関手の圏に埋め込む」で導入した、Haskellのセクション風の書き方を使います。これを復習しておくと:

  • (a+) := λx.(a + x)
  • (+a) := λx.(x + a)

ここでxは対象でも射でもかまいません。(a+), (+a) はモノイド圏C上の自己関手になります。

(a+), (+a) の括弧を外して a+, +a とも書くことがあります。つうか、以下ではだいたいこの書き方を使います。混乱の恐れも若干ありますが、括弧が面倒なので(どこまでモノグサなんだ>自分)。

以下で目標とすることは、τとτ'がモナド(F, μ, η)に対するテンソル強度*1のとき、τとτ'から構成されるペアリングが結合律を満たすことです。用語と記号の意味は計算の途中で随時説明します。計算はEnd(C)のなかの絵算を使います。サイズを調整してない原寸大の絵(手描きスキャン画像)を挿入しているので見づらいかもしれません。(とりあえず、width="600" を入れてみた。)「画像のみ」というリンクをたどると絵だけ表示されます。

ペアリングの定義

K = Kl(F, C) を圏C上のモナドFのクライスリ圏だとします。ベースの圏Cに備わっているモノイド積+をクライスリ圏Kまで持ち上げたいわけ。対象に関してはCのモノイド積をそのまま使うので特にやるべきことはありません。Kの射(クライスリ射)に対する積の定義が問題。

f:x→a in K をC内で見れば、f:x→F(a) です。f:x→F(a) と g:y→F(b) に対してうまいこと f#g:x+y → F(a+b) を定義して、それをクライスリ圏のモノイド積としたいのです。このとき、a, bに応じて決まる πa,b:F(a)+F(b)→F(a+b) を使って、f#g := (f+g);π とします。

以上の状況を絵にまとめておきます。絵の中では、F(a)の括弧も省略してFaと書いています(もうほんとにモノグサ)。

画像のみ

πは、a, bを添字とする射の族(indexed family of morphisms)です。このπをペアリングと呼びます。πを使って定義された f#g も、「fとgのペアリング」と呼ぶこともあります。クライスリ圏に行って見れば、f#g はモノイド積です -- いや、モノイド積になるようにこれからガンバルのです。

目標は結合律

(f#g)#h = f#(g#h) という結合律を f#g := (f+g);π という定義を参照しながら絵に描き下すと次の図の上半分のようになります。

画像のみ

この結合律の成立には、f, g, h は実はどうでもよくて、πの性質だけが必要です。おおよそ (π+id);π = (id+π);π という関係が成立すればいいわけです。それを描いたのが上図の下半分です。

絵算の準備

これからの計算(絵算です)はすべて、End(C) = CC のなかで行ないます。つまり、ワイヤー(紐)は関手を表し、箱やノードは自然変換を表します。Cの対象と射を、End(C)のなかに持ち込むには、「モノイド圏を自己関手の圏に埋め込む」で述べた方法を使います。対象aはスタンピング関手(+a)(モノイド積による掛け算)、射はスタンピング関手のあいだの自然変換として解釈されます。

問題は、テンソル強度τ、τ'をどのように解釈するかです。τとτ'は次の形をしています。

  • τa,b:F(a)+b → F(a+b)
  • τ'a,b:a+F(b) → F(a+b)

τに出てくるbを固定してaを変数と思いましょう。変数らしくxに書き換えます。τ'ではaを固定してbを変数と思いましょう。変数らしくyに書き換えます。

  • τx,b:F(x)+b → F(x+b)
  • τ'a,y:a+F(y) → F(a+y)

そして、次のような射の集まりを考えます。

  • x,b:F(x)+b → F(x+b) | x∈|C|}
  • {τ'a,y:a+F(y) → F(a+y) | y∈|C|}

これらは、次のような変換(この時点で自然かどうかは分からない)になります。

  • F;(+b) ⇒ (+b);F : C→C
  • (a+);F ⇒ F;(a+) : C→C

ここで、記号「;」は関手の図式順(左から右への)結合ですが、関手圏 End(C) = CC 内では「;」を非対称なモノイド積と考えます。これらの変換は、スタンピング関手とモナドの関手を入れ替える操作とみなされます。

今述べた手順で作られた F;(+b) ⇒ (+b);F と (a+);F ⇒ F;(a+) が自然変換でないと困るので、τ, τ'の条件としてこれらが自然であることを要求します。

ちょっと言い訳と世迷い言:「困る」と書いたのですけど、ほんとに困るかどうか? 確証はないです。自然性がなくてもけっこうイケそうな気もします。また、テンソル強度の通常の条件(公理)では、自然性がハッキリしません。たぶん導出できそうですが、それもハッキリしません。とりあえず自然性を要求しておけば無難だし、実例でも自然変換になっているし、という事情で上のように書いた次第です。

まだ絵算の準備

ベース圏Cのモノイド演算、モナド演算(乗法μと単位η)、テンソル強度τ, τ'が混じった計算をするときは、その下ごしらえが大変です。モナドの乗法μや単位ηは自己関手圏End(C)に棲んでいるので、モノイド演算(今回は+と0という記号)もテンソル強度も自己関手圏に引越しさせる必要があります。すべての関係者が同じ圏のなかにいないと計算できませんからね。

で、もう少し下準備。前節とは逆に、x, yを変数として次のような射の族を考えます。

  • τa,y:F(a)+y → F(a+y) (y∈|C|)
  • τ'x,b:x+F(b) → F(x+b) (x∈|C|)

これらは、次のような変換になります。

  • (F(a)+) ⇒ (a+);F
  • (+(F(b)) ⇒ (+b);F

今後の計算では、τを F;(+b) ⇒ (+b);F の形で使い、τ'を (+(F(b)) ⇒ (+b);F の形で使います。セクション記法の括弧と引数を囲む括弧を省略して、「;」は空白を使って推論図風に書くと次のようです。

    F   +b
  --------- τ
   +b   F


    +Fb
  --------- τ'
   +b   F

絵算で使うノード

関手圏における絵算では、ワイヤーは関手を表します。箱やノードは自然変換でした。今回の計算では4種類のノードを使うので、それらを次の記号で区別することにします。

画像のみ

τ'(左から1番目)とτ(左から3番目)については説明しました。μ(右)はモナド乗法です。左から2番目の黒丸は、(+a);(+b) ⇒ (+(a+b)) という自然変換ですが、これはモノイド積の結合律を与える自然変換に他なりません。

絵算で使う法則

必要な計算法則を並べます。

画像のみ

一番上はモノイド積(記号は+)の結合律を関手圏のなかで表現したものです。その下はモナド乗法の結合律。残りの2つはテンソル強度の公理で、紐の接合点が交差を通り抜けることを許しています。

いよいよ絵算を実行

ペアリング(の成分)πa,bは、F(a)+F(b)→F(a+b) という形をしています。変数xを足して、x + F(a)+F(b)→ F(x+a+b) とも書けます。これを変数xに関する関手のあいだの変換とみなすと (+Fa);(+Fb) ⇒ (+(a+b));F となります。ペアリングをこの形で定義する絵は次のとおり。

画像のみ

上の絵をπa,bの定義として、(π+id);π と (id+π);π を書き下してみれば次のよう。

画像のみ

これでもう出来たも同然; 前述した法則を使って、この絵の左から右、右から左へと変形するのは図形変形の練習です(中間の図形を設定するといいかも知れません)。左単位律と右単位率も同様に示せます。

*1:テンソル強度は、モナドとは限らない単なる自己関手 T:C→C に対しても定義できます。ここでは、モナドに関するテンソル強度だけを考えます。