雑記

なかなかブログを更新できないから、書き方のスタイルを変えようと思い、雑記風にライプニッツの「モナドは世界を表象する」テーゼと圏論について適当に書き流してみた。

しばらく後で見直してみて、これはこれで悪くないが気が向かなかった。もう少し淡々と書きたい。

最近はHaskellを触っていて、そのついでに触りだけは知っておこうと思って圏論をやったりしている。

• 圏論による論理学

読んでいる。

1章は型付きラムダ式あり高階論理で、2章以降で圏論のトポスとラムダ高階論理の対応を学ぶ。細かいところでよくわからない箇所はあるものの、コンパクトで読みやすいとは思う。著者の言う普遍論理云々はどこまで本気なのかよくわからない(きっと本気なのだろうが、なかなか共感は抱きがたい)が、トポスのスライスが再びトポスになるという辺りの証明がお気にいり。著者のように表現するかどうかはともかくこれはライプニッツふうではある。

といっても圏論はまだまだ全然わからない。

証明を追うときに、頭の中でHaskellのコードを思い描くと理解しやすくなることがあった。一応後半まで読み進めてはいるが、プルバックやmonoやepiなどの基礎的な概念の証明にもっと習熟しないと消化しがたいだろうという感覚が残っている。

Haskellはとっかかりは乗り越え、Monadを簡単に使うくらいのことはできるようになってきた(HaskellのMonadに慣れるには、do記法に習熟するのが一番の早道のようだ)。Parsecライブラリのありがたみもわかった。

ただAllowあたりのライブラリはまだ難しく感じるし、高度な技法が出てくると頭が混乱してしまう。遅延評価の評価順序にもまだ馴染めていない。

• Haskell側から見ると Monad はシンプルで、Arrow や Category は複雑。
• 圏論側から見るとふつうの射はもちろんシンプルだけどモナドは複雑。

という両面があっておもしろい。Haskellのモナドは何となく理解できたけど、圏論のモナドはまだわからないし。

両側から少しずつ理解が進んでいく感じが気持ちよくもある。

圏論が落ちついたら今度はまた形而上学、特に前から関心のあった可能的対象の非同一性問題について調べてみようと思う。

それでは、次の更新がいつになるのかわからないけど、皆様ごきげんよう。