このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

参照用 記事

今週見つけた圏

今週(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はヤヤコシイ面があります。しかし、このヤヤコシサが現実を反映しているのだとすれば、より精密なモデルなのだとも言えるでしょう。