論理や型理論の圏論的意味論

今年いっぱいくらい、まとまった時間が取りにくい状況があるので、長いブログエントリーは書けそうにない。短いエントリーをチョコチョコと書くことにします。短くて完結した書き物は難しいので、続き物になる可能性が高いです。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\hyp}{\text{－} }
%\newcommand{\id}{ \mathrm{id} }
\newcommand{\In}{ \text{ in } }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right]}
`$

今回はあまり短くもないですが。

---

さて、昨日の短いエントリー「型理論の演繹定理」から引用すると：

演繹定理は構文的な主張ですが、これを意味論的に解釈することは興味深い課題です

ここでの意味論というのは圏論的意味論〈categorical semantics〉のつもりです。論理や型理論の圏論的意味論とは、導出システムから圏への対応のことです。以下で、圏論的意味論をもう少し具体的に（あるいは抽象的に）説明します。

内容：

導出システムの圏と圏の圏

「導出システム」は次のような呼び方もされます。

• {導出 | 演繹 | 証明 | 推論}{システム | ç³»}
• {derivation | deduction | proof | inference} system

導出システム〈導出系〉*1については、「カリー／ハワード／ランベック対応のための“呼び名”と“書き方”」をみてください。

導出システムを形式的体系〈formal system〉としてキチンと定義すれば、導出システムのあいだの準同型射〈homomorphism〉も定義できます。とある種類の導出システム達は圏を形成します。導出システム達の圏を、プレースホルダー $`x`$ を使って次のように書きます。

$`\quad x\mbf{DS}`$

'DS' は 'derivation systems' または 'deduction systems' です。$`x`$ には導出システムの種類を入れます。例えば、'ConjImp' ＝ 'conjunctive implicative' を入れると、

$`\quad \mbf{ConjImpDS}`$

となり、これは、'conjunctive implicative derivation systems'〈連言含意的導出システム達〉の圏です。論理結合子〈logical connective〉として、$`\land`$〈連言 | and〉と $`\Imp`$〈含意 | implies〉だけを持つ論理の導出システムです。

一方で、圏論的意味論が“値をとる”圏達の圏は、プレースホルダー $`y`$ を使って次のように書きます。

$`\quad y\mbf{Cat}`$

$`y`$ には圏の種類を入れます。例えば、'CC' ＝ 'Cartesian closed' を入れると、

$`\quad \mbf{CCCat}`$

となり、これは、'Cartesian closed categories'〈デカルト閉圏達〉の圏です。

“圏の圏”を考える際には、いくつかのオプションがあります。

1. 対象である圏のサイズをどうするか？
2. “圏の圏”を1-圏とするか2-圏とするか？
3. “圏の圏”の1-射である関手のゆるさ〈looseness | weakness〉をどうするか？

一番単純な（しかし一般性に欠ける）オプション選択は：

1. 対象である圏のサイズは小さい〈small〉とする。
2. “圏の圏”を1-圏とする。自然変換は考えない。
3. “圏の圏”の1-射である関手は、構造を厳密〈strict〉に保存する関手とする。

デカルト閉圏達の圏に、選んだオプションの情報も添えると：

$`\quad {_1\mbf{CCCat}}^\mrm{str}`$

1. 名前の一部 $`\mbf{Cat}`$ により、小さい圏達の圏であることを示す（大きい圏を考えるなら $`\mbf{CAT}`$）。
2. 先頭の下付き $`1`$ が1-圏であることを示す。
3. 右肩の $`\mrm{str}`$ が、射が厳密にデカルト閉構造を保つことを示す。

導出システム達の圏 $`\mbf{ConjImpDS}`$ と圏達の圏 $`{_1 \mbf{CCCat}}^\mrm{str}`$ との対応は、カリー／ハワード／ランベック対応の原型となった対応です。以下、この事例を用いて説明します。

意味割り当て

「意味論」は曖昧な言葉ですし、曖昧なままに使いたいということもあるので、構文論的対象物〈syntactic object〉に意味論的対象物〈semantic objects〉を対応させるやり方は意味割り当て〈semantic assignment〉と呼ぶことにします。

いま、連言含意的導出システム $`S \in |\mbf{ConjImpDS}|`$ とデカルト閉圏 $`\cat{C}\in |{_1\mbf{CCCat}}^\mrm{str}|`$ が意味割り当て $`\rho`$ で結ばれるとします。$`S`$ と $`\cat{C}`$ は別な圏 $`\cat{C}`$ のなかに居るので、関手で結びつけるわけにはいきません。

デカルト閉圏から連言含意的導出システムを作り出す構成法があったとして、それを $`\mrm{CatDS}(\hyp)`$ とします。構成法 $`\mrm{CatDS}(\hyp)`$ は関手になると仮定すれば：

$`\quad \mrm{CatDS} : {_1\mbf{CCCat}}^\mrm{str} \to \mbf{ConjImpDS} \In \mbf{CAT}`$

関手 $`\mrm{CatDS}`$ が存在するなら、$`\mrm{CatDS}(\cat{C})`$ は $`\mbf{ConjImpDS}`$ の対象となり、次の記述が意味を持ちます。

$`\quad \rho : S \to \mrm{CatDS}(\cat{C}) \In \mbf{ConjImpDS}`$

あるいは：

$`\quad \rho \in \mbf{ConjImpDS}(S, \mrm{CatDS}(\cat{C}) )`$

圏 $`\cat{C}`$ そのままではうまくいかないが、圏から演繹システムを作る仕掛け $`\mrm{CatDS}`$ があれば、意味割り当てを関手として定義できます。

導出システムの構文圏と随伴系

連言含意的導出システム $`S\in |\mbf{ConjImpDS}|`$ から、うまいことデカルト閉圏を構成する方法があって、それが関手になっているとします。もしそういう構成法 $`\mrm{SynCat}`$ があれば、それは次のように書けます。

$`\quad \mrm{SynCat} : \mbf{ConjImpDS} \to {_1\mbf{CCCat}}^\mrm{str} \In \mbf{CAT}`$

導出システム $`S\in |\mbf{ConjInpDS}|`$ に対する $`\mrm{SynCat}(S)`$ を、$`S`$ の構文圏〈syntax category | syntactic category〉と呼びます。'syntactic category' は文法用語で構文範疇の意味もあるので注意してください。

もし、圏から導出システムを作る $`\mrm{CatDS}`$ と、導出システムから圏を作る $`\mrm{SynCat}`$ が随伴系〈adjunction〉を形成するなら非常に気持ちいいですね。そのような良い状況が実現すれば、随伴によるホムセット同型は次の形になります。

$`\quad {_1\mbf{CCCat}}^\mrm{str}(\mrm{SynCat}(S), \cat{C}) \cong \mbf{ConjImpDS}(S, \mrm{CatDS}(\cat{C}))`$

意味割り当て $`\rho\in \mbf{ConjImpDS}(S, \mrm{CatDS}(\cat{C}))`$ に対して、対応するデカルト閉圏のあいだの準同型射（厳密にデカルト閉構造を保つ関手） $`\check{\rho}`$ があります。

$`\quad \check{\rho} : \mrm{SynCat}(S) \to \cat{C} \In {_1\mbf{CCCat}}^\mrm{str}`$

しばしば、意味割り当て $`\rho`$ と対応する関手（圏達の圏の射）$`\check{\rho}`$ は同一視されます。同一視してもいいくらいに密接に関係しているわけです。

圏から導出システム、導出システムから圏、という双方向の対応を作って、それらが随伴系を形成することを示すのはけっこうな手間です。また、いつでもうまくいくとも限りません。が、構文論と意味論の関係を考える上で、この種の随伴系を想定するのは役に立ちます。

*1:「システム」か「系」かは何の違いもありません。使い分けの基準もなくて、どっちを使うかは気紛れです。