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

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

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

［参照用 記事］

アイレンベルグ／ムーア圏 その2:リストモナドのとき

雑記／備忘

「アイレンベルグ／ムーア圏 その1」において、アイレンベルグ／ムーア圏の定義をいちおうは述べたので、実例を挙げましょう。（[追記]List.map総称関数の型パラメータが間違っているなー、後で直す。[/追記]）（[さらに追記]直しました。[/さらに追記]）

内容：

リストモナド

アイレンベルグ／ムーア構成が一番鮮明な形で見えるのは、リストモナドの場合じゃないかと思います。

一般に、圏C上のモナドを (M, η, μ) と書くことにします。ここで、M:C→C、η::IdC⇒M:C→C、μ::(M;M)⇒M:C→C。リストモナド（クリーネスターモナド）を、プログラマに馴染み(?)の記法で定義するなら次のようでしょう。

  1. C := Set
  2. M0(A) := List<A>
  3. M1(f:A→B) := List.map<A, B>(f):List<A>→List<B>
  4. ηA := List.single<A>:A→List<A>
  5. μA := List.flatten<A>:List<List<A>>→List<A>

List.map はいわゆるマップ関数、List.single は要素に長さ1のリストを対応させる関数、List.flatten は入れ子リストを平坦化する関数です。もう少し補足説明を加えると：

  • 集合圏の対象を型、集合圏の射を純関数として扱います。
  • M0は、関手Mの対象部分（object part）です。つまり、M0:Obj(Set)→Obj(Set)。
  • M1は、関手Mの射部分（morphism part）です。つまり、M1:Mor(Set)→Mor(Set)。
  • List<-> は型構成子です。
  • List.map<-, ->(-) は総称の高階関数で、< , > の中に型パラメータを2つ入れて、( ) の中に関数引数を入れます。型パラメータがAとB、引数がfのとき、List.mapの値は List<A>→List<B> という関数です*1。
  • List.single<-> は総称関数です。型パラメータをAに具体化すると、A→List<A> という関数が（値として）得られます。
  • List.flatten<-> は総称関数です。型パラメータをAに具体化すると、List<List<A>>→List<A> という関数が（値として）得られます。

集合（型と言っても同じ）Aの要素をn個並べたリストを [x1, ..., xn] のような形で書くことにします。長さnのリストの全体を An と書きます。このときの上付き添字のnは直積累乗の指数と思ってかまいません。An = A× ... ×A (n個の直積) 。特に、A0 = {[]}, A1 = {[x] | x∈A} です。

集合の直和を + で表すと、リストモナドの型構成子は次のように書けます。

  • M0(A) = List<A> = A0 + A1 + A2 + ...

右辺の無限級数表示を、Aのクリーネスターと呼びます。よって、リストモナドとクリーネスターモナドは同じものです。

リスト関手の余タプル表現

(M, η, μ) が圏C上のモナドのとき、M代数とは、Cの対象Aと、a:M(A)→A という射の組 (A, a) で、ある条件を満たすものでした（「アイレンベルグ／ムーア圏 その1」参照）。

リストモナドの場合にモナドの代数を考えましょう。(A, a) がリストモナドの代数であるとは、A∈|Set|、a:List<A>→A in Set のことです。（条件については後で考えます。）List<A> をクリーネスターの形に展開すると、関数aは、

  • a: (A0 + A1 + A2 + ...) → A

となります。関数aの域は無限直和ですが、各直和成分ごとに考えればいいわけです。関数aを集合An（直和成分）に制限したものをanと書きましょう。つまり：

  • a0:A0→A
  • a1:A1→A
  • a2:A2→A
  • a3:A3→A
  • ...

となります。もとの関数aは、a0, a1, a2, a3, ... 達の無限余タプルで与えられます。余タプルの表現は [a0, a1, a2, a3, ...] の形を使うことが多いですが、既にリストの意味で使ってしまったので、ユニオン演算子の縦棒を使って次のように書くことにします。

  • a = (a0 | a1 | a2 | a3 | ...)

モナドの代数の単位律

(A, a) が、モナド (M, η, μ) の代数であるとは、単に a:M(A)→A in C なだけではダメです。まずは、次の図式が可換になる必要があります。

  A - η_A --> M(A)
  |            |
  |            a
  |            |
  v            v
  A ---------> A

何も書いてない矢印は恒等で、冗長な図式となっているので、等式で書いたほうがコンパクトです。

  • ηA;a = idA

リストモナドの場合に、この等式は次のように書けます。

  • for-all x in A { a(List.single<A>(x)) = x }

List.single<A>(x) = [x] ですから、より簡略に書けば：

  • a([x]) = x

[x] は長さ1のリストなので、クリーネスターのA1の部分に入ります。aのなかで長さ1のリストに働く部分はa1なので、次のようにも書けます。

  • a1([x]) = x

モナドの代数の結合律

さらに、次の図式の可換性も要求されます。

  M(M(A)) - M(a) --> M(A)
   |                  |
  μ_A                a
   |                  |
   v                  v
  M(A) ----- a -----> A

等式で書けば：

  • M(a);a = μA;a

リストモナドの場合に具体的に書き下してみると：

  • for-all lislis in List<List<A>> { a(List.map<List<A>, A>(a)(lislis)) = a(List.flatten<A>(lislis)) }

lislisは、[lis1, lis2, ..., lisn] のような形のリストで、リストの各成分がList<A>の要素、つまりフラットリストになっているものです。lislisは入れ子のリストということです。

上の等式のいわんとしていることは； 入れ子のリストlislistの各成分に演算aをほどこして得られたフラットリストに再度演算aを適用した結果（左辺）と、入れ子のリストlislisをまず平坦化してしまい、得られた長いリストに演算aを適用した結果（右辺）が同じ、ということです。

なんだか分かりにくいですね。演算aのクリーネスター表示を考えて、a0, a1, a2, a3 あたりを考えると事情がハッキリします。

短いリストで確認する

一般的な等式 a(List.map<List<A>, A>(a)(lislis)) = a(List.flatten<A>(lislis)) を理解するために、長さが短いリストに関して具体例を試してみます。

まず、代数演算aの長さ0リストの部分 a0:A0→A に対して、a([]) = e と置きます。e∈A で、eは定数だと考えてかまいません。次に、代数演算aの長さ1リストの部分 a1:A1→A は、a1([x]) = x だったので、事実上a1は何もしない操作になります。

lislis = [[], [x]] という入れ子リストに関して a(List.map<List<A>, A>(a)(lislis)) = a(List.flatten<A>(lislis)) を考えると：

  • a(List.map<List<A>, A>(a)([[], [x]])) = a(List.flatten<A>([[], [x]]))

List.mapとList.flattenの定義から：

  1. List.map<List<A>, A>(a)([[], [x]]) = [a0([]), a1([x])] = [e, x],
  2. List.flatten<A>([[], [x]])) = [x]

これらを使えば：

  • a2([e, x]) = a1([x]) = x

同様にして：

  • a2([x, e]) = a1([x]) = x

a2([x, y]) = x・y という記法を使ってみると次のようになります。

  1. e・x = x
  2. x・e = x

つまり、左単位律と右単位律です。

さて、lislis = [[x, y], [z]] ならどうでしょうか。

  • a(List.map<List<A>, A>(a)([[x, y], [z]])) = a(List.flatten<A>([[x, y], [z]]))

List.mapとList.flattenの定義から：

  1. List.map<List<A>, A>(a)([[x, y], [z]]) = [a2([x, y]), a1([z])] = [a2([x, y]), z]
  2. List.flatten<A>([[x, y], [z]]) = [x, y, z]

これらを使えば：

  • a2([a2([x, y]), z]) = a3([x, y, z])

同様にして：

  • a2([x, a2([y, z])]) = a3([x, y, z])

これらより：

  • a2([a2([x, y]), z]) = a2([x, a2([y, z])])

a2([x, y]) = x・y という記法を使ってみると：

  • (x・y)・z = x・(y・z)

そう、結合律ですね。a3([x, y, z]) は、公平な（unbiased）3項演算だったのです。左から先に2項演算しても、右から先に2項演算しても、どちらも公平に3項演算したのと同じだよ、ってのが結合律なのです。

a4, a5, ... などに関してもn項演算に関する結合律が得られます。それらの結合律を一挙に表現している等式が a(List.map<List<A>, A>(a)(lislis)) = a(List.flatten<A>(lislis)) だったのです。

結局、リストモナドの代数って

(A, a) がリストモナドの代数のとき、a:List<A>→A は、0項演算a0、1項演算a1、2項演算a2、3項演算a3 など寄せ集めたもので、a = (a0 | a1 | a2 | a3 | ...) という無限余タプル、あるいはクリーネスターの形で書けるのでした。

モナド代数の単位律から、a1([x]) = x が出てきます。a0([]) = e, a2([x, y]) = x・y と置くと、モナド代数の結合律から次の等式が出てきます。

  1. e・x = x・e = x
  • (x・y)・z = x・(y・z)

つまり、リストモナドの代数 (A, a) とは、普通のモノイド (A, e, ・) に過ぎなかったのです。あまり厳密には示してませんが、通常のモノイドの定義では、a0とa2しか使わないのに対して、a:List<A>→A では、すべてのn項演算を全部同時に考えてしまう方式になっているのです。すべてのn項演算の表現には通常、総和記号や総積記号が使われ、それはモナドに深く関係します。「総和と総積の記号法」を参照してください。

以上のことから、リストモナドのアイレンベルグ／ムーア圏 EM(Set, List) は、集合圏内のモノイドの圏 Mon(Set) と同じ（圏同値）になることがわかりました。


お馴染みのモナドのアイレンベルグ／ムーア圏を作るとお馴染みの圏が出てきましたよっ、というオハナシでした。

*1:関手を、ホムセットごとに定義していることになります。