Category Theory for Computing Science,
by M. Barr and C. Wells
1998
Michael Barr and Charles Wells の Category Theory for Computing Science は,1998 年に 出版され,2012 年に reprint 版がでています.このページを作ったあと, 2020年3月末に著者の一人の Michael Barr 教授とコンタクトが取れましたので,この本の PDF の所在については詳しく書くことができます(もう一人の著者の Charles Wells 教授は 残念なことに 2017 年に亡くなられてました).この本の PDF は次の2か所に置いてあります.
いつものことながら間違いがあるかもしれませんから,大体,どんなことが書いてあるかの参考に するくらいに受け取ってください.
- Preface
- Preliminaries
- Categories
- Functors
- Diagrams, naturality and sketches
- Products and sums
- Cartesian closed categories
- Finite product sketches
- Finite discrete sketches
- Limits and colimits
- More about sketches
- The category of sketches
- Fibrations
- Adjoints
- Algebras for endofunctors
- Toposes
- Categories with monoidal structure
だいたい,本の前書きにはその本の性格や各章の概要が書いてあるので, ここを読めばおよそどんな本か分かるはずですが,往々にして初心者には これが読めません.多くの著者は初心者に対する優しさを持って前書きを 書いてくれませんし,ひどい場合は,同業他者に対して,「似たような本があるのに なんで,この本を書くのか」と言った言い訳が書いてあることがあります.
この本はそのような言い訳は書いてないようですので,きちんとここを読み解けば この本を学習して得られることが分かりそうです.やってみましょう.
最初の数行は次のようなことが書いてあります.
まず,この本は計算機科学の研究者や学生が圏論の基礎的なことを学習する目的で 書いてあります.計算機科学の例や応用の文脈でも圏論的な構成方法について説明 されています.
圏論のある種のアイデアや構成法(多分,デカルト閉圏(ccc)など)は, すでに計算機科学の中に深く取り入れられています.この本ではこれらの多くに ついて説明します.また,別のアイデア,例えば,「随伴(Adjoint)」については まだ,それほど広くは取り入れられていませんが,これらも可能な応用と一緒に 説明します.
この本の1つの特徴は
後日記: sketches の最初の節を読んで,なんとなくどんなものか 分かりましたので概略を こちらに書きました.ご興味があれば. 2019.08.20 (火)
いくつか,この本の方針に関する注意というか言い訳が書いてあります.
次に
この部分を私がきちんと読み取っているという自信はありませんし,また, これらが排他的な記述になっているような気もしませんが,一応,自分の理解で説明しておきます.
一つ目は圏の元々の動機に繋がっていることで,数学の一つの構造を別の構造に 移すための記述に使うというものです.圏論は数学の複数分野に横断的にまたがる 共通のアイデア,構成を明確にしてくれます.
二つ目は,圏を数学的な構造としてみることです. 例えば,順序集合(poset)やモノイド(群から逆元の存在の要請を除いた代数的構造)の ようにです.さらに実際,この二つの数学的構造(poset とモノイド)は,圏の二つの極端な例になっています.
三つ目がこの本で強調されている見方で,圏を理論(Theory)としてみる見方です.
これは数学者がある種の構造を形式化するための
次にこの本が扱っているトピックスですが,次の図のような内容です.右下に 書いてあるページはそれぞれの章の終わりのページです.したがって,その章の ページ数を出すためには直前の章のページ番号をその章のページ番号から引けば 良い訳です.
第1章の Preliminaries は準備と記号合わせで,内容は,集合論,関数,グラフに ついてです.グラフは圏論の基礎ですから,しっかりやっておいてください.
図の左側のラインの説明に入ります.
まず,第5章は,product と sum で,集合で言うと 直積と直和にあたります.これは第9章 Limits and Colimits で,極限(Limits)と 余極限(Colimits)という概念に一般化されるものです.そういう一般化をする前に 具体的に色々扱っておくということみたいです.また, product は次の第6章の Cartesian closed categories を定義するために必要になります.あと, product や sum はプログラミング言語の 構造体(C言語のstruct)や可変レコード(C言語の union)にあたります.
第6章は計算機科学関係の人には重要な章です.ここでは,デカルト閉圏(cartesian closed categories)というものが型付きラムダ計算と同等であることが示されます.したがって, ここまでなんとかたどり着くことが,この本を勉強するときの一つのマイルストーンと いうことになります.この章の終わりが 218 ページですね.なんとか, 頑張ってここまで読みましょう.
第9章は Limits と Colimits で,第5章の Products と Sums を一般化した概念です. 圏論の圏論らしい概念ですのでしっかりと.
第12章の Fibrations も計算機科学と関係の深い章です.こちらはオートマトンと 関係しています.
第13章は Adjoints (随伴) です.これは圏論の真髄であると,他の圏論の本(例えば, S. Awodey や T. Leinster )でも言われているものです. T. Leinster の本では, これはかなり前の方に現れています.Leinster の意見では,Adjoints は圏論のとても 重要な概念であり,また,それほど難しくない概念であるので,ぜひ,最初の方から, この概念になじんでそれを活用すると言う恩恵に預かるのが良いということらしいです. S. Awodey はこの本と同じように後ろのほうにあります.この本の著者らは, Adjoints は圏の重要な概念ではあるが,動機が分かりにくく,具体例に沢山触れた後の方が 良いと言う意見で,この位置にあるようです.あと,Adjoints は次の章に出てくるモナドの 説明に必要な概念なのも,Adjoints がこの位置にある理由です.
第14章は代数と自己関手の話でモナド(Triples)の話も出てきます.しかし, Haskell でのモナドとの関連などは出てきません.個人的には,あれはあれで,なんか色々な 話が混ざっているような気がしますので,別の論文などで正体を見極めたら良いのでは ないかと思います.そのときの基礎のためにも,この章を理解しておくのが良いでしょう. 一応,モナドに関する調査・お勉強に関連の 文献をいくつか挙げておきます.
第15章は Toposes のお話です.これは一般化された集合論とかロジックとの関係の 話があるようです.最近,計算機科学でも活用されており重要だと思います.
第16章はモノイダル構造を持った圏のお話です.線形論理(linear logic)と関わりがあるそうです.
以上で,この本で扱うトピックスのお話は終わりです.次はいよいよ本章の概要に入ります. と言っても,次の章は「準備」の章ですが.
第一章は準備(Preliminaries)です.ここでは,この本で使う 集合と関数の記法と用語の確認をします.
集合については,ものの集まりを無制限に「集合」と 考えるとパラドックスを起こす場合があること,集合の大きい(large),小さい(small)に ついての注意があります.これは分からなければあまり気にしないで良いです. 関数については,立場ごとに多少の定義の違いがあることがあります.ここでは 関数が移す元の集合と移す先の集合が異なれば関数も異なると考えます(集合論では 移し先の集合が多少違っても同じ関数と見ることもありますが,ここでは移し先が違えば 別の関数と考えるということです).あと,関数については, 集合 S から集合 T への関数の集合 Hom(S, T) を考えることができることの説明と練習問題があります.これはきちんと やっておいた方が良いです.後々,ずっと使いますから.特に関数 f : T → V をとってきて,
Hom(S, f) : Hom(S, T) → Hom(S, V)と言った,関数の集合 Hom(S, T) から関数の集合 Hom(S, V) への関数 Hom(S, f) の 作り方や記法(Hom(-, -) を引数が集合のときも関数のときも使うと言うオーバーロード的な 使い方)に慣れる必要があります.where Hom(S, f)(g)(v) := f・g(v)
もう一つのトピックスのグラフですが,これは, 圏,可換図式,スケッチ(sketches)の本質的な部分ですので,しっかりやっておいた方が良いです.
繰り返しますと,Hom(S, T) とグラフはしっかりやっておくことが重要です.
圏(category)とはグラフに,そのエッジ(arrow)の合成方法が付いたものです. エッジの合成についてはある種の制約を守らなければなりません.それが,第1節で 正確に述べられます.なお,ここでは arrow のことは矢あるいは射ともいうことに します.用語を統一することができずにすみません.あと,圏の場合, グラフのノードはオブジェクトと言います.
第2節では,関数型プログラミング言語を圏としてみる見方がインフォーマルに 紹介されます.ここでのプログラミング言語は Backus-style のものです. Backus は 1977 年にACM Turing Award を得たときに, Can Programming Be Liberated from the von Neumann Style? というタイトルの論文で関数型言語を 発表しています.これは私も読んで,関数が合成され,プログラムが作成される 様を見るのは新鮮な気持ちでした.ここでは,これより少し遅い 1981 年の論文が 2つ参照されています.
後日記: この節は読みましたので,ここの 関数型プログラミング言語の圏がどんなものかを こちらに書きました.ご興味があれば. 2019.08.20 (火)
第3節は,Preorders, posets, semigroups, monoids が導入され,これらを 圏としてみることができるということが示されます.ここで圏としてみるのはこれら 自身であり,これらの集まりではありません.これらの集まりを圏としてみる見方は また後で出てきます.
第4節と第5節は,もともと圏論が考えられた動機に近い圏の例です.
第4節では この教科書をちらっと見たとき
気になったのは,ω-chain の定義が出てきて,その後の記述でω-がとれて chain に
なっています.これらは全部 ω- がついているものと思われます.(注意)
ω-CPOs だけでなく,
posets の圏も monoids の圏も重要ですから,ゆっくりと確実にやっていったらよいと
思います.
(注意)2020.04.01 (水) : 著者の一人の M. Barr に連絡が取れたので, このことを言ったら,すべてに ω- を付けるのではなく,「ω-chain のことを 簡単に chain ともいう」という類の修正になりました.一応,この本の この部分では整合性がありますし,たぶん,計算機科学では一般の chain より, ω-chain の方が圧倒的によく表れるのでしょう.このページの最初に記載した M. Barr の site の版はすでに修正されています.ついでですので,ω-complete, chain-complete, complete について 少しコメントを補助資料の ω- について(2.4.3 ω-complete partial orders, 2.4.4 Definition) に載せました.
第6節は,すでにある圏やグラフから新しい圏を構成する方法について書かれています. 圏論ではこういう構成(construction)という行為が重要です.特に, slice category は,数学的構造の商空間をとったり,あるいは,上階の概念を 構成していく思考的訓練になって重要だと思います.
第7節から第9節では arrow の色々な性質について論じられます.isomorphism, monomorphism, epimorphism などです.集合で言うと isomorphism は全単射, monomorphism は単射(1:1写像),epimorphism は全射にあたります. 第8節の subobjects の考え方は重要です.集合論のように「要素である」 関係(∈)の無いところに部分集合などの「部分」関係を定義するアイデアが 紹介されます.
第10節は,arrow を分解する方法について書かれています.ここでは epi-mono 分解 について書いてあるようです.つまり,arrow f をある epimorphism e と ある monomorphism m によって,f = m・e のように分けるということです.集合で言うと,写像 f をまず全射をとる関数を適用し,その次に単射をとる関数を適用するという ように分けることにあたります.これは第9章 Limits and Colimits,第16章 Categories with monoidal structures で使うそうです.私は,別の人の本 (Michael A. Arbib の Arrows, Structures, and Functors: The Categorical Imperative)で,オートマトンを圏として扱う時に使っているのをみたことがあります.
第2章はpp15-63 の49ページあります.指導者が居なくて,自分,あるいは自分たち だけで学習するときは,ゆっくり,じっくりやったら良いと思います.計算機科学の 学習者は,とりあえず,第6章の Cartesian closed cateories のところで, 型付きλ計算での圏論の応用を理解するところまでを一つの目標にして 腰を落ち着けてやるとか.特に,社会人で業務を持っていて,さらに勉強したいと 言う人たちは,業務の忙しさで結構挫折しやすいので,高すぎる目標を掲げるのでは なく,それぞれの基礎的な章でも何かの学習して気付きを得ていくというのが良いと 思います.
この章では,圏から圏への準同型に相当する
次の役割は,圏を数学のワークスペースと考えたときの役割で,これは圏として与えられた 一つの構造から別の構造の変換を行うという役割です.最後に,これがこの本では重要になるのですが, 数学上の興味深い対象は,ある圏から集合への Functors をオブジェクトとするある自然な 圏となっていることが多いということに基づくものです.つまり,そのような数学的な対象を Functors の集まりで表現するという役割です.
各節の内容は具体的には以下のようになっています.
最初の3つは Functors の定義,例,そしていくつかの性質を述べています.3.2 節の 例は,「3.2 Actions」とあり,やや特殊な例のように見えます.これは群論を学習した人は 分かると思いますが,「群の作用」という概念があります.ここではそれを少し一般化した モノイドの作用を考えるようです.さらにオートマトンを勉強したかたは分かるかもしれませんが, これはオートマトンの理論に非常に関連しています.実際,ここでも3.2 の先頭を見てみると, 第12章 Fibrations に関係していると書かれています.第12章もオートマトンに関連した トピックスです.「3.3 Types of functors」では faithful な Functors,full な Functors などの概念が登場します.これは集合における1:1写像や全射のような概念で 非常に基本的で重要な概念です.ただ,これらは正確に集合の1:1写像と全射と 重なるものではないので,きちんと差異を押さえて学ばなければなりません.
第4節は Functors を使った,二つの圏の同値の概念が導入されます.これは圏論の見地から 二つの圏が同じであるという基準を与えます.
最後は圏の商の概念が導入されます.これについては sketches に関連した章でしか 使わないと書かれています.圏の商の概念は一般的な概念なので sketches に限定しないでも 良さそうな気がするのですが.
タイトル通りですが,この章ではダイアグラム,自然変換(natural transformation),そして sketches を学習します.可換図式(可換タイアグラム)は(連立)方程式の圏論的な表現方法です. 下の図の1番目を見てください.可換図式はこの図の矢の合成がすべて等しいことをいう ものですが, これは,等式 g・f・x=h・y を表します.最初の2つの矢の x と y はわざと変数っぽい 名前にしてあります.最初の矢の合成のところを図のように g・f(x)=h(y) 書くと, もっと x と y の方程式っぽく見えるでしょう.
次の自然変換(natural transformation)α は関手(functors)間の写像(map)です. これは,関手がある種の構成(construction)を与えていると思えば,一つの構成から 別の構成への変形(deformation)にあたります.
最後に,この本特有の sketches ですが,これはある可換性とその他の条件が課せられたグラフです. これは構造を表す方法の一つです.その構造のモデルは関手をオブジェクト,自然変換を矢とした 圏で表すことができます.
これらの概念はお互いに密接に関連しています.実際,diagrams も,関手も,sketches の モデルも,同じアイデア,すなわち,グラフの準同型の別の側面にすぎません.そのグラフの 一部,あるいは,全部が圏になっているといった違いはありますが.
次に各節の概要を説明しておきます.
最初の3つの節は,圏論の基礎である,図式,可換図式,自然変換が述べられます. これらは以後,かなり使われますので,しっかり理解してください.
次に自然変換の Godement calculus が述べられます.これは矢と自然変換の代数の基礎 だそうで,また,この章の最後,「4.8 2-categories」でさらに抽象的な形で述べられます.
次は,representable functors, 米田の埋め込み,universal elements が導入されます. representable functor は圏から集合の圏への関手で,米田の埋め込みは,与えられた圏の オブジェクトを representable functor (正確には Hom functor)で表現します. 集合については我々はかなりの 経験と知識の蓄積があるため,米田の埋め込みは,元の圏の性質を解析する強力な方法になる訳です. ここのトピックスについて詳細を実際にやってみるのは自然変換の学習に,とっても役に立つと 説明されています.これは正しいと思いますが,それとは別に,米田のレンマは本当に 重要ですから特にしっかりとやることが重要と思います.
4.6 節と 4.7 節は sketches については話題です.ここは飛ばしても構わないと書いて ありますが,同時に,可換図式と自然変換でものごとを表現することに慣れるのによいので 学習することを推奨するとも書いてあります.ちなみに, sketches がどんなものかは こちらに書きました.ご興味があれば.
最後に 4.8 節の 2-categories ですが,これは矢の間の mappings (2-ccells)を 許す圏について書かれています.これはプログラムの詳細化(program refinement)を モデル化することに使うことができるそうです.
この章では,Products と Sums を導入します.Products は任意の個数の引数をとる操作の 定義を可能にする構成(construction)です.ちょっと,この部分は,表現が 分かりにくいかもしれませんが,(x1, ..., xn) という組を一つのものとして扱うことが できるということを言っていると思われます. Sum は代替的な仕様(alternative, a か b かというように選択が可能な仕様)を可能にする構成です.集合論で言うと, Products は直積(cartesian product)で, Sums は直和 (disjoint union) です.
また,これらは第9章で学ぶ limits と colimits の例になっていますので, ここでしっかり学習しておくことが第9章を学びやすくすることにつながると思います.
この章の内容は以下のようになっています.まず,5.1 から 5.3 までで Products について 述べて,5.4 で Sums について述べます.
これらのProducts と Sums の概念を利用した構成が 5.5 から 5.7 で述べられます. この3つの節はお互いに独立みたいで,どれを先に読んでも構わないみたいです.
5.5 は自然数のオブジェクトが Products と Sums を使って定義されます.
5.6 では,形式的言語と形式的演繹システム(formal deductive system)を 圏としてみる方法が紹介されます.そこでは Products と Sums はとても身近なもの であることが分かります.例えば,Products はプログラミング言語では複数のフィールドを もったレコードにあたり,形式的演繹システムでは conjunction (連言, A かつ B)に あたります.
最後に,5.7 では distributive categories が紹介されます.これは大雑把に言って, 和(Sums)に対して積(Products)が分配できることを表します.つまり,等式
A×(B + C) = A×B + A×Cなどが成立するということです. このような圏は我々が演繹システムに期待するような,ある(良い)性質を持ちます.
いよいよ,私たちが圏論の計算機科学応用の最初のマイルストーンと見なしていた CCC の章に入ります.
この章ではデカルト閉圏(Cartesian closed categories),略して,
という条件を満たす圏です. product は前の章で導入されたもので,集合では直積 ( A × B ) になるものでした. 冪はこの章で定義され,BA = A → B は,集合で言うと A から B への関数の集合になります.このような性質を持つ圏は図の下に書いてある 型付きλ式と同等であることがこの章で示されます.λ式は計算のモデルですから, CCC でも計算をモデル化できることになります.
この章の具体的な内容は以下の通りです.
まず,6.1 と 6.2 で CCC の定義といくつかの性質が示されます.次に 6.3 で 型付きラムダ式が導入されます.これらの定義の元に,6.4 で型付きラムダ式と CCC の相互の変換が証明無しに説明されます. 6.5 ではそのときの変換に関して テクニカルな議論がなされます.6.6 では,CCC での, ω-complete partial ordered object の自己準同型の不動点を構成する方法について述べられます. ω-complete partial ordered object は第2章で出てきていました.この不動点は プログラミング言語の If 文や While 文の意味論を提供するとのことです. この節は 6.4 を読み終わったあとにすぐ読んでも良いそうです.
最後に,一言コメントですが,計算機科学で使われる CCC は,ここでの CCC より 少し強い条件,locally cartesian closed であることという条件を付けることが 多いそうです.これは第13章の Adjoints のところで詳しく説明されます.
(sketches は知らないのでこの章は保留 2019.07.27 (土))
(sketches は知らないのでこの章は保留 2019.07.27 (土))
Limit は等式の集まりで定義された product の部分集合の圏論バージョンです. 例としては以下のようなものがあります.
同様に Colimit は Sum から同値関係の商空間をとったものの圏論バージョンです. この章ではこの Limits と Colimits について学習します.ただし,ここで学習するのは 有限の Limits と Colimits だけです.無限 Limits および Colimits も 数学で広く使われていますが,それらは有限のものに似ていて,この章では扱いません.
この章の具体的な内容は以下の通りです. まず,9.1, 9.2, 9.3 の3つの節では Limits について述べ,続いて,9.4 で Colimits が述べ ます. Limits の最初に登場する Equalizer だけ図示しておきました.Equalizer はオブジェクト A から B への射 f, g が与えられたとき,あるオブジェクト E と射 h : E → A で, f・h = g・h を成立させるものの中で,もっとも「射の先端」にあるものです.つまり, 図では h' : E' → A もこの性質を満たすものとすると,このとき図を可換にする k : E' → E が一意に決るというものです.つまり,等式を満たす E' に対して, Limit E は,E' から一意の射があると言う訳です. この「射の先端」にあるという言葉は Limit の感じを伝えるために私が今,勝手に作った言葉なので,正確な内容はこの章を 読んで下さい.
9.6 はプログラミング言語の意味論において望ましい Sums の性質について述べています. Sums は第5章で勉強しましたが,実は Colimits の一種です. 9.7 は,論理型プログラミングのユニフィケーションはある種の colimits であるという ことが書かれています.ユニフィケーションは論理型言語の Prolog などの変数ありの 複数の項を同じ形にする,変数への代入のことです.これは興味深いですね.この節は 多少 sketches の知識を必要とするようです.最期の 9.8 は Limits, Colimits それと Factorization の関係について述べられています.
(sketches は知らないのでこの章は保留 2019.07.27 (土))
(sketches は知らないのでこの章は保留 2019.07.27 (土))
圏は部分順序集合(partially ordered set, poset)やモノイドを一般化した概念です. 圏の中で,特に poset とモノイドは両極端な圏です.
一応,poset (P, ≤) とモノイド (M, ・) を圏として見る見方を復習しておきます.
poset (P, ≤) はオブジェクト間の射が 高々1つしかない圏で,x≤y の時に限り,一意な射 x→y があるとします. モノイド (M, ・) はオブジェクトが一つだけ(例えば * とする)で, 射は M の元 m に対応して一つ,m : * → * があり,二つの射 m, n の合成は,モノイドの 演算で,m・n になります.
話をもとに戻します.圏は両極端な例 poset とモノイドを一般化した概念であるという 話でした.ここで,圏の新しい概念が出たとき,それがどのようなものか理解するには 一般的には poset でどのような概念になるかを見てみることが役に立ちます.例えば, product が何かを poset で考えてみると,二つのオブジェクト a, b の下限, 束論の記法で書けば,a ∧ b になります.一般的には,もう一つの極端な例のモノイドに 当てはめるのはあまりお勧めではないと書いてあります.
ところが,モノイドのある代数的な構造に関する概念はとても自然に圏論の中に 入っていく場合があります.そのとき,モノイドで成立していた多くの定理も 同様に圏論の中で成立します.また,モノイドの応用として計算機科学のオートマトン 理論に関するものがあるのですが,それも圏論の中に自然に入っていきます. この章ではそういったモノイドの一般化に関する圏論の理論を学習します.
私は上の説明で結構,分かった気になったのですが,よくよく考えてみると, 「ここでは圏論の中のモノイドっぽいことを話します」としか言ってないんですね. とにかくそういうことみたいです.
この章の具体的な内容は以下の通りです.
まず,12.1 で
wreath product は大昔(1960年代) のオートマトンの 理論に出てきます.例えば,「任意の有限オートマトンは,複数のリセットオートマトンと パーミュテーションオートマトンのカスケード積の中に埋め込める」という定理( Krohn-Rhodes の定理 1963 )があり,このオートマトンのカスケード積が対応する モノイドの wreath product になります.私は,こういう,計算機械の分解・合成に 関する理論は重要だと思うのですが,ほぼ,すでに忘れ去られた理論になりつつ あります.きっと,いつかまた,他の状況が揃ったとき,別の形で再発明されるのでしょう.
愚痴はこのくらいにして,話を先に進めます.12.1 の Fibrations は最近の多相型( polymorphism )の 研究でも使われていると書かれています.楽しみですね. 12.2 は, Fibration を構成する方法で グロタンディークによるものが紹介されます.これはモノイドの半直積の拡張だと 書いてあります.12.3 はある種の fibrations や 圏を値にとる関手の同値に関することが書かれ,最期の 12.4 ではモノイドの wreath product の拡張の圏の wreath product が書かれています.
いよいよ,圏論の最高峰(?)と言われる「随伴(Adjoints)」の章に入りました. ここでも最初から
と言っています.その割に,Adjoints がどんなものかの記述が無いので, 申し訳程度ですが,図を補いました.Adjoints とは二つの圏 C と D があり,その間に相対する関手 F : C → D と U : D → C がある種の関係を満たすときにこの圏と関手の組を adjoint であると言います.それらの 関手が満たすべき条件とは,同値な条件が何種類かありますが,そのうちの一つでいうと, 射の集合 C(C, U(D)) と D(F(C), D) が「自然に」同型という条件です. これは C(C, U(D)) と D(F(C), D) が一対一に対応し,かつ,ある種の条件を 満たすということですが,詳細は本文を参照してください.ここでは, 圏 C と圏 D がお互いに関手+ある種の条件で拘束しあう関係だと思ってください.Adjoints は類似の representable functors の概念を除いて,圏論で最も重要な アイデアである
Adjoints という概念は非常に強力です.この本に書かれている色々な概念, Products と Sums ,Limits と Colimits ,Exponentials ,自由モノイドなどの構成を Adjoints で 記述することができます.また,第15章で述べる Topos も Adjoints の言葉で 最も都合よく記述することができます.
この章の具体的な内容は以下の通りです.
まず 13.1 で自由モノイドの構成を復習します.この構成はある Adjoint の一方の関手に なります.ここでは,そのことが分かり,Adjoints の定義に繋がる様な記述がなされます.
13.2 ではいよいよ Adjoints が定義され,13.3 でその性質が述べられます. そして最後に 13.4 で Locally cartesian closed categories が述べられます. これは第6章 Cartesian close categories (CCC) の扉の説明にあったように,計算機科学に 現れる CCC には,通常の CCC の条件以外にこれが課されると予告されていたものです. この Locally cartesian closed categories は Adjoints を使うと,もっともよく記述できる とのことです.
第14章では自己関手(endofunctors)に基づく構成法を学習します.自己関手とは, ある圏 C からそれ自身への関手のことです.代表的なものと しては Triples (これは最近は Monads と呼ばれています)があります.Monads は 関数型言語 Haskell などで,副作用を関数型の部分から分離する手段として使われて いるらしいので,興味のある人が多いのではないでしょうか.しかし,ここでは Haskell の話は無いみたいです.Haskell などで Monads がどう使われているかは, 発案者の Moggi や,それを Haskell に取り入れた Wadler らの論文を読むのが良いのでは ないでしょうか.いくつか関連する文献をモナドに関する調査・お勉強に置いておきました.これらを読むためにも,本章をしっかり勉強するのが 重要だと思います.
この章でのお話は5つあります.まず,14.1 では自己関手の不動点と最小不動点についての 概念が導入されます.不動点になるための自然な構造は 自己関手の代数(algebra for the endofunctor)と呼ばれるそうです.次の 14.2 では,これらの概念を使って,リストや 状態遷移機械の圏論版が述べられます.14.3 と 14.5 は treiples (monads) に関する節です. monads は adjoints のアイデアを抽象化したものです.実際,Adjoint をの左から右へ合成 した自己関手は,monads になります.最期の節は,Scott domain に関する節です. これは計算機科学でプログラミング言語の意味論をやっている人は良く知っている理論 だと思います(D ≅ [D→D] のような領域を作る技術ですね).ここでは,そのような領域の 作り方として,Smith & Plotkin のものが紹介されます.これは CCC の中の計算のモデルを 与え,再帰に不動点による意味を与えることができると言うことです.そのドメイン自身も 不動点で与えられます.
この章ではトポス(topos)を学習します.Topos の名前はあちらこちらで聞き, 計算機科学でもよく参照されます.Topos は,次の図の先頭にあるように,CCC (Cartesian closed category) に ある特別な構造を入れた圏です.どんな構造かというと,部分オブジェクトを考えることが できるようになる構造です.部分オブジェクトというのは,例えば,集合に対して,その 部分集合という関係を持つオブジェクトです.これを可能にする構造というのは大雑把に 真偽値と思って良いと思います.true, false があれば,オブジェクト A の中にオブジェクト x が入っているかどうかの判断基準を用意することができるようになる訳です. 所属 関係が導入出来れば,部分の関係も導入できます.ただし, ここでの真偽値は古典論理の二値の真偽値だけでなくもっと拡張された概念になっています.
結果として,Topos は集合の圏 Sets に似た圏であり,かつ,その構成法は, 「部分オブジェクトを可能にする特別な構造」の取り方やその他の条件の設定で,集合にない他の 性質を持った圏を Topos として構成する手段を提供することになります.
まず,Topos は,計算をモデル化するために有用とのことです.「計算」の一つの特徴は,非決定性を 持つということです.つまり,ある集合を effective に列挙する手段(再帰式などに よって規則的に生成する手段)があっても,その補集合を effective に列挙する手段が無い ことがあるというのが計算の一つの特徴な訳ですが,Topos では必ずしも,補集合にあたる オブジェクトの存在を要求しないということがあります.したがって,Topos は, 計算の母体となるものや関数の世界を表すのに相性が良いということが想像されます.
次に数学の中でも Topos は興味があるものになっています.一つには Topos は純粋数学で 使われる層(sheaf)の抽象化になっており,これは二階の命題を解釈することができる 圏を提供します.そのため,Topos は数学の基礎としての集合の代替物としての可能性が あります.
数学における Topos のもう一つの興味は,Topos が内部に真偽値を備えた集合と解釈できる ことにあります.この章の先頭で説明したように「部分オブジェクトを表す特別な構造」の 取り方によっては,古典論理の二値の真偽値より柔軟な真偽値を準備することができる わけです.これを利用して,a variable set theory, a time dependent set theory, fuzzy set theory など様々な集合論のモデルを Topos として提供することができます.
各節の具体的な内容は以下のようになっています.
まず,15.1 と 15.2 では Topos の定義といくつかの性質が述べられます. 15.3 は計算の「より良い」モデルを提供可能にする Toposes の側面を詳しく見ていきます.
15.4 と 15.5 では前層(presheaves),層(sheaves)になる特殊なケースの圏に ついて述べます.これは集合論で∈関係が true, false だけでなく, 色々な度合いがあるようなものと関係があります.ここではグラフの圏が例として 議論されます.15.6 は fuzzy set に関してです.15.7 と 15.8 は realiability toposes と modest set について述べられます.15.7 では 15.8 で使われる概念が導入されます.
この章では二つの圏の間の演算を考えます.計算機科学に現れる多くの圏ではオブジェクトや 射の二項演算があるものがあります.しかし,これらが結合法則を満たすことは非常にまれです. わたしは,ここまで読んで,具体的にはどんな二項演算なのかなと章の中身を見てみたのですが, product を取るとかの例題が書いてあって,特に計算機科学特有というものでは無いような 気がしました.それで,and elsewhere と書いてあるのかもしれません.話をもとに戻します. そういう二項演算,例えば,集合の圏で A×B を考えてみると,(A×B)×C≠A×(B×C) の ようには,めったに結合法則を満たすことは無いのですが,同型で考えると等しいと考えてよい 場合があります.そのようにおよそ結合法則を満たすと考えてよい圏を monoidal categories と 呼んで,この章で勉強します.
具体的な内容は以下の通りです. 16.1 と 16.2 で monoidal categories の定義といくつかの性質を見ていきます. 16.2 では A ⊸C のような記法が使われていますが,これは A⊗_の右 Adjoint です. つまり, A×_ (積)に対する A→_ (冪) のようなものです.
16.3 では,*-autonomous categories という概念が導入されます.これはある種の dual functor Cop→C を持った monoidal closed categories であり,線形論理(linear logic)のモデルになるということです.最後に16.4 では そのような *-autonomous categories の構成方法が紹介されます.
以上で,各章の扉の説明は終わりです.現時点で,sketches に関する章の扉の説明は まだ作成していません.これは私が最初からこの本を読んで行って, sketches について勉強したら,書くかもしれませんし,書かないかもしれません. とりあえず,私は,最初から時間を掛けて読んで行こうと思っています.私自身の 目的意識は,計算機科学の分野の人がどうやったら圏論を効率的に学習できるかを, 自分が勉強しながら考えることで,その考察に,この本も参考にさせていただこうと思っています.
2020年4月9日(木)追記:著者の一人の M. Barr とコンタクトが取れたので,このズレを言ったら, 修正してくれました.2020年4月9日時点で TAC reprints のページのものは まだ修正されていませんが,このページの最初に挙げた M. Barr のサイトの PDF は修正が済んでいます.ただし,index からの出現ページへのハイパーリンクは なにか問題があってうまく働かないそうです.
したがって,
次のズレの表はそれ以前の版について ということになります.
インターネット上にあるすべての PDF でどうかはわかりませんが, 私の手元にある 2013-09-22 の改訂版はページの後ろの方に行くほど ズレが大きくなっています.改定を繰り返したのだけど索引のページを 生成しわすれたのかもしれません.
索引を使って用語の出現箇所を探したい人は 以下の表で見当をつけると,その付近に出現ページを見つけられるかもしれません.
用語例 | 索引のページ(A) | 実際のページ(B) | 差 (B - A) |
---|---|---|---|
GRF | 27 | 27 | 0 |
monotone function | 27 | 28 | 1 |
monic | 46 | 47 | 1 |
ufunctor | 63 | 65 | 2 |
unary operation | 99 | 101 | 2 |
linear sketch | 125 | 128 | 3 |
cartesian product | 149 | 153 | 4 |
conjunction calculus | 182 | 187 | 5 |
curry | 190 | 196 | 6 |
finite discrete cone | 214 | 221 | 7 |
topos | 377 | 385 | 8 |
symmetric monoidal category | 403 | 413 | 10 |
duality functor | 411 | 422 | 11 |
著者の方々に連絡をとって索引だけもう一度生成しなおしてもらえばよいのかも しれませんが,私はどうやって著者の方々に連絡をとればよいのか分かりません.
後日記(2020.04.01 (水)):著者の一人の M. Barr に連絡がとれたので,このことを 言ったら,索引を生成しなおすとのことでした.次の版では修正されると思います. そうしたら,この部分は消します.
圏論のトップページ