Avendia20

日記 (2020 年 4 月 5 日)

論理体系と型システムの間には直接的な対応があることは古くから知られており、 これは Curry–Howard 対応と呼ばれている。 例えば、 直観主義論理は単純型付きラムダ計算と対応し、 この 2 つは実質同じものを別々の視点から捉えたものと見なすことができる。 さらに、 型システムと特定の構造をもつ圏の間にも同様の対応があり、 これら 3 つの関係は Curry–Howard–Lambek 対応と呼ばれることがある。 例えば、 今例に挙げた単純型付きラムダ計算はカルテシアン閉圏と対応するので、 直観主義論理と単純型付きラムダ計算とカルテシアン閉圏という 3 つの数学的対象は実質同じものと言える。

さて、 1987 年に Girard†2 によって線型論理という新しい論理体系が導入された。 すると、 今の述べた Curry–Howard–Lambek 対応において、 線型論理と対応する圏の構造とはどのようなものだろうかという疑問が湧いてくる。 そのような圏の構造については、 線型論理の発表から盛んに研究されており、 いくつかの候補が提唱されている。 今後しばらく、 それらの圏についてまとめていこうと思う。

いくつか記号に関する注意をしておく。 モノイダル圏のテンソル積は常に ⊗ で表し、 その単位対象は ⊤ で表す。 これは他の日記の記号と食い違う (1 で表している) 場合があるので注意すること。 代わりに、 終対象を 1 で表す。

まずは、 Bierman†1 による線型圏を挙げる。 私はこの圏が線型論理に対応する圏として最も適切だと (今のところ) 感じているので、 以降の議論はこの圏をベースとする。 なお、 この圏については 2018 年 3 月 5 日ですでに詳しく触れているので、 ここでは定義をおさらいするに留める。

定義 2.1.

対称モノイダル圏 󰒚 が以下の条件を全て満たすとする。

このとき、 󰒚 を線型圏 (linear category) という。

次に扱う圏の定義を述べる前に、 余 Kleisli 圏について復習しておく。

定義 2.2.

圏 󰒚 上のコモナド (!,δ,ε) に対し、 圏 󰒚! を以下のように定義する。

このように定めた圏 󰒚 を、 󰒚 の余 Kleisli 圏 (co— category) という。

定義から分かるように、 余 Kleisli 圏はもとの圏と比べて射の定義だけが異なる。 したがって、 考えている射や図式がどちらの圏のものであるか、 常に注意する必要がある。

余 Kleisli 圏ともとの圏との間には、 以下のような標準的な随伴が存在する。

命題 2.3.

圏 󰒚 上のコモナド (!,δ,ε) をとる。 関手 F: 󰒚! ⟶ 󰒚 ❲ABf❲ ⟼ ❲!A!B!f∘δA❲ G: 󰒚 ⟶ 󰒚! ❲ABf❲ ⟼ ❲ABf∘εA❲ は随伴 F⊣G を成す。 このとき、 !=F∘G が成り立ち、 随伴の余単位は ε に一致する。 さらに、 随伴の単位を η と書けば δ=F∗η∗G が成り立つ。

この命題により、 圏 󰒚 上のコモナド (!,δ,ε) があるとき、 上の定義の G:󰒚→󰒚! は左随伴をもつので、 極限を保存する。 したがって、 󰒚! の極限は (対象だけを考えれば) 󰒚 の極限と一致する。 特に、 󰒚 が有限直積をもてば 󰒚! も有限直積をもち、 それらは (対象だけを考えれば) 一致する。 以降、 󰒚 が有限直積をもつ文脈では、 󰒚! を直積によってモノイダル圏と見なす。

次に扱う圏は、 Seely†3 によって導入されたものである。 オリジナルの定義では、 圏に課している条件が少なく、 線型論理 (とそこから作られる計算体系) におけるいくつかの等式が、 圏の射に対応させたときに等しくならない可能性があった。 そのため、 ここではオリジナルの定義ではなく、 Bierman によって修正された定義を述べる。 この定義のモチベーションは、 圏に定まったコモノイドが定める余 Kleisli 圏をカルテシアン閉にすることである。

定義 2.4.

対称モノイダル圏 󰒚 が以下の条件を全て満たすとする。

このとき、 󰒚 を新 Seely 圏 (new — category) という。

いくつか記号を定義しておく。 新 Seely 圏 󰒚 において、 F はモノイダル関手であるから、 任意の 󰒚! の対象 A,B に対し、 󰒚 の射 󰔃χAB:FA⊗FB→F(A×B)χ:⊤→F1 が定まっている。 同様に、 G に対しても、 任意の 󰒚 の対象 A,B に対し、 󰒚! の射 󰔃ξAB:GA×GB→G(A⊗B)ξ:1→G⊤ が定まっている。 すると、 η がモノイダル自然変換であるとは、 任意の 󰒚! の対象 A,B に対し、 󰒚! における図式 A×BGFA×GFBG(FA⊗FB)A×BGF(A×B)ηA×ηBηA×B󰔃ξFA,FBG󰔃χAB1G⊤1GF1η1ξGχ が可換であるということである。 また、 ε のモノイダル自然変換であるとは、 任意の 󰒚 の対象 A,B に対し、 󰒚 における図式 FGA⊗FGBA⊗BF(GA×GB)FG(A⊗B)A⊗BεA⊗εBεA⊗B󰔃χGA,GBF󰔃ξAB⊤F1FG⊤⊤ε⊤χFξ が可換であるということである。

新 Seely 圏についてまず分かることとして、 F に定まる構造射は同型射になっている。 すなわち、 F は自動的に強モノイダル関手になる。

補題 2.5.

新 Seely 圏 󰒚 を考える。 F に定まる構造射 󰔃χ と χ はともに同型射である。

証明.

各対象 A,B に対し、 󰔃χAB−1 := ❲F(A×B)F(GFA×GFB)FG(FA⊗FB)FA⊗FBF(ηA×ηB)F󰔃ξFA,FBεFA⊗FB❲ χ−1 := ❲F1FG⊤⊤Fξ󰔃ξε⊤❲ である。 これが実際に逆射になっていることは、 容易に確かめられる。

この結果を用いると、 モチベーションとして述べた通り、 新 Seely 圏の余 Kleisli 圏がカルテシアン閉であることが示せる。

命題 2.6.

新 Seely 圏 󰒚 を考える。 その余 Kleisli 圏 󰒚! はカルテシアン閉である。

証明.

󰒚! が有限直積をもつことはすでに述べた通りである。 任意の 󰒚 の対象 A,B,C に対し、 補題 2.5 より 󰔃χCA:FC⊗FA→F(C×A) は同型射であるが、 F の定義によってこれは !C⊗!A≅!(C×A) が成り立つということである。 これに加えて 󰒚 のモノイダル閉性を用いれば、 Hom󰒚!(C×A,B) = Hom󰒚(!(C×A),B) ≅ Hom󰒚(!C⊗!A,B) ≅ Hom󰒚(!C,!A⊸B) = Hom󰒚!(C,!A⊸B) が成り立つ。 したがって、 󰒚! はカルテシアン閉であり、 A と B の冪は !A⊸B で与えられる。

通常の論理における含意 A→B は線型論理において !A⊸B に翻訳されることを思い出すと、 余 Kleisli 圏は線型論理に埋め込まれた通常の論理を表現していると捉えられる。

余 Kleisli 圏をカルテシアン閉にするというアイデアから定義された新 Seely 圏だが、 これは実は線型圏になっている。

定理 2.7.

新 Seely 圏は線型圏である。

証明.

命題 2.3 より !=F∘G であるから、 ! のモノイダル構造は、 各対象 A,B に対し、 󰔃φAB := ❲FGA⊗FGBF(GA×GB)FG(A⊗B)󰔃χGA,GBF󰔃ξAB❲ φ := ❲⊤F1FG⊤χFξ󰔃ξ❲ で定まる。 さらに、 補題 2.5 を用いて、 各対象 A に対し、 dA := ❲FGAF(GA×GA)FGA⊗FGAFdGA󰎘󰔃χGA,GA−1❲ eA := ❲FGAF1⊤FeGA󰎘χ−1❲ とおく。 なお、 dGA󰎘 は対角射であり、 eGA󰎘 は終対象への唯一の射である。 すると、 ここまでで定まった (!,󰔃φ,φ,δ,ε,d,e) が線型圏の公理を満たすことが容易に確かめられる。

参考文献

  1. G. M. Bierman (1993) 「On intuitionistic linear logic」 Ph. D. thesis, The University of Cambridge
  2. J. Y. Girard (1987) 「Linear logic」 『Theoretical Computer Science』 50:1–101
  3. R. A. G. Seely (1989) 「Linear logic, ∗-autonomous categories and cofree algebras」 『Conference on Categories in Computer Science and Logic』 92:371–382