日記 (2018 年 3 月 5 日)

今回の目標は、 線型論理のモデルを作るための圏を定義することである。 ここで定義するのは、 Bierman†1 が提唱したものである。 コモノイドやコモナド上の余代数などを用いるので、 定義を復習しながら順に見ていくことにする。 これらの概念をすでに扱い慣れているのなら、 図式の部分は単なる定義の確認なので無視して構わない。

対称モノイダル圏 󰒚 を考える。 これがモノイダル閉であれば、 各対象 A に対し、 関手 -⊗A:󰒚→󰒚 は右随伴をもつ。 以降、 それを A⊸-:󰒚→󰒚 と書くことにする。 すなわち、 任意の対象 A,B,C に対し、 自然な全単射 Hom(C⊗A,B)≅Hom(C,A⊸B) が成立する。

対称モノイダル関手 !:󰒚→󰒚 を考える。 すなわち、 任意の対象 A,B に対し、 両方の変数に関して自然な射 󰔃φAB:!A⊗!B→!(A⊗B) および φ:⊤→!⊤ が存在して、 ⊤⊗!A!A!⊤⊗!A!(⊤⊗A)φ⊗id󰔃φ⊤A!A⊗⊤!A!A⊗!⊤!(A⊗⊤)id⊗φ󰔃φA⊤ (!A⊗!B)⊗!C!(A⊗B)⊗!C!((A⊗B)⊗C)!A⊗(!B⊗!C)!A⊗!(B⊗C)!(A⊗(B⊗C))󰔃φAB⊗id󰔃φA⊗B,Cid⊗󰔃φBC󰔃φA,B⊗C !A⊗!B!(A⊗B)!B⊗!A!(B⊗A)󰔃φAB󰔃φBA が全て可換である。 なお、 射のラベルのない矢印は、 対称モノイダル圏の構造射が誘導するものを表しているとする。

さらに、 モノイダル自然変換 δ:!⇒!∘!,ε:!⇒id を考える。 これはすなわち、 δ に関しては、 !A⊗!B!!A⊗!!B!(!A⊗!B)!(A⊗B)!(A⊗B)δA⊗δB󰔃φAB󰔃φ!A,!B!󰔃φABδA⊗B⊤!⊤!⊤!!⊤φφ!φδ⊤ が両方とも可換であることを意味し、 ε に関しては、 !A⊗!BA⊗B!(A⊗B)A⊗BεA⊗εB󰔃φABεA⊗B⊤!⊤⊤φε⊤ が両方とも可換であることを意味する。

以降は、 (!,δ,ε) はコモナドを成すとする。 すなわち、 !A!!A!!A!!!AδAδA!δAδ!A!A!A!!A!AδAε!A!ε!A がともに可換である。

次に、 2 つの関手 !⊗!: 󰒚 ⟶ 󰒚 A ⟼ !A⊗!A ⊤: 󰒚 ⟶ 󰒚 A ⟼ ⊤ を考えると、 これらはどちらも対称モノイダル関手になっていることが確かめられる。 そこで、 モノイダル自然変換 d:!⇒!⊗!,e:!⇒⊤ を考える。 すなわち、 d に関しては、 !A⊗!B(!A⊗!A)⊗(!B⊗!B)(!A⊗!B)⊗(!A⊗!B)!(A⊗B)!(A⊗B)⊗!(A⊗B)dA⊗dB󰔃φAB󰔃φAB⊗󰔃φABdA⊗B⊤⊤⊗⊤!⊤!⊤⊗!⊤φφ⊗φd⊤ が両方とも可換であり、 e に関しては、 !A⊗!B⊤⊗⊤!(A⊗B)⊤eA⊗eB󰔃φABeA⊗B⊤!⊤⊤φe⊤ が両方とも可換である。

各対象 A に対し、 (!A,dA,eA) は可換コモノイドの構造をもち得る。 これはすなわち、 !A⊗!A!A!A⊗!A(!A⊗!A)⊗!A!A⊗(!A⊗!A)dA⊗iddAdAid⊗dA !A⊤⊗!A!A⊗!A!A⊗⊤dAeA⊗idid⊗eA!A!A⊗!A!A!A⊗!AdAdA が全て可換であるということである。 なお、 最後の図式の右側の垂直な射は、 テンソル積の左右を入れ替える同型射である。

さて、 各対象 A に対し、 !A,!A⊗!A はともに !-余代数の構造 (!A,δA),(!A⊗!A,󰔃φ!A,!A∘(δA⊗δA)) をもつ。 そこで、 dA:!A→!A⊗!A は !-余代数の間の射であるとする。 すなわち、 !A!A⊗!A!!A⊗!!A!A!(!A⊗!A)dAδAδA⊗δA󰔃φ!A,!A!dA が可換であると仮定する。 さらに、 ⊤ も !-余代数の構造 (⊤,φ) をもつので、 eA:!A→⊤ も !-余代数の射とする。 これにより、 !A⊤!!A!⊤eAδAφ!eA が可換だと仮定することになる。

これまでの仮定から、 各対象 A に対し、 !A は !-余代数の構造とコモノイドの構造を両方もつ。 したがって、 対象 A,B に対して、 射 f:!A→!B が !-余代数の射であるかを考えることもコモノイドの射であるかを考えることもできる。 f が !-余代数の射であるとは、 !A!B!!A!!BfδAδB!f が可換だということである。 また、 f がコモノイドの射であるとは、 !A!B!A⊗!A!B⊗!BfdAdBf⊗f!A!B⊤⊤feAeB がともに可換だということである。

以上のことを踏まえて、 我々はこれから以下の圏を考える。

この圏上に論理式と項の解釈を適切に定めることで、 線型論理のモデルを作ることができるのだが、 それについては次回行うことにする。

参考文献

1. G. M. Bierman (1993) 「On intuitionistic linear logic」 Ph. D. thesis, The University of Cambridge