ストリング図の使いかた

ストリング図を使った絵算が少しできるようになった。Beckの分配律の公理に出てくる五角形（つうより5点四角形）2つから、スワップ結合律を示して、結合モナドの結合律が示せる。この程度なら、ストリング図で簡単。

で、絵算の計算は何をしているかというと：

1. 可換図式、またはペースティング図から、グラフ書き換え規則をいくつか作る（機械的）。
2. 与えられたグラフ（ストリング図）を眺めて、部屋を１つ作る（チャンバリング）。
3. その部屋と書き換え規則の対応をとる。一種のパターンマッチング。
4. 書き換え規則を実行した結果で、部屋の内部を置き換える。
5. おなじことを繰り返して、目的のグラフを得る。

普通の等式的計算と比べると：

• チャンバリングが部分式の特定に対応する。
• 部屋の置き換えが等式の変形に対応する。

通常の（形式的）証明と同じように、グラフ書き換え規則の集合が公理系で、その規則集合によって得られた書き換え（のマクロ規則）が定理のようなもんだ。