ハロ多圏と上江州計算 - (保存用) 檜山正幸のキマイラ飼育記メモ編

ハロ多圏と上江州計算を組み合わせると、かなり強力な道具になりそう。

上江州計算では、重複器、放電器、交差の存在を暗黙の前提にしている。それぞれ、変数の複数回出現（重複）、変数の未出現（未使用）、変数の順序交換（出現位置の順序が変わる）ことに相当する。

上江州アタッチメントの概要； Vが変数集合、τ:V→|C|がソート（型）付けとして、C[V, τ]が定義できる。C[V, τ]には、x∈Vに対する変数射x:[x]→A（τ(x) = A）と逆変数射x^-1:A→[x]が含まれる。単にアタッチするだけなら、Cは任意の圏でよい（実はCが圏である必要もない）。

圏のブランド（セオリー）ごとに上江州アタッチメントを定義できるが、自由構成ができないとうまくいかない。モノイド圏やデカルト閉圏ではうまくいくだろう。V上のラムダ式（項）は、アタッチメントC[V, τ]に対して定義される。このとき、Vに全順序を入れておくほうが話が簡単だし、実用性もある。

有限部分集合X⊆Vに対して、Xを整列した列{x₁, ..., x_n)を作れる。これから、対象[x₁]× ...×[x_n]が決まり、この対象をXの領域[X]だと定める。上江州ラムダ項Mと、Free(M)⊆X であるXの組を {X}M と書く。Xが省略されたときは、X = Free(M)だとする。この形式が [X]→τ(M) という射を定める。ここで、τ(M)はMに対する型（再帰的に定義できる）。

Y⊆X に対して、上江州抽象 Y↑({X}M) が定義できる。

Y↑({X}M) = {X＼Y}(ΛY^→.M)

「＼」は差集合、Y^→はYを整列させた列、Λはデカルト閉圏の意味でで解釈される。

以上の構成を、ハロ多圏を使って再定式化できないか？できるはずだ。

上江州ラムダ項Mと変数集合Xが与えられると、ケリー／マックレーン・グラフもどきが描ける。Xを全順序で整列した列を上に並べ、Mの自由変数の出現から作られた列（集合やバッグではない！） FreeOcc(M) を下に並べ、対応する変数をつなぐ。このとき、つないだワイヤー群は重複、放電、公差の有限回の組み合わせとなる。これが、変数のジャンクション・パート。

変数のジャンクション・パート以外は、もとの圏Cで解釈できる。代入文を表す射（上江州さんの用語ではv←射）では、逆変数のジャンクション・パートが出現する。変数を扱う部分は、ハロ多圏内で吸収できるのかもしれない。もし、変数の使用をハロ多圏だけで済ませることができれば、上江州アタッチメントも不要になるかもしれない。いや、むしろ、変数を入れたハロ多圏を作り、それをパッキングすることで上江州アタッチメントを構成できるってことだな。

処方箋：

モノイド圏から単純ハロ多圏を作る。
ハロ多圏にジャンクションや多射を付け加える。
目的の多圏を作る。
パッキングする。
目的のモノイド圏を作る。
新しいモノイド圏と多圏がハロ構造になっていることを確認する。