『圏論の地平線』
- 圏論についていろいろな分野の人にインタビューする本
他の諸分野との関係性を通じて圏論を「圏論的に」語ろうとす る本があってもよいのではないか
1 計算機科学からの圏論
- 専門: トレース付きモノイダル圏
エディンバラにいた別の偉 い先生だったロビン・ミルナー(Robin Milner)っていう方，チューリング賞も取っている偉い先生ですけど，彼の書いたものをスコッチを飲みながら読んでいたら，自分の修論と言っていることは全然変わらないと.変わらないけど，みんなはこれが新しいプロセス計算の理論といって褒めそやしていたんです.でも，僕の修論と全然変わらないじゃん!とか，勘違いですよ，勘違いだけど，技術的にほとんど似たことをやっていて
- Hindley-Milner型推論 の Milnerさんだった
頼んでなくても量子群のこと教えてくれるんです.こんな感じって式をパパパッと書いて，ご飯食べながら教えてくれる.ただ，神保先生の本も買って読んでみたけれど，実のところよく分からなかった.そういう挫折のあとで，圏論の言葉で全部書かれた量子群の本に出会ったわけです.それがものすごく分かりやすいので，喜んで読んでいました.
いろいろ広い興味を持っていたことが後から役に立った.
量子群は群じゃないらしい
計算機科学には，もちろん専門書は良いものがたくさんあると思うんですけれども，そういう智慧がたっぷり分かる本はやっぱり少ないんでしょうかね
ないと私は思いますね
-
インタフェースとして使う圏論と数学者の研究対象である圏論は別物
-
代数幾何 はプロとアマチュアの差が大きい
-
自己言及性をモデルしようとすると圏論の助けがいる
-
- でもそれだとトポロジカル量子計算をやっている人の叡智には触れていない
-
でも表面的に語れる圏論はすごい
-
コンパイラの正しさを証明するのはファンクタが 充満忠実
-
圏論は将来的に線形代数のように発展的解消されコモディティ化する
-
1900年代初頭は物理学者で行列を知っている人は少なかった
-
モノイダル圏: 圏は型が合えば直列つなぎ出来るが並列つなぎもok
2 圏論と計算機科学
- 『Introduction to higer order categorical logic』
- 0章に モナド までの内容が書かれている
- 圏論はお遊びとされ冬の時代だった
- 後に カリー＝ハワード同型 とかの流れにつながる
- トポスでいうと 初等トポス の方, 数学者は代数幾何から グロタンディーク・トポス を思い浮かべるらしい
- 学位論文: リフレクション をうまく説明したい
- プログラム自体もデータとみなせる
- Term Rewriting は正にそうした上で成り立つ
- 項書換えを計算とみなす = 射から射に移す
- Term Rewriting は正にそうした上で成り立つ
- 多段階計算 の話
自然現象がやっぱりデフォルトでは不可逆なプロセスだよなということを考えるとき，やはり圏というのは実にいい塩梅だと
計算機科学の世界では，基本，不可逆なので
やっぱり圏というのは物理学者たちが割と自然に到達する構
造なのかなっていうのは，ちょっと思ったことがあります
計算機科学の観点で認知や現象はどう見えるか
- どこまでを系として考えるか
- e.g. コンセントまでがコンピューター?
区切りを明確にしないと何をやっているのかわからなくなる
- 自然哲学の人の前提にもにょる
フッサール現象学 はもともと数学だからいいんですよ