第４回プログラミングおよびプログラミング言語サマースクール
http://www.math.nagoya-u.ac.jp/~garrigue/ppl_ss06/
圏論の諸相（講師：木下佳樹先生）
冒頭で「諸相といっても2時間で話せるのはせいぜい1相」という前フリがあったけど、本当にそうだった。そんなわけで、Haskell→圏論というノリの参加者にはつまらなかったかもしれない。
個人的には、これまで聞きかじっている知識に横糸を何本か通すことができてよかった。以下、講義中に勝手に頭の中で構成したまとめ。絶対に参考にしてほしくないわけですが（どうせこんなページに圏論について真剣に知りたい人はこない）、詳しい人に勘違いを指摘していただくのは大歓迎です。
圏論ってのは、「集合全体の集合」とか「写像全体の写像」のように、集合論だけだとパラドクスを誘発しかねない何かを扱うべく捻り出された概念なんだよね。たしか。だから、「集合全体の集合」みたいなものにやばさを感じない限り、そもそも圏論のありがたみとか面白さはわからないような気がする。講義で「"small"な集合」という言い方を強調してたり、「集合の要素を使わずに単射の定義を与えてみよう」というクイズで「集合全体の集合を認める」という但し書きをしていたのには、そういう事情があるはず。
で、この「集合の要素を使わずに単射の定義を与えてみよう」クイズがえらく自分のツボに入った。集合AからBへの単射っていうのは、ぶっちゃけると集合Aの要素と集合Bの要素が1対1に対応しますってことで、それを「要素」とか言わないで定義しろっていうのがクイズの趣旨。答えはこうなる。
f が集合 A から集合 B への単射つまり、単射という写す集合と写される集合の要素に関する問題を、移すほうに値域を持つ別な任意の写像（ただし定義域は固定）どおしの関係として定義すればいいってこと（ちなみに講義では、たぶんあえて、定義域とか値域うんぬんの議論をぼかしてた。当たり前っちゃ当たり前のことなんだけど、これが固定されていないと f との合成写像を取ったところで何の意味もない。そのため圏論では、定義域と値域をあわせて写像ではなく「射」という言葉を使ってる。たぶん。僕のこれまでの圏論の認識といえば「射で考えるやり方」という程度だったので、今日の講義でようやくさっぱりした）。
=def
任意の集合C と任意の h,k:C→A について f・h = f・k ⇒ h = k
同じように任意の集合とそこからの任意の射を使うことで、単射に限らず数々の集合っぽい概念を再定義できる。ところで、たとえば直積がペアをあらわすように、集合の概念はデータ構造を形成できる。ってことは、圏でもやっぱりデータ構造を定式化できるよね。たぶん、これが今日の講義のメインだったんだと思う。
２時間で真似(まね)ぶ関数型言語のコンパイラ（講師：住井英二郎先生）
MinCamlの話は仕事や趣味からはいちばん近い話題で予備知識も多かったせいか、関心するところが多すぎてあまり扇動的な気分にはなれず……。実はこのサマースクールに参加した背景には、講義の内容から技術的な知見を得たいっていう以上に、精神的にアジテートされたいっていう動機があった。まあ、お前の求めてるものがおかしいって話なんですが。
余裕があったらまとめをかく。
述語抽象化によるアルゴリズムの検証 ～ シェープ解析を例として（講師：田辺良則先生）
プログラムの安全性を検証したいけどすべての状態と状態遷移を検証するのは無理だよね、それなら数学的に証明された方法で抽象化した状態とその遷移をうまく取り出して検証しましょうって話。まったく予備知識のない分野だったせいか、3時限目にもかかわらず異常に興奮した。プレゼンも面白い。
これも、余裕があったらまとめをかく。
0 件のコメント:
コメントを投稿