計算機科学のための圏論の基礎の基礎
Akihiko Koga
Ver. 0.90, 2020.3.25
私のホームページ
http://www.cs-study.com/koga/に関連の情報がありますのでご興味があればそちらも参照してみてください．
また，この資料のメンテナスもそこで行う予定です．
2020/3/23(C) 2020, Akihiko Koga

1

内容
• 動機
• 圏論の概要（集合論との比較）• 圏論の基礎概念の導入• 型付きλ計算• 型付きλ計算とCCC の関係• さらなる学習に向けて• 参考文献2020/3/23(C) 2020, Akihiko Koga2

動機
• 圏論の計算機応用に関するありそうな感想

n 1970年頃から圏論が計算機科学でも使われ始め，発表も年々増加しているらしい
n なんとなく高度なことができそうだが．．．
Ø 成果も圏論の言葉で語られるので本当に使える成果が出ているか判断できないØ 身近な成果として「モナド」があるらしいが，圏論とどう関係するのか分からない

n 圏論が分かるようになりたいが，習得にはかなりの数学の習熟度が要りそう
中々手がでない．あるいは，すでに挫折した．それも何度か• この資料を作成した動機
n 今後，圏論が計算機科学の必須の基礎になるかどうかは確信はないが，廃れてい
くことはないと思う
n 本当に計算機科学で役に立つかどうか見極めるには，圏論が分かる人口が今の数倍に増える必要があるのではないだろうか？
n しかし，通常の学習者が持っている離散数学くらいの知識では挫折しやすい
n それらの学習者が，市販の圏論の教科書を読み始められるようなところまで持っていくブースター的な教材があると良いのではないだろうか
2020/3/23(C) 2020, Akihiko Koga

3

本資料の作成方針• 応用指向の学習者が抽象数学の学習を成功させるためには次の３つが重要と考える①学習者を引きつける

応用指向の

その学習の先に豊富な応用があることを匂わせる

学習者
障壁③足腰を鍛える

抽象
数学

学習したいという動機付け②障壁を引き下げる

抽象的な概念を使って推論したり，証明したりできる体力をつける

抽象的な概念を，図解，意図の解説，
例の提示，比喩などを使ってなじみやすくする（http://www.cs-study.com/koga/lattice/index.html の絵を再利用した）

2020/3/23(C) 2020, Akihiko Koga

4

本資料の作成方針• 逆に言えば，現状は前頁の３つの条件が欠けていると思う
n 圏論が何に利用できるのか分からない
n 登場する概念の意味や意図が分からない
n 圏論の中の抽象的な概念の構成方法に頭がついていけない• これらを解決した教材を整備して，興味のある学習者が自ら学べるところまで行けるブースターを提供できたら良いと思う
2020/3/23(C) 2020, Akihiko Koga

5

本資料の作成方針• 圏論の中の非常に小さい部分で良いので，応用の香りが入っている部分を選び，その中に登場する概念の徹底的な理解容易化を図る• 今回は２時間と短いので「足腰の鍛錬」は割愛する（でも，重要）• 目標としては，その上に圏論の学習を積み上げるのではなく，一般の教科書で最初から学習を始めるための心的な準備を行うこととする
本発表

学習者ごとの独習
心的
準備

圏論
ふ～ん

圏論

has
この上に積み上げようと思わないコト

応用の香りが入っているごく狭い部分を選び，登場する概念の徹底的な理解容易化を図る
2020/3/23

動機や核となる概念のいくつかに馴染みを持った状態で，自分で頑張って勉強する(C) 2020, Akihiko Koga

6

注意事項
• 後の各自の学習では，学習者自身による足場の組直しが必要
n 今回の圏論の諸概念の理解容易化では，私自身の特殊な心的イメージを使っている．したがって，かなりバイアスの掛かった説明になっている可能性がある
n 概念の把握方法は人に寄るので学習者によってはふさわしくないかもしれない
n もともと学習は各自がそれぞれのイメージを確立していく過程であると考える
n したがって，今回の説明は各自が学習に取り掛かるまでの仮の足場にはなっても，それを保持し続けるのは弊害が出てくる可能性がある• 今回はかなり範囲を絞ったので，この後，補わないといけない基礎的な概念がかなりあるn 特に「自然変換」を外した．これはもともと，圏論が考え出される動機となった概念であり，また，圏論を高階に進めていく上ではキーとなる概念である
n 自分で学習するときは，この概念の把握がキーとなる

2020/3/23(C) 2020, Akihiko Koga

7

本日の発表の内容• 今回の資料の主な内容

Cartesian Closed Category (CCC) と呼ばれる圏が単純型付きλ計算のモデルになるということを説明する• 補足
n 単純型付きλ計算は次の２つの操作が可能で，かつ，式に型をつけることができる
簡単なプログラミング言語である
例： (λx:int.(x+3))(4)
Ø 式の中の入力を明示し，関数にする（抽象化，パラメータの明示化）
Ø 関数を式に適用する（関数適用）

整数 x を取って
x+3 を返す関数

4 に適用

n このような式を解釈し，「意味（semantics）」を与えることができる圏を構成する
n そのような圏は関数適用と抽象化を解釈できる圏であり，圏論の用語でいうと
積 A × B と冪 A → B を持つ圏である（それぞれが正確に対応する訳ではない）
n まず，圏についての大まかな説明をし，なんとなくのイメージを持てるようにする
n 次に，積と冪が定義できるだけの必要最小限の圏の概念を導入する
n 続いて，単純型付きλ計算を導入し，CCC がそのモデルになることを示す
2020/3/23(C) 2020, Akihiko Koga

8

内容（再掲）• 動機• 圏論の概要（集合論との比較）• 圏論の基礎概念の導入• 型付きλ計算• 型付きλ計算とCCC の関係• さらなる学習に向けて• 参考文献2020/3/23(C) 2020, Akihiko Koga9

圏論の概要（集合論との比較）

2020/3/23(C) 2020, Akihiko Koga

10

圏論の概要集合論との比較によるなんとなくの圏論のイメージ把握• 定義 圏（Category）
圏とは，隣あったエッジの合成が定義されているマルチエッジ有向グラフのこと
n ノードをオブジェクト（object），有向エッジを射（arrow）という
n ただし，各オブジェクト X には恒等射（identity）と呼ばれる射 1X があり，また，射の合成規則は結合則を満たす
・A, B, C, D, E がオブジェクト（ノード）圏の例
・f, g, h, ... が射（有向エッジ）
h・g・f
・各オブジェクトには恒等射がある
g・f（オブジェクトA には 1A，図では他のC
A
B
D
オブジェクトに対しては省略した）ghf・隣り合った射 f と g の合成をg・f と書く
h・g
1A
j
k
・射の合成は結合律を満たす
j, k のようにノード間に(h・g)・f = h・(g・f)E
2020/3/23

二つの射があってもよい．
・1X は射の合成について単位元になるオブジェクトも射も無限個
f・1A = f 1B・f=f
あってよい(C) 2020, Akihiko Koga
11

集合論と圏論の対比• 学習者が最初に知りたいのは，横着な疑問ではあるが「圏論とは何か？」だと思う．
• 圏論は，群論など他の多用途の数学的な概念と同様に色々な見方ができるので，ある確定的な見方は間違いに陥りやすい• しかし，導入が難しいのも確かなので，後で壊すつもりで，一時的なビューを作ってみることも良いと思う• これも色々問題はあるが，集合論との典型的な対比を見てみる（集合論を集合の圏 Set と見たときの対比になっている）
2020/3/23(C) 2020, Akihiko Koga

12

集合論と圏論の対比
集合論

圏論

理論
の
様子
・・・
・・・

・・・

説明

・モノ（集合）の内部に粒々（要素）が属している（∈）関係で数学の概念を次々に構成■自然数，整数，有理数，実数，複素数■関係，関数，無限集合の理論．．．

・モノの内部は基本的には見えない．
・モノの間（モノの外）の関係（射）で数学的概念を規定する．

長所・∈関係を使った単純な原理だけで数学の全体を具体的に構成できる・数学的概念の（要求）仕様が書ける（詳細にとらわれず横の関係が見えやすい）

短所

・実装しすぎるきらいがある（横の関係が見えなくなることがある）

・具体的なものを書こうとすると，途端に記述が複雑かつ多量になってしまう

2020/3/23(C) 2020, Akihiko Koga

13

集合論と圏論の対比
集合は「実装しすぎるきらいがある」ことの説明• 「関数」の概念の例
n 「関数」の素朴なアイデアはモノの集まりとモノの集まりの要素同士の対応
n 集合論では
Ø 順序対 (a, b) を定義
例えばクラトウスキーの順序対 (a, b) := {{a}, {a, b}}Ø 集合の直積 A×B := {(a, b) | a∈A, b∈B} を定義
Ø A と B の関係を R⊆A×B と定義Ø 関係の中で一意性を持った関係を関数と定義

n つまり関数の実体はクラトウスキーの順序対のある集合
n しかし，順序対の定義方法は一通りではない．上の定義は，その中の１つの方法で関数を実装してみただけ
n 集合で数学的概念を定義するということはこのように特殊な実装方法を１つ示すことになる場合が多い
n 人間が数学をするときは，その特殊な実装方法は無意識に無視され，もとの素朴なアイデアのもとに推論を進めている
n もっと，人間の素朴なアイデアに近い言葉で数学をしても良いのでは？
2020/3/23(C) 2020, Akihiko Koga

14

集合論と圏論の対比
実装と仕様記述
ある種の人たちの要望
n 集合論は数学的概念の実装（implementation）の記述言語．見通し良く数学を記述するためにはそのもとにある（人による）要求仕様（specification）を記述する言語が必要ではないか？
n M. Barr & C. Wells “Category Theory for Computing Science”, 1998 では明確に，implementation と specification という言葉を使っている
n c.f. 「図書館の貸し出しシステム」を開発している状況を考えてみる

多くの関係者間の合意を得るための記述は，どんな Entity があってそれにどのような操作が行われるか等であり，「本」のデータをメモリー上にどのように配置するかではない..

2020/3/23

登録機能
貸し出し機能
督促機能
・・・

貸し出しシステム借用本人(C) 2020, Akihiko Koga

メモリーの
この部分に
データを
配置します

メモリー
データ
データ
15

集合論と圏論の対比• 圏論では，集合論で見えていた容器の中の粒々を塗りつぶして，外側のモノ（オブジェクト）の間の関係（射）だけで，対象システムを記述する• モノの理解の仕方は次のように変化する
それがどの要素からできているか（集合論の外延性の原理）

・・・

その圏の中のモノからどんな射を受けて，どんな射が出ていくか
それらの射はどんな性質を持つか• 例：

上への関数 （集合論）

メソッドの集合でクラスを規定する
オブジェクト指向に少し似ている（ただし，圏論では内部状態は無い）

epi （圏論） （上への関数に相当）

h : A → B が上への関数
h : A → B がepi∀b∈B ∃a∈A h(a)=b∀f, g（h(a) で B が埋め尽くされている） h・f=h・g ならば f=g
2020/3/23(C) 2020, Akihiko Koga

h

f

g
16

集合論と圏論の対比• 圏論が集合論の「実装しすぎ」に対する正しい回答かどうかは分からないが，結果として，内部のゴテゴテしたものが見えにくくなり，全体の見通しが良くなる場合がある• 個人的な意見だが，詳細な記述が必要な場合は，粒々がなく，記述力が弱い分だけ，膨大な記述が必要になってくるように思う
n これは Java などで，抽象クラスやインタフェースを多用したフレームワークの記述が膨大になり，素人にはとっつきにくくなるのと似ている．もっとも，フレームワークを作るとき，つい種々の汎用化を考えてしまうのも大きな理由と思うが．
n 例えば，圏論では，集合論と同じような粒々を意識した部分構造を記述するためには，
subobject classifier などの道具立てをすることが必要となり，そこに至るための基礎知識として本一冊を必要とする（Topos のことを意識）
n 圏論の定義や定理は条件が多かったり，複雑だったりすることが多く，
これが初心者の学習を妨げている一因だと思う⇒ この解決が学習の困難さ克服のカギ
2020/3/23(C) 2020, Akihiko Koga

概念を出来るだけ
分かりやすくする工夫と各自の足腰の鍛錬
17圏論の基礎的概念の導入

2020/3/23(C) 2020, Akihiko Koga

18

ここでのトピックス
ここでは，単純型付き λ計算のモデルとしてのデカルト閉圏を定義するための最小限度の概念を説明する．また，関手の概念を使ってデータ型を表す応用があることも示す．
圏の定義

圏の例
Set, 1, 2, 2, GraphSyntax,
プログラミング言語

エッジが合成可能なマルチエッジ有向グラフ

関手
圏から圏への準同型

圏論の応用１関手の例
集合の圏 Set の多項式関手

代数/余代数によるデータ型の表現

他の著者の
入門用の
文献へ

型付きλ式への応用（応用２）に向けた諸概念の定義
モデルとは（極限），積，冪，デカルト閉圏
2020/3/23(C) 2020, Akihiko Koga

次章以降へ
19

圏論の概要（再掲）• 定義 圏（Category）
圏とは，隣あったエッジの合成が定義されている マルチエッジ 有向グラフのこと
n ノードをオブジェクト（object），有向エッジを射（arrow）という
n ただし，各オブジェクト X には恒等射（identity）と呼ばれる射 1X があり，また，射の合成規則は結合則を満たす
・A, B, C, D, E がオブジェクト（ノード）圏の例
・f, g, h, ... が射（有向エッジ）
h・g・f
・各オブジェクトには恒等射がある
g・f（オブジェクトA には 1A，図では他のC
A
B
D
オブジェクトに対しては省略した）ghf・隣り合った射 f と g の合成をg・f と書く
h・g
1A
j
k
・射の合成は結合律を満たす
j, k のようにノード間に(h・g)・f = h・(g・f)E
2020/3/23

二つの射があってもよい．
・1X は射の合成について単位元になるオブジェクトも射も無限個
f・1A = f 1B・f=f
あってよい(C) 2020, Akihiko Koga
20

圏の定義：用語の補足• 圏のオブジェクトと射についての記法

n C を圏とするとき，C はオブジェクトの集まりと，射の集まりからなるが，それぞれを C0，あるいはobj(C)，C1 あるいは arr(C) で表す．
n X が圏 C のオブジェクトである時，X∈C0 あるいは単に X∈C と書く
n f が圏 C の射である時，f∈C1 あるいは単に f∈C と書く• domain と codomain についてf

n 射 f:X→Y は X → Y とも書く
n このときXをfのdomain，Yをfのcodomain といい，dom(f), cod(f) と書く
fXYdom(f)
cod(f)
n 射 f と g が合成できるためには cod(f)=dom(g) であることが必要十分条件
f
g
X
Y
Z
cod(f)=dom(g)2020/3/23(C) 2020, Akihiko Koga

21

圏の例
• いくつか圏の例を見ていく
1. 集合の圏 Set
2. 集合の圏の一部分の圏
3. 前順序集合（preorder），部分順序集合（poset : partiallyordered set）
4. 小さな図式いくつか（1, 2, 2, GraphSyntax）
5. 関数型言語の圏

2020/3/23(C) 2020, Akihiko Koga

22

圏の例：集合の圏 Set• 集合の圏 Set
n オブジェクト
Ø 集合n 射
Ø 集合から集合への関数
Ø 射の合成は通常の関数の合成
g・f := λx.g(f(x))
注意）λx.exp(x) は，x を入力としてexp(x)を返す関数を
表す記法

Set

f

g
g・f := λx.g(f(x))

2020/3/23(C) 2020, Akihiko Koga

Set すべての集合の集まりなので，クラスになるが，今日のところはあまりここに神経質になる必要はない
本によっては，Sets と書く流儀もある（S. Awodey など）．
23

圏の例：集合の圏の一部分の圏• 圏Cがあるとき，そのオブジェクトの一部分を集め，集めたオブジェクト間のすべての射を集めると，それはまた圏になる• したがって次のようなものは Set の部分の圏である
n FinSet ... 有限集合とそれらの間の関数の圏

n A, B, C を集合とするとき，A, B, C をオブジェクトとし，それらの間の関数を射
とした圏

A

B
C

2020/3/23

オブジェクト：A, B, C
射： A, B, Cの間の関数すべて（図では書ききれないのでほとんど省略）
射に関しては，それらの合成が全部含まれるように絞れば，元の圏の部分的な圏ができる(C) 2020, Akihiko Koga

24

圏の例：前順序集合，部分順序集合• 定義 前順序集合と部分順序集合
n 集合 P と，その上の２項関係 ≤ の対 (P, ≤) が次の２つの条件を満たす時，(P, ≤) を前順序集合（preordered set） という．
Ø [反射律] x≤x for ∀x∈PØ [推移律] x≤y かつ y≤z ならば x≤z for ∀x, y, z∈Pn さらに (P, ≤) が上の２つの条件に加えて，次の条件を満たす時，(P, ≤) を部
分順序集合（partially ordered set あるいは poset）というØ [反対称律] x≤y かつ y≤x ならば x=y for ∀x, y∈P「反対称律」という用語は「≤」から「=」を除いて「<」による関係で考えると分かりやすいだろう[反対称律] x < y ならば y < x は成り立たない2020/3/23(C) 2020, Akihiko Koga

25

圏の例：前順序集合，部分順序集合• 前順序集合および部分順序集合は次のようにして圏とみることができる
n (P, ≤) を前順序集合とする

Ø オブジェクト
Ø P の要素Ø 射
Ø オブジェクト x, y がx≤y のとき，かつ，のときに限り他と区別のつく射 x→y が１つあるとする．
前順序集合は，推移律が成り立つので，射の連鎖は合成され，他と区別のつく１つの射になる(P, ≤)

x・x≤y のときxからyに１つの射があると考える．

y・そうでないときは射はない．

z・前順序集合は推移律を満たすので，連鎖した
射の合成ができてそれらのオブジェクト間の唯一の射になる

n 部分順序集合 (P, ≤)も同様に圏とみることができる
Ø 次の点だけが違う
部分順序集合ではお互いに相手に向かって射のある異なる
オブジェクトはないこと

2020/3/23

x(C) 2020, Akihiko Koga

y なら x≤y かつ y≤x なので
x=y26

圏の例：前順序集合，部分順序集合
補足• ここで述べたのは，前順序集合や部分順序集合そのものを圏として見る方法であり，このような集合の集まりの圏（Preorder や Poset）ではない• 前順序集合や部分順序集合そのものの圏は，無理やり例として出したように感じるかもしれないが，とても重要な圏である．
• 今日は述べないが，モノイドを圏としてみる見方と共に，圏論の二つの極端な性質を表現する役割を担っているオブジェクトが
１個だけ

モノイド

一般の圏

前順序集合

オブジェクト間の射が高々１個• 実際，前順序集合を圏としてみたものは，数学の中で「ガロア接続」という概念と結びつき，一つの研究領域を形成している• 圏の新しい概念を吟味するとき，まず前順序集合や部分順序集合で吟味してみるのがコツであるらしい
2020/3/23(C) 2020, Akihiko Koga

27

圏の例：小さな図式いくつか（１）•1

１個のオブジェクトとその恒等射だけからなる圏

1X
X

•2

•2

1X

1Y

X

Y

1X

1Y

X

f

２個のオブジェクトとそれらの恒等射だけからなる圏．二つのオブジェクトの間にはなんの射もない．
２個のオブジェクトとそれらの恒等射，片方のオブジェクトから他方への１つの射からなる圏．

Y

以下，図において恒等写像は省略する
2020/3/23(C) 2020, Akihiko Koga

28

圏の例：有限の圏いくつか（２）• GraphSyntax
Edges

start

Nodes

前頁の 2 に射が１本加わった形の圏

terminal

n グラフというものの骨格（文法）を表そうとしている．
つまり，グラフとはEdges
Ø エッジの集合 Edges とØ ノードの集合 Nodes

e

から成り，
Ø エッジ e には始点 start(e) と終点 terminal(e) がある

Nodes
start
terminal

具体的なグラフの例
ことを表そうとしている
n 具体的に，Edges と Nodes に集合が割り当てられ，射 start と terminalに関数 Edges→Nodes が割り当てられると具体的なグラフが１つ決まる
2020/3/23(C) 2020, Akihiko Koga

29

圏の例：プログラミング言語の圏
非常に簡単な関数型言語の圏• プログラミング言語を圏とみる見方は色々あると思うが，次のようなオブジェクトと射の圏が考えられる
n オブジェクト＝データ型
通常，基本データ型から C 言語でいう
構造体 struct {T1 x; T2 y;} などの型構築子を使って無数の型を作る
仕掛けが用意される
n 射＝プログラム（関数）通常，基本的な関数があり，それらを組み合わせて，さらに複雑な関数を構築するための仕掛けが用意されるプログラミング言語の圏のイメージ
Type1

fun1

fun2

Type1×Type2

Type3

fun3
Type4

・・・

射の合成規則の例
fun3・fun1:=λx.fun3(fun1(x))

注意）ここでは，「型や関数の実体が何か？」はまだ考えなくてよい．
ある文法に従った文字列と思っておいてよい．
2020/3/23(C) 2020, Akihiko Koga

30

圏の例：プログラミング言語の圏
非常に簡単な関数型言語の圏（全体像）• 「型」（オブジェクト）も「関数」（射）も基本のものから新たなものを作る
手段がある
基本型
関数型プログラミング言語の圏
TypeA1

TypeB1FunA
TypeA2型の構築手段FunBTypeB2型や関数の構築例

TypeA1×TypeB1<FunA, FunB>
TypeA2×TypeB2
2020/3/23

Bool, Int, Char, ...

・A, B ⇒ A×B
・A, N ⇒ A→B
・・・
基本関数
関数の構築手段add1(), mult2(),...

・合成 G・F・ペア <F, G>・・・(C) 2020, Akihiko Koga

31

圏の例：プログラミング言語の圏
いろいろなレベルの抽象化• 前頁で述べたプログラミング言語の圏は，まだ「意味」が入っていない• 例えば，次のような型と射があったとする
n 型

Int ... 整数型
Char ... 英文字の型

n 射

code : Char → Int
decode : Int → Char• このとき次のように合成された射は 1Char であるべきである
Char

code

Int

decodeChar

decode・code = 1Char• このような射を等しいと見なすことによって，意味をより反映した圏を作ることができ，これには色々なレベルの反映の仕方がある
2020/3/23(C) 2020, Akihiko Koga

32

関手
圏の定義

圏の例
Set, 1, 2, 2, GraphSyntax,
プログラミング言語

エッジが合成可能なマルチエッジ有向グラフ

関手
圏から圏への準同型

圏論の応用１関手の例
集合の圏 Set の多項式関手

代数/余代数によるデータ型の表現

他の著者の
入門用の
文献へ

型付きλ式への応用（応用２）に向けた諸概念の定義
モデルとは極限，積，冪，デカルト閉圏
2020/3/23(C) 2020, Akihiko Koga

次章以降へ

33

関手の定義• 定義 関手（functor） 圏の間の準同型

C, D を圏とするとき，C のオブジェクトから D のオブジェクトへの対応 F0 とCの射からDの射への対応 F1
F0 : C0→D0
F1 : C1→D1の組が以下の条件を満たす時，これらの組 F=(F0, F1) を C から D への関手
（functor）という．記号では F : C→D と書く．また，正確には，オブジェクトの対
応は F0(x)，射の対応は F1(a) だが，どちらも F を使って F(x), F(a) と書く．また，さらに括弧を省略して Fx, Fa と書くこともある．

C

条件１（1を1に移す）
F(1A)=1F(A)
条件２（合成を保つ）
F(g・f)=F(g)・F(f)2020/3/23

A
X

D

1A
f

Y
g・f

g

F
Z

(C) 2020, Akihiko Koga

F(A)

1F(A)

F(f)
F(g)
F(X)
F(Z)
F(Y)
F(g)・F(f)

34

関手の例

集合の圏 Set の上の多項式関手• 圏から圏への関手は非常に多彩である．ここではまず，特殊ではあるが，計算機科学への重要な応用を持つ集合の圏 Set から Set への多項式関手（polynomial functor）の例を紹介する
n 定数関手n 恒等関手n 定数との直積の関手
n X, X2, X3, ...
n 直和の関手
n 多項式関手（polynomial functor）

多項式関手を用いた代数と余代数によるデータ型の規定（これらは集合の圏に限った話ではないが，親しみがあり，新たな概念（積オブジェクト，和オブジェクト）を導入する必要のない集合の圏で説明する）
2020/3/23(C) 2020, Akihiko Koga

35

関手の定義の表し方• 関手はオブジェクトの対応だけではなく，射の対応も規定する• したがって，２つのオブジェクトと一つの射を含むような，つぎの書き方で定義する関手をうまく表現できるだろう

X

f

F(X)
F(f)

Y

2020/3/23

D

∈

∈

F:C

要素同士の対応を表すことにする．
本当は，出発点が縦棒の矢印「↦」を使いたかったのだが，使っている
プレゼンテーション作成ツールの線に適当なものが無かったため代用した．

F(Y)(C) 2020, Akihiko Koga

36

多項式関手
定数関手と恒等関手• 定数関手 X↦A
X

A

∈

Set

∈

A : Setf

1A
Y• 恒等関手 X↦X

A

X

X

∈

Set

∈

1 : Setff
Y

2020/3/23

例） X ↦ {0}Y(C) 2020, Akihiko Koga37

多項式関手• 直積による関手n X ↦ A×X．．．ある決まった集合 A と直積をとる関手

f

∈

Set

∈

A×- : Set
X

A×X

<1A, f>Yn X ↦ X, X ↦ X2, ..., X ↦ Xnf
2020/3/23

X

Set
∈

∈

-×- =(-)2: Set

A×Y

X×X

<f, f>Y

Y×Y(C) 2020, Akihiko Koga

38

多項式関手• 直和による関手XSet
F(X)+G(X)

F(f)+G(f)

f
Y

u

∈

∈

F+G : Set

F(X)

F(Y)+G(Y)

G(X)
+

v

F(f)(u) + G(f)(v)• 多項式関手（polynomial functor）

F(Y)

G(Y)

n A+B×X + C×X×X+... のような有限項の和からなる関手
n 形式的には定義を理解できると思うが，具体的には，多項式関手にどんな意味があるのか？

→ひとつには代数や余代数と関係がある
2020/3/23(C) 2020, Akihiko Koga

39

代数（Algebra）と余代数（Coalgebra）• 定義

n C を圏，F : C → C を自分自身への関手，X∈C とする．このとき，（気持ち的にはオブジェクト X や関手 F も含めて），圏 C の中の射
射

a : FX → X

を 代数（algebra）

c : X → FX

を 余代数（coalgebra）

C
X

と言う

C
F

FX

C

a
X

代数（algebra）
2020/3/23

X

C
F

FX

c
X

余代数（coalgebra）(C) 2020, Akihiko Koga

40

代数（Algebra）と余代数（Coalgebra）• 代数・余代数

a
FX → X代数

c
X → FX
余代数• これらは何を意味しているのか？

n 関手 F : Set → Set （FX := A + X2 ） で考えてみる
n このとき，例えば代数（つまり Set の中の写像）は
A + X2i+mX

次のことを言っている
Ø X には A の要素が埋め込まれている（i）
Ø X の二つの要素 x, y に対して，X の要素 m(x, y) を割り当てる規則がある

n つまり A の要素から二項演算 m を使ってできる集合（代数）を表している
2020/3/23(C) 2020, Akihiko Koga

41

代数（Algebra）と余代数（Coalgebra）
抽象データ型と代数• 代数の例 list of integern 適当な架空のプログラミング言語を仮定して記載している
data_type list_of_integer
empty : → list_of_integercons : (integer, list_of_integer) → list_of_integerendn これは，
Ø A: {empty_list}Ø Integer : 整数の集合の定義のもとに，F=A + Integer×(-) : Set → Set という多項式関手の代数<empty, cons>
F(D)
D
である
2020/3/23(C) 2020, Akihiko Koga

42

代数（Algebra）と余代数（Coalgebra）
計算機科学における余代数の例• 余代数の例 infinite list of A

n GX := A + X で次のような余代数の例を考えてみる
X

head + tail

GX=A + X

n つまり， X は

Ø A に属するデータを取り出す関数 head : X → A と
Ø X の部分を取り出す関数
tail : X → X がある

ような領域（集合）であり，これは無限リストを表している
head

tail

a1

・・・

a2

無限に tail : X → X を取り続けられる

一般に余代数は，このような無限のデータ構造や状態遷移機械（無限に動き続け，
何か信号を入れるとその都度反応を返す機械は無限リストと同じ）を表すのに利用できる
2020/3/23(C) 2020, Akihiko Koga

43

代数（Algebra）と余代数（Coalgebra）
まとめと補足• 多項式関手 F に対して，代数 FX→X，余代数 X→FX が一意に決まる訳
ではない．
• これらを一意に決めるときには，それらが，「始代数（initial algebra）」
や「終代数（final algebra）」であることを要求する必要がある• 始代数や終代数で規定されたデータ型に関する関数の定義方法や証明方法として，帰納法（induction），余帰納法（coinduction）がある
n list_of_integer の長さ length の帰納法による定義（constructor に対する関数の挙動を指定することで関数を定義）
Ø length(empty) = 0
Ø length(cons(_, x)) = 1 + length(x)n infinite list of A のマップ関数 map の余帰納法による定義（関数に対する destructor の挙動を指定することで関数を定義）
Ø head(map(list, f)) = f(head(x))Ø tail(map(list, f)) = map(tail(list), f)

2020/3/23(C) 2020, Akihiko Koga

44

代数（Algebra）と余代数（Coalgebra）
読み物• この代数，余代数の話題に関しては次の秀悦なチュートリアルがある．
これはすでに今までの圏論の知識で読み始められる（と言うか，集合の圏に特化して圏論の最初から解説してあるのでいつでも読める）
n Bart Jacobs , Jan Rutten : A Tutorial on (Co)Algebras and(Co)Induction, 1997, 38 pages• 代数，余代数の両方の性質を持つ dialgebra というものもある
C

これは C → D の型の二つの関手 F と G を使ったa
FX → GX

X

F

G

D
FX
↓a
GX

の形の構成物で，萩野達也氏はこれや随伴関手を使っていろいろなデータ型を作ることができる言語（CPL：Categorical Programming Language）を提案した■

萩野達也「カテゴリー理論的関数型プログラミング言語」1990年1月 等

2020/3/23(C) 2020, Akihiko Koga45

型付きλ式への応用（応用２）に向けた諸概念の定義
圏の定義

圏の例
Set, 1, 2, 2, GraphSyntax,
プログラミング言語

エッジが合成可能なマルチエッジ有向グラフ

関手
圏から圏への準同型

圏論の応用１関手の例
集合の圏 Set の多項式関手

代数/余代数によるデータ型の表現

他の著者の
入門用の
文献へ

型付きλ式への応用（応用２）に向けた諸概念の定義
モデルとは極限，積，冪，デカルト閉圏

2020/3/23(C) 2020, Akihiko Koga

次章以降へ

46

モデルとしての関手• 定義

n 関手 F : C → Set を圏 C のモデルと言うn 関手 F : C → D を圏 C の圏 D によるモデルと言う• 例 （圏の例で紹介した）圏 GraphSyntax のモデル
n F : GraphSyntax → Set を関手とする
GraphSyntax

Edges

start

Nodes

F

F(Edges)terminal

Set
F(start)F(Nodes)F(terminal)n F は具体的に，Edges にエッジの集合を，Nodes の頂点の集合を与え，エッジにその始まり（start）と終わり（terminal）となる頂点を割り当てている
n つまり，関手 F は具体的なグラフを一つ定義しているのに他ならない

2020/3/23(C) 2020, Akihiko Koga

47

モデルとしての関手
脇道：「自然変換」との関係• 関手 F1 と F2 がともに，GraphSyntax → Set の関手とすると，F1,F2 はそれぞれ具体的なグラフを決めている
GraphSyntax

F1
F2

Set

α

F1（GraphSyntax)
F2（GraphSyntax)

α

この場合は
グラフの準同型になる

n 今日は触れないが，圏論では関手から関手への射として，「自然変換（natural transformation）」という概念を考える（上図のα）
n このGraphSyntax の例の場合，自然変換 α は関手 F1 が表すグラフからもう一つの関手 F2 が表すグラフへの準同型になっている• 圏論を勉強するときは「自然変換」はとても重要な概念である• ここで述べた，自然変換がモデルの間の準同型になっているということは，自然変換をイメージするのに非常に役に立つと思う
2020/3/23(C) 2020, Akihiko Koga

48

意味を定めるための圏
特にプログラミング言語を解釈するための圏• 集合の圏などへの関手がモデルを定めることを見てきた
n F1 : C → Set
n F2 : C → D

C で規定される概念を集合で解釈
C で規定される概念を圏 D の言葉で解釈• 圏論の計算機科学への応用の一つとして，このモデルを定めるということを使い，プログラミング言語などの意味論を与えるというテーマがある• 今日の発表はこのテーマに沿って，単純型付きλ計算の意味論を与える圏 （デカルト閉圏）を構成する（Set もこのような圏だが，ここではSet 以外の圏も考える）• まずは，プログラミング言語を埋め込むことができる圏がどのような特徴を持っていればよいかを見ていく
2020/3/23(C) 2020, Akihiko Koga

49

単純型付きλ計算の意味を与える圏の条件• 少し先走って，「単純型付きλ計算」の特徴を説明する．
• 「単純型付きλ計算」は次の２つの操作を持つ言語である
n 関数を式に適用する

Ø f を式 3 に適用する (f 3)

n 式から変数を抽象化して関数を作り出す
Ø 式 3+x*y の x をパラメータと考えた関数 λx.(3+x*y) を作り出す
Ø 上の関数適用の例で f と書いていたものの実際の形は，このようなλx を伴った式である

式
3+x*y

関数
λx.3+x*y

x をパラメータと考えて式から関数を作り出す• 「単純型付きλ計算」のモデルとなる圏は，これらの操作，関数適用と関数への抽象化に対応する機構を内部に持たねばならない• 以下，どんな機構を持たねばならないかを説明する．それらを持つという条件が，デカルト閉圏（CCC）の条件になる
2020/3/23(C) 2020, Akihiko Koga

50

単純型付きλ計算の意味を与える圏の条件• 圏における関数適用と式から関数への抽象化を表現する機構とは？
• つぎの３つの機構でこれらを表現する
n 二つのオブジェクトの情報を一つのオブジェクトへのパッキングn パッキングされたオブジェクトの評価
n オブジェクト Y からオブジェクトX の部分を抽象化して関数のオブジェクト F を作る
関数のオブジェクトF

データのオブジェクトX

２つの情報をパッキングしたオブジェクト（F×X）を作る
２つのオブジェクトの情報を含んだオブジェクト
関数のオブジェクトFとデータのオブジェクトX

評価
データのオブジェクトY

データのオブジェクト Y から X の部分を抽象化して関数のオブジェクト（X→Y）を作る
2020/3/23(C) 2020, Akihiko Koga

51

単純型付きλ計算の意味を与える圏の条件
積オブジェクトと冪オブジェクトを持つこと• これも先走って言うと，前頁の図を実現するための圏の概念は「積」と「冪」で，集合の圏 Set での対応物は次のようになる
名称

記号

直感的な説明集合の圏での対応物

積（Product）

A×B

２つのオブジェクトA と Bの情報をパッキングした
オブジェクトA×B（A と B の直積）

A→B
データのオブジェクト B（あるいはBA） から A の部分を抽象化した関数のオブジェクト

A→B（A から B への関数の集合）冪（Exponential）• 以下，Set 以外の一般の圏において，これらのモノを定義していく
2020/3/23(C) 2020, Akihiko Koga

52

積オブジェクト

準備：Generalized Elements• 二つのオブジェクト A と B の両方の「情報（あるいはデータ）を含んだ」「積オブジェクト（product）」を作りたい• オブジェクトの「情報（あるいはデータ）を含んだ」とは何か？
n 圏論では一般にオブジェクトの内部の要素は見えないが，それに代わる概念
はある
n それは射である
n 特に集合の圏 Set で１個の要素の集合 {*} からの写像 f : {*} → A は，Aの要素と同一視できる f(*)∈A
定義
射 f: X → A を，A の generalized element という■ これは，射はオブジェクトの中の要素のように見えることもあるので，それを思い起こさせる
別名をつけておこうというだけである■ 圏論では，「モノの中の要素は重要でない」と言いつつ，ここでは，「モノの持つ情報」を考える直感的な道具として「要素」のアナロジーを使わせていただく
2020/3/23(C) 2020, Akihiko Koga

53

二つのオブジェクトの積オブジェクト
二つのオブジェクトへの射の組合せを中継できるオブジェクト• ２つのオブジェクト A と B の情報（データ）をすべて持っているオブジェ
クト「A と B」とは？
n 任意のオブジェクト C に対して
Ø Cから A への任意の射 f とØ Cから B への任意の射 g
∀
∀

∃

f
πA

A
2020/3/23

C

h

AとB

∀
g
πB
B

を中継することができるオブジェクト「AとB」
は A と B の情報をすべて含んでいると考えてよいだろう！
なぜなら任意の generalized elements
f : C→A, g : C→B の組を中継する射h : C→AとB があるので，f, g を考える
かわりに 「AとB」のgeneralized
element h を考えれば良いから「AとB」
πA : 「AとB」→A
πB : 「AとB」→B(C) 2020, Akihiko Koga

は固定

54

二つのオブジェクトの積オブジェクト
中継能力のあるオブジェクトの中の最小のオブジェクト• 「A と B」は，f, g を中継する射 h が存在するだけの条件で良いか？

n 集合の圏で考えると，集合 A と B の直積 A×B = {(a, b) | a∈A, b∈B} は，
このような h の存在を保証するが，じつは，このような保証は，A×B より大きな集合ならなんでも可能である（すべての (a, b) の組を含んでいれば良い）
∀

∀

∃

f
πA

A

C

h

AとB

∀
g

A×B, {0, 1}×A×B など，A×B より大きければ，どんな集合でも，
この「AとB]の条件を満たす．

πB
B

通常は，最小性の条件を課す（次頁）（＝h が一意に決まるという条件）
2020/3/23(C) 2020, Akihiko Koga

55

二つのオブジェクトの積オブジェクト
改めて標準的な定義• 定義 オブジェクト A と B の積オブジェクト（product）

n オブジェクト A と B に対して，オブジェクト A×B と二つの射 πA と πB
πA
πB
A
A×B
B
が，オブジェクトAとBの積オブジェクト（product）であるとは，n 任意のオブジェクト C と∀n Cから A への任意の射 f とCn Cから B への任意の射 g に対して∃!
f = πA・hh∀fg = πB・hとなる射 h : C → A×B がただ一つ存在
A×B
することである．このように図式の中の射のπA合成が等しくなることを「図式を可換にする」
Aという．

2020/3/23

∀
g
πB
B

注意）∃! あるいは単に ! は「ただ一つだけ存在する」ことを表す記号である(C) 2020, Akihiko Koga

56

終対象：0個のオブジェクトの積オブジェクト• ここまで２個のオブジェクトの積オブジェクトを定義してきた• これは一般に n≧1 個のオブジェクトの積オブジェクトへと拡張できる
n つまり n 個のオブジェクトへの任意の射の組合せを中継できる１個のオブジェ
クトという具合に• また，逆にオブジェクトの数を減らして，0 個にすることも考えられる
n つまり，「どのオブジェクトからの射を中継する必要がある」という制約が全く無く，すべてのオブジェクトから１個だけの射を持つオブジェクトである．このようなオブジェクトを終対象という．終対象は，t や 1 で表すことが多い．

• 定義 終対象
n 圏の中の任意のオブジェクトからただ１つの射があるオブジェクトを
終対象（terminal object, final
object）と言う
2020/3/23(C) 2020, Akihiko Koga

圏C
∀
∃!

C
t
57

比喩：組織の中の積オブジェクト• 次のような Z社の圏を考えてみる
n オブジェクト
Ø 社員

出金して

n 射

Xさん

Ø 社員から社員への指示
Ø 合成は適当に決めて！

• 積オブジェクト A × B は，A さんと B さんへの指示を中継できる最も職位の低い人，つまり，A さんと B さんの共通の上長で最も職位の低い人である．
こういう比喩はいくらでもできる．

社長
A×B

部長
課長

グループ２

グループ１

また，射の向きを逆にすると概念ががらっと変わることもあるので，そのことに注意しながら，いくつか味わってみることも面白い．
2020/3/23

Yさん(C) 2020, Akihiko Koga

A

B
58

補足：積オブジェクトと「極限」との関係• 通常の圏論のテキストでは，積オブジェクトは「極限」の一種としての統一的な説明がなされる• 本資料では，できるだけ速やかに積オブジェクトと冪オブジェクトを定義するため，この扱いを避けた• 「極限」，およびその双対（射が反対向き）の概念である「余極限」の理解のためには，「終対象」，「始対象」の理解が基本的である
n 終対象についてはすでに説明した．オブジェクト 1 が終対象であるというのは，C の任意のオブジェクト X から，1 にただ一つの射があること．つまり，
∀X

!X

1

n 始対象 0 はこの逆，つまり任意のオブジェクトにただ一つの射がある
0

!X

∀X

• オブジェクト A と B の積 A×B は，大まかに言えば，「A と B の両方にアクセスできるオブジェクトがなす圏の終対象」である（次頁）
2020/3/23(C) 2020, Akihiko Koga

59

補足：積オブジェクトと「極限」との関係• A×B : A と B の両方にアクセスできるオブジェクトがなす圏の終対象
n 圏 C から次のようにして，圏 C(A, B) を作る
n 圏 C(A, B)Ø オブジェクト
X∈C で，A にも B にも射があるものに対して，X とそれらの射を組にしたもの

Ø 射

A

pA

X

pB

B

qA=pA・f かつ qB=pB・f となる
f をオブジェクト (Y, qA, qB) から(X, pA, pB) への射とし，射の合成は
圏 C の中の射の合成のままとする．

qA

A

pA

f

X

Y
pB

qB

B

• このようにして作られた圏 C(A, B) の終対象が A×B である．意味的には A, B にアクセス可能（射がある）オブジェクトからの射を中継できるオブジェクトの中の最小のものである
2020/3/23(C) 2020, Akihiko Koga

60

評価射（eval） と冪オブジェクト（Exponentials）• 前頁までで，二つのオブジェクトの積 F × X が定義できた• 次に関数適用（eval: (F×X)→Y）と関数への抽象化（X→Y）を定義したい
F
(X→Y)

×

X

eval 評価（関数適用）(f(x) for f∈F, x∈X)Y

F=X→Y としてX を与える
X→Y

Y から X を抽象化して関数化

eval• (X→Y)×X → Y はどのような性質を持っていれば良いだろうか？
X と Y に対してこのような射 eval がありさえすれば良いのだろうか？
2020/3/23(C) 2020, Akihiko Koga

61

冪オブジェクトと評価射
関数空間の中の関数空間，インタープリタの中のインタープリタ• X→Y を単に「射 f : F×X → Y が存在する F」とすると，かなりつまらないオブジェクトが X→Y になり得る
n 例えば，集合では F=Y, f=πY と置けば，πY : Y×X→Y の形になる• 関数空間相当の X→Y としては，これらの評価用の射をすべて取り込
み得るオブジェクトの中の最も小さいものととるべきだろう• これは積オブジェクトの時と同じように，次のような条件を置けばよい
∀

F

∃! f♭

× X
×

(X→Y) × X
2020/3/23

∀f

Y

1X

1Y
eval

Y

任意の関数適用の形式 f : F×X→Y に対して，f♭ : F→(X→Y) がただ１つ存在してeval・(f♭, 1X)=f
となる．
つまり，
・任意の関数適用形式 f : F×X→Y を
eval : (X→Y)×X→Y がシミュレートできる．
・∃! f♭の部分から，それは最小のオブジェクト
である(C) 2020, Akihiko Koga

62

冪オブジェクトの定義
標準的な教科書の形式• 定義 A と B の冪（exponential） A→B （BA が普通）

n C は任意の二つのオブジェクトの積が存在する圏とし，A, B, C を C のオブジェク
トとする
n C のオブジェクト A→B が（射 eval : (A→B)×A→B を伴って），A と B の冪オブジェクト（exponential）であるとは，次の条件が成立することである．
Ø 任意のオブジェクト C と任意の射 f : C×A→B に対して，次の式が成り立つ
射 f♭ :C→ (A→B) が一意に存在する
∀

C

∃! ♭
f

∀

× A
×

(A→B) × A

1A

左の図式が可換になる f♭， つまり

f

eval

eval・<f♭, 1A>=f

Bになる f♭ が一意に存在する

注意）オブジェクト (A→B) は BA が普通の記法である．
私は関数空間っぽい (A→B) を使うことが多い．
2020/3/23(C) 2020, Akihiko Koga

63

冪オブジェクトの統一的な理解に向けて• 圏の多くの概念が極限と余極限で整理できるが，冪は直接には，これらで整理出来ず，
通常は，随伴関手の概念の登場を待つ必要がある• しかし，もう少し簡単な理解方法として，冪は「陰関数型の極限」，あるいは「逆関数型の極限」とみる方法もある
n F : C → D を関手とする（冪の理解の時は F(C) := C×X と置く）
n 冪 P=X→Y は圏 D' := {Z∈F(C) | 射 F(Z)→Y が存在} の終対象（極限）のF に関する元像であるC
D の部分圏 D'
D
オブジェクト：F(D) の中でF(D)Y への射があるもの
D'
∃! P'
f♭
F(P')
F
これは単に「冪がコンマ圏 」
f
P=X→Y((-)×X ↓ Y) の終対象であるとF(P)2020/3/23

F に関する元像

Y(C) 2020, Akihiko Koga

言っているにすぎないのだが，コンマ圏自体がイメージしにくかったりする．
64デカルト閉圏
Cartesian Closed Category CCC• 定義

n 任意のオブジェクト X と Y に対して，積 X × Y，冪オブジェクト X → Y が存在し，さらに終対象が存在する圏をデカルト閉圏（Cartesian closed
category） という．デカルト閉圏は英語の頭文字をとって，CCC と略されることもある．
n デカルト閉圏は関数適用と関数への抽象化を表現する機構が入った圏である

デカルト閉圏 C
積（終対象も積の一種）(X→Y) × X

evalY

X の部分を抜き出し，関数への抽象化
2020/3/23(C) 2020, Akihiko Koga

65

デカルト閉圏の例• 集合の圏 Set

n A×B = {(a, b) | a∈A, b∈B}
n A→B = {f | f は A から B への関数}

Ø eval : (A→B)×A→B, eval(f, x) = f(x)n 終対象 1 は一つの要素だけからなる任意の集合 {*}• 部分順序集合の圏 Posetn 圏の定義Ø オブジェクト
Ø 部分順序集合 (P, ≤)Ø 射Ø 順序を保つ関数 f : P→Q such that if p1≤p2 then f(p1)≤f(p2)n P×Q = {(p, q) | p∈P, q∈Q} (p1, q1)≤(p2, q2) iff (p1≤p2 & q1≤q2)
n P→Q = {f | f は PからQへの順序を保つ関数} f1≤f2 iff f1(p)≤f2(p) ∀p∈Pn 終対象 1 は一つの要素だけからなる集合 {*}, *≤*2020/3/23(C) 2020, Akihiko Koga

66

デカルト閉圏の例• Heyting Algebran 次のような条件を満たす poset (H, ≤)Ø 任意の２元 x, y∈H に対して下限 x∧y∈H が存在する
Ø 任意の２元 x, y∈H に対して z∧x ≤ y となる z の上限が存在する．これをx→yと表す
Ø H の最小元が存在する

n poset H を圏と考えたとき，これは CCC になるØ 圏H
Ø オブジェクトは H の元
Ø 射 x→y は x≤y の時，かつそのときに限り x→y が唯一存在するとする
Ø x×y は x∧yØ x→y は上で定義した x→yØ 終対象は H の最小元

n Heyting Algebra は直感主義命題論理のモデルになる
n これは CCC が単純型付きλ計算のモデルになるのと並んで，CCC の大切な用途の一つである
2020/3/23(C) 2020, Akihiko Koga

67

デカルト閉圏に関する補足• デカルト閉圏は射の集合相当をオブジェクトとして扱える圏
X→Y

X

×

C(X, Y)
Y

X

評価する

Y
C(X, Y) は，圏C におけるオブジェクトX から Y への射の集合を表す• 領域理論で関数空間をデータ空間に埋め込める領域 D[D→D] ≅ Dを構成する必要に迫られることがあるが，そのような領域の候補である
2020/3/23(C) 2020, Akihiko Koga

68

単純型付きλ計算

2020/3/23(C) 2020, Akihiko Koga

69

型なしλ計算と単純型付きλ計算• まず，型なしのλ計算について簡単に説明する
n ご参考：次の場所にλ計算の簡単な解説を書いた

http://www.cs-study.com/koga/computer/lambda.html
動かして遊ぶλ計算の初歩 in Ruby

• 次に，そのλ計算に，型による制限を加えた体系として単純型付きλ計
算を導入する• 簡単にいうと単純型付きλ計算は，型によって，λ計算に，自己参照ができないような制限を加えたものである．したがって，再帰呼び出しができない（組込み型を導入することによる抜け道はある）
2020/3/23(C) 2020, Akihiko Koga70

型なしλ計算• 前提
n 変数が可算無限個，用意されているとする（変数は好きなだけ使えるという意味）• λ式 ... 次のように作られたものだけがλ式である

n 変数はλ式である
n Exp がλ式で，x が変数なら λx.Exp はλ式である
n Exp1, Exp2 がλ式なら，(Exp1 Exp2) はλ式である• 例: λx.x，λf.λx.(f x), ...
• 用語，記法

n λx.Exp という形があったとき，Exp 内に現れる変数 x は束縛（bound）されているという．また，変数（仮に u とする）はそれを取り囲むλu という形のものがな
いとき，自由（free）であるという
例： λx.λy.(z λz.(x (y z)))
左括弧の直後の z のみが自由で他は束縛されている
n λ式の括弧は分かると思うときは，適宜省略する

2020/3/23(C) 2020, Akihiko Koga

71

型なしλ式の計算• 次の２つの変換ルールを導入する

n α変換 ... 変数（パラメータ）の名前変更

Ø λx.Exp において，x を別の変数，例えば，y に変えて，λy.Exp' にしてよい．ただし，Exp' は Exp の中の free な x をすべて y に変えたものである．また，Exp の中に y は free に現れないものとする

n β変換 ... 代入操作

Ø λx.Exp1 Exp2 という形のλ式を Exp1[x := Exp2] に変えてよい．ただし，
Exp1[x := Exp2] は，Exp1 の中の free な x を Exp2 に置き換えたものである．また，このとき， Exp2 の中の free な変数が束縛されるようなことがあってはならない• λ式の計算n α変換，β変換の繰り返しを計算の過程とみなす
n もうβ変換が適用できないλ式を正規形（normal form）であるといい，これを計算の結果とみなす
n 例(λx.λy.x λu.u) v → λy.(λu.u) v → λu.u

2020/3/23(C) 2020, Akihiko Koga

72

いろいろなλ式とその計算能力（１）• 自然数, 0, 1, 2, ... （チャーチ数）n $n = λf.λx.f(f(...f(x)...))

注意）$n はこの資料だけの記法

fがn個

n $n は与えられた関数 f を n 回適用するという働きを持ったλ式である• 真偽値（ブール値）

n true = λx.λy.x
n false = λx.λy.yØ true と false は，次のような簡約が行われるλ式である．プログラミング言語の
if 文 「if B then Exp1 else Exp2」の B の位置にそれらがあると，それぞれ then-part，else-part が取り出される性質をもったλ式である
Ø true Exp1 Exp2 => Exp1
Ø false Exp1 Exp2 => Exp2
Ø ちなみに false は $0 と同じ

2020/3/23(C) 2020, Akihiko Koga

73

いろいろなλ式とその計算能力（２）• 不動点コンビネータ Y

n Y= (λf . (λx . f (x x)) (λx . f (x x)))= (λf . (λx . f (x x))(λx . f (x x)))n YF→F(YF)→F(F(YF))→... と無限に簡約化が進むλ式（つまり，指定されたFを何回も何回も繰り返し適用するλ式）
n 再帰関数（あるいはループ相当の計算）の表現に使う
n 再帰関数を導入できる不動点コンビネータは Y だけでなく無数にある• λ計算の計算能力

n 数が表現でき，関数適用の連接，if 文，再帰（ループ）が表現できるので，再帰関数を表現することができる（再帰的に枚挙可能な関数も表現可能）• 単純型付きλ計算の計算能力
n 次に紹介する単純型付きλ計算はこれより少し計算能力が落ちる
2020/3/23(C) 2020, Akihiko Koga

74

単純型付きλ計算• これから単純型付きλ計算を定義していく• 基本的には型無しλ式のλx.・・・の部分の変数 x にλx:τ のように型をつけただけだが，１つ扱いで困難な点がある• それは，λで導入されない自由変数を扱う必要が発生し，λ式単独で意味を与えることが難しいということである
n 例えば，λx:τ.λy:σ.x は τ→(σ→τ) と型が決まるが，中の式のλy:σ.x はx の型が不定のため単独では型を決めることができない．
n 自由変数を持たない式だけ扱うようにすれば良いと考えるかもしれないが，後者の式は前者の式を解釈する途中に現れてしまう• そのため自由変数の型の宣言とλ式の対に意味を与える必要がある
自由変数とその型の宣言の列例：

x : τ ⊢ λy:σ.x型付きλ式（x の型が τ である文脈での型付きλ式 λy:σ.x）⊢ の左を文脈（context）という2020/3/23⊢(C) 2020, Akihiko Koga

75

単純型付きλ計算
この資料での記述方法についての注意• いろいろな書物では，文脈と単純型付きλ式をそれぞれ定義して，あとで組み合わせる方法をとっている文脈Γ f:o→0, d:o

単純型付きλ式
λx:o.λy:o.x型の言明
Γ ⊢ λx:o.λy:o.x : o→(o→o)

n これは，λ式を再帰的に定義するとき，変数単独のものをλ式として定義する際に型が決まっていないという困難が発生するように思う
n 「予め型の決まった変数がたくさん用意してある」という設定を置いているものもあるが，λx:T で導入される変数との扱いの違いが気になる• 本資料ではそれらの書物と異なるが，最初から，文脈付きのλ式を定義してみる（直接，上の図の「型の言明」を定義）• 一般の書物で勉強しなおすとき，このことを注意してほしい
2020/3/23(C) 2020, Akihiko Koga

76

単純型付きλ計算（Simply Typed λ-calculus）• ここでは以下の概念の定義を行う
型(Types )1, o, o×o,(o×o)→o, ...

文脈(Context )Γ x: o×o, f : (o×o)→o...

Γ ⊢ λx:o.(λy:o.x) : o→(o→o)
f:o→o ⊢ λu : o. (f u) : o...
Γ⊢t1=t2 : T1...

λ式(λ-Terms )Γ ⊢ λx:o.(λy:o.x)Γ ⊢ λu : o. (f u)...

公理(Axioms )x: T1, y:T2 ⊢ y:T2...

型の言明(Judgements )2020/3/23

文脈付き

導出

(C) 2020, Akihiko Koga

導出規則(Rules )Γ⊢f:T1→T2 Γ⊢x:T1
Γ⊢(f x):T2...
77

Simply Typed λ-calculus型（Types）と文脈（Context）• 型（Types）

基本の型の集合 BasicTypes がある （例 BasicTypes={Bool, Int, Real, ...}）
n 1 は型である（デカルト閉圏 C で終対象 1C に対応する特殊な型）
n BasicTypes の要素は型である
n α, β が型なら
Ø α→β は型である（αからβへの関数の型を意図）
Ø α×β は型である（αとβの直積の型を意図）
補足） 実用の言語でなく理論的な扱いのためだけの場合 BasicTypes はただ一つの型からなる {o} とすることも多い（o はチャーチが命題の型に使ったもの）• 文脈（Context）
変数と型の組の列

x1:T1, ..., xn:Tn

を文脈（Context）と言う．0 個の列も許す（ここでは ∅ と書くことにする）
文脈は Γ, Δ など，ギリシャ文字の大文字で表す
2020/3/23(C) 2020, Akihiko Koga

78

Simply Typed λ-calculus
文脈付きのλ式（Terms）• 前提
n 変数として使える記号が可算無限個用意されているとする
n 必要に応じて，型が指定された定数（関数も含む）を用意してもよい
c : A, f : A→B, ...

• 文脈付きの型付きλ式 (λ-Terms)

Ø 定数： c が型τの定数なら任意の文脈Γに対して，Γ⊢c:τ は型付きλ式である
Ø 変数： Γが変数 x に対して，x:τ を含むなら，Γ⊢x:τ はτの型付きλ式である
Ø * : Γ⊢*:1
Ø 組み込みの関数の適用：Ø Γ⊢<a, b>:τ×ρ は型付きλ式．ただし Γ⊢a:τ，Γ⊢b:ρ とするØ Γ⊢fst(a) :τ は型付きλ式．ただし，Γ⊢a:τ×ρ とする．
Ø Γ⊢snd(a):ρ は型付きλ式．ただし，Γ⊢a:τ×ρ とする．
Ø 関数適用： Γ⊢(c a):ρ は型付きλ式．ただし，Γ⊢c:τ→ρ，Γ⊢a:τ とする．
Ø 関数抽象化： Γ⊢λx:τ.b:τ→ρ は型付きλ式．ただし，Γ⊢b:ρ とする．
注意）λ式のすべてに型を書くのは，視認性を悪くするので，きちんと型が付くと分かっている場
合は，省略することがある（ただし，「λx:T. 」の部分は省略しない）
2020/3/23(C) 2020, Akihiko Koga

79

型の言明(Judgements )• 言明としては次の２つの形式を扱う
n Γ ⊢t : Type

Ø これはすでに文脈付き単純型付きλ式として定義した
Ø 文脈 Γ の自由変数宣言のもとではλ式 t の型は Type になるという言明である
Ø 本資料では，λ式の構成方法として，正しく型が付くλ式しか出来ないようにしたので，これに関する公理も推論ルールも特に設けないn Γ ⊢t=t' : TypeØ Γ ⊢t:Type かつ Γ ⊢t':Type であるとき，t と t' が等しいことを表す言明である
Ø 例えば，
d:o ⊢ (λx:o.x d)=d:oØ 他に次のようなものもある
p:o×o ⊢ <fst(p), snd(p)>=p:o×o
Ø 単純型付きλ計算には，理論を構築する必要に応じて等式による公理を入れること
で，いろいろな等式が証明できるようになる

2020/3/23(C) 2020, Akihiko Koga

80

単純型付きλ計算の公理• 公理（スキーム）n Γ ⊢ fst(<a, b>) = a:τn Γ ⊢ snd(<a, b>) = b:σn Γ ⊢ <fst(c), snd(c)>=c:τ×σn Γ ⊢ ((λx:τ.b:σ) a:τ)=b[x:=a] : σØ ここで代入 t[x:=r] は以下のように再帰的に定義されるものとする

x[x:=r] = ry[x:=r] = yc[x:=r] = c*[x:=r] = *<s, t>[x:=r] = <s[x:=r], t[x:=r]>fst(s)[x := r] = fst(s[x:=r])snd(s)[x:=r] 0 snd(s[x:=r])(s t)[x:=r] = (s[x:=r] t[x:=r])(λx.s)[x:=s] = λx.s
(λy.s)[x:=r] = λy.(s[x:=r]) if x≠y かつ r の
自由変数がs[x:=r]で束縛されないn Γ ⊢ λx:τ.(c x)=c:σ ただし，Γ ⊢ c:σ かつ x が c に現れない）（これはη変換の公理．η変換は単純型付きλ計算の公理に含めないこともある）
2020/3/23(C) 2020, Akihiko Koga

81

Simply Typed λ-calculus• 導出規則 (Rules)
n 型の導出Ø 文脈付き単純λ式の構成方法の中に取り込んだので，特に必要ない

n s=t:τ の導出規則
Ø = の同値性

Γ⊢t:τΓ ⊢ t=t : τΓ ⊢ s=t : τΓ ⊢ t=s : τΓ ⊢ s=t : τ Γ ⊢ r=r : τΓ ⊢ s=r : τØ 弱化（Weakening）
Γ ⊢ s=t : τΓ, x:σ ⊢ s=t : τ

2020/3/23(C) 2020, Akihiko Koga

82

Simply Typed λ-calculus
n s=t:τ 続き
Ø product types
Γ ⊢ s=u : τΓ ⊢ t=v : σΓ ⊢ <s, t>=<u, v> : τ×σΓ ⊢ s=t:τ×σΓ ⊢ fst(s)=fst(t) : τΓ ⊢ s=t:τ×σΓ ⊢ snd(s)=snd(t) : σΓ ⊢ s : τ×σΓ ⊢ <fst(s), snd(s)>=s : τ×σΓ⊢s:τΓ ⊢ fst(<s, t>)=s : τ
2020/3/23

Γ⊢t:σΓ ⊢ snd(<s, t>)=t : σ(C) 2020, Akihiko Koga

83

Simply Typed λ-calculus
n s=t:τ 続き

Ø function types

Γ ⊢ s=t : τ→σΓ ⊢ u=v : τΓ ⊢ (s u)=(t v) : σ
Γ, x:τ ⊢ s=t : σΓ ⊢ λx:τ.s = λx:τ.t : τ→σΓ⊢s:τ
Γ, x:τ ⊢ t : σΓ ⊢ (λx:τ.t) s = t[x:=s] : σΓ⊢ t : σ（η変換）Γ ⊢ λx:τ.(t x) = t : σ

ただし，t に x は自由変数として現れないとする

Ø unit typeΓ ⊢ t:1
Γ ⊢ t=* : 1

2020/3/23

unit value * は unit type 1 の唯一の値(C) 2020, Akihiko Koga

84

単純型付きλ計算で表現できる関数• 型付きλ計算は再帰関数を定義することができないので，プログラミン
グ言語でいえば，文の連接と if 文だけでできるプログラムに相当する• このことから，ほとんど表現力がないと思うかもしれないが，λ式での数の表現（チャーチ数）がかなり強力なので，足し算，掛け算，べき乗などいろいろな関数を表現することができる
n plus := λm.λn.λf.λx.(m f (n f x))
n mult := λm.λn.λf.(m (n f)) ... f を n 回適用することを m 回繰り返す
n power := λm.λn.(n m)
先に紹介したページのインタープリタのログ（このインタープリタでは，$n は n のチャーチ数の略記．またλは省略）

lb> mult ($2) ($3)
Input = m.n.f.(m (n f)) f.x.(f (f x)) f.x.(f (f (f x)))・・・
Result = f.x.(f (f (f (f (f (f x))))))
f.x. の後ろに f が 2*3=6個ついています．
2020/3/23(C) 2020, Akihiko Koga

85

単純型付きλ計算の理論としての表現力
代数などの表現• 単純型付きλ計算の体系には，BasicTypes, 定数，公理（等式）の集合を入れることにより，いろいろな理論を表現することができる
n 群

Ø BaiscTypes={G}
Ø 定数
Ø e:G
Ø inv:G→GØ mult:G×G→GØ 等式
Ø x:G ⊢ mult(x, e)=x:G
Ø x:G ⊢ mult(e, x)=x:G
Ø x:G ⊢ mult(x, inv(x))=e:G
Ø x:G ⊢ mult(inv(x), x)=e:G
Ø x:G, y:G, z:G ⊢mult(mult(x, y), z)=mult(x, mult(y, z)):G

n 同様に等式で表現することができる代数（普遍代数）は表現することができる（環や加群など．しかし，体は 1/0 が定義できないため不可）

2020/3/23(C) 2020, Akihiko Koga

86

単純型付きλ計算の理論としての表現力
自己参照的な型の表現
n 自己参照的な型
次のような型，定数，等式を加えることにより，関数をデータとして埋め込むことができる
データ型を表現することができる
Ø BasicTypes={D}Ø 定数
Ø decode : D→(D→D)Ø encode : (D→D)→D
Ø 等式
Ø f:D→D ⊢ decode(encode(f))=f : D→D
つまり，関数 f : D→D を encode(f) : D というデータに変換し，それをdecode(encode(f)) とすることで，もう一度もとの関数 f に戻すことができる
この機構を使えば，自分自身を encode して引数として受け取り，decode して呼び出す
ことができるので，実質的に再帰呼び出しを実現することができる
再帰呼び出しd:D ⊢ (λf:D→D→D.f(encode(f))(d)) (λg:D.λu:D.・・・ decode(g)(g)(u) ・・・)
2020/3/23(C) 2020, Akihiko Koga

87

単純型付きλ計算とCCC の関係2020/3/23(C) 2020, Akihiko Koga

88

型付λ計算と CCC の対応• ここでは，単純型付λ計算にデカルト閉圏（CCC） C で意味をつける方
法を説明する．意味づけにあたっては次のような対応をとる
型付λ計算

圏（CCC）型（type）

オブジェクト文脈（context）

オブジェクト（積オブジェクト）

文脈付きλ式項（λ-term）

射

デカルト閉圏 C・文脈〚Γ〛・文脈付きλ式・型(=〚τ1〛×...×〚τn〛for Γ=x1:τ1, ..., xn:τn)〚Γ⊢t:τ〛〚τ〛

2020/3/23〚XXX〛は XXX を C の中で意味づけしたものを表すとする(C) 2020, Akihiko Koga

89

単純型付きλ計算の CCC による解釈• 解釈のルール
オブジェクトとなるもの

型付きλ計算n 型（Type）

Ø 基本型 T には予め C のオブジェクト〚T〛が割り当てられているとするØ 〚τ→σ〛=〚τ〛→〚σ〛Ø 〚τ×σ〛=〚τ〛×〚σ〛Ø 〚*〛=1Cn 文脈（Context）

Ø 〚x1:τ1, ..., xn:τn〛=〚τ1〛× ... ×〚τn〛

2020/3/23*
BasicTypes
T

デカルト閉圏 C
1C
〚T〛
...

...

τ→σ
τ×σ
x1:τ1, ..., xn:τn(C) 2020, Akihiko Koga

〚τ〛→〚σ〛〚τ〛×〚σ〛〚τ1〛× ... ×〚τn〛90

単純型付きλ計算の CCC による解釈
射になるものn 文脈付きλ式（Context ⊢ Term）〚Γ⊢t : τ〛は次のように射〚Γ〛→〚τ〛に割り当てられる
Ø 定数〚Γ ⊢ c:τ〛=〚c〛

〚Γ〛

!

1C

Ø 変数〚x1:τ1, ..., xn:τn ⊢ xi:τi〛=πi〚τ1〛×...×〚τn〛

〚c〛
πi

〚τ〛

予め定数 c に割り当てられている射〚τi〛Ø fst 〚Γ⊢(fst s) : τ〛=π1・〚Γ⊢s : τ×σ〛〚Γ⊢s : τ×σ〛〚Γ〛〚τ〛×〚σ〛π1〚τ〛π1・〚Γ⊢s : τ×σ〛

Ø snd 〚Γ⊢(snd s) : σ〛=π2・〚Γ⊢s : τ×σ〛
上と同様

2020/3/23(C) 2020, Akihiko Koga

91

単純型付きλ計算の CCC による解釈
Ø ペアを作る関数〚Γ⊢<s, t>:τ×σ〛=<〚Γ⊢s:τ〛, Γ⊢t:σ〛>〚Γ⊢s:τ〛∃!

〚Γ〛<〚Γ⊢s:τ〛, Γ⊢t:σ〛>〚τ〛
π1〚τ〛×〚σ〛π2〚Γ⊢t:σ〛〚σ〛注意）積オブジェクトを，前頁に合わせて横向きに書いていることに注意

2020/3/23(C) 2020, Akihiko Koga

92

[重要] 単純型付きλ計算の CCC による解釈
Ø λ抽象化〚Γ⊢λx:τ.t : (τ→σ)〛=〚Γ, x:τ ⊢ t:σ〛♭Ø 文脈 Γに宣言 x:τ を加えて，t:σ が導かれていたなら，下の図式のような〚Γ〛→(〚τ〛→〚σ〛）が一意に存在する

× 〚τ〛

〚Γ〛

∃!

〚Γ, x:τ ⊢ t:σ〛〚Γ, x:τ ⊢ t:σ〛♭

1〚σ〛

1〚τ〛
eval

〚τ〛→〚σ〛 × 〚τ〛

〚σ〛

〚σ〛

Ø λ式の関数適用〚Γ⊢(t s):σ〛= eval・<〚Γ⊢t:(τ→σ)〛, 〚Γ⊢s:τ 〛><〚Γ⊢t:(τ→σ)〛, 〚Γ⊢s:τ 〛>〚Γ〛〚Γ⊢t:(τ→σ)〛〚τ〛→〚σ〛 ×2020/3/23〚Γ⊢s:τ 〛〚τ〛(C) 2020, Akihiko Koga

eval

〚σ〛
93

単純型付きλ計算の項モデル• 単純型付きλ計算 T から項モデルと呼ばれるデカルト閉圏 C(T) を次のようにして構成できるn C(T) のオブジェクト
Ø すべての文脈

n C(T) の射

Ø Δ→Γ=x1:T1, ..., xn:Tn は <[t1], ..., [tn]>Ø ここでΔ⊢ti:Ti for i = 1, ..., nØ [ti] はΔ⊢ti=t'i : Ti が証明できる項を１つにまとめた同値類とする
Ø 射の合成ΘσΔ

τ=<[t1], ..., [tn]>Γ

σ・τ=<[t1[σ]], ..., [tn[σ]]>代入
2020/3/23(C) 2020, Akihiko Koga

94

単純型付きλ計算の項モデル• 項モデル C(T) はデカルト閉圏になる

n Γ×Δ は二つの文脈を並べたもの Γ, Δn Γ→Δ は Γ=x1:T1, ..., xn:Tn, Δ=y1:S1, ..., ym:Sm としたとき
Ø Γ→Δ=f1:S1Γ, ..., fm:SmΓ
ここで fi:SiΓ=T1→...→Tn→SiØ eval : (Γ→Δ)×Γ → Δ はeval = <f1(x1)...(xn), ..., fm(x1)...(xn)>n 終対象は空の文脈 ∅• C(T) ではn Γ⊢t=t':T ⇔ [Γ⊢t]=[Γ⊢t']• したがって，単純型付きλ計算については次の完全性定理が成り立つ• 定理 （完全性定理）

Γ ⊢ t=t':T ⇔ [Γ⊢t] = [Γ⊢t'] がすべてのデカルト閉圏のモデルで成り立つ

2020/3/23(C) 2020, Akihiko Koga

95

計算機屋さんにとっての成果• 以上でデカルト閉圏が単純型付きλ計算のモデルになることが分かったが，この事実は計算機屋さんにとって何か良いことがあるのだろうか？
• あまり，「こんなに素晴らしいことがある」と言うものは思いつかないが，
なんとなく良いと思うことを上げていってみよう
n 一応，意味を定めることができる理論的な領域（デカルト閉圏）を得たので心の平安が得られたn 同じことだが，プログラミング言語の意味を原理的には CCC で定めることができるようになった
n λ式について t ≠s は，一つでもこのような CCC があれば良いのだから楽に示せる場合はあるn すべての CCC モデルで統合が成立すれば，単純型付きλ計算でも統合が成立するので等式を証明する道具は１つ増えた
n CCC は D→D を D に埋め込めるような領域の作成に役にたつ．．．

まあ，自分で色々やってみたり，論文をサーベイしていけば色々な良いことが見えてくるのかもしれない．
2020/3/23(C) 2020, Akihiko Koga

96

Excuse!
• 以上でデカルト閉圏が単純型付きλ計算のモデルになる話を終わる• しかし，実は，ここの話は「関手 F : GraphSyntax→Set がグラフのモデルを与える」とか，「一般に，関手 F : C → D が C のモデルを与える」という前振りからは，次の２点でずれてきている
n デカルト閉圏は圏であるが，単純型付きλ計算は圏ととらえていないのでモデルの付与は関手を使っていない
n 単純型付きλ計算側も項モデルやそれより緩い（等しいことが証明できる式すべてを必ずしも同一視しない）モデルにより圏にすることができるが，その場合のF : λ計算の圏→デカルト閉圏 では，「λ計算の圏」は，GraphSyntax のようにλ計算の文法を与えている訳ではない
Ø GraphSyntax と同じノリなら，その圏は，変数，定数，文脈，．．．のオブジェクトで構成されるハズである• うまく話を進めれば繋がるようにできるのかもしれないが，この資料の最初の版ではここで時間と力が尽きたので，このままにしておく• 次の版で修正するかもしれない
2020/3/23(C) 2020, Akihiko Koga

97

この資料で学習したことと今後の学習のアドバイス• 圏論の基礎的な概念（定義，関手，積，冪，デカルト閉圏）を学んだ• この範囲で圏論の応用を感じるトピックスとして次のものに触れた
n 代数と余代数によるプログラミング言語の型の扱い
Ø 代数
Ø 自然数や有限リストなどを表現することができる
Ø 始対象の意味論で帰納法による定義と証明が可能
Ø 余代数
Ø 無限リストや状態遷移マシンを表現することができる
Ø 終対象の意味論で余帰納法による定義と証明が可能

n 単純型付きλ計算のモデルとデカルト閉圏の同等性• これらのことを踏まえて学習することで，どこまで我慢すればどのような応用に触れられるかが分かり，学習の計画が立てやすくなると思う• 今後，独力で圏論を学習するためには，極限・余極限，自然変換，随伴関手を深く理解することが学習成功のカギとなる
2020/3/23(C) 2020, Akihiko Koga

98

さらなる学習に向けて

2020/3/23(C) 2020, Akihiko Koga

99

圏論のいろいろなトピック• 圏論の基礎部分 ．．． まずは一冊やってみる
通常の圏論の基礎的なテキストに載っているトピックスを上げておく．この資料ではこのなかのごく一部（関手，積，冪）について，概念のイメージを添え，応用に関連させて説明した
Ø 関手
Ø 極限と余極限
Ø 冪オブジェクトとデカルト閉圏
Ø 自然変換Ø 米田のレンマØ 随伴関手Ø モナド
Ø トポス

途中で挫折しないためには，特に・極限，余極限・自然変換・随伴関手を十分すぎるくらいしっかり学習することが重要• 論文などでの応用のサーベイ
多少分からないところがあっても応用的な論文を読んでみるのが良いと思う• 発展的なトピックス
圏に演算を入れたり，高階の圏を考えるなど，圏の色々な拡張がある
モノイダル圏，高階の圏，豊穣圏，．．．

2020/3/23(C) 2020, Akihiko Koga

100

参考文献
計算機科学向きの圏論のテキスト• S. Awodey : Category Theory, 2005～

n 計算機科学など，マクレーンの Category Theory for Working
Mathematicians が想定しているほどの数学的知識を持たない学習者に対するテキストと著者は言っている．単純型付きλ計算や論理学の例などがたくさん載っており，私は結構，興味深いテキストだと思う
n 私はあまり数学が（英語も）得意ではないので，何回か，最初から読み直した．数
回目にこんなことが書いてあったのかと思ったこともあるので，理解の深度が深まった時点で例題などを読み返しても良いと思う
n 英語で読むのが味わい深くて良いのではないかと思う• M. Barr and C. Wells : Category Theory for Computing
Science, 1998, 558ページ
n タイトルからして計算機科学の学習者向けのテキストである．すでに廃版になっているが，著者らによってPDF の形で公開されている．分厚いが，計算機科学のトピックスがたくさん載っており，あまりしり込みしないで読むのが良いように思う
n 「モナド」は古い用語の「triple」を使っているが，歴史的経緯を知るには良いのかもしれない
2020/3/23(C) 2020, Akihiko Koga

101

参考文献
圏論一般
• Tom Leinster : Basic Category Theory, 2014

n 計算機科学に関するテキストではないが，短く，簡単に，かつ，直感的な理解を助ける文言が散りばめられているので，最初にざっと読んで，学習すべき概念を頭に入れてから，他のテキストにあたるのも良いかもしれない
n 随伴関手（Adjoints）が最初の方に説明されている．著者の考えでは，圏論において随伴関手はとても重要であり，また，それほど難しい概念でもないので，学習の早い時期から，この恩恵にあずかるのが良いのではないかとのこと
n 少し古い arxiv 版は無料で読める
n 第３章の “Interlude on sets” は集合論に関する話題なのだが，これは，F.W.
Lawvere による集合論を圏論的に記述するという話もかなり含んでいる• Emily Riehl : Category Theory in Context, 2014, xvii
+ 240 pages
n 良いテキストだと思う．著者本人は簡単な集合論が分かれば分かるだろうと言っているが，私は少し難しめと思う．
n これも arxiv 版があり，そちらは無料で読める
2020/3/23(C) 2020, Akihiko Koga

102

参考文献
プログラミング言語のデータ型と代数/余代数• B. Jacobs , J. Rutten : A Tutorial on (Co)Algebras and (Co)Induction, 1997,
38 pagesn 集合の圏を使って具体的に代数，余代数を利用したデータ型への圏論の応用を紹介している．
n それらのデータ型での証明方法として，（余）帰納法があることが説明されている• B. Pierce : A Taste of Category Theory for Computer Scientists, 1988, 75
pages
n 計算機科学者に向けた短い圏論のチュートリアルn ３部構成になっていて，第２部で当時の計算機科学での応用例が書かれている．
最初の例が，次に述べる萩野氏のカテゴリカルプログラミングに関する短い紹介になっている• 萩野達也：カテゴリー理論的関数型プログラミング言語，1990年1月

n Dialgebra（di- は，両，二の意）や随伴関手を利用したプログラミング言語の提案．
ほとんど何も仮定しないレベルから，それらの圏論の原理を使ってデータ型，デー
タ型の構築子，プログラムの構築を可能にしている
2020/3/23(C) 2020, Akihiko Koga

103

参考文献
（単純型付き）λ計算とCCCについて• （単純型付き）λ計算

n R. Loader : Notes on Simply Typed Lambda Calculus, 1998
n A. Jung : A short introducion to the Lambda Calculus, 2004
n Wikipedia : Simply typed lambda calculus• 単純型付きλ計算とCCC

n S. Awodey : Category Theory, 2005 の第６章 Exponentials
n M. Barr and C. Wells : Category Theory for Computing Science,
1998 の第６章 Cartesian Closed Categories
n J. L. Bell : The Development of Categorical Logic, 2005 の第４章
Cartesian Closed Categories and the λ-Calculusn その他，多くのレクチャーノート
Ø 単純型付きλ計算とCCC については，インターネット上で検索をかけてみると，大学の授業のレクチャーノートが PDF で見つかる．それらの著者の公開の意思が明確ではないので，ここで個別に URL は書かないが，調べてみるとコンパクトで分かりやすい
教材に出会えることがある
2020/3/23(C) 2020, Akihiko Koga

104