日記 (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.1.
対称モノイダル圏 が以下の条件を全て満たすとする。
- はモノイダル閉である。
- 対称モノイダル関手 !:→ およびモノイダル自然変換 δ:!⇒!∘!, ε:!⇒id が存在し、 (!,δ,ε) はコモナドを成す。
- モノイダル自然変換 d:!→!⊗!, e:!⇒⊤ が存在し、 任意の対象 A に対し、 (!A,dA,eA) は可換コモノイドであり、 dA:!A→!A⊗!A, eA:!A→!⊤ は !-余代数の射である。
- 任意の対象 A,B および射 f:!A→!B に対し、 f が !-余代数の射であれば、 f はコモノイドの射でもある。
このとき、 を線型圏 (linear category) という。
この圏上に論理式と項の解釈を適切に定めることで、 線型論理のモデルを作ることができるのだが、 それについては次回行うことにする。
参考文献
- G. M. Bierman (1993) 「On intuitionistic linear logic」 Ph. D. thesis, The University of Cambridge