運算的圏論 フォッキンガ流
そう言えば、オランダのフォッキンガ（Fokkinga）達がcalculationalな圏論というのをやっていたな。
やや古い（90年代）が、
- Title: A Gentle Introduction to Category Theory - the calculational approach -
- Author: Maarten M. Fokkinga
- URL: http://wwwhome.cs.utwente.nl/~fokkinga/mmf92b.pdf
- Title: Category Theory for Program Construction by Calculation
- Author: Lambert Meertens
- URl: http://www.kestrel.edu/home/people/meertens/diverse/ct4pc.pdf
バックハウスなんかも運算的な流派だと思う。
で、A Gentle ... の付録で随伴を扱った所を少し読んでみたが、これは僕の性に合わない。記号の使い方とかは参考になるが、やっぱり何をやっているかが分からなくなる。
なかでもムッとしたのは、2つの自然変換に「;」という演算を入れているんだが、これはどうかな。「;」じゃなくて「#」を使って書いてみる。以下で使う記法は僕のDOTN記法。
- α:: J⇒F;;G : A→(B)→C
- β:: G::H⇒K : B→(C)→D
という状況。ここで「;;」は関手の普通の結合。
- α#β := (α;;H)|(F;;β)
ここでの「;;」は関手と自然変換の横結合で、結果は自然変換。「|」は自然変換の縦結合。なんつうか、すこしズラした結合で、多圏とかだと自然かもしれないが。やりすぎな気がする。
ただし、概念とか用語法とかでは使えそうなのもあるから、後でたぶんまた書く。
