多線形代数

「多ベクトル空間＝ベクトル空間のリスト」を対象として多線形写像を射とする圏をPLとする。PLは複線形写像の圏（ちょっと奇妙な圏だが）の上のモナドのクライスリ圏。そのモナドは拡張スタイルで定義すると：

  • 型構成子は、T: (V1, ..., Vn) \mapsto (V1\otimes...\otimesVn)
  • 単位は、τV:V→T(V)
  • 拡張は、複線形写像の線形化 f \mapsto fL

クライスリ圏PLにおけるプロファイル計算を、ゲンツェンのLK風に行う。

プロファイル＝シーケントの推論を、多線形写像の“変換”と呼ぶことにする。

   プロファイル
  -------------- 変換
   プロファイル

変換は、PLのホムセットのあいだの写像になる。変換は：

  1. 換： リストの置換、置換射の前結合と後結合
  2. 増減： Iの挿入と削除
  3. カット： 縮約
  4. \otimes導入： 左辺または右辺に\otimesを入れてよい
  5. ゲルファント変換： 右辺の項目を、￢を付けて左辺に移動
  6. 反ゲルファント変換： 左辺の項目を、￢を付けて右辺に移動

使ってよい基本シーケントは：

  1. A → A
  2. ￢A, A → I
  3. I→A, ￢A
  4. A, B → B, A （換と同等）
  5. I, A → A, A→I, A （増減と同等）
  6. A → ￢￢A, ￢￢A → A （ゲルファント同型）

カリー化／反カリー化：

  U, V → W
 ---------------- カリー化
  U → [V → W]

ここで、[V → W] = homPL(V, W) \cong PL(V, W)。

他にシェーピング〈shaping〉という操作がある。

  U, ￢V → W
 ---------------- シェーピング
  [￢V/U] → W

フル・ゲルファント変換とシェーピングを続けた変換をネルソン変換と呼ぶ。

  U → V
  ----------- フル・ゲルファント変換
  ￢V, U →
  ----------- シェーピング
  [￢V/U] →

ネルソン変換に基底選択を続けると、成分表示

  U → V in PL
  ------------------- ネルソン変換
  [￢V/U] → in PL
  ------------------- 基底選択
  [J/I] >→ R in Set

シェーピングに関連して

  1. 形状付き型
  2. 形状付きデータ
  3. 形状付き引数
  4. 形状付き引数関数

形状の書き方：

\newcommand{\hyph}{\mbox{-}} \begin{pmatrix} \begin{pmatrix} \hyph, & \hyph \end{pmatrix} \\ \begin{pmatrix} \hyph, & \hyph, & \hyph, & \hyph \end{pmatrix} \\ \hyph \end{pmatrix}