結合法則のお絵描き

絵をテキストで表示する。

まず、ベータの定義：

β0 := I^

  :: I⇒I : 1→1

βn+1 := [(I ∇n I)^*α'];[βn∨I^]

  :: I∨∇n ⇒ ∇1+n : 1+n → 1

プサイの定義：

ψ1, m := βm

  :: I∨∇m ⇒ ∇1+m  : 1+m → 1

ψn, m := [(∇n I ∇m)^*α];[∇n^∨βm];[(∇n ∇m I)^*α'];[ψn,m∨I^]

  :: (∇n I)∨∇m ⇒ ∇n+m∨I : n+1+m → 1

βの上付き添字が0からで、ψの上付き添字はnが1からmが0からでズレている。βも1からにして、0は単位に対してとっておく（reserve）がいいと思う。

---

次も定義だった。

• d∨e := (d e)*Y
• ∇¹ = I, ∇ⁿ⁺¹ := ∇ⁿ∨I = (∇ⁿ I)*Y

2-射である書き換えの図示は、アニメーション＝状態遷移シーケンス でも描ける。状態遷移シーケンスの場合、書き換えボックスのランド（ope-randのrand）位置だけでも描くと分かりやすい。書き換えそのものを図の要素とするために、書き換えボックスとテンプレート図がある。上記の定義はテンプレート図のシーケンスとして表現できる。

[追記]β⁰をやめて、β¹ := Y^:: Y⇒Y : 1+1→1 から定義を始めればよい。[/追記]