はじめに
Plotkin-Powerの代数的効果(algebraic effects)を理解したい。ただし、それには普遍代数・Lawvere理論の理解が必要になるようだ。おどろおどろしいネーミングだが、エミリー・リールのスライドを眺める限り、そこまで難しくないと踏んでいる。圏論の専門家エミリー・リールによるプログラミングのモナドが必要な理由も普通に考えてショボいものであった。
-
エミリー・リール(Emily Riehl)による計算効果(モナド)の説明
要約(プログラミングのモナドが必要になる理由は、A → T B 型プログラム(T-プログラム)が合成できる(圏になる)ようにするため)
以上のこともあり、現実的な労力で代数的効果のアイディアに到達できると思っている。
ただ、概観を眺められそうな文献を訳してみたが、専門的なところでさっぱり意味がわからなかった。
千里の道も一歩からということで、まず用語調べから始める。でも、普遍代数の情報ってほとんどないので難航しそう。と思っていたら、
1日目、2日目とすごくタイムリー(当然じっくり読んで理解しないとわからないが、少なくとも定義が書いてある)。
用語
クローン(clone)
Aを空ではない集合、$\mathcal{O}(A)$をA上のすべての有限的演算(finitary operations)の集合とする。
すなわち、$\mathcal{O}(A)$ は、分離和(disjoint sum)を用いた次の形式を持つ
$\mathcal{O}(A) = \coprod \mathcal{O}_n(A)$
ここで、$\mathcal{O}_n(A)$ は、A上の全てのn項演算(n-ary operations)の集合である。
任意の m 項 $\alpha_1,\cdots \alpha_m \in \mathcal(O)_n$ と $\beta \in \mathcal{O}_m$ が与えられたとき、(なお、ここで合成順序は普通とは逆とする)
(1) 全ての $c \in A^n$ に対して、$c \gamma = (c\alpha_1)\cdots (c\alpha_m)\beta$
で定義される n 項演算 $\gamma$ がただ一つ存在する。
演算 $\gamma$ は $\alpha_1 \cdots \alpha_m \beta$ で表すものとし、$\alpha_1, \cdots \alpha_m$ と $\beta$ の 合成(composition) と呼び、
(2) $c(\alpha_1 \cdots \alpha_m \beta) = (c \alpha_1)\cdots (c \alpha_m) \beta$
と書くことができる。
各 n > 0 に対して、次で定義される n 項演算 $\delta_n^{(i)} \in \mathcal{O}_n$ が存在する。
(3) $c \delta_n^{(i)} = c_i$ ここで、 $c = (c_1,\cdots,c_n) \in A^n$ とする。
$\delta_n^{(i)}$ は、i番目の座標の要素を選び出すものであり、$\delta_n^{(i)}$ は、単位演算子(unit operator) と呼ぶ。
A上の演算の任意の集合で、(1)と(3)の演算を許すもの、すなわち合成の下で閉じており単位演算を含んでいるものを、A上の演算で閉じた集合(closed set of operations on A)、もしくはより簡単にA上のクローン(clone on A)1と呼ぶ。
参考
- Paul M.Cohn, "Universal Algebra" 1981版(数少ない普遍代数の教科書だがLawvere理論については詳しくない)
シグネチャ(signature)
S を集合とする。S-シグネチャ(signature)とは、
- 集合 $\Omega$
- 写像 $ar : \Omega \rightarrow S^{<\omega}$ 2
- 写像 $t : \Omega \rightarrow S$
から成る組 $(\Omega,ar,t)$ を言う。
S の元はソート(sort)と言う。
$\Omega$ の元は関数記号(function symbol)と言う。
各関数記号 $\omega \in \Omega$ について、ソートの語 $ar(\omega)=(s_1,...,s_n)$を、そのアリティ(arity)と言う。
ソート $t(\omega)=s$ を型(type)と言う。
参考
まとめ
情報も少なく、調べながらになるので、気長にやっていきたい。