スキーマとインスタンスと一般行列

かつてのCatyスキーマを今一度使おうと思う、理論的・教育的な目的で。

A, B, C などは型名を表すメタ変数、S, T などはスキーマを表すメタ変数として、スキーマは、

  1. A
  2. [], [A], [A, B], [A, B, C] など、
  3. {}, {a:A}, {a:A, b:B} など
  4. これらの入れ子

以上で作られるのは有限シェープの型だけだが、一般行列では、有限シェープの型しか使わない。

帰納的に定義される有限シェープのスキーマSに対して、そのインスタンス集合を Inst(S) と書く。基本型が有限個しかなく、型の外延がすべて有限集合である有限シェープのスキーマ完全有限スキーマ〈completely finite schema〉と呼ぶ。

Sが完全有限スキーマ、Vがベクトル空間のとき、Map(Inst(S), V) の要素を一般行列と呼ぶ。一般行列の全体は定義よりベクトル空間となる。完全有限スキーマSを、行列のシェープまたは型と呼ぶ。次の書き方を使う。

  • GMat[V](S) = GMat(S, V) := Map(Inst(S), V)
  • Mat[V](n, m) = GMat[V]([1..m, 1..n])
  • Mat(n, m) := Mat[R]([1..m, 1..n])

一般行列集合の集まりに、演算を入れたシステムを行列系または行列計算系〈matrix calculus | matrix caluculation system〉と呼ぶ。

テンソルドミニオンの一部を行列計算系に移す操作を行列化〈matricization | 動詞 matricize〉と呼ぶ。行列化には、色々な手法があり、関手になってくれるわけでもない。綺麗な定式化は期待できない。

いずれにしても、行列化のためには、問題となるベクトル空間に基底割り当てする必要がある。基底割り当てが決まっても行列化が決まるわけではない。どのような行列化手法を採るかも決めてなくはならない。

行列化した後で、次の計算が必要。

  1. 2つの射の結合
  2. 2つの射の適用
  3. 2つの射のテンソル
  4. 2つの射の適当なリンケージ(繋ぎ情報)による縮約
  5. 1つの射の適当なリンケージによるトレース
  6. 1つの射の転置または双対


記号のジレンマ:オーバーロードすれば意味が曖昧化する。オーバーロードしなければ記号が増えて記憶が大変。