たけをさんの記事「ドメイン付きクリーネ代数をAlloyで」をきっかけに昔考えていたことを蒸し返しているわけです。たけをさんは、「Alloyで直和を考える」という合いの手を入れたりもしてくれました。
「クリーニ代数と圏論」で、圏Cの構造から、対象AのエンドセットC(A, A)にクリーネ代数*1の構造が入ると言いました。しかし、「クリーネ代数の「テスト」を圏論的に定義できるだろうか？」において、同様な圏の構造からテスト付きクリーネ代数を構成するのは難しそうだ、と述べました。
前の記事の一部を引用してみると：
人為的な条件を付けないで、“自然に”テストの代数（ブール代数またはハイティング代数）が出てくるには、外の圏 (C, ×, 1, σ) の構造が弱すぎるんじゃないかと思っています。双積以外に、もう一つのモノイド積が必要なんじゃないかと。
テストの代数を天下りに与える方式はどうもスッキリしないのですが、外の圏がもっと豊かな構造を持つなら、テストの代数も自然に出現するだろう、と期待もしてます。
今日は、ここらへんについて、思い出すまま／思い付くままに記します。寄り道して色々なことをしゃべっています。
内容：
- 記法を変更する
- 論理半環
- 論理半環を絞り出すシナリオ
- 個体と世界の関係
- 半環圏と追加の構造
- 関係圏を観察してみる
- 論理演算は天から降りてきた
記法を変更する
Cを零対象と双積を持つ圏として、それを対称モノイド圏とみなしたものを (C, ×, 1, σ) と書いてきました。直積と直和が一致して、終対称と始対象が一致しているので、(C, +, 0, σ) と書いても同じことです。ここから先では、双積を+、零対象を0と書くことにします。
なぜ、双積を+に変えたかというと、×を別な意味で使いたいからです。×は双積とは別なモノイド積を表す心積りです。また、以前は+を射の足し算の意味で使っていたので、これも変更して、射の足し算は∨にします。
| 意味 | 旧記法 | 新記法 |
|---|---|---|
| 双積 | × | + |
| 零対象 | 1 | 0 |
| 射の足し算 | + | ∨ |
| 別なモノイド積 | × |
論理半環
テスト付きクリーネ代数でテストと呼ばれるモノは、命題、述語、条件、真偽値、プロパティなどとも呼ばれます。そのようなモノを扱う計算が論理計算です。論理計算の舞台となる代数はブール代数やハイティング代数ですが、もう少し弱い構造として、論理半環（logical semiring）を定義します。「論理半環」は一般的な用語ではありませんのでご注意。
論理半環の足し算（論理和）を∨、掛け算（論理積）を∧で表し、足し算と掛け算の単位元はそれぞれ0と1とします。論理半環はその名のとおり半環ですが、次の条件を加えます。
- 足し算がベキ等である。a∨a = a
- 掛け算が可換である。a∧b = b∧a
- 掛け算がベキ等である。a∧a = a
- a∧b = a と a∨b = b は同値である。
一番最後の条件は、掛け算から導かれる順序と足し算から導かれる順序が同じだ、ということです。つまり：
- a∧b = a ⇔ a∨b = b ⇔ a≦b
ハイティング代数やブール代数は、論理半環に演算や条件を追加して定義できます。
論理半環を絞り出すシナリオ
以下では、圏Cの対象Aごとに、論理半環P(A)を構成することを目標に進みます。天下りにP(A)を与えるのではなくて、具体的に論理半環を作り出しましょう。
圏Cが双積に関する対称モノイド圏で、ベキ等律 Δ;∇ = id が成立し、トレースも持っているなら、エンドセットC(A, A)はクリーネ代数となります。テスト付きクリーネ代数の定義を踏襲するなら、クリーネ代数C(A, A)の部分半環として論理半環（テストの代数）を見出して特定することになります。このアプローチでは、論理半環の掛け算（論理積）∧は、自己射の結合（composition）と一致します。僕の感覚では、これに違和感を感じます。∧は、本来、圏の結合（合成）とは別物と思えるのです。∧は、結合とは別な圏論的構造に由来するべきだと思います。
この「感覚」とか「思い」は、「良い・悪い」、「正しい・間違っている」という話ではなくて、「好み」の問題かも知れません。そもそも、天下りがイヤで作り出したい、というのも僕の「好み」でしょう。「対象Aごとに、論理半環P(A)があったとさ」で話を始めても特に不都合はありません。でも僕は「気持ちが悪い」のです。
以上のごとき断りを入れた上で、論理積∧はどこからやってくるべきでしょう？ それは、双積+とは別なモノイド積×からです。論理和∨としては、既に述べた一般的な射の足し算 p∨q = Δ;(p + q);∇ を採用するのですが、論理積∧も、p∧q = δ;(p×q);ρ と定義をしたいのです。ここでδとρは、モノイド積×に関して対角／余対角に相当する射です（詳しくは後述）。
論理和∨は、双積によるモノイド構造に由来し、論理積∧はもう一つの別なモノイド構造に由来することになります。つまり、論理半環を構成するには、外の圏が2つのモノイド構造を備える必要があります。圏に備わった2つのモノイド構造が、対象やホムセットに構造を与えるのです。
個体と世界の関係
論理和∨や論理積∧を、プリミティブな演算として捉えないで、わざわざ外の圏の構造から作り出すのは面倒なことです。なんでそんなシチメンドクサイことをするのか？ 「好み」ではありますが、「個体に構造は内在しない」が背後にあるスローガンです。
圏の事例の多くは、構造を持つ集合と準同型写像の集まりです。モノイドの圏とか順序集合の圏とか。これらの事例では、個体（個々の集合）に構造があり、構造を持つ個体達が集まって世界を形成しています。
しかしですね、圏の定義に「対象は集合だ」という前提はなくて、むしろ対象はアトミックな点です。点に構造なんてありません。ホムセットなら集合だから構造を持ってもいいのですが、ホムセットの構造は圏の構造から“導入される”べきだと思うんですよ、好みだけどね。そして、ホムセットの構造から、あたかも対象が構造を備えているように見えるってことだろう、と。
個体の構造は、個体自身が本来的に持っているのではなくて、世界の構造を反映しているのだ、という発想です。そうなると、ある程度複雑な構造を個体に入れるには、世界である外の圏もそれなりに複雑な構造を持つ必要があることになります。僕が考えている構造を持つ圏は、半環圏にさらに構造と条件を付け加えたものです。
半環圏と追加の構造
半環圏（semiringal category）とは、2つのモノイド積を持つ圏で、圏全体として半環のような構造を持つものです。対象が半環である「半環の圏」とか、エンドセットが半環になる話とかとは別物です。
圏Cの2つのモノイド積を足し算+と掛け算×で表して、単位対象は0と1、足し算の対称性をσで表します。すると、（記号の乱用で）C = (C, +, 0, σ, ×, 1) と書けます。Cが半環圏であるとは：
- (C, +, 0, σ) は対称モノイド圏
- (C, ×, 1) は（対称とは限らない）モノイド圏
- +と×のあいだに左右の分配法則が成立する。
モノイド法則も分配法則も、等式ではなくて一貫性（coherence）と呼ばれる自然同型（成分が同型射である自然変換）で記述します。半環圏の法則はデカルト半環圏の定義を確認してみる（デカルト半環作用圏のために）に書いてあります。
半環圏において、掛け算モノイド積×にも対称性があるとき、対称半環圏と呼びます。対称半環圏では、圏全体が、可換半環のような構造を持ちます。
ここで考える半環圏は、対称半環圏であり、足し算のモノイド積+が双積で与えられるものです。双積は単なるモノイド積ではなくて、ペアリング（より一般にはタプリング）、射影、対角、余ペアリング（より一般には余タプリング）、入射（余射影）、余対角などの豊かな構造を持ちます。射の足し算は、対角、双積、余対角の組み合わせで定義されるのでした。
対称半環圏の掛け算モノイド積を、以下ではテンソル積と呼ぶことにします。テンソル積から射の掛け算を導きたいのです。しかし、単なるモノイド積であるテンソル積には、対角、余対角が付随していません。射の掛け算の定義には、対角と余対角が必要です。これらも仮定しましょうか？ ウーン、ちょっとやり過ぎなような。
「天下りな前提はイヤ」とか言いながら、外の圏にドンドン前提を加えると、その前提がまた人為的なご都合主義的なのではないか？ と疑問になります。双積はともかく、対角・余対角を備えたテンソル積は“自然”なものなのでしょうか？
関係圏を観察してみる
今しようとしていることは、外の圏を公理的に定義して、そのなかでテスト付きクリーネ代数を構成することです。外の圏の典型的具体例としては、関係圏Relがあります。関係圏Relが、一番“自然”な例だと言ってもいいでしょう。
自然な例である関係圏Relにおいて、テンソル積は存在します。それは集合の直積で与えられます。何度か注意しているのですが、とてもヤヤコシイので再度言っておくと； 関係圏Relにおける圏論的直積は集合の直積ではありません。集合の直和が圏論的直積であり、圏論的双積でもあります。
「双積である集合の直和」と、それとは別な「テンソル積である集合の直積」を備えた関係圏 Rel = (Rel, +, 0, σ, ×, 1, σ') （σ'はテンソル積の対称性）は、対称半環圏となります。あっ、それと、ベキ等律 Δ;∇ = id もOKです。
関係圏のテンソル積（実体は集合の直積）には対角があります。テンソル積の対角は、双積の対角（加法的対角）Δとは区別してδと書くことにすると、δA:A→A×A は、δA(a) = (a, a) で与えられます。δAは、（Aの）乗法的対角と呼ぶことにします。
乗法的対角を公理的に特徴づける必要がありますが、それは後回しにして、関係圏において乗法的余対角を探してみます。すると、なんだか見つからないのですよ。テンソル積の余対角を期待することは出来ないようです。[追記]関係圏には転置があるので、対角 δA:A→A×A の転置として、余対角 tδA:A×A→A を定義できます。その意味で、「存在しない」はウソです。僕が当初期待していた性質を持つ余対角ではないだけです。tδも利用価値はあると思います。[/追記]
しかしガッカリする必要はありません。我々の目的からは、任意の f, g:A→B に対して掛け算 f∧g を定義する必要はありません。「命題」と呼べるような射 p, q に対して論理積 p∧q が定義できればいいのです。関係圏において命題（あるいは、述語、条件、真偽値、プロパティ）と呼べる射とは何でしょうか？ そこをよく観察すると、論理積を定義する方法が見えてきます。
論理演算は天から降りてきた
集合圏Setにおいて、対象（集合）A上の命題の集合とは、ベキ集合Pow(A)だと言っていいでしょう。ベキ集合Pow(A)はホムセット Set(A, {0, 1}) と同じです。もっと言うと、反変のベキ集合関手は、二値真偽値{0, 1}によって表現（represent）されます。この方向を発展させると、トポスの定義になります。
関係圏Relでは、ホムセット Rel(A, {0, 1}) はAのベキ集合にはなりません。Rel(A, {0}) がAのベキ集合なのです。{0}は単元集合1です。1は、関係圏においては始対象でも終対象でもありません（始対象＝終対象＝空集合です）。1は、テンソル積（集合の直積でした）の単位対象として特徴付けられます。
この観察から、テンソル積の単位対象が、真偽値対象のような役割を果たすことが示唆されます。単位対象＝真偽値対象に乗法的余対角があれば、それに基いて命題の論理積を定義可能となりそうです。
乗法的余対角（テンソル積の余対角）を持つ対称半環圏（ただし、足し算モノイド積は双積、ベキ等律が成立）Cにおいて、対象Aの論理半環P(A)は次のように構成できます。
- 台集合は、ホムセットC(A, 1)。1はテンソル積の単位対象。
- 論理和∨は、p, q:A→1 に対して、ΔA;(p + q);∇1 と定義する。
- 論理積∧は、p, q:A→1 に対して、δA;(p×q);ρ と定義する。ρ:1×1→1 は、テンソル積の単位法則に伴う自然同型。
テンソル積×もモノイド積なので、左右の単位法則に伴う同型 λA:1×A→A、ρA:A×1→A があります。単位対象1に関しては λ1 = ρ1 なので、それを単にρと書きました。
乗法的対角δの公理的定義をまだしてないし、実は、δA以外に εA:A→1 という射も必要だったりします。簡単に言うと、対象Aごとに、(A, δA, εA) が、Aを台対象とする余可換余モノイドになるのです。δAが余乗法、εAが余単位を与えます。
圏の直積（デカルト積）も、終対象を単位対象とする対角付きモノイド積として特徴付けることができます。対角／余対角、余単位／単位の観点から3つの積（実際には、双積として2つに退化する）をまとめてみると：
- 圏論的直積は、対角Δを持つ。余単位の射は、終対象への唯一の射である。
- 圏論的直和は、余対角∇を持つ。単位の射は、始対象からの唯一の射である。
- テンソル積は、対角δを持つ。余単位の射εは、構造の一部として与えられる。
直積と直和が一致して双積となることやベキ等律 Δ;∇ = id と共に、対角／余対角の構造が論理演算∨、∧の源泉となっています。
対角／余対角の構造を実際に書き下してみると、これは圏Cが持つ構造というよりは、Cの自己関手に働く自然変換のなかで定義される構造です。つまり、世界である圏を制御する、より上位（メタレベル）にある天上界の法則性と言えます。天上界の法則が、世界のなかの個体に構造を与え、個体どうしの関連性を支配しているのです。
なんか神学っぽいけど、具体的に定義を書き下すと実際にそうなっているはずです。実際のところメンドクサイし、途中でほったらかした所もあるのですが、テンソル積に付随する対角から論理積が出てくるのは割と確実じゃないのかな。
気力が残っていれば、そのうち具体的な定義も書き下すかも。
