今週（2012-06-04からの週）は、圏TotPtRelの話をしてましたね。
- 月曜： 役に立ちそうだが奇妙な圏
- 火曜： 続報・役に立ちそうだが奇妙な圏： コレ、使えそう
- 木曜： 奇妙じゃなかった、これは役に立つ圏
月曜日は「変なものを見つけちゃったよ」という感じでしたが、今日（土曜日）は「いいものを見つけたようだ」と思ってます。
圏TotPtRelが面白いのは、テンソル積を2つ持つことです。しかも、2つのテンソル積に対角と余対角が揃っています。対角と余対角があれば、ホムセットに足し算を導入できます。
- f +× g := Δ×;(f×g);∇×
- f +* g := Δ*;(f*g);∇*
2つの対角はほとんど同じなので、足し算の性格は余対角が決めているといっていいでしょう。その余対角は次のように定義できます。
- ∇× := W×;∇#
- ∇* := W*;∇#
W×とW*は、テンソル積を直和に写す射です。
- W×A,B:A×B→(A # B)
- W*A,B:A*B→(A # B)
結局、2つの足し算 +×, +* はW×とW*に起因するのですが、W×とW*の直感的な意味は：
- 計算が早く終わったほうの値を採用する。
- 両方の計算が終わるのを待ち、どちらかを採用する。
「待ち」に対する態度が違うのですね。計算が常に有限時間で終わる状況なら、上記の2つは同じことです。どちらが早く終わるかも非決定的だし、どちらかを採用するかも非決定的だとすると、「どちらかの値を採用する」ことになり、違いは出ません。「待ち」に対する態度により差が出るのは「無限に待たされた」ときです。
圏TotPtRelの対象である集合 {1, ⊥} は、void型に対応します。通常、void型は単元集合ですが、「無限待ち」を表現する⊥を加えています。ホムセット TotPtRel({1, ⊥}, {1, ⊥}) = End({1, ⊥}) は、void→void という非決定性計算を表現しますが、このホムセットのなかでは、2つの足し算が論理ORと論理ANDのように振る舞います。否定を持たない三値論理と解釈できます。
通常のブール値 {true, false} を、Ω = {true, false, ⊥} として圏TotPtRelの対象と考えることもできますから、否定を使った計算を排除しているわけではありません。ですが、A上の述語 A→Ω は、結果を出さないこと（結果が⊥）もあれば、どっちつかずの値（{true, false}、{true, false, ⊥}）となることもあります。
集合圏Setや関係圏Relに比べると、圏TotPtRelはヤヤコシイ面があります。しかし、このヤヤコシサが現実を反映しているのだとすれば、より精密なモデルなのだとも言えるでしょう。
