圏論の教科書の概要説明をいくつか書きましたが,各概要ページに載せると量が嵩張って 読みにくくなるような事柄がときどきあります.でも,人によってはそこまで知りたいと いう場合もあると思いますので,そのような個別のことについて書くページを作りました.
この本の概要のページは
関連ページ:Barr and Wells の圏論の概説に行くにあります.また,この本自体の PDF へのリンクに関する情報もそこにあります.
圏の定義が終わった後,早速,圏の例として関数型プログラミング言語が示されるのは, 計算機科学の学習者には嬉しいのですが,同時に,定義が終わったばかりで,それほど 高等な例が示されるはずがないという気もするでしょう.ということで, ここではどの程度の例が示されるのか見ておきましょう.
ここで示される関数型言語は,Backus-style のプログラミング言語とのことです.
関数型言語の説明としては次の図に書いたような言語が想定されます.まず,その言語には 基本的な型 (Basic Types) がいくつか定めてあります.例えば,NAT, BOOLEAN, CHAR などです. そしてそれらの型に対して,それぞれ定数の集合も定めてあります.例えば,BOOLEAN には true, false , NAT には 0, CHAR には,'a', 'b', ... などです.そして,それらの型には 基本的な演算(Basic operations)が定めてあります.例えば,BOOLEAN → BOOLEAN として真偽値を逆転する ¬(not),NAT → NAT として次の自然数をとる succ, CHAR → NAT として文字の番号(あるいはコード)を返す ord,そしてその逆に 番号を与えられて,その番号の文字を返す chr : NAT → CHAR などです.
ここで想定している言語は,これらの基本的な材料を元にして,型や演算を
作り出す手段が与えられています.それが上の図の右側の箱です.ただし,この章では
どんな手段が与えられているかは具体的には書かれていません.一般のプログラミング
言語では,複数の型を組み合わせたレコード型や同じ型のデータを沢山持つことが
できるリスト型や配列型を作る手段などが用意されます.また,言語によっては,新たな型が持つ
演算の集合を定めることで型を作り出せるものもあるでしょう.ここでは当面,そういうものを
イメージしながら読み進めてみます.こうして規定されるものが(関数型)言語
というように言語 L を規定したのですが,教科書の該当ページでは,このイメージを直接
使うのではなく,ほんの少し,追加の仮定を設けています.例えば,各型 T にはそれ自身への
データを変更しない一項演算 idT があるとか,特殊な型
このような関数型言語 L に対して,このモデル(上のプログラミング言語が言語の形式を与えるとして,その
形式の意味を与えるもの)として,次のような圏
ord・(chr・succ・ord) = ord・(chr・succ・ord・chr・ord)
などです.このように等号が成り立つ射の合成を一つに束ねたものを 改めて C(L) の射と考えます.
上のように L から圏 C(L) を作ることができます.C(L) はプログラミング言語(の形式) 自身を表している訳ではなく,それが表す意味(セマンティクス)を表しています.
これで関数型プログラミング言語を圏として見る一つの見方を説明した訳ですが, 例えば次のように,まだ,色々と解決しなければいけないことがあります.
最初の問題は「5.3 Finite products」で,二番目の問題は 「5.7 Distributive categories (Products and sums の章)」と 「14.2 Recursive categories (Algebras for endofunctors の章)」で論じられます.関数型言語の他の「5.3 Finite products」と 「5.4 Sums」で考察されます.私としては想定する関数型言語の型や演算を新たに作る 手段(最初の図の右側の箱)をもう少し明確にしないと,プログラミング言語の 意味論の圏として何が必要か分かりにくいなとも思うのですが,もしかしたら, それらも後の方の章で追々述べられるのかもしれません.
あと,ここでは直接言及されていませんでしたが,「3.5 Quotient categories」でも このプログラミング言語の例が出てきました.上で書いた「射の合成で同じになるものを 束ねる」行為が圏の商を取る行為になるという関連です.
2013-09-22 版では,2.4.3 で
s0 ≤ s1 ≤ s2 ≤ ...という特殊な形の chain であり,これら二つは異なる概念です.また, ω-chain は,列において等号が成立しても良いと言っているので, 単調関数 s : N→(P, ≤) と同一視してもよいものかもしれません. 2020年3月29日に著者の一人の M. Barr とコンタクトを取ることができたので, 他の見つけた typos と一緒にこのことを伝えると修正してくれました. ただし,私は全部に ω- を付けてくれるように言ったのですが, 列の方を,「ω-chain あるいは単に chain と呼ぶ」という具合に 修正されてしまいました.たぶん,計算機科学で出てくるのがほとんど ω-chain で,わざわざ,ω- をつけたくないなどの事情が あるのかもしれません.本来,ω-complete とすべての chain に上限が ある chain-complete は異なる概念です.でも,この修正はこの教科書のこの部分 としては整合性が取れているのでまあ良いかなと思います.これは次の版で修正が 掛かるかなと思います.
で,ここの話ですが,M. Barr に伝えたとき,ω-complete だが, chain-complete でない順序集合を示せるかなと思って, 考えたものがあるので,備忘録を兼ねてここに書いておきます. 一応,用語の定義をしておきます.
p0 ≤ p1 ≤ p2 ≤ ...が上限を持つことである.
ちなみに S ⊆ P の
あと,下で,
∅, {∅}, {∅ {∅}}, ...,というように,∅ から始めて,それまで出来たものすべての集合を 次々に作っていったものを言います.こういう順序数の生成は,有限集合,可算集合, は非可算集合という具合にいくらでも続けることが出来ます.詳しくは集合論の 本を参照してください.この順序数には x ≤y iff x⊆y で順序を導入 することができます.
上の定義のもとには,当然 chain-complete なら ω-complete です.
それで ω-complete だが chain-complete でない順序集合のイメージは 次のようなものです.
このような例 (P, ≤)としてはあまり構成的ではないですが,次のものがそうです. これは上の図で,「?」のところを最初の非可算順序数として,それより小さい順序数 だけを集めたものです.
とすれば,P 自身は全順序集合で,P の任意の ℵ0 個の点列 Ni i=0, 1, 2, ... に対して, (∪i=0,1,2,...Ni)∈P がその上限になるが, P 自身の(順序数全体の中の)上限は最初の非可算な Von-Neumann 順序数になり,P には入っていません.
これで反例になっていると思います (^^;)
もう少し構成的で直感的なものが取れるような気がしたのですが,結構難しくて,とりあえず, これにしておきます.
参考までに,もうひとつ,complete を次のように定義します.
[Proof]
X := ∪i=0,1,2,...Xiと置けば,Xi それぞれが可算集合であり,それらの可算個の和も可算集合になるため,X は Rの可算集合であり,X∈P0(R) となり,これが {Xi} の上限になる.
[Q.E.D.]
ということで,こちらはかなり直感的に分かりやすい例になっていると思います.
第4章の終わりの方から sketches という概念がでてきます.これはこの本の特徴だそうで,具体的には以下の箇所に現れます.
4.6 Linear sketches (graphs with diagrams)
4.7 Linear sketches with constants: initial term models
7 Finite product sketches
8 Finite discrete sketches
10 More about sketches
11 The category of sketches
4章を読むと,どうも,sketch とは,次の図のように, 表現したい数学的構造を次の二つのペアで表現したもののようです.
上図の左側が sketch です.sketch S は数学的構造の仕様に あたります.sketch S のグラフ部分 G から 何らかの圏 C への準同型 F があれば,圏 C は 表現したい数学的構造をその一部分に含むものになっている訳です.つまり, その圏は,与えられた sketch の「モデル」になっている訳です.
可換図式を与えるときに使えるものによって,sketch の表現力は変わってきます. この教科書では,それを小出しに説明していっています.最初は 本当に可換図式の集まりだけで,それだと一項演算を持った構造だけが表現できて, 次は,それに定数を使って良いようにして,自然数などが表現できるようになります. これらが,4.6 と 4.7 の内容です.この範囲の表現力だと,基本的に一項演算を持つ 構造しか表すことはできません.教科書の中の位置としても,第5章の products and sums の前であり,n 項演算の表現のために必要な products を学習 していないのです.ということで,第5章より後に,順次,product まで表現力を 強化した sketches とか,さらに色々表現力を増やしていった sketches のことが 説明されます.
7章の扉の最後に sketches の概念の生まれについて書いてあります. sketches はフランスの Charles Ehresmann によって考え出されて,その学生が 発展させたそうです.彼らのフォーマリズムはここで書いているのとは違うとのことです. それについては以下の文献に書いてあるとのこと.
Bastiani, A. and C. Ehresmann (1972). ‘Categories of sketched structures’. Cahiers de Topologie et Géométrie Différentielle, volume 13, pages 104.213. (219, 307, 311)また,それらの現代的な記法は次の文献を見よとのことです.
Coppey, L. and C. Lair (1984). ‘Le,cons de théorie des esquisses’. Diagrammes, volume 12. (219)Coppey, L. and C. Lair (1988). ‘Le,cons de théorie des esquisses, partie II’. Diagrammes, volume 19. (219)
圏論のトップページ