購読中です 読者をやめる 読者になる 読者になる

Just $ A sandbox

プログラミングとかPCとかの技術的なメモ

ワンナイト人狼の基本戦略

ワンナイト人狼とは

ワンナイト人狼は一夜で決着が着く人狼(ジャンルとしては多人数推理ゲーム)。

ワンナイト人狼のルール

ゲームは3~5人向けだが、今回は4人でプレイするとして解説をする。
初めに6枚のカードを用意する。
内訳は「人狼2枚、村人2枚、占い師1枚、怪盗1枚」

1. 6枚のカードをよく混ぜ、一人1枚ずつカードを配る。余った2枚は中央に伏せる。
2. 各自、自分のカード(役職)を確認後、全員が顔を伏せる。
3. 占い師のターン: 占い師は以下のいずれかの行動を起こす。 A)自分以外の3人のカードのうち1枚のカードを確認する B)中央の2枚のカードを確認する
4. 人狼のターン: 人狼は顔を上げ、仲間を確認する。
5. 怪盗のターン: 怪盗は自分以外の3枚のカードのうち1枚と自分のカードを交換する。交換後、交換したカードが何の役職であるかを確認する。
6. 全員が顔を上げ、規定の時間話し合いを行う。
7. 1人ずつ、処刑したい人を選び全員で投票を行う。投票は自分には出来ない。
8. 投票の結果、最多票で2票以上を獲得した人(複数人いれば全員)を処刑し、勝敗の判定を行う。

勝利条件:

  • (村人・占い師・怪盗) 4人の中に人狼が入れば、人狼を1人でも処刑すれば勝利。投票終了時に自分が生きている必要はない。人狼がいなければ全員の投票をばらけさせることで全員勝利となる。
  • (人狼) 人狼が1人も処刑されなければ勝利。

基本戦略

基本的には、「村人っぽい」発言をしていると村人から信頼される可能性が高くなる。
ワンナイト人狼ではほぼ村人の投票で勝敗が決するので、村人は正しい人にいれること、非村人は村人から信頼を得ることが非常に重要です。

人狼の場合

二人人狼の場合

ABCDの4人の村で、AとBが二人人狼とする。このときとれる戦略としては以下の2つが簡単だが、圧倒的に(1)の方が勝ちやすい。

(1) Aが占い師を騙り、Bが村人を騙る。C=真占がいる場合は、Bが上手くDを誘導し、A→C、C→A、B→A、D→Cの投票にさせてBが裏切ればよい。Aの占いの内容は「中央の2枚を見て1枚人狼だった」が無難だが、「Bが村人」でもよい(ただしこれはグルを疑われやすい)。適当な人への村人認定は、認定する相手が占い師だと詰むので注意。
(2) AとBは平和村になるように騙りをする。占い師や怪盗がでなければAとBで騙る。ただし、白怪盗や占い師が潜伏している場合は平和村を扇動すると非常に怪しまれるので、その場合は(1)のパターンに持ち込む必要が出るかも。

一人人狼の場合

一人人狼の場合は真占いに占われたりするとあっさり負ける可能性が高いので一人で勝つのはかなり難しい。

(1) 村人のフリに徹する。占い師に占われたら(2)の場合に行くしかない。
(2) 自分が一人人狼であることをバラし、怪盗が自分とすり替えたと主張する。上手く行けば処刑を免れることもあるが、両吊りにされて終わる可能性が高い。

占い師の場合

基本的には1でよいが、対抗占いも怪盗も出ない場合は2でも可。

(1) 本当のことを言う。
(2) 占った結果を偽って報告する(中央の2枚を見て、誰かを人狼認定する等)。この場合も疑われれば自分と誰かの両吊りを提案すれば良い。占い師も村人同様情報がないと詰むので、人狼側から情報が出やすくなるように誘導することは有効。

村人の場合

ワンナイト人狼では村人の騙りがOKとなっているので、これを有効に使う。
村人にとっては、「何も情報がない」ことが最も危険な状況である。

(1) 普通に推理する。情報が出ない(しばらく待っても怪盗・占い師が出ない)場合は(2)も有効。
(2) 占い師を騙り、人狼に関する情報を出す(人狼はn枚ある、この人が人狼etc)。対抗が出れば素直に本当のことを言って、怪しい人物と両吊りにしてもらう。

怪盗の場合

白怪盗の場合

白怪盗というのは、村人サイドのカードと入れ替えた怪盗の場合。
この場合は戦略などなく、正直に情報を出すのが一番。

黒怪盗の場合

(1) 村人のフリをする。これでまず村人から疑われることはない。人狼が2人いることが確定すれば、(3)に行くとよい。
(2) 白怪盗を騙り、誰かを白認定する。対抗がいなさそうであれば占い師を騙ることも有効。
(3) 黒怪盗であることをバラすが、このとき誰と入れ替えて人狼であったかは言わない。人狼は黒怪盗を処刑できないので、二人人狼であればあなたが負けることはない。

難易度ランキング

超個人的な経験に基づく勝利難易度ランキング:

(難) 一人人狼>黒怪盗>>>村人>占い師≒白怪盗>二人人狼 (易)

どうでもいい話

上のことは大体個人的な経験に基づく話なので、必ずしもこれが正しいわけではありません。
普通に遊んでいると上の要素が複数絡んでくるので推理はもっと難しいです。

ただし、ワンナイト人狼は上のような基本戦略を抑えている人とそうでない人で実力差が激しいゲームなので、プレイの前には理解しておいた方がいいと思います。

個人的な意見では黒怪盗COして勝つのが一番楽しいです。

Linuxで音声読み上げ

ゆっくりしていってね

棒読みちゃん

# ~/.wine32に32bit環境のprefixを作っておく
~$ WINEPREFIX=~/.wine32 WINEARCH=win32 wine BouyomiChan.exe

SofTalk

AquesTalk

Open JTalk

Open JTalk

#!/bin/sh
VOICE=/usr/share/hts-voice/nitech-jp-atr503-m001/nitech_jp_atr503_m001.htsvoice

echo $1 | open_jtalk \
-m ${2:-$VOICE} \
-x /var/lib/mecab/dic/open-jtalk/naist-jdic \
-ow $3 \
-ot $4

を保存して実行するといける

  • -owは出力するwavファイル名, -otはログ

MMDAgent メイちゃん

  • http://www.mmdagent.jp/の"Sample Script"のbinary packageをダウンロードし、Voiceの中にあるhtsvoiceファイルを使う
  • open_jtalk -m /path/to/mei_hoge.htsvoiceでOK
  • 割とハキハキしゃべってくれる

他の声

Grothendieck群とBurnside環の定義

局所有限トポス上の離散数学の構築を目指して

という論文で、Burnside環という環を扱っていた.定義は「局所有限トポスの同型類から得られるGrothendieck ring」らしく, これではよく分からなかったので調べた.

Grothendieck

Grothendieck群は可換モノイドから作るAbel群のことで, しかもこの構成はfree functor \(\mathbf{CMon} \to \mathbf{Ab}\)を与えるらしい.\(\mathbb{N}\)から\(\mathbb{Z}\)を作るのと同じ方法で, 可換モノイド\(A\)に対し\(A \times A \)に同値関係を\((a,b) \sim (a',b') \iff \exists k : a + b' + k = a' + b + k\)で定めるとこれは群になる.この群をGrothendieck群という.

ToposとGrothendieck

Toposはlimit, colimitを持つので\(0,1,+,\times\)があって欲しい性質は大体満たしている. (可換半環になっている)ここから環を作るには和に関して可換モノイドを群に拡張してやればよく, 構成は大体上と同じ方法でできる.

Topos \(\mathcal{E}\)に対し, その同型類\(\mathcal{E}/\cong\)を考える. 上と同じ方法によって, \(\mathcal{E}/\cong \times \mathcal{E}/\cong\) (Toposの同型類の2つ組全体)は群になる. \(\mathcal{E}\)にもともと備わっているproductと合わせてこれは環になる.今の場合こうやって得た環をBurnside環と言うらしい.

気になったこととして和と積の分配則ってToposだと成り立つんだっけ?とか思った.よく考えれば(coproductをもつ)CCCでは直積はexponentialの左随伴なのでcolimitを保つのですぐ言える.初め\(A \times (B + C) \cong A \times B + A \times C \)の間の同型射を具体的に構成しようとしたら右から左が作れなくてつらかった.調べたら, 直接的な構成もできるみたいだけどexponentialの方にもっていったりしないといけないらしく大変そうだった.cf. Cartesian closed categories are distributive


Grothendieck群は加群の完全列を使っても定義できるらしい.つまり, 加群の同型類全体を考えて, ここに関係式を\(0 \to A \to B \to C \to 0\)が完全 iff \([A] - [B] + [C] = 0\)で定める. するとこれもAbel群になるというもの. 大体同じことがAbel圏とか三角圏でもできる.

WikipediaによるとGrothendieck群はK-theoryで重要らしい.そ, そうなのかー.

参考文献

美少女と学ぶ圏論(2)

本来ならば図式を交えて説明するべきところを図式を用意していないので非常に分かりにくいです(特に証明の部分など). 自分で可換図式を書きながら議論を追って読まれることをおすすめします.

1.2 SpecialなObjectたち

 レポートをやるというのは話を切り上げるための口実で, 実際ほとんどできていたので仕上げには全然時間がかかなかった.
 ゼミのために買ったホモロジー代数の本をパラパラめくっていると, 導来関手という文字が度々目に入った. そういえば, 千景に渡されたpdfには"関手と自然変換"というセクションがあった. 僕はカバンから紙の束を取り出して机にのせる.
 1.1は圏の定義と例で, 今日話したようなことが載っているだけだった. 1.2に進もう.

Definition\(f : A \to B \)に対し射\(g : B \to A \)が存在して\(f \circ g =1_B, g \circ f = 1_A\)を満たす時, \(f\)を同型射(isomorphism)という. またこのとき\(A,B\)は同型ともいう.

 同型はよく見る定義だ. 写像全単射であることと写像が上の意味で同型であることは同値だから, 上の定義は理解しやすくて良い.
 ただ, 全単射の定義とは違ってdomainやcodomainの元がどうなるかについては触れていない. これが千景の言っていた"元の取れない圏論"なのだろうか. 確かに元に触れずに同型射を定義しているので, なんとなく抽象的な感じはする.

Definition\(f : A \to B \)がepimorphism(epi)であるとは, 任意の\(g \circ f = h \circ f \)を満たす射\(g,h : B \to C \)に対して\(g = h\)が成り立つ.
 このとき\(f : A \twoheadrightarrow B \)とかく.
Definition\(f : A \to B \)がmonomorphism(mono, monic)であるとは, 任意の\(f \circ g = f \circ h \)を満たす射\(g,h : C \to A \)に対して\(g = h\)が成り立つ.
 このとき\(f : A \rightarrowtail B \)とかく.

 epimorphismとmonomorphismはどうやら逆の概念であるらしい. そう, よく見れば上の定義にある\(f,g,h\)の射の"向きを反転"させれば下の定義に一致する. これが千景の言っていた双対に違いない.
 ネットによると, それぞれの射にはエピ射, モノ射という訳が当てられるらしい. 千景は, 双対には"余"という漢字が当てられると言っていたが必ずしもそういうわけでもないのか.

 ところでepiやmonoが何を表しているかをもうちょっとよく考えよう.
 分かりやすいところで写像, つまりSet圏を考えることにする. \(f\)がepiなら, \(g(f(x)) = h(f(x)) \;\; (\forall x \in A)\)のとき\(g = h\)が言える. \(g,h\)\(Im f\)上で一致するなら\(B\)上全体で一致するということで, これが成り立つということは\(f\)全射ということに違いない.
 同じく, \(f\)がmonoなら, \(f(g(x)) = f(h(x)) \;\; (x \in C)\)のとき\(g = h\)だから\(f\)単射になる.
 なるほど, どうやらepiとmonoは全射, 単射に対応するらしい.

 僕は手を止めて紅茶を一口飲んだ. ハーブティーは心を落ち着けてくれる. 温かい紅茶が心に染み入るように, epiとmonoの定義は僕の脳内に染みこんでくるようだ.
 ここに千景がいたら, きっとこんな風に語りかけてくるだろう.
『さぁ, 次はisoについても考えてみよう. 集合では全射かつ単射と同型は同値. ではepiかつmonoとisoは同値?』
 そんな僕の考えを予想しているかのように, 次のページには千景が書いたと思われる走り書きがしてあった.

 isoならばmonoかつepi. しかし逆は成り立たない. 反例は?

 isoならばmonoかつepiは定義から明らかだ. さて, 反例は….


「それで? 反例は見つかったの?」
 午後. 僕はまた, 千景と教室の黒板前にいた. 学部生控室というのは便利なもので, 自由に使える黒板や椅子や机がある. こんなに素晴らしい環境の割には人も少ない.
 僕は昨日考えたことを千景に話すことにした. 人に説明すると, 頭の中も整理される.
「意外なところにあったよ. 群とか加群じゃ見つからなかった」

Counterexample \(X\)を2点以上の位相空間とする. さらに\(X_i\)\(X\)に密着位相を入れたもの, \(X_d\)\(X\)に離散位相を入れたものとする.
 集合として恒等写像である連続写像\(id : X_d \to X_i; \; x \mapsto x \)全単射で, 位相空間の圏の射としてepiかつmono. しかしこの逆写像は連続でないから, 位相空間の圏の射にはならない. よって\(id\)位相空間の圏の中でepiかつmonoだがisoではない.

「よく出来ました. 言ってなかったけど, isoとepiかつmonoが同値になる圏をbalancedという」
「ふむ?」
「一般にAbel圏はbalancedなんだ. だからAbel群や加群では同値になるよ」
「うん, それに気がついてから, 位相空間の圏で探してみたら見つかった」
「他に何か気がついたことはある?」
「そうだな…. posetを圏とみなす, というのをやったよね. この圏では全ての射はepiかつmonoで, isoな対象は等しいことが反対称律から分かる, とか」
「そうだね. それもepiかつmonoだがisoでないような例の一つね」
「あまり面白い反例とは言えないかもしれないけどね」
 千景は満足そうにニヤついて, 僕を見た.
「さて, 先に進もう. 1.2くらいは読んできた?」
「う, うん. でも, 関手と自然変換まではたどり着かなかったよ」
「いや, 別にいいよ. 昨日のアレは言ってみただけ」
 千景は僕にチョークを渡して, 一番前の席についた. 先生ではなく生徒として聞き手に回る, という意思表示. 渡されたチョークはほとんど使ってなくて, 先がほんの少しだけ欠けていた.
「1.2の残りでは圏の特別な対象を定義して, それらの例を見るって感じだね. まずはproduct」

Definition

\(A \xleftarrow{p_A} P \xrightarrow{p_B} B \)が直積(積, product)の図式である, または対象\(P\)がproductであるとは, 以下を満たすことである.

  • (UMP) 任意の\(A \xleftarrow{f} Z \xrightarrow{g} B\)なる図式に対し, \(p_A \circ h = f\)かつ\(p_B \circ h = g\)を満たす\(h : Z \to P \)が一意的に存在する. \(f,g\)から定まる射\(h\)のことを, \(h = \langle f,g \rangle\)と書く.

「ここでいう"一意的に存在する"というのは, 存在して, かつ一意的であるってことね. 条件として2つあるってことに注意してね」
「オッケー. じゃあ双対のcoproductも一緒に定義を述べるよ」

Definition

\(A \xrightarrow{i_A} Q \xleftarrow{i_B} B \)が直和(余積, coproduct)の図式である, または対象\(Q\)がcoproductであるとは, 以下を満たすことである.

  • (UMP) 任意の\(A \xrightarrow{f} Z \xleftarrow{g} B\)なる図式に対し, \(h \circ i_A = f\)かつ\(h \circ i_B = g\)を満たす\(h : Q \to Z \)が一意的に存在する.

「定義はこれだけなんだけど……UMPってなんのことかな?この条件の名前?」
「うん, UMPの説明は特にしてなかったね. UMPはUniversal Mapping Propertyの略で, 簡単に言えば"ある射が一意的に存在する"っていう性質のこと」
「〜の条件を満たす\(h\)が一意的に存在する, って条件のことだね」
「そう. universalityと言ったりもする. productのuniversalityと言えば, 上の条件のことだと思って」
「了解. じゃあもう少し例を続けるよ」

Definition

対象\(0\)が始対象(initial object)とは, 以下を満たすことである.

  • (UMP) 任意の対象\(X\)に対して\(0 \to X \)なる射が一意的に存在する

対象\(1\)が終対象(terminal object)とは, 以下を満たすことである.

  • (UMP) 任意の対象\(X\)に対して\(X \to 1 \)なる射が一意的に存在する

「例は挙げられる?」
「うん」
 昨日ノートにまとめたことを, 黒板に書いていく.

initial object terminal object product coproduct
\(\mathbf{Set}\) 空集合 \(\emptyset\) 1点集合\(\{* \}\) 直積 直和(disjoint union)
\(\mathbf{Top}\) \((\emptyset, \{\emptyset\})\) \((\{* \}, \{\emptyset, \{* \}\})\) 直積空間 直和
\(\mathrm{R}-\mathbf{Mod}\) 1点加群 \(\{0\}\) 1点群 \(\{0\}\) 直積 直和(=直積)
poset \(P\) \(P\)の最小元 \(P\)の最大元 sup(最小上界) inf(最大下界)

「注意としては, 一般に加群の直積と直和は一致しないけど, 今定義した直積と直和が有限(二項)直積/直和しか定義していないからだね. そういえば, 今の定義じゃ二項直積/直和しかないけど, 一般の直積や直和も定義できるのかな…?」
「もちろん. 一般の集合\(I\)上の直積も定義できるよ」

Definition

\(P \xrightarrow{p_i} X_i \; (i \in I)\)または\(P\)が直積とは, 以下の満たすことである.

  • (UMP) 任意の\(Z \xrightarrow{f_i} X_i\)なる図式に対し, \(p_i \circ h = f_i \;\; (i \in I)\)を満たす\(h : Z \to P \)が一意的に存在する.

「表をみていて気がついたことはある?」
「terminal objectとinitial objectが一致する圏があるね. 加群の圏とか, Abel群の圏がそうだね」
「terminal objectとinitial objectが一致する時, それをzero objectという. Abel圏にはzero objectをもつことが要請される」
「確か…加群の圏とかAbel群の圏がAbel圏だったね」
「あとはベクトル空間の圏もね」
「他には, posetではterminal objectが最大元でproductがsupになるんだね」
「posetは例として分かりやすくていいよね. うん, 私も好きだよ」
「じゃあ次に進むよ…って言っても, 次はあんまりピッタリ来る例がないんだけど」
「equalizerとpullbackね. こちらは定義だけやろう, とりあえず後で出てくるまで覚えておいてくれればいいよ」

Definition

平行射\(f,g : A \rightrightarrows B \)に対し, \(e : E \to A \)\(f,g\)のequalizerであるとは, 以下を満たすことである.

  • (図式の可換性) \(f \circ e = g \circ e \).
  • (UMP) 任意の\(z : Z \to A \)\(f \circ z = g \circ z \)を満たすものに対し, \(z = e \circ h \)を満たす\(h : Z \to E \)が一意的に存在する.

Definition

\(A \xleftarrow{q_A} P \xrightarrow{q_B} B \)が図式\(A \xrightarrow{p_A} C \xleftarrow{p_B} B \)のpullbackとは, 以下を満たすことである.

  • (図式の可換性) \(p_A \circ q_A = p_B \circ q_B \).
  • (UMP) 任意の\(z_A : Z \to A, z_B: Z \to B \)\(p_A \circ z_A = p_B \circ z_B\)を満たすものに対し, \(q_A \circ h = f, q_B \circ h = g\)を満たす\(h : Z \to P \)が一意的に存在する.

「coequalizer, pushoutがequalizer, pullbackの双対概念として定義されるよ」
「これらの概念に関していくつか性質を確認しておこう」
「うん」
「じゃあ, 次のことを証明して」

Prop terminal object, initial object, product, coproduct, equalizer, coequalizer, pullback, pushoutは同型を除いて一意的である

「同型を除いて一意的」
「つまり, 2つあったとすると同型になるってことね. 同型を同一視すると存在は一意的ということ. もちろん一般の圏がこれらを持つとは限らないけどね」
「とりあえずterminal objectの一意性をやろうか」

証明 \(1, 1'\)をterminal objectとする. \(1\)のterminal objectのUMPから, \(p': 1' \to 1 \)なる存在する. 同様にして\(p : 1 \to 1'\)も存在する.
 \(p,p'\)が同型, すなわち\(p \circ p' = id_{1'}, p' \circ p = id_{1}\)を示せば\(1 \cong 1'\)であることが分かる.

 \(p \circ p', id_{1'}\)はともに\(1' \to 1' \)なる射であるが, \(1'\)のterminal objectのUMPより\(1'\)に向かう射は一意的である. 即ち\(p\circ p', id_{1'}\)は一致するので\(p \circ p' = id_{1'}\)が分かる. 同様にして\(p' \circ p = id_1\)もわかるので, \(1 \cong 1'\)が示された. (QED)

「これでいいかな? UMPは存在+一意性という2つの条件のことだから, それを上手く使ったよ. 射を作るのに存在を, 射が等しいことを示すのに一意性を使う感じだね」
「うん, オッケー. あとについては大体同じ感じでできるからやっておいて」
「う, うん」
 大体同じ感じ……っていうのはさすがにどうだろう. あとでちゃんとチェックしないと.
「この命題はどうかな?」

Prop \(A \times (B \times C) \cong (A \times B) \times C \)

「直積の結合律だね. 証明は, すぐには思いつかなさそうだなぁ」
「じゃあ, これは私が示そうか. 証明は先と似たような感じでできるよ. ポイントは, UMPを使って射を構成するところと, 一意性から射が等しいことを導くところかな.」

証明 \(A \times (B \times C) \to (A \times B) \times C \)を構成する. \(p^{A \times B}_A : A \times B \to A \)を射影(直積に付随する射)とする.
 \(p^{A \times (B \times C)}_A : A \times (B \times C) \to A \), \(p^{B \times C}_B \circ p^{A \times (B \times C)}_{B \times C} : A \times (B \times C) \to B \)に対し, \(\langle p_A, p_B \circ p_{B \times C} \rangle : A \times (B \times C) \to A \times B \)なる射がある. また, \(p^{B \times C}_C \circ p^{A \times (B \times C)}_{B \times C} : A \times (B \times C) \to C \)と合わせて, \(h_1 = \langle \langle p_A, p_B \circ p_{B \times C} \rangle, p_C \circ p_{B \times C} \rangle : A \times (B \times C) \to (A \times B) \times C \)なる射を得る.

 逆向きの射を作ろう. 上と同じ議論により, \(h_2 = \langle p_A \circ p_{A\times B}, \langle p_B \circ p_{A \times B}, p_C \rangle \rangle : (A \times B) \times C \to A \times (B \times C)\)を得る.

 射が構成できたので, あとはこれらが同型を与えることを見ればよい. すなわち, \(h_1 \circ h_2 = 1, h_2 \circ h_1 = 1\)を示す.

 \(h_2 \circ h_1, 1\)がともに\(f\)に対して\(p_A \circ f = p_A, \; p_{B \times C} \circ f = p_{B \times C}\)という関係式を満たすことを言えば, \((A \times B) \times C \)の直積のUMPを図式\(A\times B \leftarrow (A \times B) \times C \rightarrow C \)に対して使うことで, 射の一意性より\(\langle p_{A\times B}, p_C \rangle = h_2 \circ h_1 = 1\)が分かる.
 \(p_A \circ 1 = p_A, \; p_{B \times C} \circ 1 = p_{B \times C}\)はよいから, \(p_A \circ (h_2 \circ h_1) = p_A, \; p_{B \times C} \circ (h_2 \circ h_1) = p_{B \times C}\)を示す.

\[ \begin{eqnarray} p_A \circ (h_2 \circ h_1) &=& p_A \circ \langle p_A \circ p_{A\times B}, \langle p_B \circ p_{A \times B}, p_C \rangle \rangle \circ h_1 \\ &=& p_A \circ p_{A \times B} \circ h_1 \\ &=& p_A \circ p_{A \times B} \circ \langle \langle p_A, p_B \circ p_{B \times C} \rangle, p_C \circ p_{B \times C} \rangle \\ &=& p_A \circ \langle p_A, p_B \circ p_{B \times C} \rangle \\ &=& p_A \end{eqnarray} \]

 同様にして\(p_{B \times C} \circ (h_2 \circ h_1) = p_{B \times C}\)および\(h_2 \circ h_1 = 1\)も分かる. よって\(A \times (B \times C) \cong (A \times B) \times C \)である. (QED)

「最後は一気にはしょったね」
「ただのdiagram chaseだからね, 自分で手を動かして確かめるしかないよ」
「まぁそれもそうかもね. しかし, 集合の時は元の対応を見るだけで明らかだったのに, 圏だと大変だなぁ……」
「直積が図式を使って間接的にしか定義されないからだね. 基本的にdiagram chaseは大変面倒くさい. でも圏論はなんでもかんでもエレガントにできるわけじゃない. 泥臭いことも勉強の一つ」
「自分で一度証明を追ってみるよ」
「それがいい. ついでにもう一つ宿題を出しておこう」

Prop(宿題)

\[ \begin{array}{c} \bullet & \rightarrow & \bullet & \rightarrow & \bullet \\ \downarrow & (a) & \downarrow & (b) & \downarrow \\ \bullet & \rightarrow & \bullet & \rightarrow & \bullet \\ \end{array} \]

という図式に対して, 以下を示せ.

    1. 左右の四角(a),(b)がpullbackのとき, 全体もpullback
    1. 右の四角(b)と全体がpullbackのとき, 左の四角(a)もpullback

「さてとりあえずこれでspecial objectの話は終わり」
「special object?」
「うん. ここでやった概念は覚えておくといいよ. あとでまた出てくるから」
「なるほどね」
 千景はそう言って, 椅子から立ち上がった. ゆっくりとした足取りで黒板の前に立つ. ぼうっとしている僕からチョークをひったくって黒板に向かった.
「私たちは圏とその上のspecial objectを定義した. まだ話していなかったけど, 関手は圏から圏への変換のことね」
「関手と自然変換って概念があるって言ってたね. 自然変換は?」
「自然変換は関手から関手への変換」
「変換ばっかりだね」
圏論ではこうやって, 色んな物が抽象的に定義されていく. 関手や自然変換がどの意味で"抽象的"なのかはまだ言わないけど, とにかく圏, 関手, 自然変換と進むに連れて, 視点はどんどん広くなるの」
 千景は黒板に不思議な絵を書いた. 一番右下に圏, その上に矢印を引っ張って関手, さらにその上に矢印を引っ張って自然変換と記した.
「けれど, 視点の広さは変えないで, 色んな物をより深く, より精密に見ることもできる」
「どういう意味?」
「例えばspecial objectね. 抽象度は上げないままで, 圏の上で条件をつけたりしながら特別な概念を追求する」
 圏と書かれたところから左に矢印を引っ張って, "special object"と書いた. さらに千景はその下に, "終対象, 直積, equalizer, pullbackなど"と付け足した.
「左に向かうのは理論の緻密さ, 上に向かうのは理論の高さ. 緻密な理論ほど細かい条件に対応できるし, 高い理論ほど抽象的に話が進む」
「ふむ」
 一体彼女は何がいいたいのだろう. いや楽しそうなのはすごく伝わってくるんだけどね.
「じゃあ, 関手くらいの高さで, special objectくらいの緻密さのある概念は何?」
「は?」
「言葉を変えようか. special objectを関手の言葉を使って一般化できるかな. あるいは, 関手の言葉を使ってspecial objectに対応するものは作れるかな」
「えっと, 何を言ってるのかさっぱりわからないんだけど」
「結論から言おう, それにはちゃんと名前がついてる. その説明をする前に……」
 千景はチラッと僕を見た.
「関手と自然変換の定義をしてしまおう. これでようやく, 圏のまともな絵がかける」
「うーん」
 日本語でお願いします. って言いたかったけど, 千景の楽しそうな話に水を差したくなかったので黙っていた.
 攻守交代, 僕は一番前の席に腰掛けて, 千景の話に耳を傾けた. 日暮れ前の空は紫色でなんとも得体の知れない色をしていたけれど, 僕にはそんな空もいつもと同じく綺麗に見えた.

補足

千景が出した"宿題"は, two pullbacks lemmaと呼ばれます. 証明は https://proofwiki.org/wiki/Pullback_Lemma などを参照してください.

美少女と学ぶ圏論

ここまで書いて飽きました.

1章 圏とその構造

1.1 圏の定義と千景の講義

「4月からのゼミはもう決めた?」
「うん. とりあえず,クラスの子とホモロジー代数ゼミをやろうと思ってるよ. 春休みのうちに予習を進めないと」
「ふぅん,ホモロジー代数ね」
 千景は読んでいた本をパタンと閉じて, 勢い良く立ち上がったと思ったら大きく伸びをして, つかつかと足を引っ掛けるようにして黒板の前まで歩き, そのあと立ち止まってからくるりと振り返ってこちらを見た.
「homologyはいいね. 複雑な空間から単純だけど重要な情報を抜き出せる. 複雑に絡み合った網の中の, 本当に大切なものを拾い上げるようにして情報が得られる. homologyはとてもいいよね」
「千景はホモロジー代数もやってるの?」
「必要な時に扱うだけね. Abelian categoryはそんなに詳しくないし」
「あーべりあんかてごりー?」
「そうか, 君はcategory theoryはやってないんだっけ?」
「カテゴリー…あーうん, 圏論か. 聞いたことはあるよ. 触れたことはないけどね. 元がとれないとかなんとか…」
 千景はスッとこちらを見て, ふらふらとした足取りでこちらへやってきた. そして顔を覗きこんでくる.
「圏というのは群とか体と同じような構造の名前. でも, 君のよく知っている構造とは少し違うかな. 圏は群や体よりもう少し広域的な視点なの. 言ってみれば, "群"そのものじゃなく, "群全体の構造"みたいな」
「どういう意味?」
 千景はまた黒板の方に向き直る. 今度はキビキビとした動作で黒板の前を陣取って, チョークを手に持った.
 背が高いとはお世辞にも言えない体では, 一番上から文字を書くのはつらそうだ. けれどそのことを言うと彼女はへそを曲げてしまう. 夕焼けが黒板の左半分を紅く照らしていた. 日暮れ時の風が窓から吹き込んで, カーテンと千景のサラサラした長い髪を巻き上げて逃げていった.
「例えばだけど, 圏の例はそれこそ山ほどあるの. そのうちの一つが群の圏. 圏それ自体は言ってみれば無味乾燥なんだけど, 細かい条件をつけると色々なことができるようになる」
「例えば?」
Abel群の直積と直和は一致する. Abel圏の直積と直和も一致する」
Abel圏はAbel群の一般化ということ?」
「そうね. Abel圏はAbel群や, R加群の圏の一般化. ホモロジー代数が展開できるような圏ってこと. だから重要」
「なるほど」
圏論それ自体が, 他の分野とつながっていることはよくあるの. 今言ったみたいに, Abel圏上ではホモロジー代数ができる. 同じようにホモトピー論ができる圏や, コホモロジー論ができる圏なんかもあるね」
「全然想像つかないや」
「応用例なら計算機科学分野にもよく見られるかな」
「計算機科学?」
「computer scienceね. さっき君が言ったように, 圏論は"元がとれない"と言われる. それは相手にするものが集合とは限らないからなの. 集合とは限らないものに対して議論をするから, 集合論を前提にしていない分野に応用されることもある」
「それが計算機科学ってこと?」
「もちろん他にもあるけどね」
 教室はしんと静まり返っていて, まるでたくさんの人たちが彼女の話に耳を傾けているような気になった.
「あるいはもっと純粋な圏論もある. 圏論それ自体を研究する分野. 極限まで抽象化を重ねたその先にあるのはなんだろう, とかね」
「そこに何かがあるわけ?」
「どうかな. でも, 広大な圏論がたった一つの概念で全て説明できたら面白いと思わない?」
「…そんなに上手くいくかなぁ」
「上手くいかない理由があるわけじゃないでしょ. あと最近の流れでは, 圏論をベースに数学を置き換えるなんてことをしている人もいるみたい. ある圏の上で集合を模倣する, 集合論ができる圏みたいなものがあって, それを使うと集合論ベースだった数学は全部圏の言葉で書き直せるんじゃないかってね」
「数学を置き換える?それって大変じゃないの?」
「まぁそりゃあそうでしょうね. でも圏論の言葉で書くから分かることもあるよ. 本質的なことが何かってことが見えやすかったり, 抽象的な議論で済ませることができたりね」
「なるほどね」
「話を戻そうか. 圏というのは, 例えば群と群準同型, みたいなものの集まりね. 点と矢印の集まりみたいな感じ」
 千景が点をたくさん打ってから, 点と点の間にめちゃくちゃに矢印を書いた.
「つまり, 群が点で, 矢印一つ一つが群準同型になるような圏があるわけだね」
「そうね. それは圏の例の一つ. でも圏の例は他にももっとたくさんあるよ. 定義を書こうか」
 千景はすらすらと, 黒板に定義を書いた.

Definition \(\mathcal{C}\)が圏とは, 対象, 射, dom, codom, 合成の組からなるものであって, 以下を満たすもののことである.

  • (dom, codom) dom, codomは射から対象への対応とする. 射\(f\)であって, \(\mathrm{dom}(f)=A, \mathrm{codom}(f)=B\)であるようなものを\(f : A \to B \)と表記する.
  • (合成の存在) 任意の射\(f,g\)に対し, \(\mathrm{dom}(f) = \mathrm{codom}(g)\)を満たすならば, 射\(f \circ g : \mathrm{dom}(g) \to \mathrm{codom}(f)\)が定義される.
  • (identityの存在) 任意の対象\(X\)に対し, 射\(1_X : X \to X \)が存在する. これをidentity arrowとよぶ.
  • (identity laws) 任意の射\(f : A \to B \)に対し, \(f \circ 1_A = f = 1_B \circ f \).
  • (associativity law) 合成が定義できるような射\(f,g,h\)に対し, \(f \circ (g \circ h) = (f \circ g) \circ h \).

Definition \(\mathrm{Hom}_\mathcal{C}(A,B) = \{f : A \to B; f \text{は} \mathcal{C} \text{の対象} \}\) (\(f : A \to B \)の形の射全体をHomで表す.)

「始めの3つはあとの公理を成り立たせるために必要な条件を述べているだけね. 公理として機能するのは最後の2つ」
「identity lawとassociativity law…モノイドみたいだね」
「monoidは底集合に対して単位元が1つ存在. 圏は全ての対象に対して恒等射が存在」
「ならモノイドとはかなり違うかぁ. モノイドは圏じゃないんだね…」
「待ちなさい」
 千景はキリッとした顔をこちらに向ける. 大きな目の奥が一瞬, キラリと光ったように見えた.
「圏になるかどうかはどういう対象とどういう射を考えるかに依る. 圏の例をいくつか見て, 圏という構造に慣れましょう」

Example

  • \(\mathbf{Set}\): 対象を集合, 射を集合から集合への写像とする圏. dom, cod写像のdomain, codomainとし, 合成は写像の合成, 恒等射は恒等写像と考える.

「これはいいわね?」
「えっと, 任意の集合が対象になるんだね. 恒等写像に対してなら恒等射律も言えるし, 写像の合成に関して結合律も言えるね. いいよ」

  • \(\mathbf{Group} \; (\mathbf{Mon}, \mathbf{Ring}, \mathbf{Vec}_\mathbb{C}, \mathbf{Ab}) \): 対象を群(resp. モノイド, 環, \(\mathbb{C}\)上のベクトル空間, アーベル群), 射を準同型とする圏.
  • \(\mathbf{Top}\): 対象を位相空間, 射を連続写像全体とする圏.

「これもいい?」
「群の圏…さっき言ってたやつのことだね. モノイドとか環とかも確かに圏になるね」

  • poset \(P\): \(P\)を半順序集合(partially ordered set)とする. 対象は\(P\)の元, 射は\(a \leq b \iff a \to b \)によって, "順序関係があること"によって定める.

「じゃあ, これはどう?」
「えーっと, 確認だけど, 半順序っていうのは反射律と推移律と反対称律が成り立つ順序だよね?」
「そう. 全順序じゃないことがポイントね. 任意の2元は大小関係が"ある"or"ない"のどちらかだから, 前者は射がある, 後者は射がないとみなすってこと」
「ふむ」
\(a,b \in P \)に対し, \(a \leq b \)なら\(\mathrm{Hom}(a,b)\)は1点集合. そうでなければ空集合
「なるほど, なんとなくわかった気がする」
「このように, Homがたかだか1点しかない圏を痩せた(thin)圏と言う. 射が少ないから痩せてるんだね」

  • group \(G\): \(G\)を群とする. 対象は\(G\)のみ, 射は\(g \in G \)に対し\(G \to G; x \mapsto x \star g \)全体を考える.

「さて, これはどうかな」
「対象は$G\(1つしかないんだね」 「そう. その代わり, 射が\)G\(の元の数だけある. \)G$の単位元から定まる射が恒等射になる」
「なるほど」
「これと同じ理屈で, モノイドも圏になるよ」
「"単位元がある"から恒等射が作れるって話か」
「こんなのもある」

  • 双対圏 \(\mathcal{C}^{op}\): \(\mathcal{C}\)を圏とする. 対象は\(\mathcal{C}\)と同じ, 射は\(\mathcal{C}\)の射を向きだけ反転させて得られる圏\(\mathcal{C}^{op}\)を双対圏という.

「射の向きだけ反転?」
「そう. 圏を点と矢印で書くと, その矢印の向きをひっくり返したものが双対圏. 他の分野の"双対"って言葉はここから来ている. 双対には"余"という漢字を当てることもあるよ」
「僕が知っているのはベクトル空間の双対空間くらいかな. そういえば, 多様体の接空間と余接空間は, 双対空間だけど"余"という漢字を当ててるね」
「そうね. とりあえずこのくらい分かってもらえればいいかな」
「よく出てくる圏はこれくらいなの?」
「いや, そんなことないよ. もっと面白い圏に触れるためには色々準備が必要だから」
 千景はニコニコしながら, こちらを見ている.
「圏の例を挙げたけど, これだけじゃあ何もわからないでしょうね」
「そうだね. 圏になることは分かるんだけど, これをどうやって使うのかは全然イメージが沸かないな」
「例えば」
 千景がチョークを持った手でこっちを指さす.
「いくつかの圏では共通することがあるね. 例えばだけど…集合, 加群, 環, 位相空間. これらには全て"直和"が定義される」
「集合の直和っていうのは, 添字をつけてdisjoint unionを取るんだっけ. 加群の直和は形式的な有限和に加群の構造を入れたもので, 環はテンソル積で, 位相空間は集合として直和を取って位相をいれるんだね」
「そう. でもこれらはあまり似ているとは思えないのに, "直和"と名前が付いているのはどうしてかな」
「うーん…気にはなってたけど, 理由は知らないなぁ」
「実は, 一般の圏に"直和"(coproduct)という概念が定義できて, 集合の圏や加群の圏だと今君が言った直和と一致するからなんだ」
「え?本当に?」
「そう. 他にもこうやって一般の圏で考えることで見えてくるものはあるよ. 一般化によって高い視点で物事を捉えられる. 異なる構造に共通する部分を見つけたり, より本質的なことを考えたり」
「なるほどねえ」
「どう, 少しは興味が沸いてきた?」
 千景がキラキラした目でこちらを見つめてきた. こういうときの彼女はすごく楽しそうで, 僕としてもそんな彼女を見ているのはとても好きなんだけど, 残念ながらもう帰る時間だ.
 すでに日は暮れて, あたりは暗くなっていた.
「どうだろうね. それより, 帰ってレポート仕上げなくちゃ」
「えー」
「そんな顔しないでよ」
「んー. じゃあ今日のところは勘弁してあげよう. その代わり, 来週までにこれの関手と自然変換のセクションまで読んできて」
 そう言って, 千景はカバンからホッチキス留めされた紙の束を取り出した.
「なにこれ…何かのpdf?」
「まぁそんなところ. それじゃあ, よろしく!」
 千景は長い髪をひらひらさせながら, 教室を飛び出していった.
 僕は黒板を綺麗に消してから, 教室を後にした.

参考

千景が言っている"色々な"圏論については以下のキーワードなどを参照してみてください.

objective覚書

objective-0.6.1

O' = data Object e m
= forall x. e x -> m (x, Object e m)
= hom(e, m . (-,O'))   (as Nat)

functor Kを用いてe = hom(a,K-) = forall x. a -> K xと書けるとき(Data.Functor.Kan.Ranを見よ)

O' = hom(hom(a,K-), m . (-,O'))
= hom(K^-1(hom(a,-)), m . (-,O'))
  -- by K^-1 -| Ran K
= hom(hom(a,-), Ran K (m . (-,O')))
  -- covariant yoneda
= Ran K (m . (-,O')) a
= forall r. (a -> K r) -> m (r,O')

Object e mがわかっているとき, eと適当な型の直積をとっても良い:

O' = data Object (forall x. (a,e x)) m
= hom((a×-) . e, m . (-,O'))
= hom(e , hom(a,-) . m . (-,O'))
= data Object e (forall x. a -> m x)

eとして Request a b r = (a,b->r) を取ったものはProcessとして定義されている.

P' = data Process a b m
= Object (Request a b) m
= hom((a×-) . hom(b,-), m . (-,P'))
= hom(hom(b,-), hom(a,-) . m . (-,P'))
= a -> m (b, P')

左Kan拡張を使ってもいいけれど同値な式以上の意味はなさそう.
Lanがより単純な項に書き換えられるなら何かあるのかも?

O' = data Object e m = Hom(Lan (-,O') e, m)

Codensity Monad

Codensity という型がある. 定義は以下.

newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }

instance Functor (Codensity k) where
  fmap f (Codensity m) = Codensity (\k -> m (k . f))

instance Monad (Codensity f) where
  return x = Codensity (\k -> k x)
  m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))

これの何が良いかと言うと, これは以下のようにMonadFreeな作用を持つ.

instance (Functor f, MonadFree f m) => MonadFree f (Codensity m) where
  wrap t = Codensity (\h -> wrap (fmap (\p -> runCodensity p h) t))

Codensityはnewtypeで実装されているから, 実行時には CodensityrunCodensity によるオーバーヘッドは考えなくて良い. だから, m のMonadFreeのメソッドを直接呼ぶよりも効率よくなる可能性が高い. 特に, 元々のmが「重い」モナドなら, Codensity をかぶせるだけで劇的に速くなることがある.

Codensityのパフォーマンスの話は http://www.iai.uni-bonn.de/~jv/mpc08.pdf などを参考にしてもらうことにして, 以下ではCodensityの(圏論的な)説明をしてみる.

以下, 定義などは逐一述べないので必要に応じてnLabなり参考文献に挙げたものを参照してください.

RanとCodensity

functor p : C → Dに対し, functor  p^{-1} \colon \mathcal{E}^\mathcal{D} → \mathcal{E}^\mathcal{C}を,  p^{-1}(F) = F \circ p によって定める. ただしここで  \mathcal{E}^\mathcal{D} とはDからEへの関手のなす関手圏のこと.

functor f : C → E, p : C → Dに対し, pに沿ったfの右Kan拡張  p \ddagger f を考える.
 p \ddagger が存在すれば, これは  p^{-1} の右随伴である.

D
↑ ↘ p‡f
| ⇓ ↘
C ――→ E

随伴の定義から,

 \hom(p^{-1}(-),f) \cong \hom(-,p \ddagger f)

ここで,  \mathcal{C} の対象aを一つ固定し, 米田関手yを用いて

 \hom(p^{-1}(ya),f) \cong \hom(ya,p \ddagger f)

 p^{-1} の定義に戻れば,

 \hom(ya \circ p,f) \cong \hom(ya,p \ddagger f)

さらに右辺で(共変)米田の補題を用いて,

 \hom(ya \circ p,f) \cong \hom(ya,p \ddagger f) \cong (p \ddagger f)(a)

なる同型を得る. ゆえに (p \ddagger f)(a) が存在したとすれば最左辺と同型になる.
さて今はHaskellでの話がしたいので, 対象とは型であり, 射とは函数である.  \hom(ya \circ p,f) とは, 自然変換の集合であるが, これを ya \circ p \rightarrow fなる自然変換からなる型と同一視する.

このような仕方で (p \ddagger f)(a)を最左辺で定義すると,
自然変換 ya . p ~> fRankNTypes を用いて, forall b. (a -> p b) -> f b なる型を持つ.

よって,

newtype Ran p f a = Ran (forall b. (a -> p b) -> f b)

を得る. これは http://hackage.haskell.org/package/kan-extensions-4.1.0.1/docs/Data-Functor-Kan-Ran.html で定義されている.

最後に, pもfもmで固定してしまうと,

newtype Ran     m m a = Ran       (forall b. (a -> m b) -> m b)
newtype Codensity m a = Codensity (forall b. (a -> m b) -> m b)

により, Codensityが得られた.

HaskellでのFunctor, Monad

上のような操作でCodensityは得られるが, 上の操作では pやfは関手 であった.
しかしCodensityはFunctorのinstanceで(Functor m) =>を要求しない (つまり, mがFunctorやMonadでなくとも, CodensityはFunctorおよびMonadになる).

最初の実装で確かにCodensityがFunctorやMonadになることは確認が必要なので, Agdaで証明を書いてみた.

確かに,

instance Functor (Ran p f)
instance Functor (Codensity k)
instance Monad (Codensity f)

なるインスタンスが正しく実装されていることが分かる.

参考文献