「テンソル半加法圏とプログラム意味論」で述べた半加法圏（semiadditive category）とテンソル半加法圏（tensor semiadditive category）の計算をチョビチョビとしています。割と昔から知っているものなんですが、あらためて計算してみると面白いことがけっこう見つかります。一方で、分からない事が増えたりもします。
半加法圏／テンソル半加法圏をプログラム意味論に使いたい、というのが僕の希望です。そして、使えるだろう、というのが僕の見通しです。なぜそのように思うのか、動機とか情況証拠とかを述べます。
まず、アーベル圏に触れます。まー、アーベル圏ってのがあるんですが、僕はそんなによく知らないです。が、とにかくモノ凄く豊かで役に立つ圏（の種類）です。なんでアーベル圏がそんなに使えるシロモノなのかと言うと、その上で（「その中で」か？）線形代数が出来るからです。つまり、アーベル圏の力とは線形代数の力です。
計算科学／情報科学でもアーベル圏が使えたらいいな、とは思うのですが、どうも計算（プログラム）のモデルとしてアーベル圏は出てこないようです。アーベル圏をこの分野に直接応用することはなんか無理っぽい。
しかし、アーベル圏から引き算や準同型定理を除いた半加法圏なら計算（プログラム）と関連します。実際、関係圏という具体例があります。論理やオートマトンのモデルにも半加法圏が使えます。半加法圏だけでは構造が弱いなら、テンソル積を入れてテンソル半加法圏とすれば相当にリッチな計算（むしろメタ計算）が出来ます。
ところで、計算（プログラム）のモデルとして今まで一番役に立った圏は何でしょう？ 人により評価は違うでしょうが、僕はデカルト閉圏だと思います。デカルト閉圏は、その名の通り、次の構造を持ちます。
デカルト積の代わりに一般のモノイド積を考えると、モノイド閉圏（閉モノイド圏とも言う）となります。関係圏は、モノイド閉圏の例にもなっています（「Alloyの矢印記法と、モノイド閉圏としての関係圏」、その他参照）。さらに関係圏は、テンソル積（指数でもある）に関してコンパクト閉圏にもなっています。（関係圏の転置は、コンパクト閉圏としては双対です。）
デカルト閉圏に直和の構造（余デカルト構造）を一緒に考えると双デカルト閉圏となります（閉構造は直積に関してだけ）。すべてのデカルト閉圏が双デカルト閉圏になるわけではありませんが、集合圏には双デカルト閉構造が載ります。case文のような場合分けを含む決定性の計算のモデルは双デカルト閉圏なのだと思います。
一方、非決定性の計算は半加法圏をベースにモデル化されるのでしょう。「決定性→非決定性」≒「集合圏→関係圏」 という移行において、直積と直和は融合して単一の演算に潰れてしまいます。なんか相転移みたいな現象です。それにも関わらず、台集合の構成法である集合の直積（圏論的直積とは限らない）はテンソル積として（別な形で）復活します。集合圏の直積は、直和に退化する方向とテンソル積になって生まれ変わる方向に、二つの変容を遂げるようです。とても不思議です。
また、トレースが色々と形を変えて現れて、テンソル半加法圏では、加法的トレース（双積のトレース）と乗法的トレース（テンソル積のトレース）の二つのトレースを考えるべきなのかも知れません。テンソル積に関してコンパクト閉な圏では、乗法的トレースは自動的に入っています。加法的トレースと乗法的トレースはどういう関係があるのでしょうか？ ハッキリしません。
直積、直和、双積、テンソル積などの色々な“積”と、それらに関するトレースや閉構造の相互関係は（僕には）謎が多いってことです。ベースとなる半加法圏／テンソル半加法圏について調べると何か分かるかも知れません。特に、エンドセットの半環構造と行列計算あたりが当面の調査対象でしょう。さらに具体的な目標は、テスト付きクリーネ代数の絞り出しです。
