コンパクト閉圏（compact closed categories）やその仲間の圏が、だいぶ利用されるようになってきました。それで、「なんで『コンパクト』なんだろう？」と一度は疑問に感じますよね。トポロジーのコンパクトとは関係しそうにありません。
僕は、コンパクト論理（compact logic）に由来するとどこかで読んで、それでスッカリ納得していました。が、最近、再確認しようと調べたら、コンパクト論理に関する記述が全然見つかりません。という事情で、裏を取れてないのですが、僕のうろ憶えに基づき、コンパクト論理とコンパクト閉圏の関係を書いておきます。
古典論理
論理記号（「論理記号のいろいろ」参照）として次を採用します。
- ∧ 連言（かつ）
- ∨ 選言 （または）
- ¬ 否定（でない）
- ⊃ 含意 （ならば）
- T 真
記号「|-」は、証明可能性です。証明可能性に関しては「論理とはなにか？」や「さまざまな「ならば」達」で説明してます。
まずは古典論理を考えることにして、次のような法則はお馴染みでしょう。
- (A∧B)∧C ≡ A∧(B∧C) （∧の結合律）
- T∧A ≡ A∧T ≡ A （真との連言）
- ¬¬A ≡ A （二重否定）
- ¬(A∧B) ≡ ¬A∨¬B （ド・モルガンの法則）
- A⊃B ≡ ¬A∨B （含意の言い換え）
ここで、記号「≡」は論理的な同値を示し、A ≡ B は、 A |- B と B |- A の両方が成立することだと思えばいいでしょう。あるいは、|- (A⊃B)∧(B⊃A) と解釈しても同じです。後者の場合、表現 A ≡ B を (A⊃B)∧(B⊃A) の略記だと思い、何の仮定もなしに証明できる論理式を“法則”と呼んでいるのだ、とも理解できます。
古典論理の有名なメタ定理に、次の演繹定理（えんえきていり；deduction theorem）があります*1。
- A, B |- C ならば、B |- A⊃C
AとBを仮定することはA∧Bを仮定することだし、A⊃C は ¬A∨C だったので、次のように書いても同じです。
- A∧B |- C ならば、B |- ¬A∨C
連言と選言が一致した奇妙な論理
僕の記憶によれば、連言∧と選言∨が一致してしまった論理がコンパクト論理です。連言でもあり選言でもある論理演算を記号×で表すことにします。
この論理は、論理としては相当に変なものです。なにしろ、真Tと偽Fも一致してしまいますから。真と偽が一致してしまった論理定数をIと書きます。すると、次は成立します。
- (A×B)×C ≡ A×(B×C)
- I×A ≡ A×I ≡ A
二重否定、ド・モルガンの法則、含意の言い換えも成立します（そういう論理を考えるのです）。
- ¬¬A ≡ A
- ¬(A×B) ≡ ¬A׬B *2
- A⊃B ≡ ¬A×B
線形代数への翻訳からコンパクト閉圏へ
コンパクト閉圏の典型例は有限次元ベクトル空間の圏に、双対とテンソル積を考えたものです。コンパクト論理の変数や記号を、次のように線形代数の概念・用語に翻訳します。
| コンパクト論理 | 線形代数 |
|---|---|
| 命題A, B | ベクトル空間A, B |
| 連言（選言）A×B | テンソル積空間 A×B |
| 否定 ¬A | 双対空間 A* |
| 含意 A⊃B | 線形写像の空間*3 A --o B |
| 論理定数 I | スカラー体 K |
「≡」はベクトル空間の同型とみなすと、次の法則は有限次元ベクトル空間で妥当なものです。
- (A×B)×C ≡ A×(B×C)
- K×A ≡ A×K ≡ A
- A** ≡ A
- (A×B)* ≡ A*×B*
- A --o B ≡ A*×B
演繹定理「A∧B |- C ならば、B |- ¬A∨C 」は、次の形になります。
「証明できる」を「線形写像がある」と解釈するわけです。演繹定理は逆も成立するので、線形写像の集合Lin(A, B)を使って書けば：
- Lin(A×B, C) と Lin(B, A*×C) は同型
圏論的な言葉で言えば、「A×(-) というテンソル積関手と A*×(-) という双対をテンソル積する関手が随伴になっている」ってことですね。
ベクトル空間のテンソル積を一般的なモノイド積に置き換え、ベクトル空間の双対をジグザグ恒等式を満たすスター関手（「ベル状態、少し分かった、がやっぱりよくは分からん」のまんなかへんを参照）に置き換えればコンパクト閉圏の定義になります。
[追記]線形論理の創始者ジラール（J.-Y. Girard）が、compact linear logic って言葉を確かに使っています。「コンパクト」の意味は、論理記号／論理法則が少なくて簡略化された、ということでしょう。[/追記]
