1. No category

東大 蓮尾研
検索
東京大学 コンピュータ科学専攻
蓮尾研究室
Dept. Computer Science, The University of Tokyo
Group MMM (aka. Hasuo Laboratory)
ジミなことを， ド派手にやる
「理論計算機科学」
ほとんど数学
5 Foundational study: concurrency and the microcosm principle
one !m" ◦ !m × id" on the right edge is such that
(X1 , X2 , X3 )
C−1
m,m×id
#−→
(X1 ⊗ X2 ) ⊗ X3 .
• Cm,id×m of the iso-2-cells is what gives us a natural
w the composite
∼
=
(X1 ⊗ X2 ) ⊗ X3 .
morphism α : X1 ⊗ (X2 ⊗ X3 ) →
Moreover, the coherence condition on such isomorphisms in a monoidal category
[14, 96]) requires that “any two compositions of such natural isomorphisms are
ntical.” A well-known instance is commutativity of the following “pentagon diam.”
α
(X1 ⊗ X2 ) ⊗ (X3 ⊗ X4 )
X1 ⊗ (X2 ⊗ (X3 ⊗ X4 ))
X1 ⊗ α
α
X1 ⊗ ((X2 ⊗ X3 ) ⊗ X4 )
α
(X1 ⊗ (X2 ⊗ X3 )) ⊗ X4
((X1 ⊗ X2 ) ⊗ X3 ) ⊗ X4
α ⊗ X4
圏論・代数学・
数理論理学
新パラダイム計算を
ねじふせる
量子計算
ハイブリッドシステム
（情報＋物理）
eed, commutativity of this pentagon is derived from the fact that the following
composed iso-2-cells are identical.
C4
C3
!1·2,3"
!1·2,3"
C2
!1·2"
!1·2"
C
C3
!1,2·3"
id
C3
!1,2·3"
!1·2,3"
α
C2
!1·2,3"
C2
α
⇓
C2
α
!1,2,3·4"
!1·2,3,4"
⇓
!1,2·3"
!1,2·3"
⇓
C3
C4
⇓
C×α
α×C
⇓
!1,2·3,4"
C3
⇓
!1,2,3·4"
!1·2,3,4"
C2
!1·2"
!1·2"
!1·2"
C
se two composites are identical due to the coherence condition on the mediating 2s Cb,a of a pseudo functor (see [19]). Here the notation 1· 2, 3, 4—with its intention
ng x1 , x2 , x3 , x4 ( x1 · x2 , x3 , x4 following the categorical logic tradition—denotes
arrow )m ◦ )π1 , π2 *, π3 , π4 * : 4 → 3 in Mon.
May However,
16, 14 at this moment it is not clear what is a canonical
SoFriday,
far so good.
1
東大 蓮尾研
検索
東京大学 コンピュータ科学専攻
蓮尾研究室
Dept. Computer Science, The University of Tokyo
Group MMM (aka. Hasuo Laboratory)
王様のように遊び，
数学って
楽しいよね
大統領のように働く
Kleisli 圏での余代数
けれど応用上の
インパクトも狙う！
Geometry of Interaction
Hoare 論理 ＋ 超準解析
数学的な定式化
「数学的本質」
パラメータを
を見極める
変えて具体化
既存の手法
非決定的システム
ふつうの計算
Friday, May 16, 14
離散的システム
新たな手法
確率的システム
ハイブリッドシステム
量子計算
東大 蓮尾研
検索
東京大学 コンピュータ科学専攻
蓮尾研究室
Dept. Computer Science, The University of Tokyo
Group MMM (aka. Hasuo Laboratory)
求める学生像
数学的な議論に慣れていると良い
前提知識は不問
目指す学生像
理論研究における共同研究のスキル
俯瞰力と問題設定力
やる気スイッチを見つけよう（成功体験）
地味な研究だからこそ，ハデにやろう！
Friday, May 16, 14
圏論とは？
単射の概念（element による）
の，矢印だけによる言い換え
練習問題
P
s
'>1 ko
s
>1 k o
'! >^1
6
· · · b0
x
'i > 1 f o
··· o
'
C
1 osk
!
s
F 1 ko
··· o
Fi
1
!
i
x
F 1 fo
⇡i
Fi !
!+1
>1
F ! 1_ 8
··· b
F ⇡i 1 ⌃
F !+1 1
F (beh(c))
_ _ _ _ _/ F Z
FX
O
O
c
final
For a function f : X ! Y , the following are
equivalent.
• f is injective, that is,
f (x) = f (x0 )
=)
x = x0 .
• f is left-cancelable, that is, for any set
Z and any functions g, h : Z ◆ X,
f
g=f
h
=)
g=h .
_ _ _ _/ Z
X _ _beh(c)
Category Theory
矢印ばっかり書いているのだ
もともと代数学の道具
抽象化と一般化の「乗り物」
計算機科学での応用
余代数 (coalgebra)
オートマトンの抽象化
関数型プログラムの意味論
Haskell のモナドとか．
Friday, May 16, 14
藤井 宗一郎
修士課程
メンバー
片岡 俊基
博士課程
(計数出身)
(数学科出身)
圏論的論理，topos，
圏論的双対性，
超準解析
普遍代数，豊穣圏
由水 輝
博士課程
(内部生)
線形論理，
量子プログラミング
パリVIIに行ってる
蓮尾 一郎
木戸 肩吾
赤崎 拓未
小川 浩志
講師
修士課程
ボス！！
プログラム検証，
量子的システム，
物理情報
物理情報システム
coalgebra
システム
津曲 紀宏
ポスドク
確率的システム，
クリーニ代数
Friday, May 16, 14
(内部生)
(内部生)
中川 翔太
室屋 晃子
修士課程
修士課程
修士課程
(内部生)
線形論理，
圏論的意味論
修士課程
(内部生)
卜部 夏木
(内部生)
修士課程
(内部生)
確率的システム，
確率的システム，
ゲーム論的確率論
coalgebra
教員は一人だけど
いろんな人に話を聞けます
研究協力者
京都大学 数理解析研究所の先生方
長谷川真人，照井一成，勝股審也，星野直彦
圏論，プログラム意味論，線形論理，...
毎年夏に合同セミナー実施
この他にも...
末永 幸平 先生
京都大学
プログラム検証，ハイ
ブリッド・システム
Friday, May 16, 14
国内外，大学，企業
などに（ゆかいな）
協力者多数