平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

プログラミング言語の意味論と圏論 ∗長谷川真人
京都大学数理解析研究所

概要
プログラミング言語の意味論（プログラム意味論）は、プログラムの構造を数学的に定式化・抽象化することによってコンピュータソフトウェアに関する諸問題を解決することを目的とする、コンピュータサイエンスの一分野です。そこでは、抽象的な現代数学の象徴とも言われる圏論が活発に応用されてきており、今や圏論抜きにプログラム意味論を語ることは困難といっても過言ではありません。
この講義では、圏論を用いたプログラム意味論の概要を紹介しつつ、そもそもプログラム意味論に求められる数学とはどのようなものなのか、なぜ圏論なのか、という素朴な疑問に、私なりに答えてみたいと思います。

プログラミング言語の意味論とはなにか

1

プログラミング言語の意味論とは、複雑なプログラムの背後にある数学的な構造をつきとめ、分析することによって、プログラムに関して成り立つ本質的な原理を導くことを目的とする研究分野です。
その応用として、プログラムの見通し良い設計、プログラムの性質の検証、およびプログラムの効率化・最適化などがあげられます。しかし、ほとんどの方にとって、意味論というのはあまり馴染みのない言葉ではないかと思いますし、それが数学とどのように関係するのか、想像することも困難かも知れません。そこで、まずは、そもそもプログラミング言語の意味論とはどのような分野なのかについて、基本的なところから解説していきたいと思います。

1.1

プログラムの意味とはプログラミング言語のプログラムは、コンピュータに何かをさせるための指示を記述する文章であり、通常、有限長の記号の列として与えられます。しかし、記号列にはじめからなにか固有の意味が備わっているわけではもちろんなく、プログラムの表現する計算＝プログラムの意味（semantics）については、別に定義する必要があります。この、プログラムの意味を数学的に定義すること、およびその理論的な枠組みのことを、プログラミング言語の意味論（プログラム意味論）と呼びます。
プログラミング言語の意味論にはいくつかの種類があります。ここでは、その概要を、とても単純なプログラミング言語を例にとって説明します。
簡単な言語 真偽値を計算する、とても簡単な（関数型）プログラミング言語 FB を与えます 1 。準備として、変数をあらわす記号 x, y, z, . . . をあらかじめ用意しておきます。FB のプログラムは、以下のようなものです。

1. 変数記号は FB のプログラムである。
∗
1

数理解析研究所第 38 回数学入門公開講座配布資料（2016 年 9 月修正）
真偽値 (Boolean) を扱う関数型（Functional）プログラミング言語、というつもりで適当につけた名称です。

平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

2. 記号 T と F は FB のプログラムである。
3. P が FB のプログラムであるとき、(not P ) は FB のプログラムである。
4. P1 と P2 が FB のプログラムであるとき、(P1 and P2 ) は FB のプログラムである。
5. x が変数記号、P1 と P2 が FB のプログラムであるとき、(let x be P1 in P2 ) は FB のプログラム
である。
6. 以上の規則で得られるものだけが、FB のプログラムである。
このように、どのような記号列が正しいプログラムであるかを定める規則＝文法（とその理論的枠組み）のことを、プログラミング言語の構文論（syntax）と言います。
たとえば、以下のような記号列は FB のプログラムです。

(let x be (T and y) in ((not x) and F))
プログラム P の中の束縛されていない変数（自由変数）の集まり fv (P ) を、

• fv (x) = {x} （ただし x は変数記号）• fv (T) = fv (F) = ∅• fv ((not P )) = fv (P ), fv ((P1 and P2 )) = fv (P1 ) ∪ fv (P2 )• fv ((let x be P1 in P2 )) = fv (P1 ) ∪ (fv (P2 ) − {x})と定め、fv (P ) = ∅ となるような P のことを閉じたプログラムと呼ぶことにします。閉じたプログラ
ムは、定義が不明な変数がないプログラムのことだ、とも言えます。
FB の閉じたプログラムの意味は、直感的にはほぼ自明だと思います。たとえば、プログラム (P1 and P2 )は、P1 の計算結果と P2 の計算結果の論理積を求めるものです。また、(let x be P1 in P2 ) は、P1 の計算結果を P2 中の x にあてはめ、然る後に P2 の計算を行うもの、と考えて差し支えありません。

1.2

操作的意味論

実際にプログラミング言語の処理系が行っているような具体的な計算の規則によってプログラムの意味を与える流儀は、操作的意味論（operational semantics）と呼ばれます。操作的意味論が与えられると、コンピュータ上で動作するプログラミング言語の処理系を与えることが（少なくとも原理的には）できるので、現在では、操作的意味論は、プログラミング言語の定義を与える有力な手法とみなされています。
FB の操作的意味論は、以下のように定められます。閉じたプログラム P に対し、その実行結果がV ∈ {T, F} であることを、P ⇓ V と書くことにします。

1. T ⇓ T である。また、F ⇓ F である。
2. P ⇓ T ならば (not P ) ⇓ F である。P ⇓ F ならば (not P ) ⇓ T である。
3. P1 ⇓ T かつ P2 ⇓ T ならば (P1 and P2 ) ⇓ T である。P1 ⇓ T かつ P2 ⇓ F ならば (P1 and P2 ) ⇓ Fである。P1 ⇓ F ならば (P1 and P2 ) ⇓ F である。
4. P1 ⇓ V1 かつ P2 [x := V1 ] ⇓ V2 ならば (let x be P1 in P2 ) ⇓ V2 である。ここで、P [x := V ] は、Pのなかの（自由な）変数 x をすべて V に置き換えて得られるプログラムである。

2

平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

数理論理学の記法（導出木）を用いて、「Z である」「X ならば Z である」「X かつ Y ならば Z であ
る」を
X
X Y
Z
Z
Z
と表記すると、操作的意味論の規則は

T⇓T

F⇓F

P1 ⇓ T P2 ⇓ F((P1 and P2 ) ⇓ F

P ⇓T(not P ) ⇓ F

P ⇓F(not P ) ⇓ T

P1 ⇓ F((P1 and P2 ) ⇓ F

P1 ⇓ T P2 ⇓ T((P1 and P2 ) ⇓ T

P1 ⇓ V1 P2 [x := V1 ] ⇓ V2
(let x be P1 in P2 ) ⇓ V2となります。たとえば、プログラム (let x be (not F) in (x and F)) の操作的意味は、以下の導出木で表され、その実行結果は F となります。

F⇓F
T⇓T F⇓F(not F) ⇓ T (T and F) ⇓ F(let x be (not F) in (x and F)) ⇓ F
これは、プログラムの一部を順次書き換えていく、以下のような計算ステップの列に対応しています。

(let x be (not F) in (x and F)) → (let x be T in (x and F)) → (T and F) → F

1.3

表示的意味論

一方、プログラムを、具体的な実行方法とは独立に、なんらかの数学的な対象に対応させて意味を定める、という流儀もあります。これを、表示的意味論（denotational semantics）と呼びます。
FB のプログラム P の表示的意味は、fv (P ) ⊆ Γ であるような変数の集合 Γ と以下の規則で定まる
真偽値関数 [[P ]] : {0, 1}Γ −→ {0, 1} で与えられます。ただし、{0, 1}Γ の要素を写像 ρ : Γ −→ {0, 1}で表すことにします。また、表示的意味論の慣習で、[[P ]](ρ) を [[P ]]ρ と書くことにします。

[[x]]ρ
[[T]]ρ
[[F]]ρ
[[(not P )]]ρ[[(P1 and P2 )]]ρ[[(let x be P1 in P2 )]]ρ

=
=
=
=
=
=

ρ(x)
1
0
1 − [[P ]]ρ
[[P1 ]]ρ · [[P2 ]]ρ
[[P2 ]]ρ[x7→[[P1 ]]ρ ]ただし最後の行の右辺で、ρ[x 7→ v] は、x 以外の変数については ρ が定める値を取り、x については
v を値とする写像です。
特に P が閉じたプログラム、すなわち fv (P ) = ∅ の場合は、[[P ]]ρ の値は Γ と ρ の取り方によらないので、Γ = ∅、ρ は空集合を定義域とする一意に定まる写像として構いません。この場合、[[P ]] = [[P ]]ρ
は {0, 1} の要素と同一視できます。
たとえば、プログラム (let x be (not F) in (x and F)) の表示的意味は、[[(let x be (not F) in (x and F))]] =
=
=
=
=
=
=
3

[[(x and F)]][x7→[[(not F)]]][[(x and F)]][x7→(1−[[F]])][[(x and F)]][x7→(1−0)][[(x and F)]][x7→1][[x]][x7→1] · [[F]][x7→1]
1·00平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催となります。前に見た操作的意味論と比較すると、計算結果こそ同じ（P ⇓ V ならば [[P ]] = [[V ]]）ですが、表示的意味論の計算は必ずしも操作的意味論が定める計算ステップとは対応していないことに注意してください。
FB の (共通する自由変数を持つ) プログラム上に、同値関係 ∼ をP ∼ P ′ ⇔ [[P ]] = [[P ′ ]]で定めます。閉じたプログラム P , P ′ については、P ∼ P ′ であることと、P と P ′ の計算結果が一致すること（ある V について P ⇓ V かつ P ′ ⇓ V となること）が一致します。
操作的意味論がプログラムの実際の挙動に基づくものであるのに対し、表示的意味論は、プログラ
ムの抽象的な内容（FB なら真偽値および真偽値関数）に着目します。抽象化する際に、プログラムの細かい計算ステップなどの情報を気にする必要はありません。FB の場合は単純すぎてこれ以上どうしようもありませんが、より複雑な、現実的なプログラミング言語については、プログラムの持つ情報の、特に知りたい部分だけをなんとかして上手に取りだすことが大変重要になってきますが、そこが表示的意味論の醍醐味ともいうべきところです。プログラムの性質のうち、プログラムの正しさの検証や改良に役立てるために必要となる部分を抽象化して取り出す、というわけです。さらに、抽象化することで、あるプログラミング言語について得られた結果を、類似した構造を持つ多くのプログ
ラミング言語にも共通して利用できるようになる、汎用性・一般性も表示的意味論の長所です。それに対し、操作的意味論は、具体的であるがゆえに、すこし規則を変更するだけでプログラムの意味が大きく変わってしまうかも知れないという精密さ・繊細さを持っています。現在のプログラム意味論
は、操作的意味論と表示的意味論を密接に関連させ、両者の長所を生かして研究・応用されています。

1.4

表示的意味論＝計算の不変量

先に、表示的意味論が、プログラムの抽象的な内容に着目するものであると述べました。その内容の決め方は実はかなり自由なのですが、最低限外せないポイントとして、表示的意味論は計算の実行の過程において不変であるように定める、ということがあります。たとえば、FB の操作的意味論が定める計算の過程(let x be (not F) in (x and F)) → (let x be T in (x and F)) → (T and F) → F
を見ると、[[(let x be (not F) in (x and F))]] = [[(let x be T in (x and F))]] = [[(T and F)]] = [[F]]と、表示的意味は各計算ステップの前後で変化していないことがわかります。
クラインは、有名なエルランゲン・プログラムの中で、「幾何学は与えられた変換群に属する任意の変換で不変な図形の性質を研究する学問である」と述べ、幾何学を、図形の変換の不変量を研究する数学として特徴づけました。プログラミング言語の意味論についても、クライン流の見方がとても有効であると、私は考えています。うんと乱暴にまとめるなら、プログラムの変換＝計算過程を定めるのが操作的意味論であり、一方、プログラムの計算の過程で不変な性質＝不変量を調べるのが表示的意味論の役割と言えます。
この、表示的意味論＝計算の不変量という視点は、プログラム意味論と数学（特に幾何学）を概念的に対比させ理解するうえで大変便利ですが、実は、技術的にも、プログラム意味論で用いられる圏論的な構造が、低次元トポロジー、特に結び目の不変量において用いられる圏論的な構造と密接に関連していることがわかっています。このことについては、講義の後のほうで触れたいと思います。

4平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

1.5

この講義の構成

通常のプログラミング言語の理論の講義では、考察の対象となるプログラミング言語の構文・文法の定義をきちんと与え、然る後に意味論等の議論をはじめます。実際、FB については、おおむねその定跡を踏襲して解説しました。しかし、この講義では、今後は、プログラムの構文論はほとんど扱いません。最大の理由は、構文論の説明は、時間と手間が非常にかかるということ、そして、（構文論の専門家からはお叱りを受けると思いますが）構文論の大半は教えるのも教わるのも退屈だということです。限られた時間のなかで圏論を用いたプログラム意味論の本質（と私が思うこと）をお伝えするために、構文論はほぼ無視します。
もうひとつ、以下の講義では、基本的に表示的意味論だけを扱い、操作的意味論に触れることはあまりありません。これは、構文論を無視するために、構文論に深く依存する操作的意味論について論じることが難しい、ということもありますが、なにより、圏論に基づく意味論は、表示的意味論のほうがより基本的であり、操作的意味論について圏論的に論じるためには、表示的意味論を十分に理解することが不可避である、という理由があります。
また、圏論的なプログラム意味論（表示的意味論）の全部について語ることはもとより無理ですので、思い切り題材を絞り込み、以下のような進め方をしたいと思います。まず、圏論的な意味論の一
般的な方針について説明します。然る後、ふたつの重要なケースについて紹介します。ひとつは、カルテジアン閉圏と呼ばれる構造に関する話題です。これは、ラムダ計算と呼ばれる計算モデルや、関数型プログラミング言語、さらに定理証明支援システムなどの意味論の、もっとも基礎的な部分になります。
もうひとつは、トレース付きモノイダル圏に関する話題です。こちらは、再帰プログラムの意味論や、相互作用の幾何と呼ばれる計算モデルの基礎となるものですが、実は結び目の量子不変量とも深い関係があります。
他にも重要なケースは多々ありますが、（１）分野の研究者の間で重要性が広く認められていること、（２）それほど説明がむつかしくないこと、そして（３）応用が豊富なこと、（４）講義の流れが自然になること、という観点からこれらに注目することにしました。（もちろん、私にとってなじみ
深い話題であるということも大きな理由です。）
この話題の性質上、圏論の知識は全く仮定しないというわけにはいきません。基礎的な圏論については、講義中にもなるべく補足していきたいと思いますが、最小限、これだけ知っていればたぶん大丈夫、というまとめを末尾（付録 A）につけておきますので、参考にしていただけますと幸いです。

2

圏論的な意味論

2.1

FB の意味論再考

FB では、プログラム P の表示的意味は、真偽値関数[[P ]] : {0, 1}Γ −→ {0, 1}(fv (P ) ⊆ Γ)として定められていました。実は、集合 {0, 1} は任意の集合 X に置き換えても問題ありません（[[T]]と [[F]] を区別するためには、ふたつ以上の要素を持つ集合である必要はあります）。また、自由変数の集合 fv (P ) は有限集合ですので、Γ も有限集合として良く、プログラム P の表示的意味は、写像[[P ]] : X n −→ X
（ただし n = |Γ|、すなわち Γ の要素の個数）により与えられます。
さらに、ここまで集合間の写像としてきましたが、実のところ、[[P ]] を、適当な圏の適当な対象 Xについて、X n から X への射、としてしまっても何ら差し支えありません。ただし、どんな圏でも良いというわけではなく、有限直積を持つことが必要です。

5平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

2.2

有限直積を持つ圏

圏 C の有限個の対象 X1 , · · · , Xn の直積は、対象 P と射 πi : P → Xi (i = 1, · · · , n)（射影と呼ばれます）の組で、以下の条件を満たすものです。
任意の対象 Z と射 fi : Z → Xi (i = 1, · · · , n) に対し、

f i = πi ◦ h(i = 1, · · · , n)となる射 h : Z → P がただひとつ存在する。
対象 X1 , · · · , Xn の直積は、存在すれば、同型を除いて一意に定まります（複数あっても、それらはすべて互いに同型になります）。以下では、圏 C はすべての有限直積を持つものとし、対象 X1 , · · · , Xnの直積を (同型なもののうちから) ひとつ固定して対象 X1 × · · · × Xn および射 πi : X1 × · · · × Xn → Xi
(i = 1, · · · , n) の組で表すことにします。そして、対象 Z と射 fi : Z → Xi (i = 1, · · · , n) に対し、
fi = πi ◦ h (i = 1, · · · , n) となる射 h を、

⟨f1 , · · · , fn ⟩ : Z → X1 × · · · × Xn
で表すことにします。すると、

πi ◦ ⟨f1 , · · · , fn ⟩ = fi

⟨π1 ◦ g, · · · , πn ◦ g⟩ = g(ただし g : Z → X1 × · · · × Xn ) が成り立ちます。
諸定義• n = 0 の場合の直積を対象 1 で表すと、任意の対象 Z に対し、Z から 1 への射 ⟨ ⟩ : Z → 1 が唯一つ存在することになります。このような対象は終対象と呼ばれます。
• 射 fi : Xi → Yi (i = 1, 2, . . . , n) に対し、射 f1 × . . . × fn : X1 × . . . × Xn → Y1 × . . . × Yn を、
f1 × . . . × fn = ⟨f1 ◦ π1 , . . . , fn ◦ πn ⟩ で定めます。この定義により、有限直積を持つ圏 C において、写像 (X1 , . . . , Xn ) 7→ X1 × . . . × Xn : (Ob(C))n → Ob(C) は Cn から C への関手に拡張
されます。

2.3

FB の圏論的意味論

有限直積を持つ圏で FB の意味論を与えてみましょう。C を有限直積を持つ圏とし、X を C の対象とします。また、射 tt, ﬀ : 1 → X, not : X → X および and : X 2 → X が存在し、

not ◦ tt = ﬀ
and ◦ ⟨tt, tt⟩ = tt
and ◦ ⟨ﬀ , tt⟩ = ﬀ

not ◦ ﬀ = tt
and ◦ ⟨tt, ﬀ ⟩ = ﬀ
and ◦ ⟨ﬀ , ﬀ ⟩ = ﬀ

を満たすものとします。
FB のプログラム P と、互いに異なる変数の列 x1 , . . . , xn について、fv (P ) の要素が x1 , . . . , xn の中に含まれているとき、[[x1 , . . . , xn ⊢ P ]] : X n → X を以下のように定めます。

[[x1 , . . . , xn ⊢ xi ]]= πi[[x1 , . . . , xn ⊢ T]]= tt ◦ ⟨ ⟩[[x1 , . . . , xn ⊢ F]]= ﬀ ◦ ⟨⟩[[x1 , . . . , xn ⊢ (not P )]]= not ◦ [[x1 , . . . , xn ⊢ P ]][[x1 , . . . , xn ⊢ (P1 and P2 )]] = and ◦ ⟨[[x1 , . . . , xn ⊢ P1 ]], [[x1 , . . . , xn ⊢ P2 ]]⟩[[x1 , . . . , xn ⊢ (let x be P1 in P2 )]] =[[x1 , . . . , xn , x ⊢ P2 ]] ◦ ⟨π1 , . . . , πn , [[x1 , . . . , xn ⊢ P1 ]]⟩6平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

たとえば、プログラム (let x be (not F) in (x and F)) の C における意味は、以下のように求められます。

[[⊢ (let x be (not F) in (x and F))]] =
=
=
=
=
=
=

[[x ⊢ (x and F)]] ◦ [[⊢ (not F)]]and ◦ ⟨[[x ⊢ x]], [[x ⊢ F]]⟩ ◦ not ◦ [[⊢ F]]
and ◦ ⟨id , ﬀ ◦ ⟨ ⟩⟩ ◦ not ◦ ﬀ
and ◦ ⟨id , ﬀ ◦ ⟨ ⟩⟩ ◦ tt
and ◦ ⟨tt, ﬀ ◦ ⟨ ⟩ ◦ tt⟩
and ◦ ⟨tt, ﬀ ⟩ﬀ

特に、C を Set、X を {0, 1} とし、tt 、ﬀ 、not 、and を適切に定めれば、前に与えた FB の表示意味論
は、この圏論的な意味論の一例となっていることがわかります。すなわち、ρ(xi ) = vi (i = 1, 2, . . . , n)であるとすると、[[P ]]ρ = [[x1 , . . . , xn ⊢ P ]](v1 , . . . , vn ) が成り立ちます。
直積を持つ圏の例と表示的意味論 表示的意味論でよく用いられる圏のひとつに、完備半順序集合（正確には最小元を持つ ω-完備半順序集合）の圏 Cpo があります。半順序集合 (X, ⊑) が最小の要素を持ち、X の任意の可算単調列
x0 ⊑ x1 ⊑ x2 ⊑ x3 ⊑ . . .
⊔が上限 xi を持つとき、(X, ⊑) は完備半順序集合と呼ばれます。完備半順序集合 (X, ⊑) の最小元
を、しばしば ⊥X と表記します。完備半順序集合 (X, ⊑) と (Y, ⊑) について、写像 f : X → Y が連続であるとは、

1. x1 ⊑ x2 なら f (x1 ) ⊑ f (x2 )2. 可算単調列 x0 ⊑ x1 ⊑ x2 ⊑ . . . について⊔⊔f ( xi ) = f (xi )が成り立つことをいいます。Cpo は、完備半順序集合を対象とし、連続写像を射に持つ圏であり、有限直積を持ちます。直感的には、完備半順序集合の最小元は、値が未定義な計算＝停止しない計算をあらわします。実際的なプログラミング言語では、とまらないプログラムを書けることも実はとても重要です。特に、再帰プログラム（自分自身を呼び出すように書かれたプログラム）を持つ言語では、
非停止性は避けては通れませんが、Cpo を用いて、そのような再帰プログラムの意味論を非常にエレガントにあたえることが可能です。この話題については、また後程触れます。
{0, 1}⊥ を、要素を 0, 1, ⊥ とし、順序が x ⊑ y ⇔ (x = ⊥X または x = y) で定まる完備半順序
集合とします。FB の圏論的意味論で、C を Cpo、X を {0, 1}⊥ とし、tt 、ﬀ 、not 、and を適切に定めれば、Cpo における FB の表示的意味論が得られます。FB の計算はすべて停止するので、Cpoを使うご利益は FB そのものに対してはありませんが、FB を再帰プログラムを許すように拡張すると、Cpo を用いた意味論が役に立ちます。
有限直積を保存する関手 有限直積を持つ圏 C および D について、関手 F : C → D が有限直積を保存するとは、C の対象 X1 , . . . , Xn の直積 X1 × . . . × Xn とその射影 πi : X1 × . . . × Xn → Xi
（i = 1, . . . , n）に対し、F (X1 × . . . × Xn ) と F (πi ) : F (X1 × . . . × Xn ) → F (Xi ) （i = 1, . . . , n）が、D における F (X1 ), . . . , F (Xn ) の直積になることをいいます。
今、圏 C(FB) を以下のように定めます：• C(FB) の対象は非負整数 0, 1, 2, . . .
• C(FB) における m から n への射は、自由変数が x1 , . . . , xm に含まれているようなプログラム
P1 . . . . Pn の ∼ の同値類の組 ([P1 ], . . . , [Pn ])(x1 ,...,xm )7

平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

図 1: 様々なプログラミング言語の機能と対応する圏論的構造の例
一階関数型プログラム

有限直積を持つ圏

高階関数型プログラム

カルテジアン閉圏

副作用を伴うプログラム

有限直積を持つ圏上の強モナド

再帰プログラム有限直積を持つ圏上の不動点演算子

依存型

局所カルテジアン閉圏

線形型

モノイダル圏

相互作用の幾何トレース付きモノイダル圏

種々のデータ構造

関手の始代数、終代数、双代数• n 上の恒等射は ([x1 ], . . . , [xn ])(x1 ,...,xn )• ([P1 ], . . . , [Pm ])(x1 ,...,xl ) : l → m と ([Q1 ], . . . , [Qn ])(x1 ,...,xm ) : m → n の合成は([let x1 be P1 in . . . let xm be Pm in Q1 ], . . . , [let x1 be P1 in . . . let xm be Pm in Qn ])(x1 ,...,xl )C(FB) は有限直積を持つ圏です（m1 , . . . , mn の直積は m1 + . . . + mn です）。実は、有限直積を持つ圏 C に対し、C(FB) から C への直積を保存する関手を与えることは、C における FB の意味論を与えることと、ぴったり対応しています。どういうことかというと、C(FB) の対象 1 を関手でうつした先を X とし、and を ([x1 and x2 ](x1 ,x2 ) ) : 2 → 1 を関手で写した先、などとすれば、C における FB の意味論を得ることができますし、逆に、C における FB の意味論から、C(FB) から C への直積を保存する関手を構成することも可能です。
ここまで FB の意味論について細かく見てきましたが、圏論の言葉で要約すると、FB の表示的意味論を与えることは、C(FB) からの直積を保存する関手を与えることに他なりません。

2.4

圏論的意味論＝構造を保存する関手

このように、FB のような単純な関数型プログラミング言語については、有限直積を持つ圏と、有限直積を保存する関手が表示的意味論を与えます。これは偶然ではなく、より複雑な言語についても、同様のことが言えます。ただし、言語の機能に応じて、直積だけでなく、さまざまな構造を持つ圏と、それらの構造を保存する関手を考える必要があります。圏論を用いたプログラム意味論では、そのような構造を特定し、構造を持つ圏・構造を保存する関手の性質や具体例を調べることが本質的です。
図 1 に、よく用いられる構造の例を列挙してみました。
この講義の残りでは、そのような構造の代表例として、カルテジアン閉圏とトレース付きモノイダ
ル圏について解説します。

3

カルテジアン閉圏

3.1型付きラムダ計算と関数型プログラミング

多くのプログラミング言語では、プログラムをデータとみなすことができます。つまり、プログラ
ムをデータとして受け取り、処理するプログラムを書くことが可能です。さらに、「プログラムを処理するプログラム」をまたデータとして受け取るようなプログラムも考えることができます。一般に、
型付きラムダ計算や（高階）関数型プログラミング言語では、データ型 σ1 と σ2 に対し、σ1 のデー

8

平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

タを入力とし σ2 のデータを出力するプログラムのデータ型（関数型）σ1 → σ2 が用意されています。
たとえば、整数のデータ型を int であらわすと、整数上の関数を入力とし、整数を出力する（汎）関数の型は (int → int) → int となります。
このような関数型の意味論を与えるのが、カルテジアン閉圏です。

3.2

カルテジアン閉圏

有限直積を持つ圏の対象 X と Y に対し、X と Y の冪とは、対象 E と射 ε : E × X → Y の組で、以下の条件を満たすものです。
任意の対象 Z と射 f : Z × X → Y に対し、ε ◦ (h × id X ) = fとなる射 h : Z → E がただ一つ存在する。
以下では、そのような対象 E をひとつ選んで Y X と表記し、f : Z × X → Y に対し一意に定まる
h : Z → Y X を f で表すことにします。すると、等式ε ◦ (f × id X ) = f(f : Z × X → Y )ε ◦ (h × id X ) = h (h : Z → Y X )が成り立ちます。
有限直積とすべての冪をもつ圏を、カルテジアン閉圏と呼びます。
例• 集合と写像の圏 Set は、カルテジアン閉圏です。集合 X と Y の冪は、冪集合 Y X = {f : X → Y }および ε(f, x) = f (x) で定められる写像 ε : Y X ×X → Y によって与えられます。f : Z ×X → Y
に対し、f : Z → Y X は、(f (z))(x) = f (z, x) で定まります。
• 任意の圏 C に対し、関手の圏 [C, Set] （しばしば前層の圏と呼ばれます）はカルテジアン閉圏です。
• 完備半順序集合と連続写像の圏 Cpo はカルテジアン閉圏です。完備半順序集合 X = (X, ⊑) とY = (Y, ⊑) に対し、冪対象は、X から Y への連続写像全体の集合 Y X に、半順序
f ⊑ g ⇔ すべての x ∈ X について f (x) ⊑ g(x)を入れたものと、ε(f, x) = f (x) で定められる写像 ε : Y X × X → Y によって与えられます。

• ベクトル空間の圏 VectK と有限次元ベクトル空間の圏 Vectfd
K は、いずれも有限直積を持ちます（直和空間で与えられます）が、これらの圏は冪を持たないので、カルテジアン閉圏ではありません。
単純型付きラムダ計算の意味論 ここでは詳細には立ち入りませんが、単純型付きラムダ計算 λ→ と呼ばれる計算系があります。λ→ は、基底型と呼ばれる基礎的な型と、関数型だけが用意されている、すべての高階関数型プログラミング言語の雛形ともいうべきものです。FB から有限直積を持つ圏
C(FB) を構成したのと全く同じ流儀で、λ→ から、カルテジアン閉圏 C(λ→ ) を構成することができます。そして、FB の場合と同様に、単純型付きラムダ計算のカルテジアン閉圏 C における表示的意味論を、C(λ→ ) から C へのカルテジアン閉圏の構造を保存する関手として定式化することができます。

9

平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

トレース付きモノイダル圏

4

ここからは、少々駆け足になりますが、テンソル積やトレースを持つ圏と、そのプログラム意味論
における応用について紹介します。

4.1

再帰プログラムの不動点意味論

プログラム意味論における古典的な話題である、再帰プログラムの表示的意味論について、簡単な例をもとに説明します。 整数を入力に取り整数を出力する簡単なプログラム

sum(x) ≡ if x = 0 then 0 else x + sum(x − 1)を考えます。これは、プログラムの定義（≡ の右辺）で自身（sum）を呼び出す再帰プログラムになっています。たとえば、sum(3) の実行は、3 ̸= 0 なので 3 + sum(2) と sum 自身を呼び出し、以下同様に続けて 3 + (2 + (1 + sum(0))) に到達し、sum(0) = 0 なので和 3 + (2 + (1 + 0)) を計算して 6 を答えとして返します。sum のような再帰プログラムは、その実行が常に停止するとは限らないので、整数上の部分関数を定めます。そして、sum の定める部分関数は、部分関数全体の上の（汎）関数
(x = 0)0
F (f )(x) = x+f (x−1) (x ̸= 0 かつ f (x − 1) が定義されている場合)
未定義(その他の場合)の不動点として理解できます。sum に限らず、再帰プログラムの表示的意味は、適切な写像の不動点として与えることができます。圏論を用いた表示的意味論では、そのような再帰プログラムの意味論に必要な不動点を取る操作は、以下のように定式化されます。有限直積を持つ圏 C において、以下の条件をみたす写像の族 (−)† : C(A × X, X) → C(A, X) をコンウェイ不動点演算子と呼びます：• f : A × X → X, h : A′ → A について f † ◦ h = (f ◦ (h × id X ))† : A′ → X• f : A × Y → X, g : A × X → Y について (f ◦ ⟨πA,X , g⟩)† = f ◦ ⟨id A , (g ◦ ⟨πA,Y , f ⟩)† ⟩ : A → X• f : A × X × X → X について f †† = (f ◦ (id A × ∆X ))† : A → X
これらの条件は、再帰プログラムの不動点意味論のほとんどすべてについて成立しています。代表的な例として、完備半順序集合の圏 Cpo があげられます。Cpo では、連続写像 f : (X, ⊑) → (X, ⊑)は最小の不動点を持ち、それは可算単調列⊥ ⊑ f (⊥) ⊑ f 2 (⊥) ⊑ f 3 (⊥) ⊑ . . .
⊔の上限 f n (⊥) で与えられます。先の sum を例にとると、汎関数 F は整数上の部分関数全体がなす
完備半順序集合の上の連続写像であり、その最小不動点は sum の定める部分関数に他なりません。
以上で述べた圏論的な不動点意味論は、おおむね１９８０年代までに完成された、標準的なものです。１９９０年代になって、トレース付きモノイダル圏という構造が不動点意味論と関係づけられてから、この分野の見方に変化が生じました。この講義の残りでは、その比較的新しい展開について、時間の許す範囲で紹介します。

4.2

モノイダル圏とトレース

モノイダル圏 モノイダル圏あるいはテンソル圏 C = (C, ⊗, I, a, l, r) とは、圏 C と、それに付随するテンソル積またはモノイダル積と呼ばれる関手 ⊗ : C2 → C、単位対象と呼ばれる C の対象 I 、テンソ

10

平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催∼

ル積と単位対象の結合律・単位律に相当し適当な公理をみたす可逆な自然変換 aA,B,C : (A ⊗ B) ⊗ C →∼∼A ⊗ (B ⊗ C), lA : I ⊗ A → A および rA : A ⊗ I → A の組のことをいいます。a, l, r がすべて恒等射であるようなモノイダル圏は、厳格であるといいます。厳格なモノイダル圏では、A ⊗ (B ⊗ C) と(A ⊗ B) ⊗ C は同一の対象であり、A ⊗ I 、I ⊗ A と A についても同様です。任意のモノイダル圏は、
厳格なモノイダル圏と（モノイダル圏の構造を厳格に保存する関手を介して）同値です（コヒーレンス定理）。ですから、モノイダル圏について考察する際には、a, l, r のことは忘れて、あたかも厳格な
モノイダル圏を扱っているようにみなしても問題ありません。以下でも、a, l, r のことは無視して話を進めます。
ブレイド、バランス、対称性 モノイダル圏で、条件 cA,B⊗C = (id B ⊗ cA,C ) ◦ (cA,B ⊗ id C ) および
∼
−1
−1
c−1
B⊗C,A = (id B ⊗ cC,A ) ◦ (cB,A ⊗ id C ) を満たす可逆な自然変換 cA,B : A ⊗ B → B ⊗ A を持つものを、
ブレイド付きモノイダル圏と呼び、c はブレイドと呼ばれます。さらに、バランスあるいはツイストと∼呼ばれる可逆な自然変換 θA : A → A が存在して θI = id I および θA⊗B = cB,A ◦ (θB ⊗ θA ) ◦ cA,B をみたすブレイド付きモノイダル圏を、バランス付きモノイダル圏と呼びます。バランス付きモノイダ
ル圏で、θ = id （したがって c = c−1 ）が成り立つものは、対称モノイダル圏（symmetric monoidal
category）と呼ばれます。
ストリング図式 モノイダル圏の射は、簡潔に図示することができ（しばしばペンローズ図式やス
トリング図式と呼ばれます）、それは図の連続的な変形にたいして整合的です。この講義では、射f : A1 ⊗ A2 ⊗ . . . ⊗ Am → B1 ⊗ B2 ⊗ . . . ⊗ Bn を
Am

Bn

:

:

f

A2
A1

B2
B1

とあらわします。射の合成やテンソル積は、それぞれの射が対応する図の直列つなぎおよび並列つなぎであらわします。
C
X

f

Y Y

g

Z

7→ X f

Y

g

Z
A

交差

A
B

@
@

B

B

A

A

B

D

C

7→

g◦f

ブレイド cA,B : A ⊗ B → B ⊗ A は交差

g
f

g

D

A

f B
f ⊗g

B

として、また c−1
A,B : B ⊗ A → A ⊗ B は逆向きのとしてあらわします。ブレイドの条件式は、以下のように図示できます。

A
C
B
A

PP 
P 
P P
PP

P

A

C

A

C

C
B

= B

C

B

A

B

A

PP 
PP
PP P
 PP
P

A

C

C

= B

B

A

@
@

−1
バランス θA : A → A は、ねじれであらわします。θAは逆向きのねじれ件式も以下のようにあらわせます。



B

B

A

A

=

11

B

B

A

A

@
@

A
C
B

です。バランスの条平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

双対性とリボン圏 次に、モノイダル圏における双対性の概念を導入します。モノイダル圏の対象 A
A
A∗の（左）双対とは、対象 A∗ および射 ηA : I → A ⊗ A∗ と εA : A∗ ⊗ A → I （それぞれと A∗
Aで図示します）で、条件==を満たすものです。リボン圏とは、すべての対象が双対を持ち、
=が成り立つようなバランス付きモノイダル圏です。なお、対称な（θ = 1, c = c−1 であるような）リ
ボン圏は、しばしばコンパクト閉圏とも呼ばれます。
たとえば、体 K について、K 上の有限次元線形空間を対象に、また線形写像を射に持つ圏 Vectfd
Kは、対称なリボン圏（すなわちコンパクト閉圏）です。この場合、テンソル積 U ⊗ V は線形空間のテンソル積 U ⊗K V 、単位対象は K 、ブレイド cU,V は U ⊗ V から V ⊗ U への自明な同型写像、バランスは恒等写像であり、U の双対 U ∗ は双対空間 hom(U, K) により与えられます。
似た例では、対象が集合、射が集合の間の二項関係である圏 Rel があります。Rel の恒等射 id X :X → X は恒等関係 {(x, x) | x ∈ X}、また二項関係 R : X → Y と S : Y → Z の合成 S ◦ R : X → Z
は {(x, z) ∈ X × Z | ∃y ∈ Y (x, y) ∈ R, (y, z) ∈ S} で与えられます。テンソル積 X ⊗ Y は集合の直積 X × Y 、単位対象は一点集合 1 です。集合 X の双対は X 自身です。Rel は、非決定的な計算のモデルとして、また線形論理のモデルとして、プログラム意味論でよく用いられている圏です。
量子不変量とリボン圏 結び目の理論では、以下のような（向きづけられた、枠付きの）タングルの圏 Tangle を考えます。Tangle の対象は、（タングルの向きを表わす）記号 + と − の有限列です。そ′′して、(s1 , . . . , sm ) から (s1 , . . . , sn ) への射は、下図のような、+ では左から右に、− では右から左に向き付けられた、s1 , . . . , sm , s′1 , . . . , s′n を端点とするタングルの、連続変形に関する同値類です。
+

−
+

+
+

−

(+, −, +) −→ (−, +, +)

-

+
+

−
+
(−, +, +) −→ (+)

Tangle は、リボン圏です。それも、ただのリボン圏ではなく、ひとつの対象から自由生成されたリボン圏です。したがって、任意のリボン圏 C とその対象をひとつ選ぶことにより、Tangle から C へのリボン圏の構造を保存する関手が定まり、この関手からタングルの不変量がひとつ得られます。たとえば、量子群から、その表現の圏としてリボン圏を構成することができます。すなわち、量子群から、タングルの不変量を構成することができるわけです。
同様のことは、集合と二項関係の圏 Rel についても可能です。Rel の中で量子群に相当するもの（リボンホップ代数）を見つけ、その” 表現” の圏として非対称なリボン圏を得ることができます。
トレース付きモノイダル圏 トレース付きモノイダル圏には、二つの特徴付けがあります。一つは、抽象的なトレース演算子を備えたバランス付きモノイダル圏というもので、これが Joyal, Street, Verityの原論文における定義でもあります。もう一つは、同じ論文で与えられている構造定理によるもので、トレース付きモノイダル圏は、必ずあるリボン圏の充満部分モノイダル圏になっている、というものです。トレース付きモノイダル圏では、対象の双対は必ずしも存在しません。構造定理については後で触れることにして、まず、トレース演算子による特徴付けから説明します。

12平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

図 2: トレースの公理

X
X
T rA
′ ,B ′ ((k ⊗ id X ) ◦ f ◦ (h ⊗ id X )) = k ◦ T rA,B (f ) ◦ h



h

f



=

k

f

h

k

−1
X
X
T rX,X(cX,X ) ◦ θX
= id X = T rX,X
(c−1
X,X ) ◦ θX





=

@
@

=

X
X
T rC⊗A,C⊗B(id C ⊗ f ) = id C ⊗ T rA,B
(f )



f



f

=

X
Y
Y
X
T rA,B(T rA⊗X,B⊗X(f )) = T rA,B
(T rA⊗Y,B⊗Y((id B ⊗ cY,X ) ◦ f ◦ (id A ⊗ c−1
Y,X )))

'

$'

$


&
f


%&

=

f

@
@

%

バランス付きモノイダル圏 C が与えられているものとします。このとき、C 上のトレース演算子とX : C(A ⊗ X, B ⊗ X) → C(A, B) で、図 2 の四つの条
は、C の対象で添字付けられた写像の族 T rA,B
X (f ) : A → B を
件を満たすものです。ここで、f : A ⊗ X → B ⊗ X のトレース T rA,B

A

f

B

で図示することにします。トレース演算子を持つバランス付きモノイダル圏を、トレース付きモノイ
ダル圏と呼びます。
トレース付きモノイダル圏の例として、第一にリボン圏が挙げられます。任意のリボン圏はトレース演算子をただひとつ持ちます。有限次元線形空間の対称リボン圏 Vectfd
K では、トレース演算子は通常のトレース（行列の対角和）を対象 A, B でパラメータ化したものです。通常のトレースは A = B = I
X : C(X, X) → C(I, I) に相当します。量子群の表現のなすリボン圏では、トレーの場合、つまり T rI,Iス演算子は、量子トレースと呼ばれるもの（のパラメータ化）になります。
X R : A → B は、{(a, b) ∈ A ×
Rel では、二項関係 R : A × X → B × X のトレース T rA,B
B | ∃x((a, x), (b, x)) ∈ R} です。
リボン圏でないトレース付きモノイダル圏の例としては、Tangle の対象を + の列だけに制限した充満部分圏 Tangle+ があります。（Tangle+ は、ひとつの対象から自由生成されたトレース付きモ
ノイダル圏です）。Rel も別のテンソル積（有限双直積）についてトレース演算子を持つことが知られており、こちらはリボン圏ではありません。（このトレースは後で述べる相互作用の幾何でよく用

13

平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

いられます。）一般に、リボン圏の充満部分モノイダル圏はトレース付きモノイダル圏ですが、後述
する構造定理より、実はその逆も成り立ちます。

4.3

トレースと再帰プログラムの不動点意味論

実は、コンウェイ不動点演算子は、トレース演算子の特別な場合であるとみなすことができます。
有限直積を持つ圏は、直積をテンソル積とみなすことにより、対称モノイダル圏の例になっています。
有限直積をテンソル積とみなした対称モノイダル圏においては、コンウェイ不動点演算子とトレース演算子の間には一対一対応がつくことが、1990 年代中頃に、筆者と Hyland によって独立に示されました。このことから、Cpo など、プログラム意味論で用いられている多くの圏が、実はトレース付
きモノイダル圏になっていることがわかります。結び目の理論で必要とされる非対称なリボン圏ではありませんが、対称リボン圏の断片が、プログラム意味論において（誰にも気づかれることなく）古くから用いられていた、というのは興味深いことだと思います。
この結果はさらに一般化でき、直積でないテンソル積を持つモノイダル圏においても、適当な（プログラム意味論でよく用いられるような）条件を満たすものにおいては、トレースから不動点演算子を構成することがわかっています。それを用いて、古典的なプログラム意味論では説明できなかった、
巡回的な共有データ構造から生み出される再帰計算の意味論を展開することが可能です。

4.4

相互作用の幾何トレース付きモノイダル圏のもうひとつの特徴付けのもととなる構造定理は、以下のようなものです。
任意のトレース付きモノイダル圏 C について、C からのトレース付きモノイダル圏の構造を保つ充満忠実関手があるようなリボン圏 Int C が存在します。
ここで登場する Int 構成は、計算機科学において思いがけない応用をもたらしました。それは、Int構成により得られるリボン圏が、双方向の情報のやりとりを伴なう計算（相互作用）の意味論を与えるために非常に便利なものだからです。
トレース付きモノイダル圏 C に対し、リボン圏 Int C は、C の対象の組を対象とし、Int C における (X, U ) から (Y, V ) への射は、C における X ⊗ V から Y ⊗ U への射として与えられます。射の定義の中で、対象の第２成分の順番がひっくり返っている（反変になっている）ことに注意してください。Int C における射 f : (X, U ) → (Y, V ) と g : (Y, V ) → (Z, W ) の合成は、以下のように行います。

V

W

f
X

@
@
Y

U

g
Z

左から右への素直な流れと、トレースを用いて右から左へと逆順に合成される流れとが共存している
ことがおわかりいただけるでしょうか。計算機科学の感覚では、これはまさに「上り」と「下り」の情報流が共存する状況を表しています。
Int 構成は、Girard が 1980 年代末に創始した双方向の情報流を伴なう計算の理論である相互作用の幾何（Geometry of Interaction）の核心部分に暗黙のうちにあらわれています。のちに、Abramsky
らは、Int 構成を基礎とした相互作用の幾何の再構成と一般化を与えました。
勝股は、40 年以上前に Knuth が導入した属性文法と呼ばれるコンパイラ等で文脈自由言語の意味の記述に用いられる技法が、Int 構成を用いて明快に理解できることを示しました。属性文法ではプ
ログラムの構文木の構造に沿って双方向の情報のやりとりがなされるのですが、ここでもトレース付
きモノイダル圏と Int 構成が重要な役割を果たします（下図）。

14平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

構文木

属性文法
?6

f

f

 SS

7 SS
oS

/
wS

x

g

y

x

トレースによる解釈
'


g

?6

$

y
&

g



x
f

y

%
-

特に、高階のデータ（プログラム）を属性に用いる属性文法は、トレース付きモノイダル閉圏（モノイダル閉圏はカルテジアン閉圏の直積をテンソル積に一般化したもの）の上の Int 構成により理解できます。トレース付きモノイダル閉圏 C では、Int C への埋め込みが右随伴関手を持ち、このことから、高階属性を用いて双方向の情報流が一方向の情報流に帰着されることを説明できます。例えば、
Cpo はそのような例を与えます。プログラムのコンパイル時の最適化技法であるプログラム変換においても、関連する結果が得られています。

5

おわりに

プログラム意味論においてなぜ圏論が重要なのか、という問いに対する、現時点での私の答えは次のようになります：「プログラム意味論の本質は、プログラミング言語に内在する構造を捉え、その構造を保存する変換を与え分析することにある。その目的を達成するための数学の枠組みとしては、
現状では圏論がもっとも適している。」我ながらあまり面白みのない答えですが、道具として圏論を使ってきた経験から、それほど外してはいないと思います。
全く意図していなかったのですが、FB のような単純な関数型プログラミング言語からはじめて、
ラムダ計算と高階関数型プログラミング言語の意味論、そしてトレース付きモノイダル圏を用いたプ
ログラム意味論と相互作用の幾何、というこの講義の流れは、実は、私自身の研究がこれまで進んできた道（の一番太い部分）に、ほぼ沿ったものとなっています。自分が重要だと思うこと、自然に話せると思うことを軸に話を組み立て書き進めていったら、いつの間にかこうなっていました。限られた時間と紙数ではありますが、この分野の面白さを多少なりとも感じ取っていただけたら幸いです。
参考文献には、日本語で気軽に手に取って頂けそうなものを中心に挙げています。私自身が書いたものでは、[3] がもっとも一般の方向けですが、この講義では飽き足らないという方には、[1, 2] をお試しいただければと思います（いずれも私のページからダウンロードできます）。これらの内容は、講義と一部重複しています。数理解析研究所の過去の数学入門公開講座のテキストでは、勝股先生 [5]と星野先生 [4] のものが、この講義の内容と深く関連しています。いずれも圏論は隠し味程度に留められていますが、この講義のあとで読んでみると発見があるかも知れません。[3] が収録されている本には、鈴木先生達のタングルの圏に関する解説 [7] や、勝股先生のモナドと計算効果に関する解説[6] も含められています（鈴木・葉廣→長谷川→勝股の順に話がつながるように書かれています）。プ
ログラム意味論について日本語で書かれた本には、[10] があります。圏論については、Mac Lane の古典的な教科書 [9] があります。最近の本では英語ですが Leinster の入門書 [8] が良いと思います。

参考文献[1] 長谷川真人, 再帰プログラムの意味論について, 数学 59 (2007), 180–191.
[2] 長谷川真人, プログラム意味論とトポロジー - 再帰, 相互作用, 結び目, 日本数学会 2010 年度秋
季総合分科会企画特別講演アブストラクト.
[3] 長谷川真人, プログラム意味論と圏論, 圏論の歩き方 第４章, 日本評論社, 2015.
15平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催[4] 星野直彦, 型無しラムダ計算とモデル, 数理解析研究所数学入門公開講座, 2013.
[5] 勝股審也, プログラミング言語の意味論. 数理解析研究所数学入門公開講座, 2007.
[6] 勝股審也, モナドと計算効果, 圏論の歩き方 第５章, 日本評論社, 2015.
[7] 鈴木咲衣, 葉廣和夫, タングルの圏, 圏論の歩き方 第３章, 日本評論社, 2015.
[8] T. Leinster, Basic Category Theory, Cambridge University Press, 2014.
[9] S. Mac Lane, Categories for the Working Mathematician, 2nd ed., Springer-Verlag, 1998 （邦訳： 三好博之, 高木 理 （訳）, 圏論の基礎, シュプリンガー・ジャパン, 2005 / 丸善出版, 2012）.
[10] 横内寛文, プログラム意味論, 共立出版, 1994.

圏論の諸定義などA

ここでは、この講義で必要となる圏論の諸定義や例についてまとめています。簡単のため、圏の大きさ（大きい圏・小さい圏、ユニバース等）については曖昧にして書いていますが、この講義の範囲
では問題はありません。

A.1

圏

定義

圏 C とは、• 対象の集まり Ob(C)、• 各 A, B ∈ Ob(C) に対し、A から B への射の集まり C(A, B)、• 各 A ∈ Ob(C) に対し、射 id A ∈ C(A, A)、• 各 A, B, C ∈ Ob(C) に対し、写像◦ : C(B, C) × C(A, B) → C(A, C)( g, f )7→g◦fの組で、結合律 (h ◦ g) ◦ f = h ◦ (g ◦ f ) （f ∈ C(A, B), g ∈ C(B, C), h ∈ C(C, D)）および単位律
id B ◦ f = f = f ◦ id A （f ∈ C(A, B)）を満たすものです。id A を（対象 A のうえの）恒等射、g ◦ f
を射 f と g の合成射と呼びます。
注意

文献によっては、C(A, B) を HomC (A, B) または単に Hom(A, B) と書くことがあります。まfた、f ∈ C(A, B) であることを、f : A → B や A → B などとも書きます。
例• 対象が集合、射が集合の間の写像である圏 Set• 対象が集合、射が集合の間の二項関係である圏 Rel （本文参照）• 対象が体 K 上のベクトル空間、射がベクトル空間の間の線形写像である圏 VectK• 対象が体 K 上の有限次元ベクトル空間、射がベクトル空間の間の線形写像である圏 Vectfd
K• 対象が群、射が群の間の準同型写像である圏 Grp• 対象が完備半順序集合、射が完備半順序集合の間の連続写像である圏 Cpo （本文参照）
16

平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

諸定義• 圏 C の射 f : A → B が同型射であるとは、ある g : B → A が存在して g ◦ f = id A およびf ◦ g = id B が成り立つことをいいます。このとき、g を f の逆と呼び、f −1 であらわします。
また、対象 A と B の間に同型射が存在するとき、A と B は同型であるといい、A ∼= B とあらわします。
• 圏 C に対し、双対圏 Cop とは、Ob(Cop ) かつ Cop (A, B) = C(B, A) であり、C と同じ恒等射、および C の合成射をひっくり返した合成射を持つものです。
• C と D を圏とするとき、C と D の直積圏 C × D とは、Ob(C × D) = ObC) × Ob(D) かつ(C × D)((A, A′ ), (B, B ′ )) = C(A, B) × D(A′ , B ′ ) であり、恒等射 id (A,A′ ) = (id A , id A′ ) および合成射 (g, g ′ ) ◦ (f, f ′ ) = (g ◦ f, g ′ ◦ f ′ ) を持つものです。

A.2

関手

定義

C と D を圏とするとき、C から D への関手 F : C → D とは• 写像 A 7→ F (A) : Ob(C) → Ob(D)• 各 A, B ∈ Ob(C) に対し、写像

f 7→ F (f ) : C(A, B) → D(F (A), F (B))

の組で、F (id A ) = id F (A) および F (g ◦ f ) = F (g) ◦ F (f ) をみたすものです。
諸定義• 圏 C に対し、C 上の恒等関手 id C : C → C を、id C (A) = A、id C (f ) = f により定めます。また、
関手 F : C → D および G : D → E に対し、合成関手 G ◦ F : C → E を、(G ◦ F )(A) = G(F (A))
および (G ◦ F )(f ) = G(F (f )) により定めます。これらにより、対象を圏、射を圏の間の関手とする（大きな）圏 Cat が定まります。
• 関手 F : C → D は、– 各 A, B ∈ Ob(C) について写像 f 7→ F (f ) : C(A, B) → D(F (A), F (B)) が単射であるとき、忠実であるといいます。
– 各 A, B ∈ Ob(C) について写像 f 7→ F (f ) : C(A, B) → D(F (A), F (B)) が全射であるとき、充満であるといいます。
• 圏 C が圏 D の部分圏であるとは、Ob(C) ⊆ Ob(D) かつ各 A, B ∈ Ob(C) について C(A, B) ⊆D(A, B) であり、かつ C の恒等射および合成射は D のものの制限となっていることをいいます。このとき、C から D への包含関手を取ることができます。包含関手は常に忠実ですが、充満であるとは限りません。包含関手が充満忠実であるとき（すなわち各 A, B ∈ Ob(C) について C(A, B) = D(A, B) であるとき）C は D の充満部分圏であるといいます。
例• 集合 X に対し X 自身を、写像 f : X → Y に対し二項関係 J(f ) = {(x, y) ∈ X × Y | f (x) = y}を対応させる関手 J : Set → Rel は、忠実ですが充満ではありません。
• 集合 X に対し完備半順序集合 X⊥ を、X⊥ = X ∪ {⊥X }、x ⊑ y ⇔ (x = ⊥X または x = y) と定め、写像 f : X → Y に対し連続写像 f⊥ : X⊥ → Y⊥ を f (x) = x (x ∈ X), f (⊥X ) = ⊥Y と定めることで、関手 (−)⊥ : Set → Cpo が得られます。F も、忠実ですが充満ではありません。
• Vectfd
K は VectK の充満部分圏です。
17平成28年度(第38回)数学入門公開講座テキスト(京都大学数理解析研究所，平成28年8月1日～8月4日開催

A.3

自然変換

定義 関手 F, G : C → D に対し、F から G への自然変換 α : F → G とは、C の対象で添字付けられた D の射の族 {αA : F (A) → G(A)}A∈Ob(C) で、任意の射 f : A → B に対し αB ◦ F (f ) = G(f ) ◦ αA
を満たすものです。αA : F (A) → G(A) を、α の A 成分と呼びます。
諸定義• 関手 F : C → D について、F 上の恒等変換 id F : F → F を、(id F )A = id F (A) により定めます。また、関手 F, G, H : C → D と自然変換 α : F → G および β : G → H について、合成変換 β ◦ α : F → H を、(β ◦ α)A = βA ◦ αA により定めます。これらにより、C から D への関手
を対象、関手の間の自然変換を射とする圏 [C, D] （文献によっては DC ）が定まります。この圏を、しばしば関手の圏と呼びます。
• 各成分が同型射となる自然変換を自然同型射と呼びます。自然同型射は、圏 [C, D] の同型射に他なりません。関手 F, G : C → D について、F と G の間に自然同型射が存在するとき、F とG は自然同型であるといい、F ∼= G と書きます。
• 圏 C, D について、– G ◦ F = id C および F ◦ G = id D となる関手 F : C → D と G : D → C が存在するとき、C と D は同型であるといいます。
– G◦F ∼
= id C および F ◦ G ∼= id D となる関手 F : C → D と G : D → C が存在するとき、C と D は同値（圏同値）であるといいます。

A.4

随伴関手

定義

圏 C, D と関手 F : C → D および U : D → C について、関手(C, D) 7→ D(F (C), D) : Cop × D → Setと、関手(C, D) 7→ C(C, U (D)) : Cop × D → Set
が自然同型であるとき、F を U の左随伴関手、U を F の右随伴関手であるといいます。
例• C を有限直積を持つ圏とするとき、対象 X1 , . . . , Xn を直積 X1 × . . . × Xn に写す関手は、対象
X を n 個の組 (X, X, . . . , X) に写す対角関手 ∆n : C → Cn の右随伴関手になります。
• C をカルテジアン閉圏とし、X を C の対象とします。対象 Y を Y × X に、射 f : Y1 → Y2 を
f × id X : Y1 × X → Y2 × X に写す関手 (−) × X : C → C は、対象 Z を Z X に、射 g : Z1 → Z2
を g ◦ ε : Z1X → Z2X に写す関手 (−)X : C → C の左随伴関手です。
• 関手 J : Set → Rel は、集合 X を冪集合 2X に写す右随伴関手を持ちます。
• Cpo の対象 X を Int(Cpo) の対象 (X, 1) に、射 f : X1 → X2 を f × id 1 : (X1 , 1) → (X2 , 1)に写す関手 J : Cpo → Int(Cpo) は、(X, U ) を X U に写す右随伴関手を持ちます。

18