ビジュアルプログラミング(1) - エレファント・ビジュアライザー調査記録

ビジュアルプログラミングで数式の変形を行うものを作りたいと思います。「Blockly | Google Developers」を使ってみようと思いますが、何ができるのかわからないのでできるかどうかはわかりません。

「エレファントな群とリー代数(3) - エレファント・コンピューティング調査報告」、「エレファントな群とリー代数(5) - エレファント・コンピューティング調査報告」で扱った群の式の変形について考えます(「【電子復刻版】bit 1988年04月号(通巻230号)」、「【電子復刻版】bit 1989年04月号(通巻242号)」参照)。

以下のようになります。

次の3個の書き換え規則
$\begin{eqnarray*} e x & \to & x \\ x^{-1} x & \to & e \\ (x y) z & \to & x (y z) \\ \end{eqnarray*}$
の集合から出発して、以下の書き換え規則の集合を得る方法が「【電子復刻版】bit 1988年04月号(通巻230号)」、「【電子復刻版】bit 1989年04月号(通巻242号)」に書かれています。
$\begin{eqnarray*} e x & \to & x \\ x^{-1} x & \to & e \\ (x y) z & \to & x (y z) \\ x^{-1} (x y) & \to & y \\ x e & \to & x \\ (x^{-1})^{-1} & \to & x \\ x x^{-1} & \to & e \\ e^{-1} & \to & e \\ x (x^{-1} y) & \to & y \\ (x y)^{-1} & \to & y^{-1} x^{-1} \\ \end{eqnarray*}$
この書き換え規則の集合によって任意の式を標準形に変形することができます。

自由「単項・二項マグマ」(単項演算子と二項演算子を持つ代数的構造)によって関係式を求めていきます。

まず以下の $\rho_1$ から $\rho_6$ までの書き換え規則があるとします。
$\begin{cases} \rho_{1} & = & ( & x & \mapsto & e x & \to & x & ) \\ \rho_{2} & = & ( & x & \mapsto & x & \to & e x & ) \\ \rho_{3} & = & ( & x & \mapsto & x^{-1} x & \to & e & ) \\ \rho_{4} & = & ( & x & \mapsto & e & \to & x^{-1} x & ) \\ \rho_{5} & = & ( & x, y, z & \mapsto & (x y) z & \to & x (y z) & ) \\ \rho_{6} & = & ( & x, y, z & \mapsto & x (y z) & \to & (x y) z & ) \\ \rho_{7} & = & ( & x & \mapsto & e^{-1} x & \to & x & ) \\ \rho_{8} & = & ( & x & \mapsto & x & \to & e^{-1} x & ) \\ \rho_{9} & = & ( & x & \mapsto & (e^{-1})^{-1} x & \to & x & ) \\ \rho_{10} & = & ( & x & \mapsto & x & \to & (e^{-1})^{-1} x & ) \\ \rho_{11} & = & ( & & \mapsto & e^{-1} & \to & e & ) \\ \rho_{12} & = & ( & & \mapsto & e & \to & e^{-1} & ) \\ \rho_{13} & = & ( & x & \mapsto & (x^{-1})^{-1} e & \to & x & ) \\ \rho_{14} & = & ( & x & \mapsto & x & \to & (x^{-1})^{-1} e & ) \\ \rho_{15} & = & ( & x & \mapsto & (x^{-1})^{-1} & \to & x & ) \\ \rho_{16} & = & ( & x & \mapsto & x & \to & (x^{-1})^{-1} & ) \\ \rho_{17} & = & ( & x & \mapsto & x x^{-1} & \to & e & ) \\ \rho_{18} & = & ( & x & \mapsto & e & \to & x x^{-1} & ) \\ \rho_{19} & = & ( & x & \mapsto & x e & \to & x & ) \\ \rho_{20} & = & ( & x & \mapsto & x & \to & x e & ) \\ \rho_{21} & = & ( & x, y & \mapsto & (x y)^{-1} x & \to & y^{-1} & ) \\ \rho_{22} & = & ( & x, y & \mapsto & y^{-1} & \to & (x y)^{-1} x & ) \\ \rho_{23} & = & ( & x, y & \mapsto & (xy)^{-1} & \to & y^{-1}x^{-1} & ) \\ \rho_{24} & = & ( & x, y & \mapsto & y^{-1}x^{-1} & \to & (xy)^{-1} & ) \\ \end{cases}$
以下の手順で $\rho_7$ から $\rho_{24}$ までが得られます。書き換え規則の横にある番号は、式の部分の位置を表す番号で、式の全体から始まり左側をたどって順に $0, 1, 2, \cdots$ という番号をつけたものです。

$\rho_1, \cdots, \rho_6 \implies \rho_7, \rho_8$

$\begin{matrix} e^{-1} x & \xrightarrow{\rho_{2},3} & e^{-1} (e x) & \xrightarrow{\rho_{6},0} & (e^{-1} e) x & \xrightarrow{\rho_{3},1} & e x & \xrightarrow{\rho_{1},0} & x \\ \end{matrix}$

$\rho_1, \cdots, \rho_8 \implies \rho_9, \rho_{10}$

$\begin{matrix} (e^{-1})^{-1} x & \xrightarrow{\rho_{8},4} & (e^{-1})^{-1} (e^{-1} x) & \xrightarrow{\rho_{6},0} & ((e^{-1})^{-1} e^{-1}) x & \xrightarrow{\rho_{3},1} & e x & \xrightarrow{\rho_{1},0} & x \\ \end{matrix}$

$\rho_1, \cdots, \rho_{10} \implies \rho_{11}, \rho_{12}$

$\begin{matrix} e^{-1} & \xrightarrow{\rho_{10},0} & (e^{-1})^{-1} e^{-1} & \xrightarrow{\rho_{3},0} & e \\ \end{matrix}$

$\rho_1, \cdots, \rho_{12} \implies \rho_{13}, \rho_{14}$

$\begin{matrix} ( x^{-1} )^{-1} e & \xrightarrow{\rho_{4},4} & ( x^{-1} )^{-1} ( y^{-1} y ) & \xrightarrow{\rho_{6},0} & ( ( x^{-1} )^{-1} y^{-1} ) y & \xrightarrow{\rho_{3},1} & e x & \xrightarrow{\rho_{1},0} & x \\ \end{matrix}$

$\rho_1, \cdots, \rho_{14} \implies \rho_{15}, \rho_{16}$

$\begin{matrix} ( x^{-1} )^{-1} & \xrightarrow{\rho_{14},0} & ( ( ( x^{-1} )^{-1} )^{-1} )^{-1} e & \xrightarrow{\rho_{2},6} & ( ( ( x^{-1} )^{-1} )^{-1} )^{-1} ( e e ) \\ & \xrightarrow{\rho_{6},0} & ( ( ( ( x^{-1} )^{-1} )^{-1} )^{-1} e ) e & \xrightarrow{\rho_{13,1}} & ( x^{-1} )^{-1} e & \xrightarrow{\rho_{13},0} & x \\ \end{matrix}$

$\rho_1, \cdots, \rho_{16} \implies \rho_{17}, \rho_{18}$

$\begin{matrix} x x^{-1} & \xrightarrow{\rho_{16},1} & ( x^{-1} )^{-1} x^{-1} & \xrightarrow{\rho_{3},0} & e \\ \end{matrix}$

$\rho_1, \cdots, \rho_{18} \implies \rho_{19}, \rho_{20}$

$\begin{matrix} x e & \xrightarrow{\rho_{16},1} & ( x^{-1} )^{-1} e & \xrightarrow{\rho_{13},0} & x \\ \end{matrix}$

$\rho_1, \cdots, \rho_{20} \implies \rho_{21}, \rho_{22}$

$\begin{matrix} ( x y )^{-1} x & \xrightarrow{\rho_{20},5} & ( x y )^{-1} ( x e ) & \xrightarrow{\rho_{18},6} & ( x y )^{-1} ( x ( z z^{-1} ) ) \\ & \xrightarrow{\rho_{6},5} & ( x y )^{-1} ( ( x z ) z^{-1} ) & \xrightarrow{\rho_{6},0} & ( ( x y )^{-1} ( x z ) ) z^{-1} \\ & \xrightarrow{\rho_{3},1} & e y^{-1} & \xrightarrow{\rho_{1},0} & y^{-1} \\ \end{matrix}$

$\rho_1, \cdots, \rho_{22} \implies \rho_{23}, \rho_{24}$

$\begin{matrix} ( x y )^{-1} & \xrightarrow{\rho_{20},0} & ( x y )^{-1} e & \xrightarrow{\rho_{18},5} & ( x y )^{-1} ( z z^{-1} ) \\ & \xrightarrow{\rho_{6},0} & ( ( x y )^{-1} z ) z^{-1} & \xrightarrow{\rho_{21},0} & y^{-1} x^{-1} \\ \end{matrix}$