構造とその素材の書き表し方 - 檜山正幸のキマイラ飼育記 (はてなBlog)

構造、例えばモノイドを書き表すとき、どう書くか？省略や記号の乱用も含めたルールをどうするか？毎回悩みます。ある程度の方針を決めたいと思います。

内容：

素材だけの指標
説明的な名前
インスタンスの書き方
追記 (翌日)：もっとバリエーション

さらにモナドに関する追記

素材だけの指標

「指標」と「仕様」を使い分けるか？使い分けるならどう使い分けるか？という話題を「指標と仕様」で書きました。現時点では結論がなくて、ケースバイケースとしか言いようがないですね。

でも今回は、構造の素材〈構成素 | constituent | ingredient〉だけを扱うので、指標に法則（公理）は書きません。モノイドなら、素材だけの指標は次のようになります。

signature Monoid {
 sort A
 operation m: A×A→A
 operation i: I→A
}

出てくる記号／名前を集合圏で考えていることを明示するなら：

signature Monoid {
 sort A in Set
 operation m: A×A→A in Set
 operation i: I→A in Set
}

in Set を何度も書くのが面倒なら次でもいいとします。sortは対象のことで、operationは射のことです。

signature Monoid in Set {
 sort A
 operation m: A×A→A
 operation i: I→A
}

圏Setを他の圏に置き換えてもいいです。例えば、R-ベクトル空間の圏R-Vectにしてみると：

signature Monoid in R-Vect {
 sort A
 operation m: A×A→A
 operation i: I→A
}

このときは、'×'をテンソル積' $\otimes$ 'と解釈し、'I'を1次元ベクトル空間とみた'R'と解釈します。そして、我々がよく使っている呼び名は代数〈多元環〉ですから、次のように書けばより馴染み深いでしょう。

signature Algebra  {
 sort A in R-Vect
 operation m: AA→A in R-Vect
 operation i: R→A in R-Vect
}

説明的な名前

モノイドには幾つかの構成素〈素材〉がありました。

構成素名	指標内での名前
台集合／台ベクトル空間	A
二項演算／双線形写像	m
単位	i

A, m, i は味も素っ気もない名前で、それだけ見せられて意味を想像するのは困難です。そこで、英字（ラテン文字）からなるキーワードにします。

構成素名（日本語）	キーワード（英字）
台集合／台ベクトル空間	underlying
二項演算／双線形写像	binop
単位	unit

英字キーワードなら、ある程度は意味が想像できます。英字キーワードを使って指標を書いてみます。

signature Monoid in Set {
 sort underlying
 operation binop: underlying×underlying→underlying
 operation unit: I→underlying
}

長ったらしいので見にくくなったわ（泣）。簡潔な短い名前と長めの説明的な名前を、別名〈エイリアス | alias〉として結び付けることにしましょう。

signature Monoid in Set {
 sort A
 operation m: A×A→A
 operation i: I→A

 alias underlying = A
 alias binop = m
 alias unit = i
}

別名は使っても使わなくてもいいですが、いずれにしても、必要に応じて指標内での名前を説明的にすることができます。

インスタンスの書き方

指標で定義される構造のインスタンスを書くときよく使われる書き方は、記号の乱用を使って、

モノイド M = (M, m, i)

のように書く方法です。別なモノイドならば、

モノイド N = (N, m, i)

この書き方だと、Mの二項演算とNの二項演算を区別できません。区別するための書き方になると、人によりバラバラになります。

人によりバラバラになるのは致し方ない（対処の方法がない）ですが、なにかしら標準的な書き方を決めておきます。もちろん、ローカルな標準、僕がそうしたい標準に過ぎません。

標準的書き方：構造の構成素を表すには、構造の名前に（指標で宣言した）構成素キーワードをドット区切りで繋げる。モノイドの例ならば、次のようです。

モノイド M = (M.underlying, M.binop, M.unit)
モノイド N = (N.underlying, N.binop, N.unit)

とりあえず、これを標準にします。しかし、この書き方は、長ったらしいし、世間でそんなに使われていません。そこで、書き方に次のバリエーションを認めることにします。

ドット記法（標準の書き方）
下付き記法
転倒下付き記法
関数記法

例を見ればすぐに分かるでしょう。

ドット記法：モノイド M = (M.underlying, M.binop, M.unit)
下付き記法：モノイド M = (M_underlying, M_binop, M_unit)
転倒下付き記法：モノイド M = (underlying_M, binop_M, unit_M)
関数記法：モノイド M = (underlying(M), binop(M), unit(M))

構成素ごとに記法を変えてみいいとします（混ぜてもOK）。例えば：

モノイド M = (underlying(M), binop_M, unit_M)

さらに、記号の乱用の規則を設けます： 'underlying'を予約語として扱い、'underlying'は省略してよい。例えば：

モノイド M = (M, binop_M, unit_M)

binop, unit のような説明的な名前ではなくて、短いほうの名前でもいいので、次も許します。

モノイド M = (M, m_M, i_M)

二項演算の記号はしばしば中置演算子記号が使われるので、そのことも指標で宣言しておきましょう。

signature Monoid in Set {
 sort A
 operation m: A×A→A
 operation i: I→A

 alias underlying = A
 alias binop = m
 alias unit = i
 alias (*) = binop
}

これで、アスタリスク記号が中置演算子記号だと宣言されました。次の書き方が有効です。

モノイド M = (M, (*)_M, i_M)

インスタンスごとに固有の別名を使ってもいいとします。別名の宣言は'where'で後から修飾することにすれば：

モノイド M = (M, (#), j) where (#) = (*)_M, j = i_M
モノイド N = (N, ($), k) where ($) = (*)_N, k = i_N

このくらいのバリエーションを許せば、既存の書き方はたいてい包摂できるでしょう。

追記 (翌日)：もっとバリエーション

すぐ上（追記前の最後の文）で「このくらいのバリエーションを許せば、既存の書き方はたいてい包摂できるでしょう」と書いたのですが、まだ別のバリエーションが残っているようです。

圏（小さい圏）に対する素材だけの指標を書いてみます。

signature Category {
 sort O
 sort M
 operation dom: M→O
 operation cod: M→O
 operation id: O→M
 operation comp:M×M⊇→M
}

ここで、記号'⊇→'は部分写像を表します。圏の指標は少し特殊で、集合圏（射は写像）だけではなくて、部分写像の圏の射も必要とします。

圏論で通常使われている書き方をサポートしようとすると、別名（むしろ別記法）の宣言を強化する必要があります。この強化のために、無名ラムダ変数を使います*1。

無名ラムダ変数（ハイフンまたはアンダースコア）による記法を復習すれば：

関数〈写像〉を、型を省略した（型無しではない）ラムダ記法で書く。例：λ(x, y).(3×x² + y)
ラムダ変数をハイフンまたはアンダースコアに置き換える。視認性の都合で、ハイフン／アンダースコアを丸括弧で囲んでもよい。異なる名前の変数を区別しない。例：λ(_, _).(3×(_)² + _)
λ部分を取り除いて本体だけ取り出す：例：(3×(_)² + _)

こうして簡易ラムダ記法ができ上がります。この簡易ラムダ記法は、簡単な式以外では破綻します。上の例は破綻してます（名前による変数の区別を失っているので元に戻せない）。簡単な場合なら元に戻すことができます。

(5×_) なら λx.(5×x)
((_)³) なら λx.(x³)
(_ + _) なら λ(x, y).(x + y) （2つのアンダースコアは元は別な変数だとみなして）

関数fに対して、f(_) はfと同じです。

f(_) = λx.f(x) = f

二項演算に関しては、無名ラムダ変数も省略していいとします（Haskellと同じ記法）。

(+) = (_ + _) = λ(x, y).(x + y)

無名ラムダ変数を使って、別名（別記法）を宣言しましょう。

signature Category {
 sort O
 sort M
 operation dom: M→O
 operation cod: M→O
 operation id: O→M
 operation comp:M×M⊇→M

 alias (;) = comp
 alias id_{_} = id(_)
}

これで、comp(f, g) の代わりに f;g 、id(x) の代わりに id_x でもいいことになります。それでも、comp(f, g) = g $\circ$ f という逆順〈反図式順〉に書く演算子記号はサポートできません。「二項演算子の左右（第一引数と第二引数）を逆順で書く演算子の宣言」が必要ですが、今日は深入りしないことにします。

O, M という短すぎる名前に英字キーワードの別名を宣言しましょう。

signature Category {
 sort O
 sort M
 operation dom: M→O
 operation cod: M→O
 operation id: O→M
 operation comp:M×M⊇→M

 alias (;) = comp
 alias id_{_} = id(_)
 alias obj = O
 alias mor = M
}

これで、圏Cの対象類を C.obj, C_obj, obj_C, obj(C) などと書けます。しかし、obj_C, obj(C) よりは、Obj_C, Obj(C) が多いですね。大文字小文字の違いも別名に列挙すればいいのですが、面倒だから：

大文字小文字の違いは宣言しなくても、適宜変えてよい

としましょう。大文字小文字の違いで異なる意味を持たせたかったら？ -- そんときはそんときで対処します。

さて、Obj(C) を |C| と書くのはポピュラーですよね。これも無名ラムダ変数で書けます。

signature Category {
 sort O
 sort M
 operation dom: M→O
 operation cod: M→O
 operation id: O→M
 operation comp:M×M⊇→M

 alias (;) = comp
 alias id_{_} = id(_)
 alias obj = O
 alias mor = M
 alias |_| = obj(_)
}

aliasで宣言しているのは、構造それ自体とは無関係な書き方の約束だけです。別にどうだっていい話です。とはいえ、なにかしら書き方を約束しないと始まらないので、書き方を宣言する手段は必要です。

[追記に追記 date="翌々日"]モナドの場合を追加しておきます。モナドは圏の自己関手圏のモノイドなので、モノイドの指標をそのまま流用してもかまいません。

for C in CAT
signature Monoid {
 sort A in [C, C]
 operation m: A×A→A in [C, C]
 operation i: I→A in [C, C]
}

が、これじゃ~~モノイド~~モナドの感じが出ませんね。それらしい記号に置き換えましょう。'*'は関手の図式順結合を表すとします。

for C in CAT
signature Monad {
 sort F in [C, C]
 operation μ: F*F→F in [C, C]
 operation η: Id→F in [C, C]

 alias underlying = F
}

圏C上のモナド（のインスタンス）Mがあると、M = (M_F, M_μ, M_η) と書けます。underlying は F の別名なので、M = (M_underlying, M_μ, M_η) 。underlying は（記号の乱用により）省略可能で、転倒下付き記法でもいいので、M = (M, μ_M, η_M) 。

さらにモノグサして、下付き添字を省略して M = (M, μ, η) と書きたいとなると、これは演算子記号・関数記号のオーバーロード解決の問題になります。現実の記法では、省略（暗黙の前提）、記号の乱用、オーバーロードが入り乱れているのですが、無節操なモノグサ記法は誤解と混乱をまねくので、たいがいにしましょうね。[/追記に追記]

*1:無名ラムダ変数については「リー微分は共変微分か？ -- 代数的に考えれば // ラムダ記法と無名ラムダ変数」でも説明し、使っています

素材だけの指標

説明的な名前

インスタンスの書き方

追記 (翌日)： もっとバリエーション

追記 (翌日)：もっとバリエーション