ここのところ、ラムダ計算ベースのプログラム意味論とか、また考えてます。フレイド圏を基本的な道具にしようかと。
ベーシックなフレイド圏に対して追加したい構造には次のようなものがあるでしょう。
- 閉構造(指数構造)
- トレース
- インデキシング(パラメータ化)
- 強度
強度(strength)は、関手のテンソル強度以外にプロ関手の強度(プロ強度とでも呼ぶべきか)ってのもあります。
「アローの3文字演算子と対角付きプレモノイド圏」では、フレイド圏に対角構造という小物を追加しました。こういった小物もけっこう使い道があったりします。そこで、対角構造の双対とその変種についても述べておきます。
内容:
なぜプレモノイド圏か
フレイド圏 (C, K, J) のKは、モノイド圏ではなくてプレモノイド圏です。計算のモデルとしては、モノイド圏はうまくないところがあります。副作用を持つ並列計算が表現できないのです。
モノイド圏の交替律は次の形に書けます。
- fg = (fid);(idg) = (idg);(fid)
射をプログラムと解釈すると:
- プログラムfとプログラムgの同時実行(fg)が可能である。
- 同時実行は、fの次にgという順次実行((fid);(idg))と同じである。
- また、同時実行は、gの次にfという順次実行((idg);(fid))とも同じである。
fとgが副作用を持ち相互干渉があるとき、このようなことは成立しません。交替性を持つような積は一般には存在しないのです。「fの次にg」と「gの次にf」という順次積なら許されます。そして、その基本はプレモノイド積です。
すべてのプログラムにおいて交替可能な同時実行が不可能なわけではなくて、“タチのよいプログラム”なら交替性を持ちます。そのようなタチのよいプログラムが純射や中心射になるわけです。フレイド圏では、Kとは別にタチのよいプログラムだけの世界Cを想定しています。
タチのよくないプログラムまで考えると、モノイド圏には収まらなくてプレモノイド圏が必要になります。
余対角構造
余対角構造は対角構造の双対なので、その定義は矢印をひっくり返すだけす。「アローの3文字演算子と対角付きプレモノイド圏」の対角の定義から完全に機械的に構成できます。が、いちおう書いておきます。*1
K = (K, `×, ×', ×, I, α, λ, ρ, σ) が対称プレモノイド圏だとします。K上の余対角構造は、|K|でインデックスされた射の族 ∇A, θAで、次のような条件を満たすものです。
- ∇A:A×A→A
- θA:I→A
- (A, ∇A, θA) は、K内で(Aを台とする)可換モノイドとなる。
次の一貫性条件も仮定します。
θI:I→I ------------[ = ] idI:I→I I I×I θA×θB:I×I→A×B -------------------------------[ = ] θA×B:I→A×B (A×B)×(A×B) (A×A)×(B×B) ∇A×∇B:(A×A)×(B×B)→A×B --------------------------------------------------------------[ = ] ∇A×B:(A×B)×(A×B)→(A×B)
例を挙げます。Cを始対象と直和(デカルト余積)を持つ圏とします。始対象と直和によるモノイド圏を (C, +, 0) とします。f:A→Y, g:B→Y に対する余ペアリングを [f, g]:(A + B)→Y とします。∇A := [idA, idA] として、θAは始対象からの唯一の射(始射)とすると、(A, ∇A, θA) は直和に関する可換モノイドになります。一貫性条件も満たすので、{(∇A, θA) | A∈|C|} はC上の余対角構造になります。
擬余対角構造
余対角構造の定義から、(A, ∇A, θA) の可換性と、一貫性の三番目の条件を外した構造を擬余対角(quasi-codiagonal)構造と呼ぶことにします。一貫性の最初の2つは残しますが、残して意味があるかどうか分かりません。三番目を落とすと、対称性が不要になるので、対称性を持たないプレモノイド圏でも擬余対角は定義可能です。いずれにしても、かなりゆるーい構造です。
以下に擬余対角の例をあげます。
付点集合(pointed set)の圏をPtSetとします。圏PtSetの対象を、記号の乱用で A = (A, ⊥A) のように書きます。(A, ⊥A)×(B, ⊥B) := (A×B, (⊥A, ⊥B)) としてPtSetにおける直積を定義できるので、PtSetは直積でデカルト・モノイド圏になります。
∇A:(A×A, ⊥A×A)→(A, ⊥A) in PtSet を次のように定義します。(⊥A×A = (⊥A, ⊥A) に注意。)
- ∇A(x, ⊥A) = x
- y ≠ ⊥A ならば、∇A(x, y) = y
θA:({⊥}, ⊥)→(A, ⊥A) は、Aの基点をポイントする写像 θA(⊥) = ⊥A とします。
任意の A = (A, ⊥A) に対して、(A, ∇A, θA) は(極端に非可換な)モノイドになります。しかし、モノイドであることに間違いありません。これはPtSet上の擬余対角構造になります。
(A, ∇A, θA) はモノイドなので、F(X) = X×A という掛け算関手(A-スタンピング関手)の上にモノイダル・スタンピングモナドを構成できます。このモナドは、大域変数を上書き更新していく不純計算に対応します。
擬余対角は、ゆるくてイイカゲンな構造ですが、モナドを大量生産するメカニズムは与えます。一貫性に欠けているので扱いにくいかも知れませんが、その扱いにくさは大域変数や上書き更新のダメさを表現するものでしょう。
*1:書き写す段階で、「アローの3文字演算子と対角付きプレモノイド圏」のミスを発見して直しました。機械的な変更も無駄ではなかったです。