計算機科学のための圏論の基礎の基礎

某勉強会で，「計算機科学のための圏論の基礎の基礎」と題して， 2020 年 3 月 25 日（水）に発表することになり，今朝（2020年3月23日（月））に，資料を作り終えました．その勉強会のサイトでも資料は公開されますが，ここでも公開しておき，変更があれば，ここのを修正していくことにします．

資料はプリゼンテーションの形で，話題としては，関手，単純型付きλ計算，デカルト閉圏（CCC）を含んでいます．ただし，今回の発表の話題としては，「自然変換」さえも入れてません．自然変換はきちんと圏論を勉強するためには欠かせないものですから，今回の資料では，「それは自分で勉強してね」というスタンスです．発表時間の制限から，話題をかなり絞らざるを得なかったのです．それでもスライドは 104 枚になりました（2 時間の勉強会なのですが）．

発表資料

内容梗概

某勉強会のサイトに載せた紹介文をこちらにも載せておきます．

計算機科学のための圏論の基礎の基礎

講演日：2020年3月25日（水）17:00-19:00

1970 年ごろから計算機科学への圏論の適用事例が発表されはじめ，徐々に論文数も増加してきている．適用対象としては計算機械のモデリング，型理論，意味論などがある．中にはモナドなど，実用のプログラミング言語での応用もあり，計算機科学に携わる少なくない人が圏論に関心を持っているのではないだろうか．

しかし，一般に圏論の学習には比較的多くの数学的な知識と思考能力，慣れを必要とし，通常の計算機科学の学生が持っているグラフ理論などの離散数学だけの知識では，途中で挫折することが多いように思う．特に，指導者がいない独習環境での学習は成功しにくい．

今後も圏論の計算機科学応用は確実に進んでいくと思われ，大学を卒業した後，学習を始める人も多いと思うので，上記のような数学的習熟度の学習者でも進めていける学習方法が欲しい．

私は，圏論の学習，特に独習を難しくしている理由としては

何に利用できるのか分からない
登場する概念の意味が分からない
圏論の中の抽象的な概念の構成方法に頭がついていけない

が大きいと考えている．そこで，圏論のごく一部分でも，これらを解決したコンパクトな教材を用意し，各自が本格的な教科書で独習する時の仮設の足場を提供することが一つの解決策ではないかと考えた．今回は，そのパイロット版として

圏論の計算機応用に関する概要
圏論の基礎的な概念の解説
応用の雰囲気が分かる題材の紹介
- 代数/余代数によるデータ型の表現
- デカルト閉圏（CCC）による型付きλ計算の解釈

を含んだものを試作しているので紹介したい．ただし，上記の学習困難理由のうち３番目の「圏論の中の抽象的な概念の構成方法に頭がついていけない」は，数学的な概念の認識や推論の訓練が必要になり，２時間の発表に含めることができないので割愛する．

圏論の内容以外の部分，学習とかλ計算とかが，かなりの部分を占めているかもしれません．

発表を終えて

私を除いて８名が参加し，2時間の勉強会でした．参加者の自己申告では２名以外，圏論を知らないと言われてましたが，その勉強会の実力はあなどれないので．．．

時間内に終わらせることを考えずにとにかく喋りたいことを喋ったら，1 時間 45 分で，スライド 52/104 (「単純型付きλ計算の意味を与える圏の条件：積オブジェクトと冪オブジェクトを持つこと」)までしか行きませんでした（スライド番号は初出のものの番号．以下同様）．しかたがないので，あとの 15 分は，その資料に何が書いてあるのかをざっと説明して終わりました．やはり全部をやろうとすると，最低でも 4時間，休憩や理解確認，十分な質疑応答を考えると５時間以上とった方がよさそうです．まったく休憩を挟まないと喋る方も心が折れそうになりますし．

でも，スライド 51（単純型付きλ計算の意味を与える圏の条件）

まあ，この資料は色々な機会を利用してブラッシュアップをはかり，圏論の残りのトピックスのチュートリアルも追々，整備していくことにしようと思います．

計算機科学のための圏論の基礎の基礎

目次

いきさつ，概要

発表資料

内容梗概

計算機科学のための圏論の基礎の基礎

発表を終えて