先週、「Alloyの矢印記法と、モノイド閉圏としての関係圏」で、「Alloyで直積を表す矢印記号は、関係圏で解釈するとツジツマがあう」という話をしました。より一般に、Alloyの意味論を関係圏Rel上で展開してみるのは面白そうです。とはいっても、Alloyがカテゴリカルに設計されているわけでもないので、関係圏Relと実際のAlloyではズレている部分があります。このズレを眺めてみるのも楽しいように思えます。
というわけで、Alloyみたいなナニカの圏論的意味論をやってみようかな、と。目標は、Alloy本（『抽象によるソフトウェア設計−Alloyではじめる形式手法−』）の「付録C 中核の意味論」にある小さな言語と同等な圏論的形式言語の構文と意味論を作ってみることです。意味論の舞台は関係圏（の部分圏）ですが、構文のベースにはコンパクト論理を使うことにします。
今日はコンパクト論理の紹介まで、です。
内容：
- コンパクト論理
- 否定を持たないコンパクト論理
- コンパクト論理とAlloyとの関係
コンパクト論理
コンパクト論理とは、論理結合子のAND（連言、∧）とOR（選言、∨）が一致してしまった論理です。「コンパクト」は、「小さくて簡単」といった意味あいでしょう。ANDとORが一致してしまった論理結合子（二項論理演算）を「×」と書きます。他に、含意「⊃」と否定「¬」の論理演算記号、それと論理定数「I」を使います。
A, B などを命題（を表す記号）だとして、古典論理や直観主義論理のときと同様にシーケントを考えます。例えば、A, B → C, D のような形です。二項論理演算が「×」しかないので、シーケントの左右のカンマの解釈は両側とも「×」です。
Tを真、⊥を偽として、古典論理では次のような推論が成立します。
A, B → C
---------
A∧B → CA → B, C
---------
A → B∨CT, A → B
----------
A → BA → ⊥, B
----------
A → B
コンパクト論理でも同様な推論ができます。
A, B → C
---------
A×B → CA → B, C
---------
A → B×CI, A → B
----------
A → BA → I, B
----------
A → B
次の否定の導入も、コンパクト論理で使えます。
A, B → C
-----------
A → ¬B, C
古典論理の ¬B∨C ≡ B⊃C に対応するコンパクト論理版の同値性は ¬B×C ≡ B⊃C です。これを使うと、次の演繹定理も成立します。
A, B → C
-----------
A → B⊃C
コンパクト論理のモデルを与える圏がコンパクト閉圏で、「×」をモノイド積、「I」をモノイド単位、「¬」を双対、「⊃」を指数（ベキ）に対応させます。¬B×C ≡ B⊃C という同値性は、双対とモノイド積を使って指数を定義できることを示しています -- これがコンパクト閉性で、コンパクト論理／コンパクト閉圏のミソです。
他に、次のような対応があります。
| コンパクト閉圏 | コンパクト論理 |
|---|---|
| 射の結合 | シーケントのカット規則 |
| 恒等射 idA | 公理シーケント A → A |
| 対称 σ | シーケントの換規則 |
| 双対の対合性 | 二重否定の公式 |
否定を持たないコンパクト論理
コンパクト論理の4つの基本記号「×」、「I」、「¬」、「⊃」から「¬」を取り去って、「×」、「I」、「⊃」だけで考えます。非常に頼りない感じがしますが、古典論理の「∧」、「T」、「⊃」だけからなるサブセット（フラグメント）だけでもラムダ計算（のカリー／ハワード対応）はできるので、捨てたもんでもないです。
含意命題 A⊃B が ¬B×C という形では書けません。なにしろ「¬」がないので。しかし、もっと簡単な公式 A⊃B ≡ A×B が成立します。あるいは、¬A ≡ A なのだ、と思ってもかまいません。連言（AND）と選言（OR）が一致してしまい、さらに含意までも一致してしまったわけです。超コンパクト論理と言っていいかもしれません。
否定を持たないコンパクト論理＝“超コンパクト論理” の構文論や証明論は述べませんが、意味論には触れておきます。関係圏Rel、またはRelの適当な部分圏を取れば、否定を持たないコンパクト論理のモデルを作れます。これは、関係圏Relが自己双対コンパクト閉圏だという事実の言い換えに過ぎませんが。
CがRelの適当な部分圏、より正確に言えば、Cもまた自己双対コンパクト閉圏になるように取ったとして、否定を持たないコンパクト論理の構文要素にCの対象や射を割り当てることができます。
- 命題を表す記号A, Bなどに、Cの対象を割り当てる。
- 二項論理演算記号「×」に、Cのモノイド積を割り当てる。
- 論理定数記号「I」に、Cのモノイド単位対象を割り当てる。
- 二項論理演算記号「⊃」に、Cの指数（ベキ）を割り当てる。
シーケントの意味論は、Cからいったん多圏（polycategory） Poly(C) を作ったほうが精密ですが、めんどくさいので割愛。おおよそは次のようです。
- シーケントのカンマ「,」は、Cのモノイド積だと解釈する（「×」と同じ解釈）。
- シーケントには、Cの射を割り当てる。
- 特に公理シーケントには、Cの恒等射を割り当てる。
- 推論規則には、射のあいだの変換（ホムセットのあいだの写像）を割り当てる。
コンパクト論理とAlloyとの関係
Alloyで使われている論理がコンパクト論理か？と言うと、そういうことではありません。Alloyの論理式は、普通の古典論理の命題を表現しています。コンパクト論理の命題やシーケントは、Alloyのシグニチャにほぼ対応します。関係圏への意味写像がAlloyのインスタンスになります。
Alloyにおける古典論理の論理式は、インスタンス（意味写像）の制約に使われます。つまり、メタな立場の判断に古典論理が利用されています。これは、我々が、コンパクト論理の意味写像（値の割り当て）を外から眺めて、古典論理に基づく議論をしている構造と同じものです。
次回（があれば）、Relの適当な部分圏の作り方、インスタンス＝意味写像の制約の仕方などを調べてみます。
