このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

なんでズボラでその場限りになるのか

「理解をさまたげるモノ/誤解をまねくモノ、それと対処」の最後で次のようにまとめました。

用語とか記号の使い方に関して、是非とも憶えておいて欲しいキーワードは次のようなものでしょう。

  1. バラバラ -- 集団や個人によって、用法が違います。
  2. ズボラ -- 律儀に曖昧性なく書くことは極めてまれで、省略や乱用をするのが普通です。
  3. その場限り -- 同じ用語・記号が文脈によって違った意味で用いられます。その文脈の範囲や寿命(スコープ&エクステント)は非常に小さいことがあります。

僕自身のことを言うと:

  1. なるべく標準的な用語/記号を採用しようとしてますが、趣味嗜好がある(主義主張はない)ので、若干のクセはあります。特に、「全部、左から右に書く」記法はメジャーではないです*1
  2. 平均的なズボラさだと思います。
  3. 同じ記号が通用する範囲や寿命は短めかも知れません。大文字小文字による区別とか、書体を変えるとかも、僕はあまり使いません。

「平均的」とかいう表現はアテになりませんが、僕が「ズボラでその場限り」なことは間違いありません。しかし、ちゃんと律儀にやると、ほんとにグヂャグヂャになるんですよ。1回くらいは、ちゃんと律儀にグヂャグヂャにやってみましょうか。

例文はこれ

Fはモナドだとします。μX:FF(X)→F(X) はモナド乗法です。

この程度の言い回しはよく使います。が、省略や記号の乱用が猛烈に使われているのも事実です。

上付き下付きではたまらない

ちゃんと律儀に書くときに通常使われる手段は、上付き下付きの添字による修飾です。例えば、F = (UF, μF, ηF) と書いて、

とか約束します。

しかし、添字が入れ子になったりすると書くのが大変なので、オブジェクト指向言語風(あくまでも「風」)に、ドット「.」を使った修飾記法を使うことにします。

  • F.UFunc は、モナドFの基礎となる関手(underlying functor)
  • F.mult は、モナドFの乗法
  • F.unit は、モナドFの単位

と、こんな感じ。圏に関連する記法も同じようにドット修飾方式にします。

概念 普通の記法 ここで使う記法
圏Cの対象の集合 |C| C.Obj
圏Cの射の集合 C C.Mor
圏Cの域 dom(f) C.dom(f)
圏Cの余域 cod(f) C.cod(f)
圏Cの恒等 idX C.id(X)
圏Cの結合 f;g C.comp(f, g)
圏Cのホムセット C(X, Y) C.Hom(X, Y)
関手Fの対象パート F F.obj
関手Fの射パート F F.mor

Fがモナドだとは

Fがモナドだということであれば、Fの基礎となる関手F.UFuncがあり、それは、とある圏の自己関手です。とある圏をF.UCat (underlying category)としましょう。F.UFuncには対象パートと射パートがあるので、

  • F.UFunc.obj : F.UCat.Obj → F.UCat.Obj
  • F.UFunc.mor : F.UCat.Mor → F.UCat.Mor

と、こんな感じ。F.UFuncの関手性は次のように記述できます。

  • X∈F.UCat.Obj に対して、F.UFunc.mor(F.UCat.id(X)) = F.UCat.id(F.UFunc.obj(X))
  • f∈F.UCat.Hom(X, Y), g∈F.UCat.Hom(Y, Z) に対して、F.UFunc.mor(F.UCat.comp(f, g)) = F.UCat.comp(F.UFunc.mor(f), F.UFunc.mor(g))

ちなみに、ズボラな書き方だと:

  • F(idX) = idF(X)
  • F(f;g) = F(f);F(g)

Fがモナドだということは、F.UFunc以外に、モナド乗法F.multとモナド単位F.unitがあって、結合律と単位律を満たすはずですが、単位律の片方だけ書いてみると:

  • X∈F.UCat.Obj に対して、F.UCat.comp(F.UFunc.mor(F.unit(X)), F.mult(X)) = F.UCat.id(F.UFunc.obj(X))

ちなみに、僕が日常的に使っている自家製ズボラ記法(DOTN)で同じことを書くと:

  • ηF|μ = F^

モナド乗法

F.multがモナドFの乗法だということを律儀に書くと、自然変換の記述になります。

  • F.mult :: Functor.comp(F.UFunc, F.UFunc)⇒F.UFunc : F.UCat→F.UCat

X∈F.UCat.Obj に対する F.mult のX成分を書くと:

  • F.mult(X) : Functor.comp(F.UFunc, F.UFunc).obj(X) → F.UFunc.obj(X)

矢印なんか使わずにちゃんと書くと:

  • F.UCat.dom(F.mult(X)) = Functor.comp(F.UFunc, F.UFunc).obj(X) = F.UFunc.obj(F.UFunc.obj(X))
  • F.UCat.cod(F.mult(X)) = F.UFunc.obj(X)

このことを普通は、次のようにズボラに書きます。

  • μX : FF(X) → F(X)

モナド乗法では結合律が成立していますが、これを律儀に書き下すと … … もうカンベンしてー、鬱陶しくてたまらん! DOTNによる結合律は次のとおり。

  • μF|μ = Fμ|μ

それで結局

律儀な記法は確かに、注意深く読めば分かりやすく曖昧性が少ないと言えます。しかし、律儀な書き方をずっと続けられるかというと、それは無理です。書くのも読むのも面倒過ぎて耐えられないでしょう。それに、実際に計算を遂行するときには、律儀な記法には本質的ではない情報がグヂャグヂャに大量に含まれているので、ほとんど使いものになりません。余分な情報が、一種の型宣言/型指定として役立つことがないとは言いませんが、ほとんどのケースでは邪魔なゴミです。

という次第で、ズボラでその場限りの記法を使わないと、クソめんどくさくてやってられない事情があります。もちろん、説明のときは別な配慮が必要なので、言い訳にする気はないですが。

ズボラでなければやっていけない、律儀でなければ説明する資格がない。

*1:個人的かつ曖昧な感覚では、f(x) を x.f と書くことで、計算のときの負担とストレスは 1/3 くらいになります。