型付きラムダ計算と4つの圏 - 檜山正幸のキマイラ飼育記 (はてなBlog)

型付きラムダ計算に対する“デカルト閉圏による意味論”、あるいは“カリー／ハワード対応”においては、型付きラムダ項の計算（書き換え、変換）だけではなくて、シーケント計算が必要になります。型理論では、シーケントを型判断（type judgement）と呼ぶことが多いですが、内実はシーケントです。

シーケントは、その形からいくつかの種類に分類できます。そして、シーケントの種類ごとに対応する圏も別な種類になります。これらの圏は、よく似ているので同一視することもありますが、区別したほうがいいと思います。

内容：

モノイド閉圏
シーケントの分類
4つの圏
微妙な気持ち悪さ

モノイド閉圏

型付きラムダ計算の圏的意味論（categorical semantics）はデカルト閉圏を舞台として行います。これについては、次の記事を参照してください。

ここでは、デカルト積（直積）とは限らないモノイド積を持つ閉圏、つまりモノイド閉圏（monoidal closed category）Cを考えます。モノイド閉圏Cでは、次の随伴性（adjunction）が存在します。

C(A $\otimes$ B, C) $\stackrel{\sim}{=}$ C(A, [C←B])
C(A $\otimes$ B, C) $\stackrel{\sim}{=}$ C(B, [A→C])

[A←B]は右指数、[A→C]は左指数で、それぞれ右からの $\otimes$ 掛け算、左からの $\otimes$ 掛け算の随伴パートナーです。この同型を与えるホムセット間の写像をΛr, Λlとしましょう。

Λr: C(A $\otimes$ B, C)→C(A, [C←B])
Λl: C(A $\otimes$ B, C)→C(B, [A→C])

ΛrとΛlは、右カリー化（右ラムダ抽象）と左カリー化（左ラムダ抽象）を与えます。随伴の余単位として、右評価射（right eval）と左評価射（left eval）が決まるので、これらを使ってラムダ計算が出来ます。

Cが対称モノイド圏のときは、左右を入れ替えることが出来るので、単一のΛ（カリー化、ラムダ抽象）とev（評価射、適用射）で十分で、デカルト閉圏の場合とよく似た計算ができます。デカルト閉圏ではない対称モノイド閉圏の例として、有限次元ベクトル空間の圏 (FdVect_K, $\otimes$ , K) があります。Kはスカラー体（係数体）で、 $\otimes$ はベクトル空間のテンソル積です。FdVect_K内の指数は、[W←V] := W $\otimes$ V^*, [V→W] := V^* $\otimes$ W で与えられます*1。

非対称な例は、テンパリー／リーブ圏やその変種のなかに見いだせるでしょう。アブラムスキーの論説あたりが参考になるかな。

Title: Temperley-Lieb Algebra: From Knot Theory to Logic and Computation via Quantum Mechanics
Author: Samson Abramsky
Pages: 45p
URL: https://arxiv.org/abs/0910.2737

以下では対称性を仮定します。非対称だと話が面倒になるからです。しかし、非対称でも通用する話がけっこうあります。

対称モノイド閉圏におけるラムダ計算は、だいぶ昔から「弱いラムダ計算」と呼んでいたものです。

シーケントの分類

対称モノイド閉圏Cを選んで、その上で解釈できる（型付き）ラムダ項の構文を決めます。ラムダ項の作り方はここでは省略します（「型付きラムダ計算のモデルの作り方」、「セマンティック駆動な圏的ラムダ計算とシーケント」参照）。

A₁, ..., A₁, Bを型（Cの対象）、x₁, ..., x_nを変数、Eをラムダ項とします。ただし、Eは{x₁, ..., x_n}以外の自由変数を含まないとします。このとき、次の形をシーケントと呼びます。

x₁:A₁, ..., x_n:A_n ⇒ E:B

この形のシーケント（型理論の用語では型判断）の“意味”は、A₁ $\otimes$ ... $\otimes$ A_n→B in C という射になります。

「⇒」の左側の型宣言が1つだけ（n = 1）のシーケントを単純シーケントと呼ぶことにします。また、左側が空（n = 0）のシーケントを片側シーケントと呼びます。

左辺の型宣言の個数nによる分類をまとめると：

n	名称	形式
n = 1	単純シーケント	x:A ⇒ E:B
n = 0	片側シーケント	⇒ E:B
nは任意	一般のシーケント	x₁:A₁, ..., x_n:A_n ⇒ E:B

4つの圏

前節の3種のシーケント、それと型付きラムダ項に対して、それぞれに対応する4つの圏があります。

シーケントの分類	対応する圏	圏の種類
単純シーケント	C	対称モノイド閉圏
片側シーケント	singleC	対称モノイド圏
一般のシーケント	multiC	対称モノイド複圏
型付きラムダ項のみ	typeC	C-豊饒圏

モノイド閉圏Cをもとに、singleC, multiC, typeCを作ることが出来ます。

S := singleC, M := multiC, T := typeC として、それぞれの圏の概略を記述してみます。Λ^A_B,C:C(A $\otimes$ B, C)→C(B, [A→B]) は左カリー化、ev_A,B:A $\otimes$ [A→C]→B in C を左評価射とします。

S := singleC

Sの対象類とホムセット族は次のとおりです。

|S| = |C|
S(A, B) = C(I, [A→B])

IはCの単位対象、[A→B]はCの左指数（左掛け算の随伴パートナー）です。

Cの結合／恒等とは区別して、Sの図式順結合を#、恒等をj_Aとします。a:A→B, b:B→C in S とは、a:I→[A→B], b:I→[B→C] in C のことです。C内で考えて、a#b は次の式で与えられます。（δ:I→I $\otimes$ Iは、λ、ρを左右の単位律子*2として、δ := λ_I = ρ_I です。）

a#b := Λ^A_I,C((A $\otimes$ δ);(A $\otimes$ a $\otimes$ b);(ev_A,B $\otimes$ [B→C]);ev_B,C)
j_A := Λ^A_I,A(ρ_A)

M := multiC

Mは普通の圏ではなくて複圏（multicategory）です。複圏をオペラッド（operad）とも呼びます（「形容詞「複」「多」と箙〈えびら〉」を参照）。

複圏の対象類と複ホムセット族は次のとおりです。

|M| = |C|
M([A₁, ...,A_n], B) = C(A₁ $\otimes$ ... $\otimes$ A_n, B)

対称モノイド圏から対称複圏（対称オペラッド）を作るやり方はここでは述べませんが、やり方は決まっています。例えば、次の論説などを参考にしてください。前半（20ページまで）がオペラッドの丁寧な解説になっています。

Title: From Operads to Dendroidal Sets
Author: Ittay Weiss
Pages: 40p
URL: https://arxiv.org/abs/1012.4315

T := typeC

Tは通常の圏ではなくて、対称モノイド圏Cで豊饒化された圏（enriched category）です。

|T| = |C|
T(A, B) = [A→B]

T(A, B)はホムセットではなくてホム対象です。C-豊饒圏としての結合γと恒等ιは次のように与えられます。

γ_A,B,C:[A→B] $\otimes$ [B→C]→[A→C] in C であり、γ_A,B,C := Λ^A_{[A→B],[B→C]}((ev_A,B $\otimes$ [B→C]);ev_B,C)
ι_A:I→[A→A] in C であり、ι_A := Λ^A_I,A(ρ_A)

定義を見れば分かるように、C-豊饒圏Tと通常の圏（Set-豊饒圏）Sは非常に近い関係にあります。このことについては、「豊饒圏（ピノキオ）が圏（人間）になる物語」に詳しく書いています。Cの指数を内部ホムとして作ったC-豊饒圏がTで、Tから作った通常の圏（ピノキオの人間化）がSになっています。

微妙な気持ち悪さ

型付きラムダ計算の圏的意味論において、単一の構文と単一の圏を使おうとすると、微妙な気持ち悪さが残ります。何かがズレているような感覚です。この気持ち悪さは、複数の圏を無理に同一視することが原因ではないかと思えます。前節で概略だけを示した4つの圏とその相互関係を、もっと精密に調べてみる価値はありそうです。

*1:有限次元ベクトル空間の圏はコンパクト閉圏になります。

*2:律子（りつし）に関しては「律子からカタストロフへ」を参照してください。