日々の流転

Linear Logic を *-autonomous category でモデル化した Seely は、*-autonomous category を finite product と closed involution を持った symetric monoidal closed category と定義していますね。このほうが finite product がコンテクストを扱うのだろうすぐに想像できるかなと思います。が、A^⊥ を not A として扱うので Girard のオリジナルに近いもので考えるときは dualizing object を考えたほうがよいのかな。まあ、どちらの定義も等価でしょうが、きっと。

Seely の「Linear logic, *-autonomous categories and cofree coalgebras」には以下のように書かれているので、finite product は *-autonomous category ではなく linear category の条件です。<br># ただし、この linear category は現在使われているものとは異なりますが。<br><br>1.4 Definition. A linear category G is a *-autonomous category with finite products.<br><br>Remarks. For a fuller disussion of *-autonomous category, see Barr [1979]. Here just let me say that G is a closed symmetric monoidal category G with an involution ¬: G^op → G given by dualising object φ : in our notation this means ¬A = A -o φ and the canonical arrow A → ((A -o φ) -o φ) is an isomorphism. (Barr uses * for our ¬.) <br><br>> このほうが finite product がコンテクストを扱うのだろうすぐに想像できるかなと思います。<br><br>コンテキストは基本的にはテンソルで繋げば良いので、単に additive な演算子を解釈するためではないかと思います。