テンソル計算のカリー/ハワード対応

一値論理=コンパクト論理 - (新) 檜山正幸のキマイラ飼育記 メモ編 を敷衍。

行列 線形写像 コンパクト論理 ストリング図
スカラー対象 真偽値「空」 無、点線
スカラー 矛盾シーケント 無ワイヤーノード
対象 命題 ワイヤー
複対象 命題リスト ケーブル
単純行列 単純射 単純シーケント 単純ノード
複行列 複射 複シーケント 複ノード
多行列=行列 多射=射 多シーケント=シーケント 多ノード=ノード
クロネッカー 射のテンソル シーケントのマージ ノードの横併置
縮約総和 縮約積 シーケントのカット ケーブル接続
射の結合 フルカット フル接続
パートナー対象 命題の否定 ストライクスルー
単位 一値排中律 ベント
余単位 一値矛盾律 コベント
パートナー対合 二重否定 二重ストライクスルー
双対射 待遇シーケント ジグザグ、蛇行
ポインター双対 背理法の原理 ベンディング
フォーム双対 背理法の原理 コベンディング

ポインター双対を作る操作は、ゲルファント変換。ゲルファント変換は通常 V→V** と書かれるが、V* → (¬V)* とみなす。V* は、Vのポインター空間。

次は別物:

  1. ベクトル空間(対象)
  2. ベクトル空間のパートナー空間(パートナー対象)
  3. ベクトル空間のフォーム空間=特別なホム空間
  4. ベクトル空間のポインター空間=特別なホム空間
  5. ペアの単位と余単位(スカラー積)は射

通常、次の同一視がされている。

線形代数 論理
ベクトル空間(対象)とポインター空間(ホム空間) 命題と右片側シーケント
パートナー空間(対象)とフォーム空間(ホム空間) 否定命題と左片側シーケント
ポインター空間とコフォーム空間(パートナー空間のフォーム空間) 右片側シーケントと左片側シーケント

集合圏なら:

集合 論理
集合空間(対象)とポインター集合(ホムセット) 命題と右片側シーケント
2指数集合(対象)と述語集合(ホムセット) 否定命題と左片側シーケント
ポインター集合と二階述語空間(指数空間の述語空間) 右片側シーケントと左片側シーケント

集合圏におけるゲルファント変換は、要素の評価汎関数になる。