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

by Akihiko Koga, 26th Mar. 2020 (Update)
23th Mar. 2020 (First)
ホームページトップへ戻る
圏論を勉強しようへ戻る
関連ページ:アウディの圏論の概説に行く
関連ページ:レンスターのベーシック圏論の概説へ行く
関連ページ:Barr and Wells の圏論の概説に行く

目次

  1. いきさつ,概要
  2. 発表資料
  3. 内容梗概
  4. 発表を終えて

いきさつ,概要

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

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

発表資料

資料の PDF は

「計算機科学のための圏論の基礎の基礎」のPDF, Ver. 0.91, 2020.03.26
(初出 Ver. 0.90, 2020.03.23)
においておきます.

内容梗概

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

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

講演日:2020年3月25日(水)17:00-19:00

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

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

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

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

  1. 何に利用できるのか分からない
  2. 登場する概念の意味が分からない
  3. 圏論の中の抽象的な概念の構成方法に頭がついていけない
が大きいと考えている.そこで,圏論のごく一部分でも,これらを解決したコンパクトな教材を用意し,各自が本格的な教科書で独習する時の仮設の足場を提供することが一つの解決策ではないかと考えた.今回は,そのパイロット版として を含んだものを試作しているので紹介したい.ただし,上記の学習困難理由のうち3番目の 「圏論の中の抽象的な概念の構成方法に頭がついていけない」は,数学的な概念の認識や推論の訓練が必要になり,2時間の発表に含めることができないので割愛する.

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

発表を終えて

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

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

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

まで行ったということは,CCC における関数適用と関数への抽象化の原理まで行ったと いうことなので,何段目かの目標は達成できたということかもしれません.何段階かの 目標設定は以下の通りです.読むときの,区切りの目安になると思います.私にとっては 説明の時の区切りの目安です.
  1. スライド 45 (代数(Algebra)と余代数(Coalgebra):読み物)完了
  2. スライド 51 (単純型付きλ計算の意味を与える圏の条件)完了 ... 今できた目標
  3. スライド 57 「積」の説明 完了
  4. スライド 63 「冪」の説明 完了
  5. スライド 68 「デカルト閉圏」の説明 完了
  6. スライド 87 「単純型付きλ計算」の説明 完了
  7. スライド 96 「単純型付きλ計算とCCCの関係」の説明 完了
  8. スライド 104 全部完了

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


圏論のトップページ

ホームページトップ(Top of My Homepage)