μはleast fixpoint
νはgreatest fixpoint
っていうのは再帰理論関係の方言みたいなものだから
Monadにおいてμでjoinを表わすのはjoinの定義が
μ. T T = T
になってることから来てるように思えるんだけど
何故greatestじゃなくてleastなのかってのがよくわからん
CPO(完備半順序)で μ (T(T(X)) < T(T(X))ってなってるってことなんだけど
直感ではネストが減ってるからとかそんな感じでgreatestはありえんという気はするけど
型付きラムダ計算の世界におけるCPOとしてはもう少し厳密な定義があるはずだよね