圏論

学部時代に「層圏トポス」で勉強したはずです。特に深い意味はなかったが、数学の勉強の延長線上。直観主義論理と関係があるぐらい。米田レンマぐらいは追ったはず。この時は「選択公理なんて認めん」みたいな人だったので、locally Small とは「はぁ?」だったはず。随伴関手とか双対とか面白いんだけど、面白いなぁぐらい。Category thoery for working matehmatician も、一応は読んだはずなんだけど。圏は対象(集合)と矢印(写像)で作るんだけど「なんで集合なの?」って辺りが嫌だったかも。(今は選択公理勉強したから、それほど抵抗はない)

なので、論理型プログラミング勉強した後、計算理論の方でカテゴリーが出てきたは意外な感じ。関係ないと思っていたのに、やっぱり、そこいくの? みたいな。まぁ、直観主義論理なんだから当然と言えば当然なんだけど。

とは言えば、いまだにピンとは来てない。使いこなせてもいないです。単一化の双対に minimun confilt set があるとかは面白かったが。萩野さんのカテゴリカルプログラミング言語 CPL も、ちょっとだけ見たはず。大学院とかでも何回か復習はしてるけど。

で、灘高の文化祭で

圏論によるプログラミングと論理
http://www.npca.jp/2013/

ってのが。おお、300ページ超かぁ。力作ですね。CPL とかに費やしているのは関係した人の趣味かな。λ計算、型理論、圏論、モナド、論理、カーリーハワード対応、CPL と一通り入ってます。

この手の物は自分で勉強した時の目録みたいなもの。これを作るのは良い勉強になる。僕も物理と化学では作った。数学は作りませんでした。

でも、間違ってもこういうもので学んじゃだめなんだよね。例の岩波の基礎数学と同じで、

＊　わかっている人はふんふんですむが、最初に読んでもチンプンカンプン

いろいろ理由はあるのだけど、

＊　詰め込みすぎ

＊　確認のための問題がない

そして、

＊　記法の説明が完全でない

わざとやっているわけでもないんだろうけど、そうなっちゃうものなんだよ。当たり前のところを省いちゃうわけね。でも初学者は、そこでつまづく。なので、結局は演習を地道にやるしかないです。というわけなので問題と解法がたくさん載っているものが望ましいね。

a → b → c は a → (b → c) のことなんだけど、そして、そう読まないとつじつまは合わないわけだが、そんなことを書いてくれる人はいないんだよね。

でも復習には良いんだよな。一方で、やっぱり今の段階で役に立つかというと微妙だなとも思う。その割にモナドとか証明支援系とか流行っているので、逃げるわけにもいかんし。困ったものだ。必要なところだけ近い道したいところ。学問に王道なしだけど、300ページは寄り道多すぎる。