檜山正幸のキマイラ飼育記 このページをアンテナに追加 RSSフィード Twitter

キマイラ・サイトは http://www.chimaira.org/です。
トラックバック/コメントは日付を気にせずにどうぞ。
連絡は hiyama{at}chimaira{dot}org へ。
蒸し返し歓迎!
このブログの更新は、Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama
ところで、アーカイブってけっこう便利ですよ。

2017-09-20 (水)

困った時の米田頼み、ご利益ツールズ

| 10:09 | 困った時の米田頼み、ご利益ツールズを含むブックマーク

米田埋め込みはやっぱり役に立ちますね。米田埋め込みを利用するときに便利なツールを幾つか紹介します。それらのツール達は:

  • 関手に使うラムダ記法
  • 米田の星 (-), (-)
  • 関手・自然変換のテンソル積
  • マルチ米田埋め込みのドット記法

内容:

  1. 過去の事例: CPSと確率変数
  2. 困った時の米田頼み、もうひとつの例
  3. 米田埋め込み
  4. ラムダ記法と米田の星
  5. 超巨大圏CATと直積
  6. 関手・自然変換のテンソル積
  7. マルチ米田埋め込みとテンソル積
  8. 前層の圏とマルチ米田埋め込み
  9. おわりに

過去の事例: CPSと確率変数

プログラミングにおいて、継続(continuation)という不思議な概念が登場します。継続を用いたプログラミング技法として、継続渡し方式(CPS; Continuation Passing Style)という何だかヨクワカラナイやり方があります。

継続/継続渡し方式に関わる不可解さは、米田埋め込み(Yoneda embedding)を使って解釈するとだいぶ解消します。

確率論で出てくる確率変数(random variable, stochastic variable)という概念に、僕はフラストレーションを募らせていました。なんなんだ!? アレは。確率変数を米田埋め込みとみなすと、事情はスッキリします。

これらの経験から、米田埋め込みはご利益がある、実にありがたいもんだと感じています。

困った時の米田頼み、もうひとつの例

イライラするくらい謎な現象に出会ったら、背後に米田埋め込みがいないか? と探ってみる。こういう行動様式を「困った時の米田頼み」と呼びましょう。比較的最近、また米田様のご利益に与〈あずか〉る機会がありました。ありがたや、ありがたや。

自然演繹とシーケント計算の関係は、僕が長年興味を持っているテーマのひとつです。ある程度は理解しているつもりなんですが、なんかスッキリしない。説明しろと言われれば出来そうではありますが、バシッと決められないもどかしさを感じてました。

今まで米田頼みをしたことがなかったのですが、「ひょっとしたら」と思って米田埋め込みを探してみました。… ありましたね(ニコ)。これでたぶん、バシッと決められます。でも、今日この話はしません。まだ詰め切れてないので、もう少し考えてからにします。

この記事では、米田埋め込みをより便利に使うための準備をします。ちょっとした記法を導入するだけです。しかし、記法でモノの見方が変わることもあります(「記法バイアスと記法独立な把握: 順序随伴を例として」参照)。

米田埋め込み

Cを圏とします。[C, Set]を、Cから集合圏Setへの関手の圏とします。[C, Set]は圏であり、その対象は関手、射は自然変換です。つまり、|[C, Set]| = Functor(C, Set)、F, G∈Functor(C, Set) に対してホムセットは [C, Set](F, G) = NatTransform(F, G)。同様に、[Cop, Set]は、Cから集合圏Setへの反変関手と自然変換からなる圏です。

米田埋め込みは、y:C→[Cop, Set] という関手です。“埋め込み”と呼ばれるのは、yは充満忠実(ホムセットごとに全単射な)関手であり、対象部分 |C|→Functor(Cop, Set) もup-to-isoで単射*1となるからです。

米田埋め込みの定義を見ておきましょう。まず、A∈|C| に対して、関手 y(A):CopSet を、ホムセットにより次のように定義します。

  • y(A)(X) := (C(X, A) in Set)
  • y(A)(u:X→Y) := (λw∈C(Y, A).(u;w:X→Y) : C(Y, A)→C(X, A) in Set)

上記の定義で、y(A)(X)は(y(A))(X)の意味です。このような書き方はしばしば使われるので慣れてください。二番目で定義されるy(A)(u:X→Y)は、C(u, A)とも書きます。この書き方を使うなら、

  • y(A)(X) := C(X, A)
  • y(A)(u:X→Y) := (C(u, A) : C(Y, A)→C(X, A))

あるいは簡単に、

  • y(A) := C(-, A)

ここで、ハイフンは無名のラムダ変数で、対象も射もハイフンに代入できるものとします。

f:A→B in C のとき、自然変換 y(f:A→B)::y(A)⇒y(B):CopSet を定義できます。記法が煩雑になるのを防ぐために ψ := y(f:A→B) と置きます。ψの成分は、

  • ψX : y(A)(X)→y(B)(X) in Set

これは、

  • ψX : C(X, A)→C(X, B)

というホムセットのあいだの写像です。その定義は:

  • ψX := λv∈C(X, A).(v;f:X→B) : C(X, A)→C(X, B) in Set

ψが自然変換になることは、定義を追いかければ分かります(練習問題)。

さらに、A|→(y(A) = C(-, A))、(f:A→B)|→(y(f)::C(- A)⇒C(- , B):CopSet) という対応が関手であることも分かります(練習問題)。具体的には次が成立します。

  • y(f;g) = y(f);y(g) (右辺のコロンは、自然変換の図式順縦結合)
  • y(idA) = ιy(A)

ここでιFは、関手 F:CopSet が定義する恒等自然変換 F⇒F:CopSet です。

ラムダ記法と米田の星

前節のC(-, A)のように、ハイフン(やアンダースコア)を無名変数とした書き方はよく使われます。ラムダ記号を使えば:

  • C(-, A) = λx.C(x, A)

変数が1個ならハイフンでもいいのですが、複数の変数になるとハイフンではキビシイので、通常のラムダ記号/ラムダ束縛変数も使うことにします。ラムダ束縛変数の使い方に関して、次の規約を設けておきます。

  • X, Yなどの文字は対象を表す。
  • f, gなどの文字は射を表す。
  • x, yなどの文字は対象も射も表す。

例えば、λX.C(A, X)は共変のホム関手の対象部を表し、λ(x, y).C(x, y)は反変・共変の二項ホム関手全体を表します。

さて、A∈|C| で定義される反変関手をAで表すことにします。つまり:

  • A := λx.C(x, A) : CopSet

上付きの文字はアスタリスクではなくて漢字の「米」です。米田の米〈よね〉からです。下付きの米は次のように定義します。

  • A := λy.C(A, y) : CSet

こちらは共変関手(opが付いてない)です。

f:A→B に対して、f:A⇒B:CopSet は前節で定義した自然変換です。つまり:

  • (-) = y = (米田埋め込み)

同様に、(-)Cop→[C, Set] という関手で、余米田埋め込み(coYoneda embedding)とでも呼ぶべきものです。次の点に注意してください。

  • (-) = y共変関手 C→[Cop, Set] であるが、この共変関手の特定の値 A:CopSet反変関手である。
  • (-)反変関手 Cop→[C, Set] であるが、この反変関手の特定の値 A:CSet共変関手である。

上付き/下付きで使う'米'を米田の星(Yoneda star, Yoneda asterisk)と呼ぶことにします。口頭では「うえヨネ」「したヨネ」と発音すればいいでしょう。

超巨大圏CATと直積

“圏の圏”を通常Catと書きますが、これは“小さな圏の圏”です。例えば、SetCatの対象になりません。CATを必ずしも小さくない(ただしホムセットは小さい*2)圏の圏だとします。Set∈|CAT| が成立するとします。また、Cat∈|CAT| であり、同時に CatCAT(充満部分圏)でもあるとします。

CATは存在するのか? そんなものを考えていいのか? という疑問はありますが、ここは楽観的に「あれば便利だから、あることにしちゃえ」という方針でいきます。僕はよく知らないのですが、集合論に強い公理を付け加えれば、CATを合理化できるようです。

この記事内では、集合A, Bの直積を一時的にA¥odotBと書きます。その理由のひとつは、Setを他のモノイド圏 V = (V, ¥odot, I) に取り替えても成立する議論をするからです。'¥odot'は、直積かも知れないし、他のモノイド積かも知れない、という含みがあります。もっと切実な理由は、'×'を使うと混乱してしまう危険があるからです。

記号'×'は、圏CAT内での“圏の直積”/“関手の直積”のために使います。C, DCAT に対して、C×Dは直積圏です。また、F:CC', G:DD' in CAT に対して、F×Gは関手の直積で、

  • F×G:C×C'D×D'
  • (F×G)(A, B) = (F(A), G(B))
  • (F×G)(f:A→B, f':A'→B') = (F(f:A→B), G(f':A'→B'))

ホムセットに関して次の等式が成立します。

  • (C×D)((A, B), (X, Y)) = C(A, X)¥odotD(B, Y)

もう一度繰り返しますが、'×'はCATにおける圏の直積/関手の直積で、'¥odot'はSetにおける集合の直積/写像の直積です。慣れてしまえば、どちらも'×'と書いても大丈夫ですが、当面(たぶんこの記事内だけ)は区別します。

関手・自然変換のテンソル積

F:CSet, G:DSet を2つの関手とします。新しい関手F¥otimesGを次のように定義します。

  • F¥otimesG := λ(x, y).F(x)¥odotG(y) : C×DSet

これは、次のように書いても同じです。

  • (F¥otimesG)(x, y) := (F(x)¥odotG(y) in Set)

もっと丁寧に書くと、(A, B)∈|C×D| に対しては、

  • (F¥otimesG)(A, B) := (F(A)¥odotG(B) in Set)

そして、f:A→C in C, g:B→D in D に対しては、

  • (F¥otimesG)(f, g) := (F(f)¥odotG(g):F(A)¥odotG(B)→F(C)¥odotG(D) in Set)

別な書き方として:

  • F¥otimesG := (F×G)*¥odot : C×DSet

ここで、'×'は関手の直積、'*'は関手の図式順結合です。¥odot:Set×SetSet は集合圏の直積で、二項関手です。

F¥otimesGをFとGのテンソル積(tensor product)と呼ぶことにします*3。FとGが値を取る圏がSetでなくても、モノイド圏 V = (V, ¥odot, I) ならば関手のテンソル積を定義できます。

次に、自然変換 α::F⇒H:CSet と β::G⇒K:DSetテンソル積α¥otimesβを定義しましょう。α¥otimesβ::F¥otimesG⇒H¥otimesK:C×DSet となります。具体的には、次の成分を定義すればOKです。

  • ¥otimesβ)(X, Y) : (F¥otimesG)(X, Y)→(H¥otimesK)(X, Y)

関手のテンソル積の定義から、この成分は F(X)¥odotG(Y)→H(X)¥odotK(Y) なので、次のように定義できます。

  • ¥otimesβ)(X, Y) := (αX¥odotβY : F(X)¥odotG(Y)→H(X)¥odotK(Y) in Set)

この定義が、実際に F¥otimesG⇒H¥otimesK:C×DSetという自然変換を定義することを確認するのは練習問題。

以上に定義した関手・自然変換のテンソル積は、任意の関手・自然変換に定義できるものではありません。値を集合圏(他のモノイド圏でもいいけど)に取る関手とそのあいだの自然変換に対してだけ定義できます。

この節で定義した“テンソル積”に対する適切な定式化は、おそらくラックス・モノイド関手*4でしょう。ラックス・モノイド関手については次の記事を参照してください。

Catを“小さい圏の圏”として、C∈|Cat| に対して F(C) := [C, Set] とします。Cが小さくても関手圏[C, Set]が小さいとは限りません(つうか、大きくなります)。F:CD in Cat に対して、F(F):F(D)→F(C) in CAT が引き戻しとして定義できるので、Fは反変関手 F:CatopCAT になります。

先に定義した“テンソル積”は、¥otimesC,D:F(CF(D)→F(C×D) という二項関手の族になります。¥otimesC,D達は、結合律を満たします。

Jを自明な圏(単一対象と恒等だけからなる圏)とします。F(J) = [J, Set] ¥stackrel{¥sim}{=} Set です。ε:JF(J) を、Jの単一対象にSetの単元集合を対応させる関手とします。εがラックス・モノイド関手としての単位となります。

CatCATも直積に関するモノイド圏とみなして、F:CatCAT¥otimesC,Dとεが、ラックス・モノイド関手を構成するようです。

マルチ米田埋め込みとテンソル積

Cの米田埋め込みは、C→[Cop, Set] という関手でした。複数の圏 C1, C2, ..., Cn に対して、次の形の米田埋め込みも考えられます。

  • C1×C2×...×Cn→[C1op×C2op×...×Cnop, Set]

これは、C = C1×C2×...×Cn と置いてしまえば通常の米田埋め込みと変わりませんが、それでも複数の圏が介在する状況を調べておく価値はあります。

C1×C2×...×Cn→[C1op×C2op×...×Cnop, Set] の形をした米田埋め込みをマルチ米田埋め込み(multi-Yoneda embidding)と呼ぶことにします。ここでは、n = 2 のケース、2つの圏C, Dに対する C×D→[Cop×Dop, Set] を考えます。

通常の米田埋め込み y:C→[Cop, Set] はCに依存するので、(必要があれば)yCと書くことにします。yC×Dを考えると:

  • yC×D:C×D→[(C×D)op, Set]

(C×D)op = Cop×Dop なので、次の形になります。

  • yC×D:C×D→[Cop×Dop, Set]

yC×Dの具体的な形を調べることで、次の公式を示しましょう。

  • (A, B) = A¥otimesB
  • (f, g) = f¥otimesg

米田の星(-)yと同じ意味でした。

  • (A, B) = yC×D(A, B)
  • (f, g) = yC×D(f, g)

(A, B)∈C×D に対して実際に計算してみます。

(A, B) = λ(x, y).(C×D)((x, y), (A, B))
         = λ(x, y).C(x, A)¥odotD(y, B)
         = λ(x, y).A(x)¥odotB(y)
         = A¥otimesB

次に、f:A→C in C, g:B→D in D として、(f, g)とf¥otimesg を計算してみます。X, Y∈|C×D| として、自然変換の(X, Y)成分を考えます。

  • (f, g)(X, Y) : (A, B)(X, Y)→(C, D)(X, Y)
  • (f¥otimesg)(X, Y) : (A¥otimesB)(X, Y)→(C¥otimesD)(X, Y)

先の計算から:

  • (A, B)(X, Y) = (A¥otimesB)(X, Y) = C(X, A)¥odotD(Y, B)
  • (C, D)(X, Y) = (C¥otimesD)(X, Y) = C(X, C)¥odotD(Y, D)

(v:X→A)∈C(X, A), (w:Y→B)∈D(Y, B) だとして、

 (f, g)(X, Y)(v, w)
= (v, w);(f, g)
= (v;f, w;g)

 (f¥otimesg)(X, Y)(v, w)
= (fX¥odotgY)(v, w)
= (fX(v), gY(w))
= (v;f, w;g)

よって、(f, g) = f¥otimesg が成立します。

2つの圏に関するマルチ米田埋め込みを考えましたが、より一般に、マルチ米田埋め込みの値(埋め込んだ先)はテンソル積で展開できます。

  • (A1, ..., An) = A1¥otimes ... ¥otimesAn
  • (f1, ..., fn) = f1¥otimes ... ¥otimesfn

前層の圏とマルチ米田埋め込み

米田埋め込みの余域となる圏は[Cop, Set]です。この圏は、C前層の圏(category of presheaves)と呼ばれます。CopSet という関手を前層(presheaf)と呼ぶからです。

[C, Set]は単なる(共変の)関手の圏ですが、余前層の圏(category of copresheaves)と呼ぶことがあります。単なる関手をわざわざ余前層と呼ぶのもどうかな? と思いますが、シュルマン(Mike Shulman)は「余前層」がふさわしい文脈があるのだ、と言ってました。

さて、Cの前層の圏は頻繁に登場するので、毎回[Cop, Set]と書くのは面倒です。略記を導入します。Cにハットを載せた記法をたまに見ますが、ここでは右肩にドットを付けることにします。

  • C := [Cop, Set]

この記法を使うと、米田埋め込みは次のように書けます。

  • y:CC

マルチ米田埋め込み C×C→[Cop×Cop, Set] は次のように書きます。

  • y●●:C2C●●

[(Cop)n, Set]を表すのに、Cの右肩にドットをn個載せることにして、対応するマルチ米田埋め込みもyのの右肩にドットをn個載せて表します。

余前層の圏への余米田埋め込みは y:CC と下付きドットにします。この記法の応用として、共変と反変が混じった米田埋め込みも簡略に記述できます。例えば、

  • y : C×CopC (ここで、C = [Cop×C, Set])

yは、米田の星とテンソル積で次のように書けます。

  • y(A, B) = A¥otimesB
  • y(f, g) = f¥otimesg

おわりに

今回紹介したツール達は、前層の圏・余前層の圏・米田埋め込みを扱う際に重宝するものです。「困った時の米田頼み」で、米田様にお願いするとき、これらのご利益ツールズがあると、ご利益にありつくチャンスが増えると思います。

*1:関手 F:CD の対象部分がup-to-isoで単射とは、(F(A)¥stackrel{¥sim}{=}F(B) in D) ⇒ (A¥stackrel{¥sim}{=}B in C) なことです。

*2:ホムセットも小さくない圏を扱いたいときもありますが、今回はそこまで大きな圏は登場しないので、局所小(locally small)の条件を入れておきます。

*3:「テンソル積」があまりにも多用されるので、この言葉を使うことに躊躇はあったのですが、それ以外に適切な呼び名が思い浮かばない。

*4:ラックス・モノイド関手は、関手を台(underlying thing)とするモノイド類似代数系なので、ラクソイド(laxoid)とか呼ぶべきじゃないかと思う今日このごろ。