このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」(http://d.hatena.ne.jp/m-hiyama-memo/)のデータを移行・保存したものであり、今後(2019年1月以降)更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

ベックの法則をもう少し

「ベックの法則と複合モナド」の補足をもう少し。

絵図で見ると、ベックの法則は、ワイヤー(ストリング)のクロスする場所を乗法や単位をすり抜けさせる絵になっている。つまり、ジャンクションと回路素子に関する「すり抜け」の法則。ワイヤーのクロスがベックのスワッパー。絵算的には、スワッパーとは「すり抜け可能な交差」ということになり、実際、結合律や単位律の証明は「すり抜け」を何度か使って遂行する。ブレイドσがあるなら、(1×f);σ = σ;(f×1) などがすり抜けを表現する。

ところで(ここからが本題)、スワッパーは本来「分配法則」と言うのだが、これはなぜか? (L, μ, η)がモナドとして、おおよそ、次のような雰囲気がある。

  • Lは項生成規則(term {forming,production} rules)
  • μは結合法則
  • ηは、文字や変数を項とみなすこと

これだけじゃ分かりにくいが、本編のListモナド(L, μ, η)とEnumモナド(E, ν, ξ)を例にする(記号は違う)と、

  • Lは自由掛け算モノイドの項を生成する
  • μは掛け算に対するアンバイアスな結合法則=括弧の外し方を与える
  • ηは、アルファベットの単一文字を掛け算の項(あるいは文字列)とみなす。

同様に:

  • Eは自由足し算モノイドの項を生成する
  • νは足し算に対するアンバイアスな結合法則=括弧の外し方を与える
  • ξは、アルファベットの単一文字を掛け算の項(あるいは文字列)とみなす。

Listモナドは自由モノイドまたは自由半群を作る作用となる(空列を許さないと単位はないので半群)。掛け算は可換ではないが、μが“項の積”を項とみなすやり方を与える。Enumuモナドは自由可換モノイドまたは自由可換半群を作る作用。足し算は可換となり、νが“項の和”を項とみなすやり方を与える。

ListしてEnum(L;E = E・L)すれば、半環の項が生成される。半環の項の簡約には、結合律だけではダメで分配律が必要になる。それは、EnumしてList(E;L = L・E)した形、つまり和の積を単純化する法則だから、L・E ⇒ E・L という形の変換で与えられる。これが分配法則δ:L・E⇒E・L というわけ。

僕はベックの動機をまったく知らないが、半環項の生成と掛け算/足し算の結合律、足し算に対する掛け算の分配律を備えた計算体系が作りたかったのなら、確かにスワッパーは分配法則と呼ぶのは自然だ。