【翻訳】計算機科学における圏論利用のためのマニフェスト（カテゴリカル・マニフェスト）

翻訳にあたって

圏論よくわからないけどDeepL翻訳で雑に訳しました。後半あたりからより雑になってます。
読んでも意味が分からないところは意味わかってないです。聞かれてもよくわかりません。
自分の方がうまく訳せるという人はどうぞ。
おかしなところがあればコメントまで。後々こまごまと直すかもしれません。

世にある圏論ニーズ（あるのか？）からは、はずれている内容です。
厳密に数学の圏論やりたい人は読んでもあんまり意味ないと思います。

この論文で大事なところ

数学的でない直観的な圏論概念の説明が与えられているので、この語彙を流用できます。
例：構造の種（species of struture）、構成（construction）、自然な翻訳（natural translation）、制約の系（system of constraints）など。
もちろん、数学系の人には嫌がられます。

カテゴリカル・マニフェスト（Categorical Manifesto）

著：ジョセフ・A.ゴーグエン（Joseph A. Goguen）

画像元Wikipedia:ジョセフ・ゴーグエン

原文１：A Categorical Manifesto（1991版）（こちらを底本とした）
原文２：A Categorical Manifesto（1989版）

概要

　本論文は、5つの基本的な圏論の概念（圏、関手、自然変換、随伴、そして余極限）の適用に関する発見的な指針を与えることによって、計算機科学における圏論の使用を動機づけることを試みるものである。7つの例といくつかの一般的な議論は各概念に対して与えられており、多数の参考文献が引用されている。ただし、完全なものを作ろうとは試みられていない。いくつかの追加的な圏論の概念とさらなる研究のための提案も述べられている。本論文は基礎に関するいくつかの示唆について簡潔に論じて終わる。

0 導入

　本論文は、圏論がなぜ計算機科学で有用であるのかという点について説明を試みるものである。基本的な答えとしては、計算機科学は急速に成長している若い分野であり、組織化も不十分で、あらゆる助けを必要としており、そして圏論は少なくとも次のような点で助けを提供することができる。

• 定義と理論の定式化
  計算機科学では、しばしば証明を与えることよりも、概念や結果を定式化することの方が難しいことがある。本論文の７つの指針は定式化の助けになる。また、既存の定式化のエレガンスさと一貫性を測るにあたっても使用することができる。
• 証明の実行
  いったん基本概念が圏論的言語で正しく定式化されると、しばしば証明が「まさに発生」したかのようになる。すなわち、各段階で、試すべき「自然な」ことがでてきて、しかもうまくいく。図式追跡（diagram chasing）は（１．２節を見よ）、この例を多く示している。圏論の目的は、すべての証明をこのような単純な計算に還元することであると言ってもいいくらいであろう。
• 他分野との関係の発見と開拓
  十分に抽象化された定式化は、意外なつながりを明らかにすることができる。例えば、ペトリネット（Petri nets）とλ計算の間のアナロジーは、ペトリネットの圏における閉圏構造（a closed category structure）を探すことを示唆するかもしれない。
• 抽象と表現の独立性の取り扱い
  計算機科学においては、より抽象的な視点の方が有用であることの方が多い、というのも、物事がどのように表現されるまたはどのように実装されるかという、しばしば圧倒的に複雑となる詳細から独立させる必要があるからである。最初の指針（１節で与えられる）から導かれる一つの系は、２つの対象が「抽象的に同じ（abstractly the same）」であるとはそれらが同型であるときでありかつその時に限るということである。１．１節を見よ。さらに、普遍的構成（universal construction）（すなわち、随伴）はそれらの同型を除いて一意的な結果（their results uniquely up to isomorphism）を定義する。これはすなわち、まさにこの意味において「抽象的（abstractly）」であるということである。
• 予想と研究の方向性の定式化
  他分野とのつながりは、自分の分野における新しい問いを示唆してくれる。また、７つのは研究の指針となる。例えば、あなたが興味深い関手を見つけたならば、次はその随伴を調査するよう助言を受けることになるだろう。
• 単一化（unification）
  計算機科学は非常に細分化されており、それぞれ多くの学派を伴う多くの異なるサブの規律がある。それゆえに、圏論が示すような概念的単一化がどうしても欲しいのである。

　圏論は乱用もされることがある、しかもいくつかの異なるスタイルで。乱用のスタイルの一つ目は、見せかけの一般性（specious generality） である。この乱用においては、理論または例が、実際には純粋に興味深い新しい例をなんら含まない形で一般化される。関連する乱用のスタイルは、圏論的過剰（categorical overkill） である。この乱用においては、圏論の言葉は、実際にはそのような精巧な扱いや用語を必要としないような現象を記述するために用いられる。一つの例としては、ガロア接続（Galois connection）を随伴関手の言葉で記述するというものがある。

　圏論は、友好派と否定波の両方からずっと「抽象的無意味（abstract nonsense）」と呼ばれてきた。おそらくこの言葉が両者に示唆しているのは、数学の他の分野に比べて、圏論は内容よりも形式が比較的多いということであろう。集合論的基礎に根ざした過剰な具体性と表現及びそれらが提供するエレガントかつ一貫した理論を発見するのに適した指針が比較的乏しいことと比較して、友好派はこれを美徳であると主張する。９節においてさらに論じる。

集合論的基礎の過剰な具体性と表現依存性，そしてそれらが提供するエレガントで首尾一貫した理論8を発見するための相対的に貧弱な指針とは対照的に，その友人たちはこれを美徳として主張する．第9節では、この点についてさらに論じる。

　圏論は非常に具体的な方法でも使用することができる。なぜならば、圏は結局のところ単なるもう一つの代数構造であり、モノイドと半順序関係を一般化するものであるからである（例題１．４以下も参照せよ）。

　本論文では、圏論を使うための７つの指針を、それぞれいくつかの一般的な議論と具体的な例とともに紹介する。独創性は主張しない。というのも、その根底にある直観は、本質的に圏論に従事するすべての研究者によって共有されている、と信じているからである、とはいえ、教科書やそのほかの文書¹にそのようなドグマ的な主張を掲載することに消極的であることは当然かもしれない。指針は必然的に不正確なものである、文字通り捉えすぎると誇張されたように見えるだろう。というのも、指針は客観的な事実というよりもむしろある種の数学的な概念を適用するための発見的なものであるからである。特に、状況によっては適用が困難、あるいは不可能に思えるかもしれない。また、指針は他の場面では改良が必要になるかもしれない。指針をあまりにもドグマ的に捉えるべきではないという戒めも込めて、私は指針をドグマと呼ぶこととする。

　網羅的であろうとはしていない。特に、技術的な定義は省略した。なぜなら、目的は直観を提供することであり、定義はどんな教科書にも載っているからである。したがって、もしあなたが圏論の初心者ならば、この論文に関連して何らかのテキストを使う必要があるだろう。残念ながら、既存のテキストで計算機科学に適した理想的なものはないが、ひょっとしたらGoldblattによるもの[36]が最も近いだろう。マックレーン（Mac Lane）による古典的なテキスト[47]は十分な数学的素養のある人には暖かく勧められるし、HerrlichとStreekerの本[39]は見事に徹底している。また、[2]と[45]を見よ。論文[22]は、計算機科学者のための基本的な圏論について比較的具体的かつ自己完結的な説明を与えている、理論、方程式、単一化を動機として用いながら。この論文からの多くの例は、本論文でも用いられている。

1 圏（Categories）

最初のドグマは次のとおりである。

それぞれの数学的構造の種（species of mathematical structure）に対応する一つの 圏（category） が存在しその対象はその構造を持ちその射はその構造を保存する。

ある構造を理解するためには、それを保存する射を理解する必要がある、というのがこの指針の不可欠な要素である。実際、圏論家は対象よりも射の方が重要であると主張してきた。なぜならば、構造の本質を明らかにするからである。さらには、圏概念は射の概念だけから定義することができる。おそらく現代西洋の言語と文化が関係性よりも対象に偏っていることがこれを物語っている（関連する議論については[50]、[64]参照。）。表記法として、";"を合成に1_Aを対象Aにおける恒等射として用いる。次にいくつかの例を挙げる。

1.1 集合（Sets）

集合を対象とするならば、その射は明らかに関数となる。しかしながら、集合射は単なる順序対の集合ではない。なぜならば、特定の定義域と値域の指定もしなければならないからである。これは、関数に型を割り当てる計算理論の実践と一致している。関数の集合論的表現は、数学の集合論的基礎の産物であり、そのような表現がすべてそうであるように、それが捕らえようとする概念を超えた偶発的な性質を持っている。その特性の一つは、任意の２つの順序対の集合を合成して３つ目の集合を生成することができるということである。集合の圏 ${\it Set}$ は、それとは逆の視点を体現している。それは、各関数はその引数が意味を有するドメイン、返り値が意味を有するコドメインを持ち、関数の合成はこの意味で意味を有するときのみ許されるというものである（関連する議論は[36]を参照）。

1.2 関係（Relations）

関数の場合と同様に、関係の合成はドメインが一致する場合にのみ意味を持つという見解が望ましいと思われる。したがって、集合 $A_0$ から集合 $A_1$ への関係とは、$R \subseteq A_0 \times A_1$ である三つ組 $(A_0, R, A_1)$ と定義してもよいなら、$(B_0, S, B_1)$ とは、$A_1 = B_0$ の場合かつそのときに限り合成を定義することができる。これにより、${\it Rel}$ と呼ぶ圏が生じ、${\it Set}$ はその部分圏とみなすことができる。

1.3 グラフ（Graphs）

グラフ $G$ は 辺（edge） の集合 $E$、ノード（node） の集合 $N$、そして各辺の 始域（source） と 終域（target） のそれぞれを与える２つの関数 $\partial_0, \partial_1: E \rightarrow N$ から構成される。グラフの主要素は集合であることから、それらの射の主要素は追加の構造を保存する関数に対応させる必要がある。したがって、$G=(E,N,\partial_0,\partial_1)$ から $G'=(E',N',\partial'_0,\partial'_1)$ への射は、以下の $i = 0,1$ の場合の ${\cal Set}$ の可換図式を満たすような２つの関数 $f: E \rightarrow E'$ と $g: N \rightarrow N'$ から構成される。

グラフの圏 ${\cal Graph}$ があることを示すには、そのような２つの射の合成がまた別の射となること、恒等関数の組が図式と合成における恒等射（identity）としても機能することを示す必要がある。

1.4 グラフにおける道（Paths in a Graph）

グラフ $G$ が与えられたとき、$G$ 内の各道（path）は、$G$ 内の始域ノードと終域ノードを持ち、２つの道 $p$ と $p'$ は、$p'$ の始域と $p$ の終域が等しいときかつそのときに限り、もう一つの道 $p;p'$ を形成するように合成させることができる。この合成は、定義された時点で、結合的（associative）であることは明らかであり、各ノードには、辺を持たない「恒等道（identity path）」を与えることができる。この圏は、${\cal Pa}(G)$ と表記される（詳細は、[47]、[34]、[19]などにある）。

1.5 オートマトン（Automata）

オートマトンは、入力集合 $X$、状態集合 $S$、出力集合 $Y$、追跡関数 $f: X \times S \rightarrow S$、初期状態 $s_0 \in S$、そして出力関数 $g: S \rightarrow Y$ から構成される。これらの構造をすべて保存するとはどういうことだろうか。オートマトンの主要な構成要素は集合であるから、これらの射の主要な構成要素は、その構造を保存する関数でなければならない。したがって、$A = (X,S,Y,s_0,f,g)$ から $A' = (X',S',Y',s'_0,f',g')$ への射は、以下の ${\cal Set}$ の中の可換図式を満たす $h : X \rightarrow X'$、$i : S \rightarrow S'$、そして $j : Y \rightarrow Y'$ の三つの関数で構成されなければならない。

ここで、$\lbrace \ast \rbrace$ は任意の１点集合（点 $\ast$ を持つ）を表す。このような2つの射の合成が、別のものであり、恒等射の三つ組が図式を満たし、合成にあたっての恒等射として機能することが示されなければならない。これら確認は、オートマトンの圏 ${\cal Aut}$ があることを示しており、その単純さは、定義[18]の正しさに対する信頼性を高めている。

1.6 型（Types）

型は、「もの（thing）」を分類するために使われるものであり、第一のドグマに従えば、型を対象として持つ圏を形成するはずである。もちろん、何を分類するかによって、異なる圏が生じることになる。
単純な例は、有限積型（finite product type）である。これは自然数によって簡単に表現され、「レジスタ」のタプル間の「レジスタ転送操作（register transfer operation）」とでも呼ぶべきものを記述する射を持つ。したがって、$n \in \omega$ は、n 「レジスタ」のn個のタプル $$ からなるデータ項目を示し、射 $f : m \rightarrow n$ は、関数 $\lbrace 1,...,n \rbrace \rightarrow \lbrace1,...,m\rbrace$ のことであり、これは $i = 1,...n$ に対して、レジスタ $f(i)$ の内容がレジスタ $i$ に転送されるはずであることを示している。実際、数 n を集合 $\lbrace 1,...,n \rbrace$ （0 は $\varnothing$）と同一視すると、この圏は、${\cal Set}$ の部分圏の逆圏であり、これを ${\cal N}$ と表記する。${\cal N}$ の変形は、その対象として、固定された可算集合 $X$ の有限部分集合を持ち、また射として、これらの間の関数の逆象（opposite of functions）を持つので、${\cal Set}$ の部分圏のまた別の逆圏が得られ、${\cal \chi}$ と表記する。ここで「レジスタ」は、自然数ではなく、$X$ からの「変数記号（variable symbols）」で表記される。少し先に進んで、集合 $S$ からのソート（sort）を $X$ の記号に割り当て、射がこれらソートを保存することを要求することができる。この圏を ${\cal \chi}_S$ と表記しよう。

1.7 代入（Substitutions）

代入の２つの重要な属性は、代入する変数の集合と、代入するものの中に出現する変数の集合である。したがって、上記の例1.6のように、代入は、変数の集合である自然な始域である対象と終域である対象をそれぞれ持つ。各変数集合に対して恒等代入（各変数をそれ自身に置換するもの）が存在することは明らかである。そして、代入の合成は、定義されているとき、結合的（associative）である。したがって、代入を射とする圏が得られる。

1.8 理論（Theories）

F. W. Lawvereは、1963年の論文[49]で、普遍代数に対する非常にエレガントなアプローチを開発した。このアプローチでは、代数的理論（algebraic theory） は、上記の例1.6のように、その射が項の同値類に対応し、その対象がこれら項に関係する変数を示している圏 ${\tt T}$ であると定義される。このアプローチでは、理論は有限積（finite products）（以下の例4.1のなかで定義されているように）のもとで閉じている。Lawvereのオリジナルはソートの無いもの（unsorted）だったが、これは多ソート（many-sorted）の場合にも容易に拡張でき、Ehresmann、Gray、Barr、Wellsなどによって研究されたいわゆる「スケッチ（sketch）」にも拡張できる。例えば、[3]を参照せよ。もちろん、与えられた種類の理論はすべて圏を形成する。

1.1 同型射（Isomorphism）

非常に単純ではあるが、それでもなお重要な圏論の果実の一つが、とにかくあらゆる構造の種に適合する同型射（isomorphism）の一般的な定義である。つまり、射 $f: A \rightarrow B$ が圏 ${\cal C}$ で 同型射 であるとは、圏 ${\cal C}$ $g;f = 1_A$ かつ $f;g = 1_B$ となるようなもう一つの射 $g: B \rightarrow A$ が存在するときかつその時に限るというものである。この場合において、対象 A と B は同型（isomorphic）である。これは抽象代数学でうまく確立された原理であり、今では他の分野でも同様である。同型な対象は抽象的に同じであり、もしくは、より正確には次のようになる。

２つの対象が同じ構造を持つのは、それらが 同型（isomorphic） であり、「抽象対象」が、対象のクラスと同型である場合そのときに限る

この半ドグマは、第一のドグマの系（corollary）とみなすことができる。これである構造が正しく形式化されているかどうか即座に確認することができる。これが満たされない限り、対象か射かそれとも両方が間違っていることになる。この原則は非常に広く浸透しているため、同型の対象はしばしば同じものとみなされ、$X$ が実際に同型を除いて一意的とだけ定義されているとき「an $X$」の代わりに「the $X$」が使われることになる。計算機科学の分野では、この原則は、[33]における「抽象データ型（abstract data type）」の正しい定義の探索を成功に導いた。

1.2 図式追跡（Diagram Chasing）

問題、定理もしくは証明の概要をつかむのに便利な方法は、主たる対象と射が関わる一つ以上の図式を描くことである。p と p' が同じ始域（source）と終域（target）を持つ道（path）であり、これら２つの道に沿った射の合成が等しいときかつそのときに限り、その図式は可換である。２つの可換図式を共通の辺に沿って貼り合わせると、別の可換図式が得られるという事実は、合成の等価性に関する純粋に図式的様式の推論の基礎を提供する。どのような圏の図式についても妥当であることから、この証明様式は非常に広く適用できる。例えば、（例1.5のように）置換（substitutions）にも適用できる。さらに、押し出し（pushout）、射の一意性、その他の一般的な状況にも適用できるよう拡張されている。多くの場合、証明は、既知のものと証明されるべきものの図式を単に描くことによって提案される。例1.3の簡単な例は２つのグラフ射の合成が別のグラフ射であることを証明するものである。

2 関手（Functors）

第二のドグマは次のとおりである。

もう一つの種の構造（structure of one species）から発生してくる、そのもう一つの種の構造に関わる何か自然な構成（natural construction）に対応するこの第一の種の圏から第二の圏への 関手（functor） が存在する。

構成（construction）は、単なる一方の種の対象から他方の種の対象への関数ではなく、対象間の本質的な関係も保存しなくてはならない（構造を保存する射と、それら射について合成と恒等射を含む）、というのがこのドグマの不可欠な要素である。これにより、その構成が適切に形式化されているかどうかをテストすることができる。もちろん、関手性（functoriality）は、正しい定式化を保証するものではないが、実際には驚くほど役に立つ。次にいくつかの例を挙げる。

2.1 自由モノイド（Free Monoids）

計算機科学では、集合 $X$ 上の自由モノイド $X^\ast$ を構築することはよくある。これは、空文字列 $A$ を含む、$X$ のすべての有限文字列 $x_1,...x_n$ で構成される。この構築は、集合の圏からモノイドの圏への関手を与える。この関手は、$A$ を $A$ に送り、$x_1...x_n$ を $f(x_1)...f(x_n)$ に送ることで、関数 $f: X \rightarrow Y$ は $f^\ast : X^\ast \rightarrow Y^\ast$ を誘導する。この関手は、関数型プログラミングの世界では、「多相リスト型構築子」と呼ばれる。

2.2 振る舞い（Behaviours）

オートマトン $A = (X,S,Y,f,g)$ が与えられたとき、その 振る舞い（behaviour） は、$b(u) = g(\bar{f}(u))$ で定義される、$X$ 上のすべての文字列のモノイド $X^\ast$ から $Y$ への関数 $b : X^{\ast} \rightarrow Y$ である。ここで、$\bar{f}$ は、$\bar{f}(A) = s_0$ と $\bar{f}(ux) = f(x,\bar{f}(u)), x \in X , u \in X^\ast$ によって定義される。この構成は関手的でなければならない。そのためには、振る舞いの圏が必要である。明らかな選択は、その対象を組 $(X,b : X^\ast \rightarrow Y)$とし、$(X, b : X^\ast \rightarrow Y)$ から $(X',b' : X'^\ast \rightarrow Y')$ への射を組 $(h,j)$ とすることである。ここで、$h : X \rightarrow X'$ と $j : Y \rightarrow Y'$ は、${\cal Set}$ の以下の可換図式を満たすものである。

この圏を ${\cal Beh}$ とし、$B : {\cal Aut} \rightarrow {\cal Beh}$ を $B(X,S,Y,f,g) = g; \bar{f}$ と $B(h,i,j) = (h,j)$ で定義する。これが関手であることは、前述の定義のエレガントさと一貫性を確認するのに役立つ。[18]を参照せよ。

2.3 モデル（Models）

Lawvereの普遍代数へのアプローチ[49]では、代数は、理論 ${\sf T}$ から ${\cal Set}$ への関手である。ここで、「構成（construction）」は、「解釈（interpretation）」の意味を持つ。${\sf T}$ の抽象構造は ${\cal Set}$ の中で具体的に解釈される（つまり、構成される）。すなわち、これらの関手は有限積を保存しなければならない。より一般的には、${\sf T}$ がある種の理論である場合、${\sf T}$ の「モデル」とは、これら理論の構造（例えば、有限積）を保存する関手 $M: {\sf T} \rightarrow {\cal Set}$ である。さらに一般的には、${\sf T}$ 有限積を持つ適当な圏 ${\cal C}$ における ${\sf T}$ のモデルを、有限積を保存する関手とすることができる。例えば、多ソート代数（many-sorted algebra）は、型システム ${\cal \chi}_S$ 上の理論から関手として生じる。例1.5は、$S$ が３つの要素を持つとすることで、この例としてみることができる。

2.4 忘却（Forget It）

もしすべてのウィジェットが”あれ”であるならば、ウィジェットの圏から”あれ”の圏への「忘却関手（forgetful functor）」が存在する。例えば、すべての群は、逆演算を忘れることでモノイドになり、すべてのモノイドは、単位元を忘れることで半群になる。（単位元をもつ）環は、加法構造に対してかと乗法構造に対してかの ２つの異なる方法（two different way） でモノイドになることを注意せよ。

2.5 圏（Categories）

もちろん、（小さい）圏もまた関手を射として圏をなす。これは ${\it Cat}$ と表記される。

2.6 図式とその道の圏の構成（Diagrams and the Path Category Construction）

例1.4で行った、グラフ $G$ のすべての道（path）の圏 ${\cal Pa}(G)$ の構築は、グラフから圏への関手 ${\cal Pa}: {\cal Graph} \rightarrow {\cal Cat}$ を生み出す。そして、グラフ $G$ の 形（shape） を持つ圏 ${\cal C}$ の 図式（diagram） は、関手 $D: {\cal Pa}(G) \rightarrow {\cal C}$ である。これは単に $D: G \rightarrow {\cal C}$ と書くのが一般的であり、$D$ を「関手」と呼ぶことさえもある。なぜならば、$D: {\cal Pa}(G) \rightarrow {\cal C}$ は、実際には、グラフ射である $G$ への制限によって充分に決定されるからである。以下の例6.2を参照せよ。

2.7 プログラムとプログラム・スキーム（Programs and Program Schemes）

並列代入（parallel assignment）、go-to、および任意の関数とテストを含む任意の組み込みデータ構造を持つ非決定的フロー図プログラム $P$ は、グラフ $G$（プログラムの「形（shape）」）から、対象を集合、射を関係とする圏 ${\cal Rel}$ への関手とみなすことができる。$G$ の辺（edge）$e: n \rightarrow n'$ はプログラム・ステートメントに対応し、関係 $P(e) : P(n) \rightarrow P(n')$ がその意味論を与える。例えば、自然数における「${\tt if \ X > 2}$」というテストは、${\tt X > 2}$ であるときかつそのときに限り定義される部分恒等関数 $\omega \rightarrow \omega$ に対応し、代入（assignment）「${\tt X := X - 1}$」は、${\tt X > 0 }$ のとき ${\tt X}$ を ${\tt X - 1}$ に送る部分関数 $\omega \rightarrow \omega$ に対応する。入力ノード $n$ と出力ノード $n'$ を持つ $P$ の 意味論（semantics） は、次の式で与えられる。

$P(n,n') = \bigcup\lbrace P(p) | p : n \rightarrow n' \in {\cal Pa}(G) \rbrace$

このアプローチは、Burstasllに由来する[5]。プログラムが意味論だけでなく構文を持つことを可能にする技法は[19]に記述されている²。プログラム・スキーム（program scheme） は、その射集合 ${\tt T}(A,B)$ について半順序構造で「豊穣化（enriched）」させた理論 ${\tt T}$ への関手 $P : G \rightarrow {\tt T}$ である（2-圏に詳しい読者は、これにより ${\tt T}$ が 2-圏になることに注意されたい）。ステートメントの意味論は、関手 $A : {\tt T} \rightarrow {\cal Rel}$ 、すなわち ${\tt T}$ の解釈、または ${\tt T}$-代数とよばれるものを与えることによって生じる。プログラムの意味論は、合成 $P;A : G \rightarrow {\cal Rel}$ についての上記式によって計算される。この分野ではより多くの研究ができるように思われる。例えば、[29]は、相互に再帰的な手続の集まりに対する帰納的な証明原理を与えており、同様の設定で他のプログラムの構成を考察することは興味深い。

2.8 理論解釈（Theory Interpretation）

例2.3の議論を拡張すると、理論 $T'$ における理論 $T$ の「解釈（interpretation）」は、理論構造（たとえば、型や有限積）を保存する関手 $F: T \rightarrow T'$ であるべきである。このような関手は、理論射（theory morphisms）として同じものである。特に、プログラム・スキーム（もちろんプログラムである）の解釈は、このようにして生じる。

2.9 多相型構築子（Polymorphic Type Constructors）

関数型プログラミング言語の型を、${\tt Int}$ や ${\tt Bool}$ のような対象をもつ圏 ${\cal T}$ を形成しているものと考えるとき、${\tt list}$ のような多相型構築子は、${\cal T}$ 上の自己関手、つまり、関手 ${\cal T} \rightarrow {\cal T}$ となる。それ以外のものとしては、${\tt set}$ と ${\tt list \times list}$ があるだろう。ここで、後者は、型 $\alpha$ を型 ${\tt list}(\alpha) \times {\tt list}(\alpha)$ に送っている。

3 自然性（Naturality）

第三のドグマは次のとおりである。

構成 $F: {\cal A} \rightarrow {\cal B}$ から構成 $G: {\cal A} \rightarrow {\cal B}$ へのそれぞれの自然な翻訳（natural translation）に対応する 自然変換（natural transformation） $F \Rightarrow G$ が存在する。

これは「自然な翻訳」という言葉の単なる定義のように見えるが、それにもかかわらず実際には非常に有用である。この概念は圏論の歴史的起源であるということも興味深い。アイレンバーグ（Eilenberg）とマックレーン（Mac Lane）[11]は、この概念を用いてホモロジー理論の同値性を定式化し、次にこの定義を意味をなすためには関手を定義しなければならず、関手が意味をなすためには、圏を定義しなければならないということを発見した（この歴史はなぜホモロジー理論がこうも頻繁に圏論的なテクストの中に現れるのか、そしてそれゆえに、なぜその多くが計算機科学者には不向きであるのかということを説明するものでもある）。次にいくつかの例を挙げる。

3.1 準同型射（Homomorphisms）

既に述べたように、普遍代数（universal algebra）に対するLawvereのアプローチにおいては、代数とは関手であり（algebras are functors）、準同型射は自然変換であることを期待すべきである。そして、実際にそうである。

3.2 自然同値（Natural Equivalence）

自然変換 $\eta: F \Rightarrow G$ は、各 $\eta_A: F(A) \rightarrow G(A)$ が同型射であるときかつそのときに限り自然同値（natural equivalence）となる。これは関手に対する同型の自然な概念であり、$\nu;\eta = 1_F$ であり $\eta;\nu = 1_G$ であるような $\nu: G \Rightarrow F$ の存在と同値である。これはまさにアイレンバーグ（Eilenberg）とマックレーン（Mac Lane）を動機づけた概念であり、例3.1の文脈において、代数の同型を特殊化させている。

3.3 データ詳細化（Data Refinement）

ノード（node）を型、辺（edge）を関数記号でラベル付けしたグラフは、方程式を持たず、２つ以上の引数を持つ関数記号を持たない貧弱なLawvere理論とみなすことができる。しかしながら、このような理論でも、代数（algebra）は成立する。ここで代数とは ${\cal Set}$ への関手であり、準同型射はもちろん自然変換である。これら代数はプログラミング言語の基本的なデータ型や関数の データ表現（data representation） とみなすことができ、それらの準同型射は データ詳細化（data refinement） とみなすことができる。言語の基本的なプログラム構築操作と結び付けて考えると、これは正しいプログラムを開発するための一般的な技術につながる[40]。これをLawvere理論のより一般的な変形（多ソート理論（many-sorted theory）やスケッチ（sketch））や、抽象データ型の文献（[33,9]など）で研究されているより一般的なデータ表現に拡張するということは興味深い。

3.4 プログラム準同型射（Program Homomorphisms）

例2.7はプログラムを関手として定義しているので、プログラム準同型射はプログラム間の自然変換であることが期待される。実際、Burstall[5]は、Milnerのプログラムシミュレーション[53]の弱い形がまさにこの方法で生じることを示している。[19]では、$P_0: G_0 \rightarrow C$ から $P_1: G_1 \rightarrow C$ への準同型を関手 $F: G_0 \rightarrow {\cal Pa}(G_1)$ と自然変換 $\eta : P_0 \rightarrow F;P_1$ で構成されるように定義することで、これを異なる形を持つ可能性のあるプログラム、辺（edge）から道（path）への写像に一般化している。これに関するいくつかの理論と応用は[19]にも与えられており、正当性の証明、停止（termination）、等価性（equivalence）の手法が含まれる。これは等価な無限木にプログラムを展開することによって行われる。

3.5 多相関数（Polymorphic Functions）

もし多相型構築子が、（例2.8のように）関手であるなら、多相型関数は自然変換であるべきであるし、実際そうである。例としては、

append : list list -> list

と

reverse : list -> list

がある。

3.6 関手圏（Functor Categories）

${\cal A}$ と ${\cal B}$ を圏とする。そのとき、${\cal Cat}[{\cal A, B}]$ と表記される圏があり、その対象は${\cal A}$ から ${\cal B}$ への関手であり、射は自然変換である。特に、${\sf T}$ が理論であるならば、${\sf T}$-代数は ${\cal Cat}[{\sf T},{\cal Set}]$ の部分圏である。

4 極限（Limits）

第四のドグマは次のとおりである。

圏 ${\cal C}$ の 図式（diagram） $D$ は制約の系（a system of constraints）とみることができる。そして、$D$ の 極限（limit） はその系の取りうるすべての解を表現している。

特に、図式がいくつかの物理的（または概念的）システムを表現しているならば、極限はそのシステムの与えられた制約と矛盾しないすべての取りうる振る舞いを表現する（その射影射も含めた）対象を提供する。この直観は、1969年-74年にかけての一般システム理論（General System Theory）に関するいくつかの研究[16,27]に遡り、計算機科学において多くの応用がある。

4.1 積（Products）

圏論の初期の成果は、「積（product）」という概念に正確な定義を与えることであった。この概念は、それまでは多くの特殊な場合において知られていたが、一般的な概念としては漠然と理解されていただけであった。この定義はマックレーン（Mac Lane）[46]によるものである。

4.2 直積型（Product Types）

型 $T_1$ と $T_2$ が与えられたとき、それらの「並列合成（parallel composition）」は、型の圏 ${\cal T}$ におけるそれらの積である。したがって、射 $f : T_1 \times T_2 \rightarrow T$ は、型 $T_1$ と $T_2$ の２つの「入力（input）」を並列にとり、型 $T$ の１つの出力（output）を返す。ある種の理論の定義に使われる型の圏は、通常 $1$ と表記される空積（empty product；要素の無い積、つまり終対象）も含んでいる有限積を持つと仮定するのが普通である。${\cal N}$ と ${\cal \chi}$ の両方とも、${\cal Set}^{op}$ の部分圏であり、それらの積は、${\cal Set}$ における分離和（disjoint union）である。

4.3 理論（Theories）

（有限積を持つと仮定される）型システム ${\cal T}$ 上の 一般化されたLawvere理論 ${\sf T} : {\cal T} \rightarrow {\cal A}$ は、対象について全射的（surjective）でありつつ有限積を保存する ${\cal T}$ から有限積を持つ圏 ${\cal A}$ への関手である。「退化的（degenerate）」な場合を除き、理論 ${\sf T} : {\cal T} \rightarrow {\cal A}$ は、対象について全単射的（bijective）であり、$|{\cal T}| = |{\cal A}|$ でありかつ ${\cal T}$ は ${\cal A}$ の部分圏であると仮定できる。すなわち、${\sf T}$ と ${\cal A}$ は同一視できるかもしれない。

${\cal T}$ 上の理論の 射（morphism） とは、有限積を保存しつつ ${\cal T}$ も保存する関手である。理論 ${\sf T} : {\cal T} \rightarrow {\cal A}$ の 代数（algebra） とは、${\cal Set}$（または、より一般的には、有限積を持つ圏 ${\cal C}$）への有限積保存関手である。もちろん、${\sf T}$-代数の 準同型射（homomorphism） とは、自然変換であり、${\sf T}$-代数の圏を与える。${\cal T} = {\cal N}$ のとき、Lawvere形式の、古典的な無ソートの一般代数（classical unsorted general algebra）を得る。${\cal T} = {\cal \chi}$、ここで ${\cal \chi}$ は $S$-ソートとする、のとき、$S$-ソートの一般代数（S-sorted general algebra）を得る。[22]では、一般化されたLawvere代数の合同（congruence）と商（quotient）についても論じている。

4.4 方程式と単一化（Equations and Unification）

理論における射の組 $f,g : T \rightarrow T'$ は、方程式（equation） として考えることができる。次に、第４のドグマによって、この方程式の最も一般的な解は、$f$ と $g$ の イコライザ（equaliser） が存在すれば、そのイコライザによって得られる。無ソート（unsorted）の無秩序な（つまり法則に従わない）理論といった古典的な場合において、射は項（term）であり、イコライザは ほとんど一般的な単一化子（most general unifier） を与える。単一化のより一般的な種類は、より一般的な種類の理論にすることで生じる。例えば、理論のいくつかの操作について結合則（associative law）と可換則（commutative law）を課すと、いわゆる AC-単一化（AC-unification）が導かれる。いくつかの理論では、弱いイコライザ（weak equaliser） しか見つけることができない。これらイコライザは、「一意的な射が存在する」という要件を単なる存在に弱める。実際、弱いイコライザは、単一化子（unifier）の古典的な定義を形式化したものであり、それにもかかわらず、実践的にはより強い条件が満たされることが多い。再び一般化すると、制約の系（system of constraints）は、理論の中における図式であり、そのほとんど一般的な解法は、極限が存在すれば、その極限によって得られる。

この状況には多くの例があります。連立一次方程式の解法、多相型推論、言語学における「単一化文法（unification grammar）」の意味での単一化、Scott領域方程式の解法、そして最小不動点です。これらすべての例（およびその他のいくつかの例）は、[22]でより詳細に説明されており、単一化子が存在することを証明するためのいくつかの技法も紹介されている。もう一つの例は、プログラムの意味論についての例2.7の式の正当化である。

5 随伴（Adjoints）

第五のドグマは次のとおりである。

片方の構造の種からもう一方への任意のカノニカルな構成に、対応する圏の間の 随伴（adjunction） が対応する。

これはまさに「カノニカルな構成」の定義のように見ることができるが、実際には非常に有用である。随伴の本質は、その値対象（value objects）が満たすべき 普遍的性質（universal property） である。この性質は言うなれば、ある種の条件を満たす一意的な射が存在するということである。与えられた関手について任意の２つの（右、もしくは左）随伴関手が自然に等価である、すなわち、随伴性は同型を除いて一意的に構成を決定する、ということは注目に値する。

5.1 積と和（Products and Sums）

上述した構成法の多くは直観的にカノニカルである、したがって、随伴となる。例えば、圏 ${\cal C}$ の二項積は関手 $\prod : {\cal C} \times {\cal C} \rightarrow {\cal C}$ であり、これは、圏 ${\cal C}$ の対象 $C$ を組 $(C,C)$ へ送り、${\cal C}$ の射 $c: C \rightarrow C'$ を ${\cal C} \times {\cal C}$ の射 $(c,c) : (C,C) \rightarrow (C',C')$ へ送る「対角」関手（"diagonal" functor）$\Delta : {\cal C} \rightarrow {\cal C} \times {\cal C}$ の左随伴（left adjoint）である。さらに、$\Delta$ が右随伴を持つときかつそのときに限り、${\cal C}$ は余積（「和（sum）」とも呼ばれる）を持つ。基本的に重要な２つの数学的概念を形式化するこの美しく単純な方法は、マックレーン（Mac Lane）[46]によるもので、一般的な極限と余極限に拡張される。

5.2 フリービーズ（Freebies）

もう一つの美しく単純な形式化は、「自由な（free）」構成法の一般的定義を与える。すなわち、それらは忘却関手の左随伴である。例えば、例2.6の道圏関手 ${\cal Pa} : {\cal Graph} \rightarrow {\cal Cat}$ は、忘却関手 ${\cal Cat} \rightarrow {\cal Graph}$ の左随伴であり、したがって、グラフ上の自由圏（free category）を与える。

5.3 最小限の実現（Minimal Realisation）

オートマトン $(X,S,Y,f,g)$ は、その関数 $\bar{f} : X^\ast \rightarrow S$ が全射（surjective）であるときかつそのときに限り、到達可能（reachable） である。${\cal Aut}$ の部分圏で、その対象が到達可能であり、その射 $(i,j,k)$ が $i$ 全射性を持つものを ${\cal A}$ と表記することにする。このとき、$B : {\cal Aut} \rightarrow {\cal Beh}$ の ${\cal A}$ への制限（restriction） $B : {\cal A} \rightarrow {\cal Beh}$ は、振る舞いの最小限の実現（minimal realisation of a behaviour）を与える右随伴を持つ[18]。右随伴は一意的に決定するので、これは、最小限の実現の便利な抽象的特徴を提供する。さらに、この特徴付けはより一般的な最小限の実現にまで拡張され、さらにそれを示唆する。例えば、[17]を参照せよ。

5.4 構文論と意味論（Syntax and Semantics）

より華々しい随伴の一つは、代数的理論（algebraic theory）における構文論と意味論の間の随伴がある。これはまたLawvereの彼の論文によることになる。[49]を参照。

5.5 デカルト閉圏（Cartesian Closed Categories）

デカルト閉圏は、二項積（binary product）と、$A$ を $A \times B$ に送る各関手の右随伴（right adjoint）を持つ。この概念が本質的に（型付き）λ計算であることは注目に値する。[45]を参照。この関連は、例えば、高階関数型言語の効率的なコンパイルの基礎として使用されている[8]。利点としては、純粋に等式的な推論を用いることで、最適化技術が正しい
ことを証明できることがある。

5.6 クライスリ圏（Kleisli Categories）

Lawvere理論を一般化するもう一つの方法は、任意の随伴を一種の理論として捉えることである。いわゆる モナド （トリプル とも呼ばれる）は、必要な構造を抽象化したもので、モナド上の クライスリ圏 は自由代数の圏を与える[47]。再びここでも驚くほど多くの例がある。論文[22]は、クライスリ圏がどのように一般化されたLawvere理論を生成するかを示し、次に、（つまり、方程式系を解くことの）単一化（unification）の多くの異なる問題が、クライスリ圏のイコライザ（equaliser）を見つけることととして自然に定式化することができる。その例として、順序ソートかつ連続な理論（order sorted and continuous theory）の単一化がある。Moggi[55]は、クライスリ圏を使って、λ計算の多くの興味深い一般化を生じさせている抽象的な「計算」概念（notion of "computation"）を得ている。

6 余極限（Colimits）

第六のドグマは次のとおりである。

構造の種（species of structure）、ウィジェット（widget）と言おう、が与えられたとき、ウィジェットのシステムを相互接続してスーパーウィジェットを形成する結果は、ウィジェットがどのように相互接続されているかを示す射の図式の余極限を取ることに相当する。

少なくとも私にとっては、この直観は一般システム理論（General Systems Theory）[16,27]の文脈で生まれたものである。極限と余極限の圏論的定義の間の双対性は、解と相互接続の直観的概念の間の類似した双対性を示唆していることは興味深いかもしれない。ここでいくつかの例を挙げる。

6.1 理論を組み合わせて仕様を作る（Putting Theories together to make Specifications）

複雑さは、プログラミングの方法論において基本的な問題である。大規模なプログラムやその大規模な仕様は、作成するのも、理解するのも、正しさを得るのも、修正するのも非常に難しい。複雑さを打破するための基本的な戦略は、大規模なシステムを個別に理解できる小さな断片に分割し、元のシステムに戻すことである。これが成功すれば、実質的に複雑さの「対数を取る（takes the logarithm）」ことになる。Clearの意味論[6,7]において、仕様は、Lawvereと本質的に同じ意味で理論によって表現され（ただし、多ソート（many-sorted）、シグネチャ付き）、仕様は、そのような理論の圏における余極限によってまとめられる。より具体的には、汎用理論（generic theory）の実際への適用は、押し出し（pushout）によって計算される。OBJ[13,28,14]、Eqlog[30]、そしてFOOPS[31]は、この汎用モジュールの概念を、関数型、論理型（つまりリレーショナル型）、オブジェクト指向プログラミング、およびそれらの組み合わせに拡張している。これはAdaにも適用されている[21,63]。

6.2 グラフ書き換え（Graph Rewriting）

計算機科学におけるもう一つの重要な問題は、大規模並列マシンに適した計算モデルを見つけることである。成功するモデルは、特定のマシンの実装の詳細を避けるのに十分抽象的であり、かつコンパイラの中間ターゲット言語として機能するに十分具体的であるべきである。グラフの書き換えは、そのようなモデルを探索する有望な分野の一つであり[43,32,15,41]、余極限はこの分野で非常に有用であるようである[10,58,44]。グラフの書き換えは、言語学で現在流行している単一化文法（unification grammars）にとっても重要である[60,22]。このような分野では、さらなる研究の機会が多くありそうである。

6.3 始対象性（Initiality）

とりうる最も単純な図式は、空図式である。その余極限は、始対象であり、より簡単に説明すると、任意の対象へのただ一つの射を持つ対象である。どのような随伴もそうであるように、それは同型を除いて一意的に決まるので、圏の任意の２つの始対象は同型である（もちろん、これは直接的にも示すこともできる）。すなわち、始対象性（initiality）は、実体を「抽象的に（abstractly）」定義するための簡単な方法を与える。また、普遍性（universality）は、（コンマ圏において）始対象性に還元することができ、したがって、余極限についてもそうであることに言及することは価値がある。

6.4 始モデル意味論（Initial Model Semantics）

始対象性が計算機科学において非常に有用であることは注目に値する。始代数としての抽象構文の形式化[20]に始まり、帰納法と再帰[35,51]、抽象データ型[33]、領域方程式（後述）、計算可能性[51]、並びに関数型[13]、論理型（つまりリレーショナル型）、関数型とリレーショナル型および制約論理[30]といったプログラミング言語のモデル論的意味論などに始対象性は基本的な概念の範囲を広げながら適用されている。後者は、単なるモデルではなく、モデルの拡張、すなわち射の圏における始対象を含んでおり、興味深い。一般的に、この研究は、古典的なHerbrand Universe構造[38]を形式化し、一般化し、滑らかにしたものと見ることができる。

6.5 領域方程式の解法（Solving Domain Equations）

Scott[59]は、領域方程式を解くために「逆極限」法（"inverse limit" construction）を提示し、この構成法をレトラクト（retract）の関連する圏における余極限とみなすことで明快にするというLawvereによるいくつかの提案を記載している。これらの考え方は[61]でさらに進められ、半順序（partial order）から圏へ一般化され、他の事項の中で、最小不動点（least fixpoint）が始代数（initial algebra）であることが示されている。重要な構成法は、最小不動点 $\bigsqcup_n \in \omega F^n(\perp)$ の伝統的構成法の一般化である、射の無限列の余極限である。

7 コンマ圏（Comma Categories）

第七のドグマは次のとおりである。

構造 ${\cal C}$ の種が与えられたとき、${\cal C}$ の種を「装飾化」または「豊穣化」することによって得られた構造の種は ${\cal C}$ の下方（もしくは、${\cal C}$ からの関手の下方（under a functor from ${\cal C}$））のコンマ圏に対応する。

この直観を正確に伝えることは他のものよりも難しいように思われるが、いくつかの例がこのことを明確にする助けになるのであれば幸いである。以下は、計算機科学において見られる多くの例のほんの一部である。

7.1 グラフ（Graphs）

多くのグラフの圏はコンマ圏である。例えば、もし $2\times$ が、$S$ と $S \times S$ へと移す ${\cal Set}$ → ${\cal Set}$ 関手を表示するとき、例1.3の ${\cal Graph}$ 圏は、コンマ圏 $({\cal Set} \downarrow 2\times)$ である。

7.2 ラベル付きグラフ（Labelled Graphs）

あるグラフの圏 ${\cal G}$ と忘却関手 ${\cal U} : {\cal G} \rightarrow {\cal Set}$ が与えられ、${\cal G}$ におけるグラフのノードの集合を与え、ノードのラベルとして使われる集合 $L$ が与えられるとき、コンマ圏 $({\cal U} \downarrow L)$ は、$L$ でラベル付けされたノードを持つ ${\cal G}$ のグラフの圏となる。同様に、グラフの辺や木の枝を装飾することができる。

7.3 理論（Theories）

もし ${\cal FPCat}$ が有限積と、射として有限積保存関手（finite product preserving functor）を持つ圏の圏（the category of categories）であり、 ${\cal T}$ が型システム（すなわち、${\cal FPCat}$ の一つの対象）であるとき、${\cal T}$ 上の理論の圏（the category of theories over T）とは、$({\cal T} \downarrow {\cal FPCat})$ のことである。

コンマ圏は、Lawvereの論文の中で初めて現れたもう一つの基本的構成である。射が対象として用いられているときに生じる傾向がある。一つの圏をコンマ圏とみることで、極限と余極限の存在を証明するための一般的な結果を得ることができる[25]。

8 さらなる話題

これらは特に基礎的なものではあるが、上に挙げた７つのドグマは、圏論の豊かさを網羅するには程遠いものである。本節では、さらにいくつかの圏論的構成について述べるが、それぞれについて、計算機科学における例の多さに驚かされるかもしれない。

8.1 ２-圏（2-Categories）

射は、通常の合成、恒等射、始域と終域を持つだけでなく、なにか他の、より高次元の、射の対象として機能することがある。これは、２-圏（2-category）につながり、その中でも、その射の射として自然変換を持つ圏の圏 ${\cal Cat}$ は、カノニカルな例である。この概念は、例2.7で言及され、[24]、[26]、[40]、[56]などでも使われ、[61]でも言及されている。

8.2 モノイダル圏（Monoidal Categories）

通常のデカルト積（Cartesian product）ではないものの、それにもかかわらず同じ性質の多くを享受する自然な乗法概念を圏が持つ場合は多い。[52]で研究されているペトリネット（Petri net）の圏については既に述べたし、最近の様々な研究は、モノイダル圏が並列性の様々な理論間の関係を理解する上で広く有用であるかもしれないことを示唆している。例えば、[12]を参照せよ。

8.3 インデックス付き圏（Indexed Categories）

ストリクトなインデックス付き圏（strict indexed category）とは、単に関手 ${\cal B}^{op} \rightarrow {\cal Cat}$ のことである。論文[62]と[23]は、計算機科学におけるインデックス付き圏の多くの例を与えており、[62]は、関連した「グロタンディーク」圏の完全性についての簡単な十分条件を含む、いくつかの一般的な定理を与えている。Moggi[56]は、インデックス付き圏をプログラミング言語に応用し、特に、MLのような言語のための一種の高階モジュール機能を得る方法を示している（ノンストリクト（non-strict）なインデックス付き圏は、かなりより複雑であり、基礎的な研究に使われている[57]）。

8.4 トポイ（Topoi）

理論が圏であるというアイディアの深遠な一般化は、LawvereやTierneyらによって開発されたトポス（topos）概念に現れている。ある意味で、この概念は、集合論の本質を捉えている。また、代数幾何学、計算機科学、そして直観主義論理とも驚くべき関係がある[36,2,42]。

9 議論

伝統的な基礎論の考え方では、その公理系の中で関心のあるすべての対象を構築し、関連するすべての性質を導き出すことができるような、ある性質を持ったある種のプリミティブな対象や、対象についてのプリミティブな構成が存在することを主張する公理系、できれば第一階のものを与えることを要求している。公理は、その一貫性に対する信念を育み、できるだけ使いやすくするために、できるだけ自明で、数が少なく、単純でなければならない。このアプローチは、古典ギリシャの平面幾何学の説明にヒントを得ている。

数学の基礎付けとしてよく知られているのは集合論であり、数学におけるもっとも関心の持たれる対象の構築に非常に成功している。しかしながら、集合についての単純で、自明な公理の一般的合意を得ることはできなかった。例えば、集合論の古典的な定式化（Zermello-Frankelなど）は、80年近くも直観主義者から激しい攻撃を受けてきた。さらに最近では、一般連続体仮説（the Generalised Continuum Hypothesis）が「真」であるかどうかが議論されている。これは元はと言えば、一般連続体仮説が、集合論の他の、より広く受け入れられている公理とは独立であるという（Paul Cohenによる）驚くべき証明を受けて出てきた議論である。さらに最近では、基礎の公理（the Axiom of Foundation）についての議論があり、この公理は、各 $S_{i+1}$ が $S_i$ の元であるような、集合の無限列 $S_1, S_2, S_3, ...$ は存在しないことを主張している。実際、Aczel[1]らは、このような非基底集合（non-well founded sets）の存在を積極的に主張する反基礎の公理（Anti-Foundation Axiom）を用いて、Milner[54]の意味での伝達過程（communicating process）を含む、計算における様々な現象をモデル化している。数学者の多くは、数学の基礎として一般に受け入れられている単一の基礎という英雄的な理想をもはや信じておらず、数学の全てを基礎づける「揺るぎない確かさ（unshakable certainties）」[4]を見出す可能性をもはや信じていないと言っても良いだろう。

また、集合論的な基礎付けは、圏論そのものを含むある分野では数学的実践を完全に満足させる説明を提供することができず、さらに、巨大基数（large cardinal）などの数学的実践とはほとんど、あるいは全く関係ない分野への研究を促してきた（マックレーン（Mac Lane）[48]は、これら問題について活発な議論を展開している。基礎についての多様なアプローチの概要については[37]も参照）。いずれにせよ、数学の基礎となる最も議論の余地の少ない概念の最小集合を見出そうとする試みは、計算機科学にはほとんど直接関係しない。もちろん、長い間新しいパラドックスも発見されていないため、この問題はかつてほど切迫したものではなくなっている。

本論文では、数学とその応用の様々な分野間、あるいは分野内の類似性を整理し、一般化し、発見するための指針として、圏論が広範に有用でありながら、驚くほど具体的な指針を数多く提供していることを示そうとした。私は、このような指針が存在することが、別の、より実際的な見方を支持することになると願いたい。

基礎は、数学とその応用のさまざまな分野の構造と相互関係を明らかにし、数学の実践と使用に役立つ一般的な概念と道具を提供すべきである。
Foundations should provide general concepts and tools that reveal the structures and interrelations of various areas of mathematics and its applications, and that help in doing and using mathematics.

計算機科学のようなまだあまり発展していない分野では、定義を正しく理解することが最も困難な作業であるように思われがちだが、エレガントさと一貫性という比較的明確な尺度を用いることで、どのような研究の方向性が有益化を示唆することができるということから、この意味での基礎は非常に有用である。このような目的のために圏論がうまく用いられていることは、少なくともそのような基礎の始まりを提供していることを示唆している。

参考文献

[1]

Peter Aczel. Non-Well-Founded Sets. Center for the Study of Language and Information, Stanford University, 1988. CSLI Lecture Notes, Volume 14.

[2]

Michael Ilarr and Charles Wells. Toposes, Triples and Theories. Springer, 1985. Gnmdlchren der mathemati1:1chen Wisseni,;chafter, Volume 278.

[3]

Michael Ilarr and Charles Wells. The formal description of data types using sketches. In Michael Main, A. Melton, Michael Mii,;love, and D. Schmidt, editors, Mathemat'ical Foundations of Progrnrnrn'irig Language Semar1,t'ics. Springer, 1988. Lecture Notes in Computer Science, Volume 298.

[4]

Luitzen Egbertus Jan Brouwer. Intuitionistische betrachtungen iiber den formalismus. Koninklijke Akademie van wetenschappen te Amsterdam, Proceedings of the section of sciences, 31:374-379, 1928. In From Frege to Godel, Jean van Heijenoort (editor), Harvard, 1967, pages 490 492.

[5]

Rod Burstall. An algebraic description of programs with assertiom;, verification, and simulation. In J. Mack Adams, John Johnston, and Richard Stark, editors, Proceedings, Conference on Proving Assertions about Programs, pages 7-14. A1:11:1ociation for Computing Machinery, 1972.

[6]

Rod Ilurstall and Joseph Goguen. Putting theories together to make specificationi,;. In Raj Reddy, editor, Proceedings, Fifth International Joint Conference on Artificial Intelligence, pages 1045-1058. Department of Computer Science, Carnegie-Mellon University, 1977.

[7]

Rod I3urstall and Joseph Goguen. The semantics of Clear, a specification language. In Dinei,; Bjorner, editor, Proceedings, 1979 Copenhagen Winter School on Abstract Software Speci.fi,cation, pages 292 332. Springer, 1980. Lecture Notes in Computer Science, Volume 86; based on unpublished notes handed out at the Sympoi,;ium on Algebra and Application1:11 Stefan Banach Center, Warsaw, Poland, 1978.

[8]

Pierre-Luc Curien. Categorial Combinators, Sequential Algorithms, and Functional Programming. Pitman and Wiley, 1986. Research Notes in Theoretical Computer Science.

[9]

Hans-Dieter Ehrich. On the theory of specification, implementation and parameterization of abstract data types. Journal of the Association for Computing Machinery, 29:206-227, 1982.

[10]

Hartmut Ehrig. Introduction to the algebraic theory of graph grammars. In V. Clau1:1, Hartmut Ehrig, and Gregor Rozenberg, editors, Graph Gramars and their Appl'icat'ion to Corn1mter Sc'ience and Biology, pages 1 69. Springer, 1979. Lecture Notes in Computer Science, Volume 73.

[11]

Samuel Eilenberg and Saunders Mac Lane. General theory of natural equivalences. Transactions of the American Mathematical Society, 58:231-294, 1945. 16

[12]

Gian Luigi Ferrari. Unifying Models of Concurrency. PhD thesis, University of Pisa, 1990.

[13]

Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud, and Jose Meseguer. Principles of 013.J2. In Ilrian Reid, editor, Proceedings, Twelfth ACM Symposium on Principles of Programming Languages, pagei,; 52-66. Ai,;i,;ociation for Computing Machinery, 1985.

[14]

Kokichi Futatsugi, .Joseph Goguen, Jose Meseguer, and Koji Okada. Parameterized programming in OBJ2. In Robert Balzer, editor, Proceedings, Ninth Internat'ional Conference on Software Eng·ineering, pages 51 60. IEEE Computer Society, March 1987.

[15]

J.R .. W. Glauert, K. Hanunond, .J.R. Kennaway, G.A. Papadopoulos, and M.R. Sleep. DACTL: Some introductory papers. Technical Report SYS-C88-08, School of Information Syt>tems, Univernity of East Anglia, 1988.

[16]

Joseph Goguen. Mathematical representation of hierarchically organized systems. In E. Attinger, editor, Global Systems Dynamics, pages 112-128. S. Karger, 1971.

[17]

Joseph Goguen. Minimal realiz;ation of machines in closed categories. Hulletin of the American Mathematical Society, 78(5):777-783, 1972.

[18]

Joseph Goguen. Realization is universal. Matherrwtical System Theory, 6:359 374. 1973.

[19]

Joseph Goguen. On homomorphisms, correctness, termination, u1&)ldments and equivalence of flow diagram programs. Journal of Computer and System Sciences, 8:333-365, 1974. Original vernion in Proceedings, 1972 IEEE Symposi'll.rn on Sw-itching and AHtorrwta, pages 52 60; contains an additional section on program schemes.

[20]

Joseph Goguen. Semantics of computation. In Ernest G. Manes, editor, Proceedings, First International Symposium on Category Theory Applied to Computation and Control, paget> 234-249. Univernity of Mat1t1adllrnettt1 at Arnhernt, 1974. Also in Lecture Notes in Computer Science, Volume 25, Springer, 1975, pages 151-163.

[21]

Joseph Goguen. Reusing and interconnecting software cornponenti,;. Computer, 19(2):16 28, February 1986. Reprinted in Tutorial: Software ReusoJJility, Peter Freeman, editor, IEEE Computer Society, 1987, pages 251-263, and in Domain Arwlysis and Software Systems Modell·ing, Ruben Prieto-Diaz and Guillermo Arango, editors, IEEE Computer Society, 1991, pages 125-137.

[22]

Joseph Goguen. What is unification? A categorical view of t1ubt1titution, equation and solution. In Maurice Nivat and Hassan Ait-Kaci, editors, Resolution of Equations in Algebraic Structures, Volume 1: Algebraic Techniques, pages 217-261. Academic, 1989. Also Report SRI-CSL-88-2R2, SRI International, Computer Science Lab, August 1988. 17

[23]

Joseph Goguen. Types as theories. In George Michael Reed, Andrew William Roscoe, and Ralph F. Wachter, editors, Topology and Category Theory in Computer Science, pages 357-390. Oxford, 1991. Proceedings of a Conference held at Oxford, June 1989.

[24]

Joseph Goguen and Rod Burstall. CAT, a system for the structured elaboration of correct programs from structured specifications. Technical Report Report CSL-118, SRI Computer Science Lab, October 1980.

[25]

Joseph Goguen and Rod Burstall. Some fundamental algebraic tools for the semantics of computation, part 1: Comma categories, colimits, signatures and theories. Theoretical Computer Science, 31(2):175-209, 1984.

[26]

Joseph Goguen and Rod Burstall. Some fundamental algebraic tools frn- the semantics of computation, part 2: Signed and abstract theories. Theoretical Computer Science, 31(3):263-295, 1984.

[27]

Joseph Goguen and Susanna Ginali. A categorical approach to general systems theory. In George Klir, editor, Applied General Systems Research, pages 257- 270. Plenum, 1978.

[28]

Joseph Goguen, Claude Kirchner, Helene Kirchner, Aristide Megrelis, and Jose Meseguer. An introduction to OBJ3. In Jean-Pierre Jouannaud and Stephane Kaplan, editors, Proceedings, Conference on Condit'ional Terrn Rewriting, pages 258-263. Springer, 1988. Lecture Notes in Computer Science, Volume 308.

[29]

Joseph Goguen and Jose Meseguer. Correctness of recursive parallel nondeterministic flow programs. Journal of Computer and System Sciences, 27(2):268-290, October 1983. Earlier version in Proceedings, Conference on Mathematical Foundations of Corn1mter Science, 1977, pages 580 595, Springer Lecture Notes in Computer Science, Volume 53.

[30]

Joseph Goguen and Jo:,;c Mcseguer. Models and equality for logical programming. In Hartmut Ehrig, Giorgio Levi, Robert Kowalski, and Ugo Montanari, editors, Proceedings, 1981 TAPSOFT, pages 1-22. Springer, 1987. Lecture Notes in Computer Science, Volume 250.

[31]

Joseph Goguen and Jose Meseguer. Unifying functional, object-oriented and relational programming, with logical semantics. In Bruce Shriver and Peter Wegner, editors, Resmrch Directions in 0'JjN:t-On:ented Programming, pages 417-477. MIT, 1987. Preliminary version in SIGPLAN Notices, Volume 21, Number 10, page:,; 153-162, October 1986.

[32]

Joseph Goguen and Jose Meseguer. Software for the Rewrite Rule Machine. In Hideo Aiso and Kazuhiro Fuchi, editors, Proceedings, International Conference on F4th Generation Corrqmter Systems 1988, pages 628 637. Institute for New Generation Computer Technology (ICOT), 1988.

[33]

Joseph Goguen, Jame:,; Thatcher, and Eric Wagner. An initial algebra approach to the specification, correctness and implementation of abstract data types. In Raymond Yeh, editor, Current Trends in Programming Methodology, IV, pages 80 149. Prentice Hall, 1978. 18

[34]

Joseph Goguen, .James Thatcher, Eric Wagner, and Jesse Wright. A junction between computer science and category theory, I: Dasie concepts and examples (part 1). Technical report, IBM Wattion Research Center, Yorktown Heights NY, 1973. Report RC 4526.

[35]

Joseph Goguen, James Thatcher, Eric Wagner, and Jesse Wright. Initial algebra semantics and continuous algebras . .Journal of the Association for Computing Machinery, 24(1):68 95, January 1977. An early version is "Initial Algebra Semantics", with James Thatcher, II3M T . .J. Watson Research Center, Report RC 4865, May 1974.

[36]

Robert Goldblatt. Topoi, the Categorial Analysis of Logic. North-Holland, 1979.

[37]

William S. Hatcher. The Logical Foundations of Mathematics. Permagon, 1982.

[38]

Jacqueti Herbrand. Recherches 8lff la th{~orie de la demonstration. Travaux de la Societe des Sciences et des Lettres de Vo.rsovie, Classe III, 33(128), 1930.

[39]

Horst Herrlich and George Strecker. Category Theory. Allyn and Bacon, 1974.

[40]

C.A.R. Hoare and Jifeng He. Natural transformations and data refinement, 1988. Programming Research Group, Oxford University.

[41]

Berthold Hoffmann and Detlef Plump. Jungle evaluation for efficient term rewriting. Technical Report 4/88, Fachbereich Mathematik und lnformatik, U niversitat Bremen, 1988.

[42]

Martin Hyland. The effective topos. In A.S. Troelstra and van Dalen, editors, The Brouwer Symposium. North-Holland, 1982.

[43]

Robert Keller and Jotieph Faticl, editors. Proceedings, Graph Reduction Workshop. Springer, 1987. Lecture Notes in Computer Science, Volume 279.

[44]

Richard Kennaway. On 'On graph rewritings'. Theoret'ical Cornp'IJ.ter Science, 52:37-58, 1987.

[45]

.Joachim Lambek and Phil Scott. Introduction to Higher Order Categorical Logic. Cambridge, 1986. Cambridge Studies in Advanced Mathcmatict>, Volume 7.

[46]

Saunders Mac Lane. Duality for groups. Proceedings, National Academy of Sciences, U.S.A., 34:263-267, 1948.

[47]

Saundern Mac Lane. Categories for the Working Mathematician. Springer, 1971.

[48]

Saundern Mac Lane. To the greater health of mathematics. Mathematical Intelligencer, 10(3):17 20, 1988. See also Mathematical Intelligencer 5, No. 4, pp. 53-55, 1983.

[49]

F. William Lawvere. Functorial semantics of algebraic theories. Proceedings, National Academy of Sciences, U.S.A., 50:869-872, 1963. Summary of Ph.D. Thesis, Columbia University.

[50]

Humberto Maturana and Francisco Varela. The Tree of Knowledge. Shambhala, New Science Library, 1987. 19

[51]

Jose Meseguer and Joseph Goguen. Initiality, induction and computability. In Maurice Nivat and .John Reynolds, editors, Algebraic Methods in Semantics, page:,; 459-541. Cambridge, 1985.

[52]

.Jose Meseguer and Ugo Montanari. Petri nets are monoids: A new algebraic foundation for net theory. In Proceedings, Symposium on Logic in Computer Science. IEEE Computer Society, 1988. Full version in Report SRI-CSL-88-3, Computer Science Laboratory, SR.I International, .January 1988; submitted to Information and Computation.

[53]

Robin Milner. An algebraic definition of simulation between programs. Technical Report CS-205, Stanford University, Computer Science Department, 1971.

[54]

Robin Milner. A Calculus of Cornrniur1.icating Systems. Springer, 1980. Lecture Notes in Computer Science, Volume 92.

[55]

Eugenio Moggi. Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-66, Laboratory for Foundations of Computer Science, University of Edinburgh, 1988.

[56]

Eugenio Moggi. A category-theoretic account of program modules, 1989. Laboratory for Foundations of Computer Science, University of Edinburgh.

[57]

Robert Pare and Peter John:,;tone. Indexed Categories and their Applications. Springer, 1978. Lecture Notes in Mathematics, Volume 661.

[58]

Jean Claude Raoult. On graph rewritings. Theoretical Computer Science, 32:1- 24, 1984.

[59]

Dana Scott. Continuous lattices. In Proceedings, Dalhousie Conference, pages 97-136. Springer, 1972. Lecture Notes in Mathematics, Volume 274.

[60]

Stuart Shieber. An Introduction to Unification-Based Approaches to Grammar. Center for the Study of Language and Information, 1986.

[61]

Michael Smyth and Gordon Plotkin. The category-theoretic solution of recursive domain equations. SIAM .Journal of Computation, 11:761-783, 1982. Also Report D.A.I. 60, University of Edinburgh, Department of Artificial Intelligence, December 1978.

[62]

Andrzej Tarlecki, Rod Burstall, and Joseph Goguen. Some fundamental algebraic tools for the semantics of computation, part 3: Indexed categories. Theoretical Comp·uter Science, 91:239-264, 1991. Also, Monograph PRG-77, August 1989, Programming Research Group, Oxford University.

[63]

William Joseph Tracz. Formal Spec~fi,ca.tion of Parn.meterized Programs in LILLEANN A. PhD thesis, Stanford University, to appear.

[64]

Alfred North Whitehead. Process and Reo.ldy. Free, 1969.

脚注

1. 私が知る限り、このような試みは[34]で私が行ったものが最初である。他に私が知っている唯一の試みは、LambekとScott [45]によるもので、彼は同様のスタイルで多くの「スローガン」を与えている。 ↩

2. オリジナルの1972年会議の版のみこの定義が収録されている。 ↩