-
Notifications
You must be signed in to change notification settings - Fork 4
/
10.html
704 lines (623 loc) · 28 KB
/
10.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
<!doctype html>
<html lang="ja">
<head>
<meta charset="utf-8">
<title>圏論勉強会 第10回 @ ワークスアプリケーションズ</title>
<meta name="description" content="Seminar of category theory">
<meta name="author" content="Koichi Nakamura">
<meta name="apple-mobile-web-app-capable" content="yes" />
<meta name="apple-mobile-web-app-status-bar-style" content="black-translucent" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1.0, user-scalable=no">
<link rel="stylesheet" href="css/reveal.css">
<link rel="stylesheet" href="css/theme/sky.css" id="theme">
<meta http-equiv="X-UA-Compatible" CONTENT="IE=EmulateIE7" />
<!-- For syntax highlighting -->
<link rel="stylesheet" href="plugin/highlight/styles/github.css">
<!-- If the query includes 'print-pdf', use the PDF print sheet -->
<script>
document.write( '<link rel="stylesheet" href="css/print/' + ( window.location.search.match( /print-pdf/gi ) ? 'pdf' : 'paper' ) + '.css" type="text/css" media="print">' );
</script>
<script type="text/javascript" async
src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js?config=TeX-AMS_HTML">
</script>
<script type="text/x-mathjax-config">
MathJax.Hub.Config({
tex2jax: {
inlineMath: [ ['$','$'], ["\\(","\\)"] ],
displayMath: [ ['$$','$$'], ["\\[","\\]"] ]
}
});
</script>
<style type="text/css">
<!--
div.definition {
padding-top: 10px;
padding-bottom: 10px;
padding-left: 10px;
padding-right: 10px;
border: 4px solid #333333;
box-shadow: 0 0 10px rgba(0, 0, 0, 0.15);
}
div.theorem {
padding-top: 10px;
padding-bottom: 10px;
padding-left: 10px;
padding-right: 10px;
border: 4px solid #333333;
box-shadow: 0 0 10px rgba(0, 0, 0, 0.15);
}
div.equation {
margin: 10px;
padding-top: 10px;
padding-bottom: 10px;
padding-left: 10px;
padding-right: 10px;
border: 2px solid #C0C0C0;
}
div.example {
margin: 10px;
padding-top: 10px;
padding-bottom: 10px;
padding-left: 10px;
padding-right: 10px;
border: 2px solid #C0C0C0;
}
-->
</style>
<!--[if lt IE 9]>
<script src="lib/js/html5shiv.js"></script>
<![endif]-->
</head>
<body>
<div class="reveal">
<!-- Any section element inside of this container is displayed as a slide -->
<div class="slides">
<section>
<h1>圏論勉強会<br>第10回</h1>
<h3>@ワークスアプリケーションズ</h3>
<small> 中村晃一 <br> 2013年7月18日</small>
</section>
<section>
<h3>謝辞</h3>
<p>
この勉強会の企画,会場設備の提供をして頂きました<br>
㈱ ワークスアプリケーションズ様<br>
にこの場をお借りして御礼申し上げます。
</p>
</section>
<section>
<h3> この会について </h3>
<ul>
<li> <span style="color:red">圏論(category theory)</span>を題材にいろんなことを学びます。</li>
<li> 分かり易さを重視して初歩的な例を多用します。</li>
<li> 関数型言語の経験がある方がより楽しめると思います。資料中では主にHaskellを使います。 </li>
<li> 中高生も数人見ているらしいのでプログラミングと関係が浅い内容も取り上げます。</li>
<li> この資料は<a href="http://nineties.github.com/category-seminar/">http://nineties.github.com/category-seminar</a>に置いてあります。</li>
</ul>
</section>
<section>
<h2> 第10回 </h2>
<h3> 始代数・終余代数と不動点,型函手 </h3>
</section>
<section>
$$ \newcommand\banana[1]{{(\hspace{-.2em}|#1|\hspace{-.2em})}} $$
</section>
<section>
<h3> 第10回の内容 </h3>
<p>
第7・8回に紹介した<span style="color:red">始代数・終余代数</span>と前回紹介した<span style="color:red">不動点意味論</span>の関連について説明します。データ型と関係の深い函手である,型函手というものの紹介をします。
</p>
</section>
<section>
<h3> 始代数・終余代数と不動点 </h3>
</section>
<section>
<h3> 復習: Lambekの補題 </h3>
<div class="theorem">
<p>
$(T,\mathrm{in})$が$F$始代数ならば$\mathrm{in}$は同型射、すなわち
$$ \color{red}{T \cong F(T)} $$
である。
</p>
<div align="center"> <img width="40%" src="fig/lambek_lemma2.png"> </div>
</div>
<p class="fragment">
これは<span style="color:red">対象$T$が自己函手$F$の不動点</span>であるという事を表します。
双対性により,終余代数についても同じ事が言えます。
</p>
</section>
<section>
<h3> 始代数・終余代数は不動点 </h3>
<div class="theorem">
<p>
圏$\mathbf{C}$,自己函手$F:\mathbf{C}\rightarrow\mathbf{C}$について、
<ul>
<li> $F$始代数が存在するならば、それは$F$の不動点である。</li>
<li> $F$終余代数が存在するならば、それは$F$の不動点である。</li>
</ul>
</p>
</div>
</section>
<section>
<p>
以後,$F$始代数と終余代数を区別する為に,始代数を<span style="color:red">$\mu F$</span>,終余代数を<span style="color:red">$\nu F$</span>と表します。
</p>
<div align="center"> <img width="90%" src="fig/muF_nuF.png"> </div>
</section>
<section>
<h3> 簡単な応用 </h3>
<p>
<span style="color:red">函手$F$に不動点が存在しなければ始代数も終余代数も存在しない</span>という事が言えます。
</p>
<div class="fragment">
<p>
有名な例は冪集合函手$\mathcal{P}: \mathbf{Sets}\rightarrow \mathbf{Sets}$です。これは
</p>
<ul>
<li> 集合$X$を冪集合$\mathcal{P}(X)$に移す。</li>
<li> 関数$f: X\rightarrow Y$を$\mathcal{P}(f): \mathcal{P}(X) \ni A \longmapsto f(A) \in \mathcal{P}(Y)$に移す。</li>
</ul>
<p>
という函手ですが、カントールの定理(第5回)より任意の集合$A$に対して
$$ A \not\cong \mathcal{P}(A) $$
なので,$\mu\mathcal{P}$も$\nu\mathcal{P}$も存在しません。
</p>
</div>
</section>
<section>
<h3> 復習: 連続関数$F$の最小不動点 </h3>
<p>
cpo D上の連続関数$F:D\rightarrow D$の最小不動点は
$$ \bot \leqq F(\bot) \leqq F^2(\bot) \leqq F^3(\bot) \leqq $$
という$\omega$-chainの余極限
$$ \lim_{\stackrel{\longrightarrow}{i \in\omega}}F^i(\bot) $$
として具体的に構成出来るのでした。
</p>
</section>
<section>
<h3> 始代数は最小不動点 </h3>
<p>
「cpo上の連続関数の最小不動点の構成方法」を一般化する事で(圏と$F$が良い性質を持つ場合には)$F$始代数の具体的な構成を与える事が出来ます。
<p>
<p class="fragment">
この意味で$F$始代数$\mu F$は<span style="color:red">$F$の最小不動点(least fixedpoint)</span>と呼ばれます。
</p>
</section>
<section>
<h3> initial $\omega$-chain </h3>
<p>
$\mathbf{C}$が始対象$0$をもつ場合,任意の自己函手$F:\mathbf{C}\rightarrow\mathbf{C}$に対して
$$ !: 0 \rightarrow F(0) $$
という射が<span style="color:red">唯一</span>に定まります。さらに$F$によって移すと
$$ F(!): F(0)\rightarrow F^2(0) $$
という射になります。
</p>
<p>
これを繰り返して出来る列を$F$の<span style="color:red">initial $\omega$-chain</span>と呼びます。
</p>
<div align="center"> <img width="100%" src="fig/initial_omega_chain.png"> </div>
</section>
<section>
<h3> initial $\omega$-chainの例1 </h3>
<p>
cpoの始対象は最小値$\bot$であり,射は順序$\leqq$ですから,任意の自己函手$F$について
$$ \bot \leqq F(\bot) \leqq F^2(\bot) \leqq F^3(\bot) \leqq $$
がinitial $\omega$-chainです。
</p>
</section>
<section>
<h3> initial $\omega$-chainの例2 </h3>
<p>
圏を$\mathbf{Sets}$,函手を$F(X) = X + 1$とした場合を考えます。
</p>
<div class="fragment">
<p>
$\mathbf{Sets}$において始対象$0$は空集合,終対象$1$は一点集合,余積$A+B$は$A$,$B$の直和でしたので,<span style="color:red">$F^i(0)$は要素数が$i$の集合</span>となります。<span style="font-size:60%">($0 + 1 \cong 1$, $(A+B)+C\cong A+B+C$に注意。)</span>
</p>
<div align="center"> <img width="90%" src="fig/initial_omega_chain2.png"> </div>
</div>
</section>
<section>
<h3> initial $\omega$-chainの例2 </h3>
<p>
また,$!$は空関数でした。さらに$f: X\rightarrow Y$に対して$F(f): X + 1 \rightarrow Y + 1$は
$$ F(f) = f + 1_1 $$
と定義されるので,$F^i(!)$の様子は下図の様になります。
</p>
<div align="center"> <img width="90%" src="fig/initial_omega_chain3.png"> </div>
</section>
<section>
<h3> 定理 </h3>
<div class="theorem">
<p>
圏$\mathbf{C}$が始対象を持つ$\omega$余完備な圏であるとする。自己函手$F: \mathbf{C}\rightarrow\mathbf{C}$が$\omega$余連続ならば,$F$始代数が存在し
$$ \mu F = \lim_{\stackrel{\longrightarrow}{i \in \omega}} F^i(0) $$
である。
</p>
</div>
<p style="font-size:80%">
注:「$\omega$余完備」の条件は「$F$のinitial $\omega$-chainの余極限が存在」、
「$\omega$余連続」の条件は「$F$のinitial $\omega$-chainの余極限を保つ」と弱めても良いです。
</p>
</section>
<section>
<p style="font-size:80%">
$\displaystyle \mu F = \lim_{\stackrel{\longrightarrow}{i \in \omega}}F^i(0) $ とおいて,これが始代数である事を示します。
</p>
<p style="font-size:80%">
【証明】<br>
$F$が$\omega$余連続であることより,
$$ F(\mu F) = F(\lim_{\rightarrow}F^i(0)) \cong \lim_{\rightarrow}F^{i+1}(0) = \mu F\quad \cdots (1)$$
である。
ここで,$F$のinitial $\omega$-chainの余極限の錐を$(\mu F, q_i)$とおく。すると,$(F(\mu F), F(q_{i-1}))$(但し$0$から$F(\mu F)$の射は$!$)もinitial $\omega$-chainを底とする錐となるが,$(1)$よりこれも余極限の錐である。
</p>
<div align="center"> <img width="90%" src="fig/initial_algebra_is_least_fixedpoint3.png"> </div>
</section>
<section>
<p style="font-size:80%">
従って$(F(\mu F), F(q_{i-1}))$から$(\mu F, q_i)$への射が唯一つ存在するので,これを$\mathrm{in}$と呼ぶ事にする。すなわち,$\mathrm{in}$は任意の$i \in \omega$に対して
$$ q_{i+1} = \mathrm{in}\circ F(q_i) \quad\cdots (2)$$
を満たす。この$(\mu F, \mathrm{in})$の組が$F$始代数となる事を示せば良い。<br>
</p>
<div align="center"><img width="60%" src="fig/initial_algebra_is_least_fixedpoint4.png"> </div>
</section>
<section>
<p style="font-size:80%">
ここで,$F$代数$x: F(X)\rightarrow X$を任意に取ると
$$ (X, x\circ F(x)\circ \cdots\circ F^{i-1}(x)\circ F^i(!_X)) $$
がinitial $\omega$-chainを底とする錐をなす。これを$(X, x_i)$と置くと
$x_0 = !_X$であり,
$$ \begin{aligned}
x_{i+1} &= x\circ F(x)\circ \cdots\circ F^i(x)\circ F^{i+1}(!_X) \\
&= x\circ F(x\circ \cdots F^{i-1}(x)\circ F^i(!_X)) \\
&= x\circ F(x_i) \quad \cdots (3)
\end{aligned} $$
が成り立つ。
</p>
<div align="center"><img width="90%" src="fig/initial_algebra_is_least_fixedpoint5.png"> </div>
</section>
<section>
<p style="font-size:80%">
従って$(X,x_i)$が錐であることより,錐$(\mu F,q_i)$への射$u$,すなわち
$$ u\circ q_i = x_i \quad\cdots (4) $$
が任意の$i \in \omega$について成立するような$u: \mu F\rightarrow X$が唯一つ存在する。
</p>
<div align="center"><img width="60%" src="fig/initial_algebra_is_least_fixedpoint6.png"> </div>
<p style="font-size:80%">
<img align="right" width="30%" src="fig/initial_algebra_is_least_fixedpoint7.png">
すると右図の様な四角形が出来るが,これが可換である事つまり
$$ u\circ\mathrm{in} = x\circ F(u)$$
とこれを満たす$u$が他には存在しない事を示せば$(\mu F, \mathrm{in})$が始代数となる事の証明が完了する。
</p>
</section>
<section>
<p style="font-size:80%">
まず$(3),(4)$より
$$ x\circ F(u) \circ F(q_{i-1}) = x\circ F(u\circ q_{i-1}) = x\circ F(x_{i-1}) = x_i$$
が成り立つ。また$(2),(4)$より
$$ u\circ\mathrm{in}\circ F(q_{i-1}) = u\circ q_i = x_i $$
も成り立つ。すると下図の様に,$u\circ\mathrm{in}$と$x\circ F(u)$は錐$(F(\mu F),F(q_{i-1}))$から錐$(X,x_i)$への射となるが$(F(\mu F),F(q_{i-1}))$も極限錐であることより,そのような射は唯一に定まる。すなわち
$$ u\circ\mathrm{in} = x\circ F(u)$$
が成り立つ。
<div align="center"><img width="60%" src="fig/initial_algebra_is_least_fixedpoint8.png"> </div>
</p>
</section>
<section>
<p style="font-size:80%">
一方
$$ v\circ\mathrm{in} = x\circ F(v)$$
を満たす$v: \mu F \rightarrow X$が存在すると仮定すると,両辺に$F(q_i)$を掛けて$(2)$を用いる事により
$$ v\circ q_{i+1} = x\circ F(v)\circ F(q_i) = x\circ F(v\circ q_i) $$
となる。するともし$v\circ q_i = x_i$であるならば$(3)$により
$$ v\circ q_{i+1} = x\circ F(x_i) = x_{i+1} $$
となる。ここで,$q_0$,$x_0$が共に始対象からの射であることより$ v\circ q_0 = x_0 $
であるから,帰納的に任意の$i\in\omega $に対して
$$ v\circ q_i = x_i$$
が成り立つ。ところで$(4)$が任意の$i\in\omega$について成り立つ$u$は唯一に定まるのであったから,
$ u = v $
である。以上より任意の$x:F(X)\rightarrow X$に対して
$$ u\circ\mathrm{in} = x\circ F(u)$$
を満たす$u$が一意に定まる事が示されたので$(\mu F, \mathrm{in})$は始代数である。<span style="float:right">□</span>
</section>
<section>
<h3> 終余代数は最大不動点 </h3>
<div class="theorem">
<p>
圏$\mathbf{C}$が終対象を持つ$\omega^{\mathrm{op}}$完備な圏であるとする。自己函手$F:\mathbf{C}\rightarrow\mathbf{C}$が$\omega^{\mathrm{op}}$連続ならば,$F$終余代数が存在し
$$ \nu F = \lim_{\stackrel{\longleftarrow}{i \in \omega}} F^i(1) $$
</p>
</div>
<p>
始代数の双対が終余代数ですので、自動的にこの定理を得ます。
つまり,以下の$\omega^{\mathrm{op}}$-chainの極限が終余代数となります。
</p>
<div align="center"> <img width="80%" src="fig/terminal_omegaop_chain.png"> </div>
</section>
<section>
<h3> 何が嬉しいのか? </h3>
<p>
前回の不動点意味論の所でも説明しましたが,ある概念の「具体的な構成方法を得る」事が出来ると
</p>
<ul>
<li> その概念の理解が深まる(特に直観的な理解を得られる)。</li>
<li> その構成方法に基づく証明が可能になる。 </li>
</ul>
<p>
などの有り難みがあります。
</p>
</section>
<section>
<h3> Haskellでの実装例 </h3>
<pre><code data-trim class="haskell" contenteditable>{-# LANGUAGE DeriveFunctor, TypeSynonymInstances, FlexibleInstances #-}
import Prelude hiding (succ,sum)
-- Haskellでは、以下のFixを使うと「函手fの最小不動点」を得る事が出来ます。
-- また、Haskellでは最小不動点と最大不動点は(細い事を気にしなければ)一致します。
-- 結局始代数・終余代数は全て以下のFixで作る事が出来ます。
--
-- 以下の定義は Fix f = f (Fix f) という不動点の等式に対応します。
newtype Fix f = In { out :: f (Fix f) }
-- F始代数の定義より
-- u . in = phi . F(u)
-- を満たすuはphiに対して一意に定まります。これにinの逆射を右から掛けると
-- u = phi . F(u) . in^(-1)
-- となるので,u = cata phiとしてそのままコードにすると以下のような汎用的な
-- 関数を得ます。
cata :: Functor f => (f a -> a) -> Fix f -> a
cata phi = phi . fmap (cata phi) . out
-- 同様に
-- out . u = F(u) . psi
-- を満たすuがpsiに対応するanamorphismなので、
-- 以下のコードを得ます。
ana :: Functor f => (a -> f a) -> a -> Fix f
ana psi = In . fmap (ana psi) . psi
-- ## 自然数 ##
-- NatF(X) = 1 + X
data NatF x = Zero | Succ x
deriving (Show,Functor)
-- その不動点が自然数型。
type Nat = Fix NatF
-- 補助関数
zero :: Nat
zero = In Zero
succ :: Nat -> Nat
succ n = In (Succ n)
instance Show Nat where
show x = show (cata phi x) -- 組み込み整数に変換して表示
where
phi Zero = 0
phi (Succ x) = x + 1
-- foldの例。
-- > sqrt2 (succ (succ (succ zero)))
-- 1.4142156862745097
sqrt2 = cata phi
where
phi Zero = 2
phi (Succ x) = (x+2/x)/2
-- unfoldの例。
-- > ilog2 12348712
-- 3
ilog2 = ana psi
where
psi x = if x `mod` 2 == 1 then Zero else Succ (x `div` 2)
-- ## リスト ##
-- ListF(X) = 1 + A*X という函手。
data ListF a x = Nil | Cons a x
deriving (Show,Functor)
-- その不動点がリスト型。
type List a = Fix (ListF a)
-- 補助関数
nil :: List a
nil = In Nil
cons :: a -> List a -> List a
cons a as = In (Cons a as)
instance Show a => Show (List a) where
show x = show (cata phi x) -- 組み込みリストに変換して表示
where
phi Nil = []
phi (Cons a x) = a:x
-- foldの例。
sum = cata phi
where
phi Nil = 0
phi (Cons a x) = a + x
-- unfoldの例。
-- > natFrom 10
-- [10,11,12,13,14,15,....
natFrom = ana psi
where
psi n = Cons n (n+1)
</code></pre>
</section>
<section>
<p>
前回紹介した以下のpdfに様々な例も含めて非常に詳しく解説がありますので、是非参照して下さい。
</p>
<ul>
<li>
<a style="font-size:80%" href="https://www.tu-braunschweig.de/Medien-DB/iti/survey_full.pdf">Jiri Adamek他"Initial algebras and terminal coalgebras: a survey" </a></li>
</li>
</ul>
</section>
<section>
<h3> 型函手 </h3>
</section>
<section>
<h3> 型函手とは? </h3>
<p>
データ型に関係する概念として「型函手」というものがあります。
</p>
<div class="fragment">
<p>
例えば,
</p>
<ul>
<li> 型$A$をリスト型$[A]$ </li>
<li> 関数$f$を$\mathrm{map}\ f$ </li>
</ul>
<p>
に対応させる事は函手となりますが,これが<span style="color:red">型函手(type functor)</span>の例です。
</p>
</div>
</section>
<section>
<p>
型函手はcatamorphismに基づいて定義する事が可能ですので、今回はその方法とそこから導出されるプログラム運算の規則に紹介をします。
</p>
</section>
<section>
<p>
積圏$\mathbf{D}\times\mathbf{C}$から$\mathbf{C}$への函手
$$ F: \mathbf{D}\times\mathbf{C}\rightarrow\mathbf{C} $$
が型函手の材料となります。ドメインが積圏である函手を<span style="color:red">双函手(bifunctor)</span>などと言います。
</p>
<div class="fragment">
<p>
例えば
$$ F(X, Y) = 1 + X\times Y$$
などが双函手の例です。これは以下のような函手です。
</p>
<ul>
<li> 対象$(X,Y)$を対象$1 + X\times Y$に移す。</li>
<li> 射$(f,g)$を射$1 + f\times g$に移す。</li>
</ul>
</div>
</section>
<section>
<p>
双函手$F: \mathbf{D}\times\mathbf{C}\rightarrow\mathbf{C} $の<span style="color:red">第一引数を対象$A$に固定</span>すると$\mathbf{C}$上の自己函手が出来ます。これを
$$ F_A: \mathbf{C} \rightarrow \mathbf {C}$$
と表す事にします。
</p>
<p class="fragment">
例えば,$F(X,Y) = 1 + X\times Y$とした場合
$$ F_A(X) = 1 + A\times X $$
という自己函手が得られます。すると「$F_A$の始代数$=$$A$型のリスト」のリストとなります。
</p>
</section>
<section>
<h3> 型函手 </h3>
<div class="definition">
<p>
双函手$F:\mathbf{D}\times\mathbf{C}\rightarrow\mathbf{C}$を,任意の$\mathbf{D}$の対象$A$に対して$F_A$の始代数$(T_A,\mathrm{in}_A)$が存在するものとする。
</p>
<p>
この時,以下の対応$T$は函手$\mathbf{D}\rightarrow\mathbf{C}$となり,これを$F$から導出される<span style="color:red">型函手(type functor)</span>と言う。
</p>
<ul>
<li> 対象$A$を対象$T_A$に移す。 </li>
<li> 射$f:A\rightarrow B$を$T(f) = \banana{\mathrm{in}_B\circ F(f,1_B)}$に移す。 </li>
</ul>
</div>
<div align="center"> <img width="70%" src="fig/type_functor.png"> </div>
</section>
<section>
<h3> 例 </h3>
<div style="font-size:80%">
<p> $T(f) = \banana{\mathrm{in}_B\circ F(f,1_B)}$の部分がよく解らないと思うので具体例を見てみます。</p>
<p class="fragment">
$$ F(A,X) = 1 + A\times X $$
と置くと,$T_A$は$A$型のリストに相当します。すると
$$ T(f) = \banana{\mathrm{in}\circ F(f,1)} = \banana{[\mathrm{nil},\mathrm{cons}]\circ (1 + f\times 1)} = \banana{[\mathrm{nil},\mathrm{cons}\circ (f\times 1)]}$$
すなわち,$T(f) = \mathrm{foldr}\ \mathrm{nil}\ (\mathrm{cons}\circ (f\times 1))$となります。これが$\mathrm{map}\ f$と等しくなる事を確認しましょう。
</p>
</div>
</section>
<section>
<h3> 復習: catamorphismの反射則,融合則 </h3>
<p style="font-size:80%">
catamorphismは始対象からの射ですので,今の法則がそのまま成り立ちます。
<div class="theorem">
<p>
$(T,\mathrm{in})$が$F$始代数ならば
$$ \banana{\mathrm{in}} = 1_T \quad\text{(反射則)}$$
また$h\circ f=g\circ F(h)$が成り立つならば
$$h\circ\banana{f}=\banana{g} \quad\text{(融合則)}$$
</p>
</div>
<div align="center"> <img width="70%" src="fig/cata_reflection_fusion.png"> </div>
</section>
<section>
<h3> 型函手の融合則 </h3>
<p> $T$が函手である事を示す前に,以下の法則を確認します。</p>
<div class="theorem">
$$ \banana{f}\circ T(g) = \banana{f\circ F(g,1)} $$
</div>
<p style="font-size:70%">
[証明]<br>
双函手であることより$ f\circ F(g,\banana{f}) = f\circ F(g,\banana{f}) $を変形して
$$ f\circ F(1,\banana{f})\circ F(g,1) = f\circ F(g,1)\circ F(1,\banana{f}) $$
を得る。するとcatamorphismの定義より
$$ \banana{f}\circ\mathrm{in}\circ F(g,1) = f\circ F(g,1)\circ F(1,\banana{f}) $$
となる。これにcatamorphismの融合則を用いて
$$ \banana{f}\circ\banana{\mathrm{in}\circ F(g,1)} = \banana{f\circ F(g,1)} $$
すなわち
$$ \banana{f}\circ T(g) = \banana{f\circ F(g,1)} $$
となる。<span style="float:right">□</span>
</p>
</section>
<section>
<h3> 函手である事の証明 </h3>
<p style="font-size:80%">
【恒等射を保つ事】<br>
$ F(1,1) $は積圏の恒等射なので反射則より,$$T(1_A) = \banana{\mathrm{in}\circ 1} = \banana{\mathrm{in}} = 1_{T_A}$$
【合成射を保つ事】<br>
型函手の融合則を用いて
$$\begin{aligned}
T(f)\circ T(g) &= \banana{\mathrm{in}\circ F(f,1)}\circ T(g)\\
&= \banana{\mathrm{in}\circ F(f,1)\circ F(g,1)} \\
&= \banana{\mathrm{in}\circ F(f\circ g,1)} \\
&= T(f\circ g)
\end{aligned} $$
<span style="float:right">□</span>
</p>
</section>
<section>
<h3> 練習問題 </h3>
<p>
練習として以下の様な事をやってみると良いと思います。
</p>
<ul>
<li> 二分木などの型函手及び融合則の導出 </li>
<li> $\mathrm{map}\ f\circ\mathrm{map}\ g = \mathrm{map}\ (f\circ g)$などの法則の導出。</li>
</ul>
</section>
<section>
<h3> 第10回はここで終わります </h3>
<p>
お疲れ様でした。<br>
次回は指数対象という新たな概念を紹介した後,Curry-Howard-Lambek対応というものの紹介をしたいと思います。
</p>
</section>
</div>
</div>
<script src="lib/js/head.min.js"></script>
<script src="js/reveal.min.js"></script>
<script>
// Full list of configuration options available here:
// https://github.com/hakimel/reveal.js#configuration
Reveal.initialize({
controls: false,
progress: true,
history: true,
center: true,
rollingLinks: false,
theme: Reveal.getQueryHash().theme, // available themes are in /css/theme
transition: Reveal.getQueryHash().transition || 'none', // default/cube/page/concave/zoom/linear/fade/none
// Optional libraries used to extend on reveal.js
dependencies: [
{ src: 'lib/js/classList.js', condition: function() { return !document.body.classList; } },
{ src: 'plugin/markdown/showdown.js', condition: function() { return !!document.querySelector( '[data-markdown]' ); } },
{ src: 'plugin/markdown/markdown.js', condition: function() { return !!document.querySelector( '[data-markdown]' ); } },
{ src: 'plugin/highlight/highlight.js', async: true, callback: function() { hljs.initHighlightingOnLoad(); } },
{ src: 'plugin/zoom-js/zoom.js', async: true, condition: function() { return !!document.body.classList; } },
{ src: 'plugin/notes/notes.js', async: true, condition: function() { return !!document.body.classList; } }
// { src: 'plugin/search/search.js', async: true, condition: function() { return !!document.body.classList; } }
// { src: 'plugin/remotes/remotes.js', async: true, condition: function() { return !!document.body.classList; } }
]
});
Reveal.addEventListener( 'slidechanged', function( event ) {
MathJax.Hub.Rerender(event.currentSlide);
});
</script>
</body>
</html>