線形論理とトレース
なんかのはずみで見つけた"Polarized Proof Nets with Cycles and Fixpoints Semantics"（http://www.pps.jussieu.fr/~montela/papers/tlca03.pdf）がけっこうひろいものだった。どうやって引っかけたか忘れたが：
とかでリストされる。
僕が興味を持ったのは、推論図ごとにトレース付きデカルト閉圏における解釈が表になっていたところ。実際には条件“デカルト閉”を弱められて：
- 特定のオブジェクトRが存在する。
- R(-)に相当する自己関手Pがあって、C(A×B, R)とC(A, P(B))が同型。
つまり、Rに関してだけ、ベキ、（アン）カリー化などの概念が使える。ゲンツェン風LJの解釈は、こういう圏（なんて呼ぶのか？）でもできるようだ。Rを真偽値、P(B)をB上の述語の全体（を対象とみなしたもの）と解釈できるのだろう、たぶん。デカルト閉圏とは違い、無制限に高階対象を作れるわけではない。×をテンソル積、Rをスカラー体と思うと、線形代数でも通用するハナシだと思う
mixルールがモノイド積、cutがトレース、コントラクションが余対角、水増しが終対象兼モノイド単位に対応する。明示的に換(interchange)を入れると、換は対称になるのだろう。ここで、「モノイド積と対称とトレースで、結合が表現できる」というアノ定理（トレース付きモノイド圏における結合）が意味を持つかもしれない。
