直観主義線型論理の圏論的意味論について
福田 陽介

yf00fyf@gmail.com
2018 年 12 月 11 日

1

はじめに
本文書は直観主義線型論理に対する圏論的意味論を概説することを目的とした記事です。*1
線型論理 (Linear Logic) は論理学者 Girard により考案された論理であり、普通の論理では認められる「仮定の複製」(いわゆる縮約規則) や「仮定の無視」(いわゆる弱化規則) をそのままの形では認めない論理です。
線型論理はしばしば「仮定を資源として捉える、resource-sensitive な論理」とも呼ばれ、例えば通常の論理では明らかに成り立つ以下の判断:• ` (A ∧ A) ⇒ A(「(A かつ A) ならば A」が成り立つ)• ` A ⇒ (B ⇒ A)(「A ならば (B ならば A)」が成り立つ)に対応する次の線型論理の判断は一般には成り立ちません (ここで、⊗, ( はそれぞれ ∧, ⇒ に対応する):• ` (A ⊗ A) ( A• ` A ( (B ( A)
詳しくは次の節で述べますが線型論理の基本となる論理体系では ` X ( Y という形の判断を示す際には、「結論 Y を導くためには X に現れる仮定を (Y を導くまでに) 必ず全て消費しなければならない」という制約を満たしつつ証明しなければならないからです。前者の ` (A ⊗ A) ( A では仮定の A を二つとも使わなければならないのに一つしか使えないため、また後者の ` A ( (B ( A) も余分な仮定 B が途中に現れるため共に成り立ちません。
線型論理は少々不便な論理のように思われるかもしれませんが、論理体系で通常仮定される証明の構造を細かく分解して解析するための道具として幅広く使われています (もちろん上で説明した状況では制限が強すぎるので体系に多少の構造を追加しますが)。
さて、本文書ではそのような線型論理に対して圏論的意味論 (Categorical Semantics) を与えるにはどうしたら良いかを概観します。圏論的意味論の与え方は色々と知られていて、例えば本文書で引用した文献はほぼ全て何らかの意味で線型論理の圏論的意味論を考えています。タイトルをいくつか見てみると、*1 この文書はぴあのん氏が主催する Category Theory Advent Calendar 2018 の第 11 日目の記事です。
前回は@t_uemura669101

さんによる第 9 日目の記事の「トポスと高階論理」でした。次回は第 16 日目の@math_neko さんによる「#豊穣圏は射が取れな
いからクソ ～射だけで理解できない豊穣圏～」です。

1

• “What is a categorical model for linear logic?” [Sch04]• “What is a categorical model of intuitionistic linear logic?” [Bie95]• “Categorical models of linear logic revisited” [Mel03]• “Linear λ-calculus and categorical models revisited” [BBDPH92a]
といったものがあります。読者の皆さんも一目見て分かるとは思いますが、筆者は線型論理の圏論的意味論の勉強を始めた時に「“What is” 論文が二つもあるの……？」とか「モデルに対して revisit しすぎじゃない？」と想ったものです。実際は他にもたくさんの文献があり勉強に苦労しました。そのため、本文書では筆者にとって分かりやすい流れで再構築した圏論的意味論の与え方を見ていきます。
具体的な流れは次の通りです。まず第 2 節で線型論理の証明論を定義します。ここで扱う線型論理体系はいわゆる直観主義の乗法的断片 (Multiplicative-fragment) および直観主義の MELL (Multiplicative Exponential

Linear Logic) になります。第 3 節では、それらの証明論の構造を記述するための圏である対称モノイダル閉圏および線型圏をそれぞれ定義し、圏論的意味論を与えます。最後の第 4 節では線型論理の解釈に使った線型圏が、ある随伴の関係を基礎とした LNL モデルと呼ばれる圏から記述できることを見ます。
■おことわり前提知識として数理論理学の証明論と圏論の基本的な知識を仮定します。証明論については直

観主義命題論理のシーケント計算を知っていることが望ましいですが、文法や推論規則の読み方が分かればなんとかなるかもしれません。圏論については随伴、カルテジアン閉圏などの知識は最低限仮定します。*2
また本文書では主に論文 [Sch04][Mel03][Ben94b] から内容を適当に取捨選択して説明しています。もっと言えば、本文書の第 3 節以降のほぼ全ての内容は上述の論文の各部分の丸パクリであることに注意にしてください。本文書の内容の詳細については以上の文献に直接当たることをお勧めします。
なお、本文書の間違いの指摘などは筆者の E メールアドレスにお送りいただけると幸いです。

2

直観主義線型論理の証明論
本 節 で は 直 観 主 義 線 型 論 理 の 証 明 論 を 定 義 す る。 最 初 に 直 観 主 義 線 型 論 理 の い わ ゆ る 乗 法 的 断 片(Multiplicative-fragment) を定義し、その後に直観主義の Multipilcative Exponential Linear Logic (MELL)を定義する。なお、通常「線型論理」と書いた場合は加法的断片 (Additive-fragment) も部分として含むが以降では単に「線型論理」と書いた場合は MELL を意味することとする。

2.1

直観主義線型論理の乗法的断片

ここでは直観主義論理の乗法的断片 (Intuitionistic Multiplicative Linear Logic) IMLL を定義する。
定義 1 (構文). IMLL の論理式 (Formula) および文脈 (Context) を次の文法によって定義する:

A, B, C, . . . ::= p | I | A ⊗ B | A ( BΓ, ∆, Σ, . . . ::= ∅ | Γ, A
ここで、p は命題変数の集合を動くメタ変数である。また I はテンソル積 ⊗ の単位元となる式である。各文脈

Γ について各要素を入れ替えて出来る文脈を Γ と同一視する（すなわち、記号「,」に対する可換性をメタに*2 あと本当はモノイダル圏について文書内で詳しく説明する予定だったんですが、途中で力尽きたために説明の無い用語が現れます（モノイダル自然変換とか）。なのでそこらへんは気をつけてください。まあ多分そのうち加筆修正するんじゃないかな！

2

仮定し、文脈を論理式の多重集合 (Multi-set) とみなす）。

IMLL の判断 (Judgment) とは文脈と論理式の組 hΓ, Ai であり、Γ ` A と表記する。
定義 2 (推論規則). IMLL の推論規則は図 1 に示す規則よって定義される。

Γ ` AA, ∆ ` B
I
Cut` I
Γ, ∆ ` B
Γ, A, B ` C
Γ ` A
∆ ` B
⊗R
⊗L
Γ, ∆ ` A ⊗ B
Γ, A ⊗ B ` CΓ ` A∆, B ` C
Γ, A ` B(L(RΓ, ∆, A ( B ` C
Γ ` A(BA ` A

Ax

図 1 IMLL の推論規則

注 3. まず推論規則を見て分かるように、通常の直観主義命題論理のシーケント計算で見られる以下の弱化(Weakening) と縮約 (Contraction) の構造規則:
Γ, A, A ` B
Γ ` B
W
C
Γ, A ` B
Γ, A ` B
は存在しない。また例えば規則 ⊗R などを見て分かるように、前提に出てくる仮定の多重集合 Γ や ∆ は結論においても要素数が変わらないように規則が作られている（ただし Cut 規則は例外）。以上の理由から、少々ラフな説明にはなるが IMLL で判断 Γ ` A が証明出来る際には結論 A は仮定 Γ の全要素を必ず使用して導かれることが分かる。
例 4. IMLL において以下の判断は証明可能:

1. A ` A
2. A, A 0 A
3. A ⊗ B ` B ⊗ A
4. I ⊗ A ` A
5. A ⊗ (A ( B ) ` B
6. A ⊗ (A ( B ) 0 A ⊗ B
7. A ⊗ (B ⊗ C ) ` (A ⊗ B ) ⊗ C
ここで Γ 0 A は判断 Γ ` A が証明不可能であることを表す。

2.2

直観主義線型論理

以上まででいわゆる “resource-sensitive” な論理 IMLL が定義できたが、ロジックとして利用する際にどんな状況においても仮定に対する構造規則が使えないのは流石に制限が厳しすぎる。そこで、IMLL を一項演
算子 ! を用いて拡張した直観主義線型論理 ( Intuitionistic Multiplicative Exponential Linear Logic) IMELL
を考える。

IMLL では仮定の弱化や縮約を許すための構造規則は、単項演算子 ! を用いて制御された形で定義される。

3

定義 5 (構文). IMELL の論理式および文脈を次の構文によって定義する:

A, B ::= p | I | A ⊗ B | A ( B | !AΓ, ∆ ::= ∅ | Γ, A
IMLL の場合と同様に p は命題変数の集合を動くメタ変数であり、文脈 Γ は論理式の多重集合とみなす。また、IMELL の判断 Γ ` A も IMLL の場合と同様に定義する。
定義 6 (推論規則). IMELL の推論規則は図 1 に示した IMLL の推論規則および図 2 の推論規則によって定義される。ここで、規則 P における !Γ は Γ ≡ A1 , . . . , An に対して !Γ ≡!A1 , . . . , !An と定義される文脈である。

Γ ` BWΓ, !A ` B

Γ, !A, !A ` B
CΓ, !A ` B

Γ, A ` B
D
Γ, !A ` B!Γ ` AP!Γ ` !A

図 2 演算子 ! に関する推論規則

注 7. 規則 W および規則 C から分かるように IMELL では !A という形の論理式については弱化と縮約が出来ることが分かる。論理式「!A」は直感的には「A が無制限に使える」と理解すれば良い。規則 D は公理!A ` A を実現するための規則である。規則 P は無制限な仮定 !Γ を仮定した下で結論 A が導けるならば、結論も無制限に使って良い (!A が成り立つ) ことを表す規則である。
例 8. IMELL において以下が成り立つ:

1. ` (!A⊗!A) (!A
2. ` !A ( (!B (!A)
3. !A ⊗ (!A ( B ) ` !A ⊗ B
4. !A⊗!B ` !(A ⊗ B )最初の二つの例はそれぞれ !A に対する縮約と弱化がなければ証明できない判断であることに注意せよ。

3

直観主義線型論理に対する圏論的意味論
本節では前節で定義した二つの証明体系 IMLL および IMELL に対して圏論的意味論を与える。

3.1

証明論に対して与える圏論的意味論について

始めに証明論の証明に対して圏論を用いた意味論を与えるとはどういうことかを説明する。
先に述べた IMLL や IMLL の証明論の「意味」は、形式的には論理式や判断の構造をまず決めて、さらには「それら論理式や判断に対して許される操作」を推論規則によって定めることで与えた。つまり証明そのものを直接的な数学的対象として定義するのではなく「推論のやりかた」を規定することで証明という概念の意
味を与えていた。
一方、以降で考える圏論的意味論では証明という概念を直接に数学的対象として定義する。具体的には、ある程度良い構造を備えた圏 C の存在を仮定し、IMLL や IMELL の証明を（メタ数学的対象であるところの）4

C の射として対応付けることによって解釈できることを見る。図的に表現すると、判断 Γ ` A の証明 Π が以下のように与えられた時:

ΠΓ ` A
圏 C 内で対応する射:

JΓK

JΠK

/ JAK

を定義することを考える。ここで、JΓK, JAK はそれぞれ Γ, A に基づいて定義される圏 C の適切な対象である。JΠK はそれらをドメインとコドメインに持つ圏 C の適切な射であり、Π から定まる。

3.2

乗法的断片に対する意味論

まず乗法的断片に対する圏論的意味論を考える。しかしながら、先に「ある程度良い構造を備えた圏を仮定する」と述べたが、実際に圏論的意味論を与えるためにはどのような構造を備えた圏が適切なのかを考えなければならない。
そこで以降では、非常に恣意的かつラフな説明の手続きではあるが次のステップに基づいて意味論を作る:

1. 解釈の対象である証明論 IMLL は「正しい」と仮定する（したがって、IMLL で構成可能な証明は全て対応する圏の何らかの射として構成できなければならない）

2. IMLL における可能な推論構造を確認し、圏として必要な構造を見出す
3. ある程度の構造が見出だせたら圏を定義してその圏の中で証明が解釈できることを示すと、ここまで説明したが実は IMLL に限って言えば圏に必要な構造を見出すのはそれほど難しくはない。結論から述べると対称モノイダル閉圏の構造があれば十分である。
まずそもそも IMLL の証明の構造を考えると単位元 I を持ち可換で結合的な積 ⊗ を持つべきことは分かる。
また以下の例から分かるように判断 Γ ` A の Γ に現れるカンマ「,」はテンソル積 ⊗ と同一視できる。したがって、文脈 Γ ≡ A1 , · · · , An に対する解釈 JΓK は JA1 K ⊗ · · · ⊗ JAn K として定義すれば良い。

例 9. IMLL では以下の推論が示すように、A, B ` C の証明が与えられた時に A ⊗ B ` C の証明が構成でき、また逆も可能。

ΠA, B ` C⊗LA⊗B ` C

Ax
Ax
A ` A
B ` B
A, B ` A ⊗ B
A, B ` CΠA⊗B ` CCut

加えて、以下の証明から分かるように射 JΓK → (JAK ( JB K) と射 JΓK ⊗ JAK → JB K とは対応が付く必要がある。すなわち圏の構造として C(X ⊗ Y, Z) ∼= C(X, Y ( Z) が要請される。

例 10. IMLL では以下の推論が示すように、Γ, A ` B の証明が与えられた時に Γ ` A ( B の証明が構成でき、また逆も可能。

ΠΓ, A ` B(RΓ ` A(BΠΓ ` A(B

Ax
Ax
A ` A
B ` B
(L
A, A ( B ` B
CutΓ, A ` B

以降では IMLL が対称モノイダル閉圏を用いて実際に解釈できることを述べる。
定義 11 (対称モノイダル閉圏). 対称モノイダル圏 (symmetric monoidal category) hC, ⊗, I, α, λ, ρ, σi とは5

圏 C、双関手 ⊗ : C × C → C、対象 I および以下の自然同型

1. αA,B,C : A ⊗ (B ⊗ C ) → (A ⊗ B ) ⊗ C
2. λA : I ⊗ A → A
3. ρA : A ⊗ I → A
4. σA,B : A ⊗ B → B ⊗ Aからなり、次に続く図式を可換にする圏である:
αA,B,C ⊗D

A ⊗ (B ⊗ (C ⊗ D))/ (A ⊗ B ) ⊗ (C ⊗ D)
αA⊗B,C,D

idA ⊗αB,C,D

A ⊗ ((B ⊗ C ) ⊗ D)

/ (A ⊗ (B ⊗ C )) ⊗ D

αA,B⊗C,DA ⊗ (B ⊗ C )αA,B,C/ (A ⊗ B ) ⊗ C

αA,B,C ⊗idD

σA⊗B,CA ⊗ (C ⊗ B )αA,I,C/ C ⊗ (A ⊗ B )αC,A,B

idA ⊗σB,CA ⊗ (I ⊗ C )αA,C,B/ (A ⊗ C ) ⊗ B

σA,C ⊗idB/ (A ⊗ I) ⊗ C

/ (C ⊗ A) ⊗ B

A⊗B

σA,B

'

/ B ⊗AσB,AρA ⊗idA

idA⊗B

A⊗C
以降では対称モノイダル圏 hC, ⊗, I, α, λ, ρ, σi を hC, ⊗, Ii と略記する。
idA ⊗λC/ ((A ⊗ B ) ⊗ C ) ⊗ D

% 
A⊗B

対称モノイダル閉圏 (symmetric monoidal closed category) とは対称モノイダル圏 hC, ⊗, Ii であって、以下の条件を満たすもの:• 任意の対象 A に対して、関手 (− ⊗ A) : C → C が右随伴 (A ( −) : C → C を持つ
定義 12 (型解釈). 各論理式 A に対して、対称モノイダル閉圏 hC, ⊗, Ii の対象を割り当てる型解釈 (typeinterpretation)J−K を以下の通り帰納的に定義する:
def

JpK = Apdef

JIK = Idef

JA ⊗ B K = JAK ⊗ JB K
def

JA ( B K = JAK ( JB K
ただし、Ap は C 上の固定された対象とする。
定理 13 (健全性). 任意の対称モノイダル閉圏は IMLL に対する健全なモデルとなる。すなわち、判断 Γ ` Aの IMLL の証明に対して対称モノイダル閉圏の射 JΓK → JAK が割り当てられる。*3*3 ここでは証明可能性が射の構成可能性を導くことのみを扱うが、実は証明正規化 (proof normalization) も考慮してモデルが与えられる。詳細は [Bie95][Bar96][BBDPH92a] などを参照せよ。

6

証明. 判断 Γ ` A に対する証明について、それが対称モノイダル閉圏の射に割り当てられることを証明に関する帰納法で示せば良い。例えば ⊗R, Cut, ( R はそれぞれ次の通り示せる。その他の場合については略。

• ⊗R. この場合の IMLL の証明図は以下の通り:
Π1
Π2
Γ ` A
∆ ` B
Γ, ∆ ` A ⊗ B
帰納法の仮定により Π1 および Π2 に対応する射はそれぞれ以下の通り得られる:
f

JΓK

/ JAK

/ JB Kg

J∆K

これら二つの射より、得るべき射 JΓ, ∆K → JAK ⊗ JB K は以下で定義できる:JΓ, ∆K∼=/ JΓK ⊗ J∆K

f ⊗g/ JAK ⊗ JB K

• Cut. 証明図は以下の通り:
Π1
Π2
Γ ` A
A, ∆ ` B
CutΓ, ∆ ` B
帰納法の仮定により Π1 および Π2 に対応する射はそれぞれ以下の通り得られる:
f

JΓK

/ JAK

JA, ∆Kg/ JB K

したがって、得るべき射 JΓ, ∆K → JAK ⊗ JB K は以下で定義できる:JΓ, ∆K∼=/ JΓK ⊗ J∆K

f ⊗idJ∆K∼=/ JAK ⊗ J∆K/ JA, ∆Kg

/ JBK

• ( R. 証明図は以下の通り:
ΠΓ, A ` B(RΓ ` A(B
帰納法の仮定により Π に対応する射が以下の通り得られる:JΓ, AKf/ JB K

したがって、得るべき射 JΓK → (JAK ( JB K) はモノイダル閉の性質と次の射から定義できる:

JΓK ⊗ JAK∼=7

/ JΓ, AKf

/ JB K

3.3

直観主義線型論理に対する意味論

IMELL に対する圏論的意味論を与える。ここでも IMLL に対して意味論を与えた際と同様に IMELL を解釈する際に必要となる圏の構造をまず探す必要がある。したがって、ここでは IMELL の IMLL に対する差分であるところの単項演算子 ! の構造、および ! が他の ⊗ や I に与える影響を調べなければならない。
これまたかなり天下り的な説明にはなるが、以降では必要な構造を推論規則および証明の例から探っていく。まず規則 D を証明 A ` B に適用して証明 !A ` B が得られることを考えると、圏では射 A → B から

!A → B を構成できる必要がある。そのため以下の射 εA の存在を仮定する:
!A

εA

/A

加えて、証明論 IMELL で ! の意味を規定する規則の一つである P を鑑みると、C(!Γ, !A) → C(!Γ, !A) といった対応付けを前提として要求したくなる。実際、これを射の割り当て (−)∗ として存在を仮定する:(−)∗ : C(!Γ, !A)/ C(!Γ, !A)

ここまでで εA および (−)∗ の存在を仮定したが、IMELL の証明を考えることでそれらに課すべき条件を見る。まず以下に続く三つの例を考える。
例 14 ((εA )∗ = id!A ). 以下の二つの証明は共に IMELL で証明可能:

Ax
A ` A
D
Ax
!A ` A!A ` !AP!A ` !A
まず右の証明は規則 Ax で示されているため恒等射 id!A で解釈することが自然である。また左の証明も右の証明と（きもち）同じ構造をしている。したがって天下り以外の何物でもないが圏の制約としてそれらの「同一性」を表した (εA )∗ = id!A を課す。
例 15 (εB ◦ (f )∗ = f ). 以下の二つの証明は共に IMELL で証明可能。

ΠAxΠ
!A ` BB ` B
PD!A ` !B!B ` B!A ` BCut!A ` B
左の証明図を Cut 除去した結果が右の証明図である。Cut 除去は証明の回り道を取り除くだけで証明の構造は変えない（ということにここではする）ので対応する制約として εB ◦ (f )∗ = f を課す。
例 16 ((g ◦ (f )∗ )∗ = (g)∗ ◦ (f )∗ ). 以下の二つの証明は共に IMELL で証明可能。

Π1
Π1
Π2
Π2
!A ` BP!A ` B!B ` CPP!A ` !B!B ` CCut!A ` !B!B ` !CCut!A ` CP!A ` !C!A ` !C
今までの議論と同様に対応する制約として (g ◦ (f )∗ )∗ = (g)∗ ◦ (f )∗ を課す。
以上で見た三つの例から三つの制約を考えたが、実はこれらの等式は以下で形式的に定義する co-Kleisli ト
リプルの可換性を表す。実際、三組 h!, ε, (−)∗ i は co-Kleisli トリプルをなす。
定義 17 (co-Kleisli トリプル). 圏 C の co-Kleisli トリプル (co-Kleisli triple) とは三組 h!, η, (−)∗ i:

1. 任意の対象 A に対して !A を割り当てる、対象の割当 ! : Obj(C) → Obj(C)82. 任意の対象 A に対して射 ηA :!A → A を持つ、射の族 η
3. 任意の射 f :!A → B に対して (f )∗ :!A →!B を割り当てる、射の割当 (−)∗ : C(!A, B) → C(!A, !B)
であって、任意の f :!A → B および g :!B → C に対して以下の条件を満たすものである:• (ηA )∗ = id!A
• ηB ◦ (f )∗ = f• (g ◦ (f )∗ )∗ = (g)∗ ◦ (f )∗以降では話の都合上、co-Kleisli トリプルの等価な言い換えであるコモナドを利用して意味論を考える:
定義 18 (コモナド). 圏 C のコモナド (comonad) とは、C 上の自己関手 !、自然変換 ε :! → idC , δ :! →!! からなる三組 h!, ε, δi であって、C の任意の対象 A に対して以下の図式を可換にするものである:

!A
δA


!!A

δA

/ !!A

id!A

!εA

!A

ε!A

δA

δ!A

δA

! 
/ !A


!!A

/ !!A

!δA


/ !!!A定理 19 (同値性). 任意の co-Kleisli トリプルはコモナドを導き、また任意のコモナドは co-Kleisli トリプルを導く。
証明. 略。
以上までで ! の解釈に必要な構造がある程度は求まったが、IMELL の ⊗ および I に関連する構造、また構造規則 W および C との関わりでもう少し構造を考えなければならない。具体的には次の例からも分かるように ⊗ と I との関わりから h!, ε, δi が対称モノイダルであることことを課す。また弱化規則と縮約規則の存在性より以下の射の存在を仮定する:

!A

eA

/I

!A

dA

/ !A⊗!A

加えて「縮約の異なる複数回の適用が本質的に同等である」や「弱化してから縮約を適用した結果は元の証明と本質的に同等である」といった要請から h!A, eA , dA i が可換コモノイドをなすことを課す。
例 20 (mA,B :!A⊗!B →!(A ⊗ B )). 以下が IMELL で証明可能。

Ax
Ax
A ` A
B ` B
D
D
!A ` A!B ` B⊗R!A, !B ` A ⊗ B
P!A, !B ` !(A ⊗ B )⊗L!A⊗!B ` !(A ⊗ B )例 21 (mI : I →!I). 以下が IMELL で証明可能。

I
` I
P
` !I
定義 22 (対称モノイダルコモナド). コモナド h!, ε, δi が対称モノイダル (symmetric monoidal) であるとは、! を対称モノイダル関手にする自然変換 m (射は mA,B :!A⊗!B →!(A ⊗ B)) と射 mI : I →!I が存在し、ε および δ がモノイダル自然変換であるときにいう。対称モノイダルコモナドは h!, ε, δ, m, mI i で表す。

9

定義 23 (可換コモノイド). 対称モノイダル圏 C における可換コモノイド (commutative comonoid) とは三組 hA, e : A → I, d : A → A ⊗ Ai: であって、以下の図式を可換にするもの:

A

d

/ A⊗A

d

" 
A⊗A

d

/ A⊗A

λA

" 
I⊗A

A

σA,A

/ A⊗A

d

A

d⊗idA

e⊗idA

/ (A ⊗ A) ⊗ A
αA,A,AdA⊗A/ A ⊗ (A ⊗ A)

idA ⊗d

最後に IMELL を解釈するための線型圏を定義し、健全性定理について述べる。
定義 24 (線型圏 [BBdPH92b]). 線型圏 (Linear Category) は以下からなる構造である:

1. 対称モノイダル閉圏 hC, ⊗, Ii
2. 対称モノイダルコモナド h!, ε, δ, m, mI i
3. 射 eA :!A → I および dA :!A →!A⊗!A を持つ自然変換 e および d であって次を満たす:（a）各 h!A, eA , dA i は可換コモノイドをなす（b）射 eA および dA は余代数射 (coalgebra morphism) をなす。すなわち、以下の図式を可換にする:

/ !!A

δA

!A

!A⊗!A

eA

!dA

dA

δA ⊗δA/ !!A⊗!!A

m!A,!A/ !(!A⊗!A)

/ !!A

δA

!A

!eA


I

mI


/ !I

（c）自由余代数 (free coalgebra) の間の任意の射 f : h!A, δA i → h!B, δB i は e と d によって決まるコモ
ノイド構造を保つ。すなわち、以下の図式を可換にする:

!A
f


!B

!A
eA

eB

dA

f

/


!B

I

/ !A⊗!Af ⊗fdB/ !B ⊗!B

定理 25 (健全性). 任意の線型圏は IMELL に対する健全なモデルとなる。
証明. IMELL の証明に関する帰納法による。規則 W および P のみを扱う。その他の場合については略。また型 A に関する解釈は J!AK = !JAK であることを除けば IMLL と同様である。*4
def• W. この場合の証明図は以下の通り:
Π
Γ ` B
W
Γ, !A ` B
帰納法の仮定より次の射が得られる:
f

JΓK/ JB K*4 左辺の J!AK の ! は証明論の体系内の演算子であり、右辺の !JAK の ! は圏の関手であることに注意。

10したがって得るべき射は次の通り定義できる:JΓ, !AK∼=/ JΓK⊗!JAK

idJΓK ⊗eJAK∼=/ JΓK ⊗ I

/ JΓK

f

/ JB K• P. この場合の証明図は以下の通り:Π!Γ ` AP!Γ ` !A
帰納法の仮定より次の射が得られる:

J!ΓK ≡!JA1 K ⊗ · · · ⊗!JAn K

f

/ JAK

得るべき射は以下のように定義できる:J!ΓK ≡!JA1 K ⊗ · · · ⊗!JAn K

promΓ

/ !(!JA1 K ⊗ · · · ⊗!JAn K)!f/ !JAK ≡ J!AK

ここで、射 promΓ : J!ΓK →!J!ΓK は Γ の要素数 n に関する帰納法で次の通り定義する射である:– n = 0. この場合、!Γ ≡ ∅ であるから prom∅ : I →!I としては mI を取れば良い。

– n = 1. この場合、!Γ ≡!A1 である。promA1 :!JA1 K →!!JA1 K としては δJA1 K を取れば良い。

– n > 1. この場合、!Γ ≡!A1 , . . . , !An であり、帰納法の仮定より promΓ\{An } が存在。したがって
promΓ としては以下の射を取れば良い (細かい添字などは省略):
promΓ\{An } ⊗δ/ !(!JA1 K ⊗ · · · ⊗!JAn−1 K)⊗!!JAn K

J!ΓK ∼= (!JA1 K ⊗ · · · ⊗!JAn−1 K)⊗!JAn K

4m/ !J!ΓK

Linear-Non-Linear モデルによる意味論
前節で見てきた線型圏は言わば「IMLL の証明を考えた時に満たして欲しい構造」を全て集めてきた、定義が少々複雑な圏である。もちろん、それ自体は各推論規則と圏の構造との対応関係が分かりやすく健全性
定理を満たす素晴らしい圏ではあるが、定義がもう少し簡単であれば応用上もうれしい。そこで本節では[Ben94a][Ben94b] により導入された LNL モデルを用いて別の観点から直観主義線型論理を解釈する。
LNL モデルの根幹となるのは、カルテジアン閉圏 C と対称モノイダル閉圏 S の存在とそれらの間のある随伴関手の組 F a G さえ仮定すれば線型圏を定義するのに必要な構造は再構築できるという発想である。より本質的には、定義するのに苦労した線型圏の ! の構造は関手 F ◦ G を使うことで圏 C を経由して与えられ、線型論理は圏 S の下で解釈される*5 :
F

Cf

&

⊥

Se

!=F ◦GG*5 付け加えると [Bie95] は直観主義論理から直観主義線型論理への変換である Girard 変換を念頭に置き、直観主義論理と直観主義

線型論理を一つの体系内で統合した Dual Intuitionistic Linear Logic を考案している。この体系は線型論理と等価であり LNL
モデルで解釈されるが、本質的に直観主義論理部分が CCC で解釈されて線型論理部分が SMCC で解釈される点が特徴である。

11

以降では LNL モデルを定義してそれが線型圏を導くことを見て、LNL モデルが直観主義線型論理 IMELLのモデルとして使えることを示す。
定義 26 (対称モノイダル随伴). 圏 C, D をそれぞれ対称モノイダル圏とする。対称モノイダル関手 F : C → D
および G : D → C について、F a G が成立して随伴の unit および counit がモノイダル自然変換であるとき、F と G は対称モノイダル随伴をなすという。これを普通の随伴と同一の記号を用いて F a G と表す。
定義 27 (Linear-Non-Linear モデル). Linear-Non-Linear モデル (LNL モデル) は次からなる構造である:

1. カルテジアン閉圏 hC, ×, 1i2. 対称モノイダル閉圏 hS, ⊗, Ii
3. 対称モノイダル随伴 F a G をなす関手 hF, mi : C → S および hG, ni : S → C の組
以上の定義より、以下の自然変換:

mX,Y : F X ⊗ F Y → F (X × Y )nA,B : GA × GB → G(A ⊗ B)
さらには射 m : I → F 1 および n : 1 → GI が得られる。また随伴の unit と counit をそれぞれ η と ε とすると、射の族:

pX,Y : F (X × Y ) → F X ⊗ F Y
が射 nF X,F Y ◦ (ηX × ηY ) : X × Y → G(F X ⊗ F Y ) の転置として次のように定義できる:

F (X × Y )F (η×η)/ F (GF X × GF Y )F (n)/ F G(F X ⊗ F X)ε

/ FX ⊗ FY

また射 p : F 1 → I は εI ◦ F n によって与えられる。
補題 28 ([Ben94b, 命題 1]). mX,Y は pX,Y を逆として持つ自然同型であり、かつ、m は p を逆として持つ同型である。すなわち、以下が成り立つ:

FX ⊗ FY ∼= F (X × Y )
I∼
= F1
証明. 略
次に線型圏におけるコモナドの構造について議論するため、随伴 F a G との関係を見る。まず S の任意の対象 A について射 δA : F GA → F GF GA を δA = F (ηGA ) で定めると、δ は S 上の自然変換となる。今、F G を ! で書くことにすると三組 h!, ε :! → idS , δ :! →!!i は次に示す通りコモナドをなす。
補題 29. h!, ε :! → idS , δ :! →!!i はコモナドをなす。加えて h!, ε, δi は対称モノイダルである、すなわち、• 対象 A, B に対して射 qA,B :!A⊗!B →!(A ⊗ B) を持つような自然変換 q• 射 qI : I →!Iが存在して h!, q, qI i は対称モノイダル関手をなし、ε と δ がモノイダル自然変換をなす。
証明. 略。

12

ここまでに出揃った性質から以下の定理が証明できる。
定理 30. 任意の LNL モデルは線型圏を導く。
証明. 確認する内容が多く面倒くさいので証明の概略だけ示す。詳細については [Ben94b] を参照せよ。
まず、線型圏の定義に現れる対称モノイダルコモナド h!, ε, δ, q, qI i は補題 29 と同様に定義する。加えて線型圏の定義に現れる射の組 he :!A → I, d :!A →!A⊗!Ai は LNL モデルの構造から次のように定義する:
defeA = p ◦ F (∗GA )def

dA = pGA,GA ◦ ∆GA
ここで、∗GA は GA から C の終対称 1 への射であり、∆GA は GA から GA × GA への対角射 (diagonalmap) である。
以降は LNL モデルに基づいて定義した構造が線型圏の条件を満たすことをひたすら確認するだけである。
証明の流れについては以下の通りである:

1. [Ben94b, 補題 3] 任意の対象 A について eA および dA が自然変換のための射をなす。
2. [Ben94b, 補題 4] e および d がモノイダル自然変換をなす。
3. [Ben94b, 補題 5] 任意の対象 A について h!A, eA , dA i は可換コモノイドをなす。
4. [Ben94b, 補題 6] 任意の対象 A について eA および dA が余代数射をなす。
5. [Ben94b, 補題 7] 自由余代数の間の任意の余代数射 f : h!A, δA i → h!B, δB i は e と d で与えられるコ
モノイド構造を保つ。

6. [Ben94b, 系 8] 以上で確認された構造から、LNL モデルは線型圏を定義する。
系 31. 任意の LNL モデルは直観主義線型論理を解釈できる。
注 32. 本文書の LNL モデルの定義は [Ben94a][Ben94b] に基づいており、LNL モデルを構成する圏 C がカ
ルテジアン閉であることを仮定した。しかしながら系 31 を導くためには実はこの条件は不要であり、「C は有限直積を持つ圏」と条件を変えた LNL モデルを定義できる。この場合の詳細については [Mel03] を参照せよ。

参考文献[Bar96]

Andrew Barber. Dual intuitionistic linear logic. University of Edinburgh, Department ofComputer Science, Laboratory for Foundations of Computer Science, 1996.

[BBDPH92a] Nick Benton, Gavin Bierman, Valeria De Paiva, and Martin Hyland. Linear λ-calculus
and categorical models revisited. In International Workshop on Computer Science Logic,
pages 61–84. Springer, 1992.
[BBdPH92b] Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. Term assignment for
intuitionistic linear logic (preliminary report). Technical Report 342, Computer Laboratory,
University of Cambridge, 1992.
[Ben94a]P. Nick Benton.

A Mixed Linear and Non-Linear Logic: Proofs, Terms and Mod-els (Extended Abstract). In International Workshop on Computer Science Logic, pages
121–135. Springer, 1994.
13

[Ben94b]

P. Nick Benton.

A Mixed Linear and Non-Linear Logic: Proofs, Terms and Mod-els (Preliminary Report). Technical Report 342, Computer Laboratory, University of Cambridge, 1994.
[Bie95]G. M. Bierman. What is a Categorical Model of Intuitionistic Linear Logic? In International Conference on Typed Lambda Calculi and Applications, pages 78–93. Springer, 1995.

[Mel03]Paul-André Melliès. Categorical models of linear logic revisited. Manuscript, available
from https:// hal.archives-ouvertes.fr/ hal-00154229, 2003.

[Sch04]

Andrea Schalk. What is a categorical model for Linear Logic? Manuscript, available fromhttp:// www.cs.man.ac.uk/ ~schalk/ notes/ llmodel.pdf, 2004.

14