Diary?

2009-04-24
Fri

(00:55)

第一回モニャドセミナーに行ってきた。檜山さんのコンディションがベストとは程遠かったり、親しみやすかろうと思って出した圏の例で思わぬ事故が起こったり、とにかくまあいろいろな要因が重なった結果として「少し違った視点で見れば、世界が面白くなる」というスローガンの元に始まったモニャドセミナー第一回は愉快な混沌の元に終わった。

そして俺はセミナーが始まる前から「まとめ記事は頼んだ」という無茶を振られ、終いにゃ「みんなが混乱した部分の分析頼む」という更なる無茶を振られて頭を抱えていたのだが、まとめというか補足記事の落としどころが見えてきた気がするので、風呂入ったら執筆を開始することにする。

ちなみに俺の場合テンションの高いうちに全力で突っ走って体力が尽きるか壁にぶつかったらしばらくの間くたばって休憩ってのがマイペースだったりするんで、「お前明日仕事だろ」とか「体力保つのか」といった心配はしなくて大丈夫っす。別に今は会社の仕事でろくな事してないしな。

(01:45)

というわけで第一回モニャドセミナーのまとめというか、混乱した人の出てきた部分の俺なりの説明というか、まあそういうものを書くことにする。そもそも俺自身今回は（今回も?）きちんと落とし前を付けられる自信がまったくないので、その辺は差し引いて読んでください。

まず今回のセミナーの目標は

  1. 圏の形式的な定義と直感的なイメージの両方を知る
  2. いろいろなお絵描きを実習する
  3. 圏の実例を手でいじり倒して、体になじませる
  4. 横道にそれて、面白そうな話題を紹介する

だったわけだが、混乱が起きたのは二番目から三番目にかけての部分だった。というわけで今回はその混乱の原因についての考察などがメインになるが、その前に圏の形式的な定義から。セミナーで触れた範囲で「これが圏の構成要素」というものを列挙してみよう。

  • 任意の対象が存在する
  • 任意の対象 a, b に対して a -> b となる射が存在する
  • a -> b という射において a を域、b を余域とする
  • 射 f および g において、 f の余域と g の域が一致するとき f;g という結合が可能である
  • a -> a という恒等射を持つ

以上が圏の構成要素だ。これだけの説明だと「何それ?」って感じなので、セミナーで使われた（檜山さんの過去エントリーにもある）「しりとりの圏」を例に出して説明してみる。

しりとりの圏において、前述の圏の構成要素は以下のようになる。

対象
ひらがなの集合 H
射
任意のひらがなから作られる文字列 HStr
域
任意の HStr の最初の文字 first関数で取得できるものとする
余域
任意の HStr の最後の文字 last関数で取得できるものとする
恒等射
一文字からなる文字列
結合
しりとりのルールその物。任意の射 a, b に関して last a == first b の時 a;b

この場合の結合は以下のようになる。

  • こぶた, たぬき => こぶたぬき
  • らいおん, んじゃぴー => らいおんじゃぴー
    • 任意の文字列なんでまともな日本語の単語じゃなくてもいい
    • 「ん」で終わっていようがお構いなし
  • あ, あか => あか

とりあえずここまではオーケー? とにかく、この条件下ではしりとりが圏になっている。それでは檜山セミナーでヘビーに使われる絵算で「こぶた たぬき」の結合を見てみようか。

うんまあ、見たまんまだ。じゃあ試しにここに「きつね」という射を結合させてみよう。

当然だけど射（=任意のひらがな文字列）は無数にあるし、結合の数も無数にある。

こういう風に、いくらでも結合が作れるな。めでたしめでたし。……とは行かずに、ここまでの内容に関して質問が投げられ、楽しい混乱が始まった。その質問は以下の三つ（確かこんな感じ）。

  • 例えば「た」を域に「き」を余域に持つ射はそれぞれアイデンティティを持つのか? それともすべて同じとみなせるのか?
  • 「ねんね」のように域と余域が一致する射は恒等射か?
  • 「ここ」のような同一文字二文字の射はそれを作る過程で恒等射になってしまわないか?

結論から書くとそれぞれ「アイデンティティは持つよ。『たぬき』と『たんき』などは別の射」「恒等射にはならない」「射はそこにあるもので作られるものではないし、何にしても『ここ』のような射は恒等射にはならない」といったものだった……と思う。これについては、俺がどのようにしりとりの圏を理解したかの過程を書くことで補足してみようと思う。……と思って書いたけど、案の定派手に間違っていたので、以下のツッコミ及び補足記事を代わりに読んでください。

そもそも何でこんな勘違いをしたかというのを考えてみたら、どうも恒等射についての理解が滅茶苦茶だったのが原因に思える。俺は恒等射のことを物凄く特別な射だと思い込んでいて、その特別さ加減がシグネチャから割り出せないとマズいんじゃねえのと思い、それで以下にあるようなトンデモ論法に行き着いたわけだ（他にもいろいろわかってなさげだが）。でも実際には実装の違いでしかないというのが正しい理解っぽい（まだきちんと理解できてない）。やっぱあれだ、もうちょっと圏の実例に触って圏の概念を体に覚えさせないとダメだな（あと Haskell とかの型システムのちゃんとした理解とか。これも全然ダメダメだ）。

まずは「たぬき」という射だが、そもそもこれは「たぬ」と「ぬき」という射を結合してできたものだと言える。そして圏論というのは極めて強く型付けされた体系で、結合するときに型が完全に一致しないと型エラーを引き起こす。例えば以下のようなプログラムは型エラーとなる。文法とか型のイメージは、まあ常識的に考えてください。

f :: Float -> Float
g :: Integer -> Integer
h :: Number -> Number
x = f;g;h

こういうのを暗黙の型変換で通しちゃうプログラミング言語は多いかもしれないけど、圏論で扱うような世界では間違いなくエラーになる。そのため、以下のような中継ポイントが必要になる。

f :: Float -> Float
g :: Integer -> Integer
h :: Number -> Number
i :: Float -> Integer
j :: Integer -> Number
x = f;i;g;j;h

「これとしりとりの圏の何が関係あるんじゃ」と思われるかもしれないけど、俺の理解した範囲ではしりとりの圏におけるひらがな一文字は型そのもの。そして射の文字列はそのまま関数の引数の型で、関数の戻り値の型は文字列の最後の文字。この論法に従うと、しりとりの圏における文字列というのは以下のような型の関数になる。

  • "あ" = あ -> あ
  • "ああ" = あ -> あ -> あ
  • "あい" = あ -> い -> い
  • "あいう" = あ -> い -> う -> う

というわけで、一番目の質問に出たような同じ域と余域を持つ射のアイデンティティ問題は解決。「たぬき」という射は「た -> ぬ -> き -> き型」で「たんき」という射は「た -> ん -> き -> き型」と全然違うものだし、それでいて余域が同じだから「きつね」のような射を結合可能。

二番目の質問で出た域と余域の一致する一文字より多い射が恒等射にならない理由もこれでわかると思う。恒等射である「あ」は「あ -> あ型」なのに対して、「あじあ」などは「あ -> じ -> あ型」であり、恒等射の条件は「a -> a であるような射」だからだ。三番目の質問の答えとしてもこれで良かろう。

書いててなんか不安になってきたので、 Haskell でコードを書いてみる（ちなみに俺は Haskell プログラマレベルでいうとキャラメイク途中、つまりレベル1にすら達してない）。実に投げやりなコードだけど、とりあえずしりとりの圏ってこういう問題じゃないかな。恒等射の処理が書かれてないけど、そっちはまあわかるでしょう。

main = putStrLn $ ((morph1 `compose1` morph2) `compose2` (morph3 `compose1` morph4)) 1 'a' "abc" True "xyz"
 
morph1 :: Int -> Char -> Char
morph1 x y = y
 
morph2 :: Char -> String -> String
morph2 x y = y
 
morph3 :: String -> Bool -> Bool
morph3 x y = y
 
morph4 :: Bool -> String -> String
morph4 x y = y
 
compose1 :: (a -> b -> b) -> (b -> c -> c) -> (a -> b -> c -> c)
compose1 f g = \m n o -> o
 
compose2 :: (a -> b -> c -> c) -> (c -> d -> e -> e) -> (a -> b -> c -> d -> e -> e)
compose2 f g = \m n o p q -> q

このコードをコンパイルして実行すると "xyz" という文字列が出力される。という事は、きちんとしりとりが成立したことだと思って良いはずだ。納得できない? コンパイラがこれで良いっつってんだから良いんだよ。……多分。

えーと、それでセミナーで起きた混乱の原因を考えてみると、やはり「'あ' という対象と "あ" という恒等射と "ああ" という射」など、射と対象の間に混同が起きていたような気がするのと、実例に入る前に説明された圏論における型の扱いのシビアさと射の結合あたりが有機的に関連付けられて理解されてなかったのかもしれないのと、この二点なのかなと思ったりする。

実際問題、俺もしりとりの圏の理解で使ったひらがな文字=型という連想ゲームが正しい理解といえるのかどうか、全然自信がなかったりして。というわけでツッコミ歓迎。

今回はしりとりの圏に絞って書くつもりだったから一時間ぐらいで終わるだろと思ったら、もう四時半だよ。やべえ会社行きたくねえ。

追記@04:40 大事な事を一点書き忘れた。しりとりの圏の絵算とアローダイアグラムによる関数適用・結合の類似性というのが抜け落ちてる。もういい加減眠いので寝るけど、これについては後できちんと追記した方がいいか。

(08:10)

さっそくツッコミが。えーと、とりあえず会社から帰ってきたらまた考えます。

俺もだいぶ混乱してるなあ。

(19:21)

セミナーの報告記事を大幅改訂。ってかかなりの部分を訂正というか取り下げ。詳しい内容はたけをさんのツッコミにて（素早いツッコミ thanks です）。

で、たけをさんも書かれていることだけど、しりとりの圏の場合は恒等射の扱いがややこしいってのが確かに気になる。「圏の例としてはこんなのがありますよー」という掴みとしては結構親しみ易いと思うけど、そこからほんのちょびっと考えて行ったら混乱したからな（いやそれにしてもここまでこじらせるのは俺だけかもしれんが）。そこさえ引っかからなければ、そこまでわかりにくい例ではない……かもしれないけどどうだろ。

あと懇親会で「セミナーの報告記事とかをまとめて、教科書・チュートリアル的にしたら良いんじゃない?」という意見をもらっていて、その意見には賛同したいところなんだけど、今回の報告記事でわかったとおり俺は明らかにそこまでやるだけの実力が伴ってないんで、誰か俺より頭のいい人に任せたいなあ。

Creative Commons
この怪文書はクリエイティブ・コモンズ・ライセンスの元でライセンスされています。引用した文章など Kuwata Chikara に著作権のないものについては、それらの著作権保持者に帰属します。