【翻訳】普遍代数の圏論的理解：Lawvere理論とモナド

Last updated at 2024-12-02Posted at 2024-11-30

はじめに

代数的効果（algebraic effects）を理解したい。でもそれにはLawvere理論なるものが必要らしいということで見つけた論文を機械翻訳（Kagi Translate）してそれを手直しする形で訳しました。
意味の分からないところは意味わかってないです。数学的ステートメントを利用する（ということがもしあったら）場合は必ず原文の方を確認してください。間違いあると思うので気づいたらお知らせいただいて理解できればなおすと思います。間違い勘違い理解不足の部分を見つけたら適時直していくと思います。
自分の方がうまく訳せるという人はどうぞ。野良訳なのでなにかあれば人知れず消えるかもしれませんのであしからず。

普遍代数の圏論的理解：Lawvere理論とモナド

The category theoretic understanding of universal algebra: Lawvere theories and monads（原文）
Martin Hyland, John Power著

概要

Lawvere理論とモナドは、普遍代数の２つの主要な圏論的定式化であり、Lawvere理論は1963年に、モナドとの関連はその数年後に確立された。モナドは、数学的に直接的でなく、打ち延ばしできる性質に乏しい定式化であるが、急速に優先されることになった。１世代が経過すると、モナドの定義は、普遍代数に言及することなく、計算効果をモデル化するために理論計算機科学に広く登場し始めた。しかし、それ以来、計算効果に対する普遍代数の関連性が認識されるようになり、Lawvere理論という概念が、計算論的な設定で再び注目されるようになった。この発展は、Gordon Plotkinの成熟した研究の主要な部分を形成しており、ここではその歴史を研究することとし、特に、1960年代にLawvere理論がモナドに取って変わられた理由と、計算機科学におけるLawvere理論への新たな関心が、今後どのように発展していくかを問う。

キーワード：普遍代数、Lawvere理論、モナド、計算効果

１はじめに

普遍代数の圏論的な定式化には、主に二つの形式がある。初期のものは、1963年にBill Lawvereによって彼の博士論文で提案された[23]。現在では、彼の中心的な構成は通常Lawvere理論と呼ばれ、より率直には単一ソート有限積理論（single-sorted finite product theory）と呼ばれる[2,3]。これは、普遍代数学者が持つクローン（clone）の概念のより柔軟なバージョンである。実際、Lawvere自身は、以下で説明する概念を定式化する前に、後者の概念に到達している。数学的実践において、Lawvere理論は、有限積を持つ圏への関手があり、その関手の有限積の間の自然変換を研究する際に現れる（歴史的には、このアイディアはコホモロジー演算の形で最初に現れた）。

Lawvere理論の不変的な概念と等式理論の概念とを区別することが重要である。等式理論はLawvere理論（またはクローン）の提示（presentation）の一形態である：すべての等式理論はLawvere理論を決定し、すべてのLawvere理論は等式理論の無限のクラスによって決定される。つまりは、本質的にクローンであるそれら等式理論によって決定されることになるのである。理論（たとえば、Lawvere理論）の良い提示を選び出すこと、提示から理論の不変な記述を導き出すことは、計算機科学において重要な側面であり、これについては後ほど議論する。しかし理論の意味論は、それとは独立して検討することができる。

普遍代数の第二の圏論的な定式化は、モナドに関するもので、より複雑な歴史を持っている。モナドは通常、関手の随伴対から生じる。その場合、Eilenberg-Moore[8]およびKleisli[22]のモナドの代数の圏は、元の随伴対の近似と見なすことができる随伴対を提供する。このモナド（またはトリプルまたはスタンダード構成）の概念は、普遍代数とは異なる理由で代数的トポロジーにおいて生じた、例えば、[10]を参照せよ。[8]でEilenbergとMooreは、Tが自由群モナドである場合、T-代数の彼らの圏は群の圏であると述べている。次に、Linton[29]は、モナドとLawvere理論（普遍代数）との次のような一般的な関係を示した：すべてのLawvere理論は、代数の圏がLawvere理論のモデルの圏に同値であるようなSet上のモナドを生じさせ、Lawvere理論の定義の一般化に従って、すべてのモナドはこのように、連接同型を除いて一意的に（uniquely up to coherent isomorphism）生じる。

モナドはすぐに普遍代数のより一般的な圏論的な定式化となった、例えば[31]を参照せよ。振り返ってみると、現在の著者たちは次の事実に驚いている：Lawvere理論の概念は普遍代数から直接生じたのに対し、モナドの概念はそうではない。Lawvere理論は普遍代数により密接に関連しており、普遍代数において生じる自然な構成、例えば理論の和やテンソルを取ることは即座に許す。したがって、論文の最初の主要な目標は、歴史がなぜどのようにしてモナドを優遇したのかを調査することである。

1980年代後半に進むと、計算機科学者たちは、Eugenio Moggiの指導の下、普遍代数に言及することなくモナドの概念を広範に利用し始めた[33,34,35]。Moggiは、彼がcomputationの概念（notions of computation）と呼ぶものの研究を統一したいと考えていた。その狙いは、その時点で提案されていた表示的意味論による多くの例を、一般的な構成のインスタンスとして復元することであった。彼は、例外（exception）、副作用（side-effect）、インタラクティブな入出力（interactive input/output）、非決定性（non-determinism）、部分性（partiality）、継続（continuation）のモデルを考えていた。確率的非決定性[18]もすぐにリストに追加されることになった。モナドは、元々提案されたものとは異なる文脈で計算機科学の道具として使用されるようになった（データベース[5]、純粋関数型言語[48]）が、私たちには、それらの中心的な使用法はMoggiのものであるように見える。ただし、Moggiの二つの応用、部分性と継続は、他のものとは異なる性質を持つと主張する。部分性は、命令的な振る舞いなしに再帰から生じる。この論文では、継続の特別な特徴についてさらに考察する。

振り返ってみると、普遍代数の視点は、他のcomputationの概念、現在では我々は計算効果（computational effect）と呼ぶ方を好む、にとって基本的であるように思える。しかし、その時点では明確ではなかった。さまざまな計算効果とMoggiの対応するモナドは、例外のためのraise、副作用のためのlookupとupdate、インタラクティブな入出力のためのreadとwrite、非決定性のための非決定的∨、確率的非決定性のための[0, 1]区間に定義される多くの二項演算+rなどといった計算的に自然な等式となりがちなもののように、計算的に自然な操作から生じる。したがって、Lawvere理論の（表現の）計算的正当性に関連する明白な科学的問題がある。ここでは、Moggiが彼のアプローチを提案したときにLawvere理論がどのようにして現れなかったのか、10年後にそれらが現れたときに何が起こったのか、そして計算効果と普遍代数の関係がここからどのように発展するかを調査する。

Gordon PlotkinはMoggiの博士課程の指導教官であり、後に普遍代数に関する計算効果の研究を発展させるために必要な計算の専門知識を提供した。効果の代数は、彼の成熟した科学研究の主要なテーマの一つであり、したがってこの論文の一部として我々のささやかな調査結果を提出した。

論文は以下のように構成されている。第2節では、Lawvere理論とモデルの概念の発展を振り返える。第3節では、computationにおいて後に有用であることが証明されたLawvere理論の性質と構成を説明する。第4節では、各Lawvere理論がSet上のモナドをどのように生じさせるかを説明する。第5節では、モナドの概念が、普遍代数の圏論的理解においてLawvere理論のそれよりもどのようにより突出して優位になったかを分析する。第6節では、計算効果のモデル化における、モナドとLawvere理論の使用、前者はMoggiによるもので、後者はPlotokinによるもの、を調査する。そして第7節では、計算効果と普遍代数の間のつながりの密接な関係について熟考する。

私たちは、Bill Lawvere、Mike Mislove、Eugenio Moggiに、この論文の初期草稿に対するコメントに感謝する。彼らの観察は、重要な問題の定式化に実質的に影響を与えた。

２ Lawvere理論

1930年代は、基礎数学にとって注目に値する10年であった。当時、数学はドイツによって支配されており、その規模は以降どの国によっても並ぶことはなかった。この時代には、論理における有名な発見だけでなく、圏論の観点から基本的な2つのトピック、すなわち代数的トポロジーと普遍代数の発展も見られた。これらの発展に関与した研究者たちは、しばしば同じであったり、少なくとも互いに密接に関連していた。興味深い例として、Saunders Mac Laneが挙げられる。彼はドイツに行き、論理に関する論文を書くために、世界的な代数的トポロジストの一人となり、代数に関する世界で最も影響力のあるテキストの一つを共同で執筆した。

1960年代までに、代数的トポロジーと普遍代数はより明確に区別され、新しい世代の研究者たちは、どちらか一方のトピックについて深い理解を持つ傾向があったが、両方を理解している者は少なかった。そのような環境にBill Lawvereは入ってくることになった。Lawvereは、ニューヨークにあるコロンビア大学でSamuel Eilenbergの学生であり、Eilenbergは北米の圏論における基礎的な人物たちを教育するかまたは影響を与えていた時期であった。この論文で考察する圏論の発展に寄与した他の人物としては、Lawvereの論文における重要な前任者として認識されているPeter Freydや、Michael Barr、Fred Linton、Jon Beck、そしてMyles Tierneyがいる。ちなみに、最後の2人はEilenbergの学生であった。彼らのほとんどは代数的トポロジーの専門家であったが、LawvereのEilenbergの下で書かれた博士論文は普遍代数に関するものだった（この論文の執筆が進む中で、特に計算機科学の観点から興味深い歴史の一部を知った。Eilenbergは、Lawvereの論文が書かれたときにそれを読まなかったことを公言していたが、数年後に計算機科学からの理由でそれを読んだ。どうやらこれが1967年にトロントで行われたAMS夏会議での「普遍代数とオートマトンの理論（Universal algebras and the theory of automata）」という講義に影響を与えたようである。我々が執筆している時点で、この資料を見つけて再評価する努力が進められている。）

Lawvereは、彼の論文の中で、次のように等式理論のクローン（clone）を公理化した。有限集合とそれらの間のすべての関数による圏の骨格（skelton）を取る。したがって、各自然数nに対して、nと呼ぶ、n個の要素を持つ一つの対象を持つことになる。この圏は、対象 n、m について、濃度の和 n + m によって与えられる有限余積（finite coproduct）を持っている。明らかに、これは1についての有限余積を持つ（任意のバージョンの）自由圏に等しい。なお、次のように余積構造を選択する：定値性のため（for definiteness）、+を厳密結合的（strictly associative）な標準的な（順序和）選択とする（しかし、その選択から本質的なことは何も導かれない）。

定義 2.1 $\aleph_0$ を有限集合とそれらの間のすべての関数からなる圏の骨格とし、厳密結合的（strictly associative）な余積を持つ圏として考える。

$\aleph_0$ は有限余積を備えているため、逆圏 $\aleph_0^{\text{op}}$ も有限積を備えていることは明確である。

定義 2.2 Lawvere理論は、（必然厳密結合的）有限積（(necessarily strictly associative) finite product）を持つ小さな圏 L と、厳密有限積保存かつ対象同一的関手（strict finite-product preserving identity-on-object functor） $I : \aleph_0^{\text{op}} \rightarrow L$ から成る。$L$ から $L'$ へのLawvere理論の写像は、$L$ から $L'$ への（必然厳密）有限積保存関手（(necessarily strict) finite-product preserving functor）であり、関手 I と I' は可換である。

したがって、任意のLawvere理論 L の対象は、正確に $\aleph_0$ の対象であり、そのような対象間のすべての関数は L における写像を生じる。Lawvere理論の写像は操作と呼ばれることが多く、$\aleph_0$ から生じるものが 基本的積操作（basic product operation） である。Lawvere理論間の写像の概念は、一つの理論を別の理論で単純に解釈するというアイデアをカプセル化している。積構造に対する解釈の振る舞いは決定されることに注意されたい。

自明なこととして、Lawvere理論とそれらの間の写像の定義は、通常の関手の合成によって与えられる合成を持つ圏 $Law$ を生じる。関手 I はこの点で重要な構造的役割を果たす。つまり、有限積を持つ小さな圏とそれらの間の厳密有限積保存関手（strict finite-product preserving functor）から成る圏 $FP$ は、自然に 2-圏の主要な例の一つに拡張される[16]。一方で、本質的に $FP$ の部分圏にあたる圏 $Law$ は、自然に説得力のある形で拡張されない。なぜなら、関手 I は L における有限積の振る舞いを充分（fully）に決定するからである。Lawvere理論間の写像 $F,G : L \rightarrow L'$ が与えられたとき、F から G への連接自然変換（coherent natural transformation）（すなわち、$\aleph_0^{\text{op}} \rightarrow L$ と合成して恒等射を与えるもの）は、対象 1 における恒等射によって完全に決定される。したがって、そのようなものは恒等射だけである。これはLawvere理論への通常の圏論的論理拡張よりもはるかに制限的な状況である（[2]と比較し、5節での議論を参照せよ）。$Law$ を単純な圏と見なすことが意味を持つのはこのためである（連接（coherence）がない場合、自然変換はそれぞれFとGの下でLの操作の像の間を結びつけるL'の単項演算に対応する、モデルの観点からするとこれらはあまり面白くない。）

我々は、Lawvere理論の定義において、関手 I が包含である必要はないという事実を強調する。

例 2.3 単位圏 1 に等しいLawvere理論 $Triv$ が存在する。つまり、その対象は $\aleph_0$ の対象であり、任意の対象から任意の他の対象への射が一つあるものである。関手 I は、対象同一的（identity-on-objects）であるが、写像に関しては自明である。

これは、自然に思える予想に対する反例を与える有用な例である。自明なことではあるが、それは終対象であるため、圏 $Law$ の構造にとって重要である。恒等射 $\aleph_0^{\text{op}} \rightarrow \aleph_0^{\text{op}}$ は、始対象を与える。一般に、$Law$ は良好な閉包性（closure properties）を享受する。つまり、それは完備であり、余完備であり、実際には局所有限提示可能圏（a locally finitely presentable category）である。3節で $Law$ における有限余積を簡単に調査する。

ついでに、$L(2, 1)$ のHom集合がちょうど一つの要素を持つようなLawvere理論 L がちょうど二つだけ存在することに注意する。理論 $Triv$ に加えて、次の変種がある。

例 2.4 n ≠ 0 の場合、0 から n への矢印がなく、他のすべてのケースでは対象間に一つの矢印があるLawvere理論 $Triv_0$ が存在する。関手 I は対象同一的（identity-on-objects）であり、同じドメインと余ドメインを持つすべての写像を同一視する。

$Triv$ と $Triv_0$ の関係は一般的な現象の一例である。つまり、[23] の言語で言えば、後者は定義可能な定数を表現不可能にすることによって前者を消耗させた（depleting）結果である。それはさておき、例 2.3 と 2.4 は唯一の直感に反するものである。Lawvere理論の定義における関手 I が忠実であると見なすことは、主な関心のあるすべての例においてそうであるため、一般的には無害である。

ほとんどの数学的目的において、Lawvere理論はそのモデルの研究によって理解される。

定義 2.5 有限積を持つ任意の圏 C におけるLawvere理論 L のモデルは、有限積保存関手 $M : L \rightarrow C$ である。

ここで、有限積の保存を求めるが、厳密保存（strict preservation）を求めないことに注意されたい。それは、Lawvere理論の定義における厳密性（strictness）の観点から驚くべきことかもしれない。一つの結果は、Lawvere理論 L のモデル M と M' の組が C における積の選択のためだけに異なってくる可能性があることである。しかし、Lawvereは最初の[23] で指摘したように、有限積の厳密保存（strict preservation）よりも保存（preservation）の方が基本的である。つまり、厳密保存を要求すれば、モノイドのためのLawvere理論のモデルの圏は、望まれるようにモノイドの圏となるのではなく、空となる（！）。理由は、通常の集合論的定義において、Setにおける有限積は厳密結合的（strictly associative）ではないが、一方で、Lawvere理論においては厳密結合的であるからである。厳密保存（strict preservation）であることよりも保存（preservation）であることには他の利点もある。つまり、例えば、有限保存関手 $H : C \rightarrow C'$ に沿った基底圏の変更についてのスムーズな説明を可能にする。

積の保存の一部分でもある射影（projection）を M が保存するという要件は、すべての関数 f に対する基本的な積操作 I f における M の振る舞いを決定する。つまり、L における射影は$\aleph_0$における余射影に相当し、すべての関数fは余射影の族によって与えられるためである。したがって、モデルを決定するのは他の操作の解釈である。

Lawvere理論の概念は、等式理論のクローンを公理化するものである。つまり、それが意図されたことであった。任意の等式理論が与えられたとき、Lawvere理論を生成することができる。つまり、構築する圏 L において、対象 n は、 1 の n コピーの n 重積（n-fold product）であり、したがって m から n への写像は、m から 1 への n 写像（n map）に一意的に対応する。そして後者の一つは、理論の等式に従う操作によって生成された（最大で）m の自由変数の項の同値類を意味する。

定義 2.6 任意のLawvere理論 L と有限積を持つ任意の圏 C に対して、圏 $Mod(L,C)$ は、C における L のすべてのモデルによって与えられる対象を持ち、それらの間のすべての自然変換によって与えられる写像を持つものと定義される。

$Mod(L,C)$ における写像の上記の定義の正しさは、最初に明らかにされたものよりも微妙な問題である。自然性条件が、モデル間のすべての自然変換が有限積構造を順守することを意味することは容易に証明できる。つまり、モデル M と N の間の任意の自然変換 α に対して、$\aleph_0$ の任意の n について、写像 $\alpha_n : Mn \rightarrow Nn$ は写像 $\alpha_1 : M1 \rightarrow N1$ の n コピーの積（n copies of the map）によって与えられる。したがって、$Mod(L,C)$ における写像は、すべての自然変換として定義したものであるが、L の積構造を順守するすべての自然変換としても同様に定義できる。モデル間の写像の文脈では、C における積の選択のみが異なる（この問題については上で述べた） L のモデルMとM'のペアは、$Mod(L,C)$ において同型であることがわかる。

主な関心のある意味論的圏は $Set$ である。したがって、Set におけるLawvere理論 L のモデル M を考える。集合 M1 は、L におけるすべての n に対して Mn を連接同型の違いを除いて（up to coherent isomorphism）決定する。つまり、M が L の有限積を保存するので、$\aleph_0^{\text{op}}$ と同様に、$\aleph_0^{\text{op}}$ の有限余積であり、これらは有限和によって与えられるため、Mn は M1 の n コピーの積（the product of n copies of M1）でなければならない。したがって、モデル M を与えることは、集合 X = M1 を与え、圏 L における、L の合成と積構造によって与えられる等式に従う、 $f : m \rightarrow 1$ の形式の各写像に対して $X^m$ から $X$ への関数を与えることと同値であり。そして、$Mod(L,C)$ はそのような構造の明証圏（evident category）に同値である。この分析は、有限積を持つ任意の圏 C に対して規定通りに拡張される。

モデルが求められる圏に関する柔軟性は、Lawvere理論アプローチの重要な特徴である。伝統的な例を思い出そう。群のLawvere理論 $L_G$ を取ると、Set におけるモデルの圏 $Mod(L_G, Set)$ は、群の圏（と同値）である（次節の冒頭で、理論が $Set$ におけるモデルの圏によって決定される理由を説明する）。しかし、他の圏で $L_G$ を解釈することができる。特に、位相空間の圏 Top における $L_G$ のモデルは、本質的に位相群である。他の基底圏、層の圏、微分可能多様体の圏、スキームの圏などについても同様の話をすることができる。興味深い特別なケースは、小さな群の圏 $Group \simeq Mod(L_G, Set)$ における $L_G$ のモデルである。1962年に発表されたEckmann-Hiltonの議論 [6] によれば、これらはアーベル群である。そしてこれが高次ホモトピー群がアーベルである理由を説明している。これらの例は、Lawvere理論の概念が1960年代にすでに研究されていた構造に精度と統一性をどのようにもたらしたかということを示すいくつかの指標を提供する。

モデル圏 $Mod(L,C)$ は、両方の引数において関手的であり、関手性は合成によって誘導される。解釈 $L \rightarrow L'$ は、関手 $Mod(L',C) \rightarrow Mod(L,C)$ を誘導し、一方で、有限性保存関手 $C \rightarrow C'$ は、関手 $Mod(L,C) \rightarrow Mod(L,C')$ を誘導する。我々は、これをモナドについての状況と簡単に対比する。

３ Lawvere理論の性質

さて、Lawvere理論の概念のいくつかの性質と、それらを用いて作成できるいくつかの構成を考えてみよう。等式理論とは異なり、Lawvere理論は意味的に不変である。その正確な意味は次のとおりである。各Lawvere理論 $L$ に対して、１での評価によって与えられる基底集合関手（underlying set functor）

$ev_1 : Mod(L, Set) \rightarrow Set ,$

を関連付ける（この関連付けはLawvereの意味論関手（semantics functor）である[23]）。モデルの圏 $Mod(L, Set)$ と $Mod(L', Set)$ は、それらが基底集合関手を順守する場合、連接的同型（coherently equivalent）であると言う。

命題3.1 Lawvere理論 $L$ と$L'$ が与えられたとき、圏 $Mod(L, Set)$ と $Mod(L', Set)$ が連接的同型であるならば、Lawvere理論 $L$ と $L'$ は、圏 $Law$ において同型である。

証明：任意のLawvere理論 $L$ に対して、米田埋め込みは次の形の充満忠実関手（fully faithful functor）に制限される。
$Y_L : L^{op} \rightarrow Mod(L, Set)$。

$Mod(L, Set)$ における表現可能［関手］ $Y_L (n) = L(n,-)$は、それ自身で次の関手を表現する。
$evn \cong (ev_1)^n : Mod(L, Set) \rightarrow Set .$

したがって、基底集合関手$ev_1$ を順守する $Mod(L, Set)$ と $Mod(L', Set)$ の間の同値性は、次の同型を誘導する

$Mod(L, Set)(L(n,−),L(m,−)) \cong Mod(L', Set)(L'(n,-),L'(m,-))$

そして（米田［埋め込み］を二回使用することで得られる）同型

$L(n,m) \cong L'(n,m)$

は、合成と互換性がある（compatible with composition）。この同型は、基本的な積構造を順守する。なぜなら、$ev_1$ は、次と同型であるからである。

$Mod(I, Set) : Mod(L, Set) \rightarrow Mod(\aleph^{\text{op}}_0 , Set) \simeq Set .$

概説した議論は、意味論と代数構造の間のLawvereの随伴（Lawvere's adjunction）の一部である[23]。これらのアイデアは、[38]における代数的操作の扱いにおいて拡張、洗練された。

最近の研究の主要な推進力（[15]および[13]を参照）は、Lawvere理論に関する操作の観点から、計算効果を組み合わせる計算的に自然な方法を理解することである。ここでは、価値があることが証明されたLawvere理論を組み合わせる二つの自然な方法を簡単に紹介する。

まず、Lawvere理論の和を説明する。つまり、それはまさに圏 $Law$ における余積である。これは、明らかな等式理論の和と一致するため、簡単に説明できる。つまり、それは、追加の等式のない、各理論の全ての等式に従っている、手近な等式理論の各々からすべての操作を取ることに対応する。したがって、$Set$ における $L + L'$ のモデルは、$L$ のモデルの構造と $L'$ のモデルの構造の両方を備えた集合である。

この和の概念には少し注意が必要である。しかし、いずれにしても等式理論の和に関して必要である明白な注意だけである。たとえば、Lawvere理論 $L$ と $L'$ が与えられたとき、余射影（coprojection）$L \rightarrow L+L'$ と $L' \rightarrow L+L'$ によって与えられるLawvere理論の写像が存在する。しかし、これらの余射影関手は忠実である必要はない。つまり、もし $L$ が $Triv$ であれば、$L + L'$ もまた $Triv$ であるため、 $L'$ からの余射影は自明である。（$Triv_0$にも類似の問題が存在する。）

また、Lawvere理論 $L$ と $L'$ のテンソル積 $L \otimes L'$ を考えることもでき、次のように説明できる（[9,45]の議論も参照せよ）。圏 $\aleph_0$ は有限余積だけでなく、有限積も持ち、これを$n \times n'$で表示する。対象 $n \times n'$ は、n'のnコピーの余積（coproduct of n copies of n'）としても見てよい。したがって、Lawvere理論における任意の写像 $f' : n' \rightarrow m'$ が与えられたとき、$n \times f' : n \times n' \rightarrow n \times m'$ という射によってあらわされるものの意味はすぐに明らかである。共役をとることによって $f \times n'$ を定義し、以下では標準的同型（canonical isomorphism）を省略する。

定義3.2 Lawvere理論 $L$ と $L'$ が与えられたとき、$L$ と $L'$ のテンソル積と呼ばれる Lawvere理論 $L \otimes L'$は、$L$ と $L'$ から$L \otimes L'$へのLawvere理論の写像の普遍的性質から定義される。ここで、$L$ のすべての操作とそれに対応する $L'$ のすべての操作は可換性を持つ。すなわち、$L$ における $f : n \rightarrow m$ と $L'$ における $f' : n' \rightarrow m'$ が与えられたとき、次の図式の可換性を要求することになる。

テンソル積は、操作と等式によって定義されているため、またはよりエレガントには[16]の擬似可換性（pseudo-commutativity）に関する研究に訴えることによって定義されているためかのどちらかの理由で、常に存在する。

命題3.3 テンソル積 $\otimes$ は、Lawvere理論の圏の上で対称モノイダル構造をカノニカルに拡張する。

この命題の証明は初歩的である。テンソル積の単位（unit）は、始Lawvere理論（initial Lawvere theory）、すなわち、操作も等式も生成しない理論である。これを $\aleph_0^{\text{op}} \rightarrow \aleph_0^{\text{op}}$ と考えることができるので、これはLawvere理論の圏の始対象である。したがって、和の単位（unit）でもある。

この最後の結果は、テンソル積の決定性のいくつかの指標を示すが、あまり重要ではない。可換性の意味の中心にあるものは、理論についての操作の共通する特徴ではなく、$L$ と $L'$ のモデルの圏に関する $L \otimes L'$ の単純な特徴付けである [14,15]。

定理3.4 任意の有限積を持つ圏 $C$ に対して、$Mod(L \otimes L',C)$ と $Mod(L,Mod(L',C))$ との間に圏の連接同値性（coherent equivalence of categories）が存在する。

この定理は、2節の最後で言及されたEckmann-Hiltonの議論に新しい視点を与える。この議論が示すのは、自身を伴う群のLawvere理論 $L_G$ のテンソル積が、アーベル群のLawvere理論 $L_A$ と同型であるということである。

最後の一般的な所見として、Lawvere理論の圏の性質と構造は、それ自体が興味深い研究分野であり続けることがわかる。調査では、[25]に掲載されている問題のリストと、TACの再版に対するコメントと共に、その資料を更新した。

４モナド

Lawvereが代数理論のクローン（clone）の特徴付けを行った後すぐに、LintonはすべてのLawvere理論が $Set$ 上のモナドを生み出すことを示した[29]。この構成は、$Law$ から $Set$ 上のモナドの圏 $Mnd$ への充満忠実関手に拡張される。この関手は、圏同値ではない。したがって、この正確な意味において、$Set$ 上のモナドは、Lawvere理論のモナドより一般的な概念と見なすことができる。

Lintonは、また部分的な逆も示した。任意のサイズのアリティを許すためにLawvere理論の定義を一般化した。一般化された理論はもはや小さな圏ではなく、1つの圏によって充満に決定されるものではない。次に、Lawvere理論からのモナドの構成は、圏同値に一般化される。[30]で、Lintonは、意味論と代数構造のLawvereの取り扱い方の一般化を与えた。Lawvereによって取り扱われたケースは、より一般的な理論の特別なケースとして見なされるべきであることが示唆されている。

Lintonによって分析された理論とモナドの関係のいくつかの詳細を示す。任意のLawvere理論 $L$ が与えられたとき、$\aleph_0$ に等しい、$L$ の対象 1 での評価によって与えられる標準的忘却関手（canonical forgetful functor） $U_L : Mod(L,C) \rightarrow C$ が存在する。もしその忘却関手が左随伴 $F_L$ を持つなら、$C$ が局所的提示可能（locally presentable）なときには常にそうであるように、直接またはBeckのmonadicity定理 [2] のどちらかによって、$Mod(L,C)$ が、 $C$ 上の誘導されたモナド $T_L$ に対して圏 $T_L\text{-Alg}$ と同値であることを証明できる。特に、$Set$ が局所的有限提示可能（locally finitely presentable）であることから、すべてのLawvere理論 $L$ は $Set$ 上のモナド $T_L$ を誘導する。

命題 4.1 モナド $T_L$ は、次の余極限（余エンド）によって記述できる。
$T_L X = \int^{ n \in \aleph_0 } L(n,1) \times X^n$

この余極限は、集合 $L(n,1) \times X^n$ のすべての自然数 n にわたる余積であり、$\aleph_0^{\text{op}}$ の射影と対角写像を取ることによって決定される要素を同一視することで因子化（factored）される。これは、理論内のすべての項の集合に、理論内の同等のものを除いて、対応させることで簡単にわかる。一般化された代数の多くの種類のものから生じるモナドと擬似モナド（pseudo-monad）は、類似の公式を使用することで構成できるが、ここではそれについては追求しない。この公式は、Lawvere理論からのモナドの構成が関手的でありかつ、$Law$ から $Mnd$ への関手として充満忠実であるということを、簡単に証明することを可能にする。さらに、もう少し努力すれば、次のことが証明できる。

命題 4.2 忘却関手 $U_L : Mod(L, Set) \rightarrow Set$ によって決定されるLawvere理論 $L$ をモナド $T_L$ に送る構成は、$Law$ から $Mnd$ への充満忠実関手に拡張される。さらに、比較関手（comparison functor）は、 $Mod(L, Set)$ と $T_L\text{-Alg}$ の間の同値性を示す。

モナド $T_L$ がすべてのLawvere理論 $L$ に対して有限的であることは簡単に確認できる。基底圏（base category）が $Set$ の場合、有限性は構成の像（the image of the construction）を特徴付けるが、それは後の時代での見解である [19]。

逆に、まず任意の $Set$ 上のモナド $T$ に対して、クライスリ圏 $Kl(T)$ は、すべての小さな余積を持ち、標準的関手（canonical functor） $I : Set \rightarrow Kl(T)$ はそれらを保存する。つまり、標準的関手 $I$ は、右随伴を持ち、対象同一的（identity-on-object）である。次に、$I$ を充満部分圏（full subcategory） $\aleph_0$ に制限すると、次の図式のようにLawvere理論（の逆）を得る。

次のことを示すことは難しくない。

命題 4.3 $Set$ 上のモナド $T$ を、$Kl(T)$ を $\aleph_0$ の対象に制限することによって決定される圏 $Kl(T)^{\text{op}}_{\aleph_0}$ に送る構成は、$Mnd$ から $Law$ への関手に拡張される。

この構成の背後にあるシンプルなアイデアは次のとおりである。もし $T_L$ がLawvere理論 $L$ のモナドであれば、$Kl(T)(n,m)$ は、 n と m に対する $L$ の自由モデル間の写像で構成される。そして、$Kl(T)(n,m) \cong Set(n, Tm)$ であるため、これらは $Tm$ の要素の n-タプルに対応する。しかし、自由モデルは、項の同値類によって与えられるため、これは単に $L(m, n)$ である。したがって、任意のLawvere理論 $L$ に対して、Lawvere理論 $L_{T_L}$ が $Law$ において $L$ と同型であることを確認することはルーチン的である。しかしながら、$Set$ 上のモナド $T$ から始まる対応する命題は真ではない。なぜなら、構成 $T_L$ は正確に有限的モナド（finitary monad）を生成するためである。実際、次のことがわかる。

定理 4.4 $L$ を $T_L$ に送る構成と $T$ を $L_T$ に送る構成は、$Set$ 上のモナドの圏である $Mnd$ の充満余反射的部分圏（full coreflective subcategory）としての $Law$ を示す。

Lintonによって取られたこの視点の拡張は次のようになる。一般化された理論は、すべての小さな積を持つ局所的に小さな圏 $L$ と、$Set$ の骨格の逆から $L$ への厳密積保存対象同一的関手（strict product preserving identity-on-objects functor）からなるものとして定義できる。この一般化されたLawvere理論の概念を用いることで、命題 4.2 の構成が拡張されることを示すことができる [13]。そして、定理 4.4 の対応するバージョンにおいては圏同値性を持つことになる [29]。

この拡張はスムーズで魅力的に見えるが、いくつかの反証を簡単に示す。問題は、有界ランク（bounded rank）のモナド（ランクを持つモナド）には発生しない。それらに対しては、（有限的）Lawvere理論のための資料を使いつくすことができる。しかしながら、ランクがない興味深いモナドもある [2,13]。数学では、コンパクト・ハウスドルフ空間のモナドがあり、computationの理論では、継続（continuation）のモナドがある。両方の科学分野で、上限格子（sup lattice）のモナドに出会うことができる。問題は、モナドや理論がランクを持つ場合において、一般的なモナドの概念に対応する大きなLawvere理論の概念を扱うことができないことである。したがって、この動きは本質的に普遍代数のアイデアから一歩離れることになる。

一つの点は明らかである。大きなLawvere理論の概念は和の下で閉じていない。実際、上記のランクの無いモナドのいずれかを伴う単項演算によって生成されたモナドの和は存在しない。これは継続に関して [13] で説明されているが、他のケースにおける議論は本質的に同一である。ここでは証明を繰り返すのではなく、[15] で与えられた和の分析に基づいて、なぜそうなるのか直観を示す。ランクのないモナド $T$ に対応する大きなLawvere理論では、操作のクラスがある。そして、これはこの操作のクラスにおける複雑な表現の間の等式があるということのためにのみ $Set$ 上のモナドを与える。さて、独立した単項演算 s を追加する。元のクラスから s と後方合成（postcomposing）することによって得られる操作のクラスを考える。s が独立しているため、これらの新しい操作における複雑な表現の間の非自明な等式は現在存在しない。その結果、想定される和理論において構築してもよいもののサイズを制御できなくなる。具体的には、ランクのない $T$ の単位（unit）はモニック（monic）であり、したがって任意の集合 x から始めると、和の自由代数は、関手 $T$ によって生成される自由モナド $T^{*}$ の下での x の像 $T^{∗}x = \mu y.(Ty + x)$ を含まなければならない。しかし、$T^{∗}x \cong T(T^{∗}x+x)$ であり、これは我々が知るすべてのケースにおいて濃度の理由から不可能である。したがって、これらの和は存在しない。

同様の直観は、一般化されたLawvere理論 $L$ と $L'$ のいずれかがランクを持つ場合、テンソル積 $L \otimes L'$ が存在することを明らかにする（これは [13] で正式に証明されている）。しかしながら、$L$ と $L'$ が両方ともランクを持たない場合、直観は通用せず、一般的にはテンソル積は存在しないと信じられている。

モナドとLawvere理論のアイデアの異なる一般性の範囲は、（一般化された）Lawvere理論とモナドの間の関係に影響を与える。モナドは任意の圏上で考えることができるが、Lawvere理論は $Set$ 上の（有限的な）モナドに対応する。一方で、ある圏上のモナドは、その圏においてのみ代数（すなわちモデル）を持つが、Lawvere理論は積を持つ任意の圏においてモデルを自然に持つ。したがって、$Set$ 上のモナド間のモナド写像（このモナド写像の概念については [2] を参照）は、Lawvere理論の写像に直接対応するが、積を持つ圏 $C$ における $Mod(L,C)$ の関手性に対応するものは（少なくとも、即座にアクセスできるものはない）、モナドの世界には存在しない。

この最後の点を補足するためにいくつかの所見を述べる。もし $F : C \rightarrow D$ が（例えば）局所的提示可能圏（locally presentable category）の間で積保存（product preserving）である場合、 $Mod(L, F) : Mod(L,C) \rightarrow Mod(L,D)$ は $F$ の持ち上げ（lift）であり命題 4.1 の説明に従う、したがって誘導された $C$ 上のモナド $T^C_L$ と $D$ 上のモナド $T^D_L$ の間のモナド写像（一般的な意味については、[46] を参照）に対応する。さて、この純粋にモナドの観点からこれを扱う方法はないようである。つまり、モナド（および実際にはモナド写像）の説明は、理論に依存しする。しかし、Lawvere理論の使用は、我々をより遠くへと前進させる。実例として、位相空間の圏 $Top$ に関するいくつかの問題を考える。

$Top$ における $Set$ の（離散的な）埋め込み $Set \rightarrow Top$ は、有限積を保存するため、（$Set$ における）群の圏を位相群の圏に明らかに埋め込むことができる（これは前述のように、関連するLawvere理論の $Top$ におけるモデルである）。さて、$Top$ は局所的提示可能（locally presentable）ではないため、一般的な理論がない場合、命題 4.1 の余エンド式が群のモナドを $Set$ から $Top$ に拡張できることを確認する必要がある。それはまあまあ複雑ではないが、$Set \rightarrow Top$ は他の積を保存しない。したがって、可算Lawvere理論（副作用を扱う際に必要である。例 6.2 を参照）を考慮すると、モデルのレベルで埋め込みを持ち上げる（lift）ことは期待できない。しかしながら、余エンド式は依然として適用され、$Top$ 上にモナドを得ることができる。しかし、注意が必要である。忘却［関手］ $Top \rightarrow Set$ はすべての積を保存するため、空間は期待される点（expected point）を持つ。しかし、余エンドは一般に期待される位相（expected topology）を与えない。つまり、例えば、$Set$ 上の副作用モナドから、$Top$ 上の自然な副作用モナドは得られない。さらに興味深い状況として、読者は継続モナドで何が起こるかを考慮するかもしれない。

５ Lawvere理論とモナド

1960年代中頃までに、普遍代数の圏的理解が確立されることとなった（関連する出版物のほとんどは1966年に発表された）。Lawvere理論は、等式理論のクローン（clone）の概念を公理化した。代数的トポロジーで生じたモナドは、Lawvere理論の概念を一般化するものと見なされていた。そして、4節で示したように、Lawvere理論の概念を形式的に拡張して、$Set$ におけるモナドの概念と等価な理論の概念（notion of theory）を与えることができると認識されていた。しかし、振り返ってみると、これらの発展に関与する一般化された理論の概念は、魅力的ではない。これは、それ自体が代数の範囲内での活動の大部分からの抽象化である普遍代数の活動からさらに一歩離れたものであるからである。そして、さらに有用な構成を失うことになるためである。つまり、モナドの和は一般には存在する必要がなく、テンソルでさえも存在しない可能性が高いようである。これは厄介である。なぜなら、一つの理由はこれらは自然な代数的構造であるということ、そしてもう一つの理由はもしそれらが存在するとしても、それらの普遍性をモナドの観点から自然に考える方法や理由を理解することが容易ではないためである。しかしながら、これらすべてにもかかわらず、圏論の研究者たちは圧倒的にLawvere理論よりもモナドの観点から普遍代数を概念化し始めることになった。例えば、[31] ではその概念が一文で言及されている。それでは、なぜそうなったのであろうか？人々の動機を個別にまたは集団的に理解するのは常に難しいことであるが、その当時の特定の状況には顕著な科学的歴史的事実があった。

まず第一に、たとえLawvere理論の観点から普遍代数を概念化しようという意志があったとしても、圏論の精神（ethos of category theory）は、公理的に定義された構造を持つ任意の圏の観点から構造を理解し、次に $Set$ を主要な例として扱うことであったということが挙げられる。これはモナドの概念には容易であるが、Lawvere理論の概念には難しい。なぜなら、次の質問に答える必要があるためである。

公理的条件を満たす任意の圏 $C$ の任意の対象 $X$ が与えられたとき、$X$ が有限であるとはどういう意味であるか？

この質問に対する決定的な答えは1971年に初めて現れた。GabrielとUlmerが、ドイツ語で、局所的有限的提示可能圏（locally finitely presentable category）についての彼らの説明を発表したときである[11]。

第二に、豊穣圏が評価されず、発展していなかったことが挙げられる。豊穣圏の概念は、1966年にEilenbergとKellyによって最初に定式化された[7]が、主流に入るまでには時間がかかり、豊穣化設定（enriched setting）における有限性についての決定的な説明は1982年に[20]で初めて現れた。豊穣圏が役立つ理由は、有限性の概念（notion of finiteness）が与えられた場合、Lawvere理論をその設定に一般化するのが容易であり、普遍代数の枠組みの下で有用に扱われる構造の広いクラスをカバーするからである。豊穣化Lawvere理論（enriched Lawvere theory）の概念は2000年に[43]で初めて発表されたものの、その一方でそれ以前ではよく理解されていたにもかかわらず、その理解はまだ広く普及していない。豊穣化Lawvere理論についての詳細は、後ほど短く述べる。

第三に、Lawvere理論の視点を支持する圏論的論理の発展がまだ来ていなかったことが挙げられる。[28]の付録で議論されているように、論理には二つの現存する意味がある。思考の発展に関する広い意味と、典型的には性質の論理に関する狭い意味である。今考慮している注目すべき時代において、前者は、Lawvereによって大いに刺激されて実質的な発展を遂げていた（[24,25,26,27]を参照）。しかし、1970年代になって初めて、狭い意味での洗練された圏論的論理が登場した。そして皮肉なことに、Lawvere理論はこの狭い論理の読み方に自然に適合する。Lawvere理論は、単一ソート等式理論（single-sorted equational theory）に対応する。より一般的には、有限極限理論（finite limit theory）[11]は、ホーン節（Horn clause）を穏やかに一般化し、もっとさらに一般的には、正則理論（regular theory）、連接理論（coherent theory）、幾何学的理論（geometric theory）があり、すべてが圏論的論理上のトポス理論の視点に適合する[32,2]。それら仕事の文脈においては、モナドは孤立している（monads are isolated）。それら［モナド］は、広い意味での論理の一部であるが、Lawvere理論とは対照的に、この論理の階層に即座に適合するわけではない。しかし、この発展はすべて後で来たため、1960年代中頃にはモナドとは反対にLawvere理論を支持する数学的文化を提供されなかった。

最初の二つの理由は関連しており、それらの前線での技術的発展について少し述べます。これは応用にとって重要です。豊穣化Lawvere理論は次のように定義される。$Set$ から、（対称的）モノイダル閉圏として局所的有限的提示可能圏（locally finitely presentable as a (symmetric) monoidal closed category）Vに一般化する[20]。これには、$Cat$、$Poset$、$Graph$ などの圏や、任意の通常の可換等式シグネチャ（ordinary commutative equational signature）の代数のすべての圏が含まれる。余テンソルの概念は、冪（power）の概念の決定的な豊穣化である。

定義 5.1 $V$ の対象 $X$ と V-圏 $C$ の対象 $B$ が与えられたとき、$B$ の X-余テンソル（X-cotensor of B）は、それが存在する場合、A においてV-自然である（V-natural in A）同型射の族 $C(A,B)^X \cong C(A,B^X)$ を伴う $C$ の対象 $B^X$ である。

V を $Set$ とすると、余テンソルは $B$ のコピーの X-重積（X-fold product）をまさに定義する。次に、X-余テンソルは、X が有限的提示可能（finitely presentable）であれば、GabrielとUlmerの定義的な意味で、有限（finite）であると呼ばれる。さて、上記の基本的な材料は一般化される。

定義 5.2 Lawvere-V-理論（Lawvere-V-theory）は、厳密有限余テンソル保存かつ対象同一的V-関手（strict finite-cotensor preserving and identity-on-objects V-functor）$I : V^\text{op}_f \rightarrow L$ を伴う、有限余テンソルを持つ小さな V-圏 $L$ である。ここで、 $V_f$ は、V の有限的提示可能な対象（finitely presentable object）によって決定される V の充満な部分 V-圏（full sub-V-category）の骨格（skelton）である。

定義 5.3 有限余テンソルを持つ V-圏 $C$ における $L$ のモデルは、有限余テンソル保存 V-関手（finite-cotensor preserving V-functor） $M : L \rightarrow C$ である。

V-圏 $Mod(L,C)$ を適切に定義でき、通常のLawvere理論のすべての圏理論的分析を手間なく一般化できる。通常のLawvere理論のまだ十分に拡張されていない重要な側面の一つは、等式理論の文法的概念である。我々の知る限り、現在、豊穣化Lawvere理論に対応する等式理論の豊穣化された概念は存在しない。しかし、等式理論はスケッチ（sketche）の観点から言い換えることができ、豊穣化された説明は存在するか、もしくは少なくとも文献 [21] から容易に探り出すことができる。これは、豊穣化Lawvere理論の文法的な取り扱いに対する満足のいくアプローチのように見える。

豊穣化と有限性の公理的な説明の両方が存在する状況では、これは容易に進めることができるが、前述のように、その組み合わせは1966年には存在しなかった。ついでに、有限性はあるが豊穣化がない場合、公理的に定義された条件に従う任意の基底圏（base category）に対してLawvere理論の説明を与えることがまだできることに注意せよ。しかし、それは手ごわい。それは2005年にようやく解決され、詳細は [36] に現れた。

1966年までに有限性と豊穣化が解決され、より一般的な圏論的論理の動機付けとなる経験が利用可能であった場合、歴史がどのように展開したかは計り知れない。Lawvere理論は、普遍代数の決定的な圏論的定式化として現れるかもしれないし、そうでないかもしれないが、確実により良い機会を持っていただろう。結果として、Lawvereは普遍代数を進めることはなかった（彼は豊穣化に興味を持っていたが）、むしろ $Set$ 圏を特徴づけることに進んだ[24]。この仕事の流れは、最終的に初等トポスの概念とその後の圏論的論理に至った。普遍代数の圏論的発展は、Beck、Barr、そして主に代数的トポロジーに専門知識を持つ他の人物によって進められた。そこではモナドの概念が生まれ、重要な数学的発展へとつながった。例えば[1,4]や[2]の説明を参照せよ、ただし、これらの結果の焦点はLawvere理論の概念とはかなり異なる。

６計算効果（computational effects）

さて、それでは1960年代中頃から1980年代後半に飛ぶことにする。その間に、モナドの概念は普遍代数の主要な圏論的定式化として確立された。MacLaneによる影響力のあるテキスト[31]においてはその重要な役割が証明されている。なお、そのテキストでは、Lawvere理論はモナドに関する章の最後の行で言及されているだけである。同時かつ独立して、計算機科学者たちは、表示的意味論に関連して圏論に興味を持ち始めました。そして1987年、Eugenio MoggiはGordon Plotkinの下、エディンバラ大学で博士論文を完成させ、なおMartin Hylandは外部審査員であった。まさにその時、Moggiの計算効果という新しいアイデアが経験豊富な圏論家たちの注目を集めることになったわけである。

決定的な瞬間は、Moggiの口頭試問において訪れた。Moggiは部分性に関する技術的な論文を完成させ、議論は今後の研究の話題に移ることとなった。彼はその後、computationの概念の新しいアイデアを紹介し、それらをモデル化するためにモナドを使用することを提案した。Hylandには、基本的な型理論を計算的意味を持つ項で豊かにするという特に優雅なアイデアに思えた。彼は励ましの言葉をかけた。その時の状況では、Hylandが普遍代数やLawvere理論について言及することは思いも寄らないことであった。むしろ、彼はモナドから計算的概念を学ぼうとし、それら（普遍代数やLawvere理論）に基づいて批判的な判断をするための独立した理解を持っていなかった。

1年後、Isle of Thornsでの構成論理と圏論のワークショップで、当時の計算機科学と関係をもっていた北米の主要な圏論家であったPeter FreydがMoggiのアイデアを初めて耳にした。彼もまた感銘を受け、Hylandに隣に座っていた彼に、そして他の人々にもそのことを伝えた。しかし、またMoggiのアイデアの議論の中で普遍代数やLawvere理論のアイデアは現れなかった。

Moggiの研究はすぐに[33,35]で目立って発表され、プログラミング言語について考えるためのメタ原則として非常に影響力を持つようになった。そして、それから、モナドからそれを生み出すLawvere理論への移行がこの研究の方向性を変え始めるまでには約10年かかることになった。さらに5年の研究を経て、その変化の影響が見え始めている。Moggiの各集合Xに対する計算効果と関連付けられたvalueからなる集合TXへの割り当てから、計算効果に関連付けられた操作の研究に移行することとなった。ほとんどの場合、TXの選択は何らかの計算的直感に基づいて明らかであるため、このプロセスはリバース・エンジニアリングの一種となる。さらにいえば、単に代数理論（algebraic theory）のクローン（clone）を求めるというわけではなく、理論を表現するための良いプリミティブの選択と、良い公理の選択を求めることとなるわけである。
Moggiの副作用のためのモナドが、計算的に自然な操作であるlookupとupdate（これらは計算的に自然な等式に従う）から生じるという認識（7節参照）は、アイデアの発展にとって重要であった。このケースは以下の例6.2で説明する。モナドを知り、理論を再構築するという一般的な状況は、数学ではあまり馴染みがない。理論は実践を支えるために十分に発展させなければならず、計算的に重要な例は十分に検討されなければならなかった。これにより、最近の一連の論文[37,38,39,40,41,42]が生まれた。しかし、提示（presentation）の問題も数学的に重要であることを認識すべきである。たとえば、群の理論は除算の観点からの提示を持っているが、その提示は一般的にあまり関心を持たれていないようである。

今、Moggiによってモナドの観点から与えられ、後に（可算）Lawvere理論の観点から説明された計算効果の例を調査する（より詳細な議論については[14,15]を参照）。

例 6.1 例外のための Lawvere 理論 $L_E$ は、ここで $E$ は例外の集合であるとき、$E$ 操作 $raise : 0 \rightarrow 1$ によって生成される自由 Lawvere 理論である。操作と等式の観点から見ると、これは等式のない nullary 操作の E-添字付き族（E-indexed family of nullary operations）に対応する。$L_E$ によって生成される Set 上のモナドは、 $T_E = − + E$ である。より一般的には、忘却関手 $U_L : Mod(L_E,C) \rightarrow C$ は、ここで $\underline{E}$ は 1 の $E$ 重余冪（E-fold copower）、すなわち C における余積の存在を仮定する場合の $\coprod_E 1$ であるとするとき、$C$ 上のモナド $−+\underline{E}$ を誘導する。

副作用については、Lawvere 理論から可算 Lawvere 理論（countable Lawvere theory）への所定の一般化を行う必要がある。つまり、後者は可算のアリティの操作を認める必要がある[14,15]。以下では、$Val$ は、valueの可算集合（countable set）で、$Loc$ は、位置（location）の有限集合である。なお、我々は、 $Val$ を $\aleph_0$ と、$Loc$ をその濃度へと無害な同一視をする。

例 6.2 副作用のための可算 Lawvere 理論 $L_S$ は、ここで状態 $S = \text{Val}^\text{Loc}$ とするとき、操作 $lookup : Val \rightarrow Loc$ と $update : 1 \rightarrow Loc \times Val$ によって生成される自由可算 Lawvere 理論（free countable Lawvere theory）である。$lookup$ と $update$ は、[39] にリストされた 7 つの自然な等式に従い、そのうちの 4 つは $lookup$ と $update$ の相互作用等式（interaction equation）を指定し、またそのうち 3 つは交換等式（commutation equation）を指定する。[39] では、この可算 Lawvere 理論が、$Set$ 上の Moggi の副作用モナド $(S \times -)^S$ を誘導することが示されている。より一般的には、C が可算の冪と余冪（countable powers and copowers）を持つ任意の圏である場合、[39] の結果を少し一般化すると、忘却関手 $U_L : Mod(L_S,C) \rightarrow C$ は、ここで $(S \times -)$ は S 重余冪（S-fold copower） $\coprod_S -$ を表し、$(−)^S$ は S 重冪（S-fold power） $\prod_S -$ と表すとする場合、C 上のモナド $(S \times −)^S$ を誘導する。

前の例では、位置（location）の集合が有限であると仮定した。Eugenio Moggi は、 Plotkin シンポジウムへの寄稿の中で、位置の集合 $Loc$ が無限である場合に生じるより微妙な副作用モナドに注目した。

例 6.3 $Loc$ を無限と仮定する。この場合、[39] の操作と等式は副作用モナド $(S \times -)^S$ の部分モナドを誘導する。関手部分は、各 s に対して次の性質を持つペア $(\sigma : S \rightarrow S, \alpha : S \rightarrow A)$ によって与えられる $(S \times - )^S$ の有限的なバージョンである。
(i) $\sigma (s)$ は、有限の数の位置（location）において s と異なる。
(ii) there is a finite number of locations such that if we fix s at these then
(a) that fixes $\alpha (s)$, and $\sigma (s)$ on a finite set of locations as in (i), and
(b) moreover the remaining locations are untouched.
モナド構造は、 $(S \times -)^S$ から引き継がれる。

最後の 2 つの例は、対応する理論の魅力的な提示（presentation）を抽出するという観点を伴うモナドの意味論的分析（semantic analysis of a monad）とひとつの理論からモナドを構築することの間の持ちつ持たれつの関係を示している。そもそも、副作用に関する理論なしに第二のモナドに独立して到達することはほとんどないだろう。次に、理論の言語はそのモナドからは全く明らかではない。実際、$S = \text{Val}^\text{Loc}$ は $Loc$ が有限の非空（finite non-empty）である限り可算であるため、基本的な副作用モナドのすべての非退化（non-degenerate）の場合で同じ Lawvere 理論を得る。つまり、選択された提示（chosen presentation）は位置（location）の数に依存することになる（状態に関する意味論的な問題はこれで終わりではない。位置（location）の集合を実際の無限（actually infinite）ではなく潜在的な無限（potentially）であると考えると、修正された副作用モナドの代わりに [39] のような前層アプローチを主張できるかもしれない）。

次の例では、圏 $C$ 上の任意の自己関手 $F$ が与えられたとき、$\mu y.Fy$ は、もしそれが存在すれば、始 $F$-代数を表すこととする。次に、二項和を持つ圏 $C$ 上の自己関手 $\Sigma$ に対して、対象 x 上の自由 $\Sigma$-代数は、 $\mu y.(\Sigma y + x)$ であり、片方が存在する場合にのみもう一方が存在する。これら自由代数は、$C$ が局所的に可算的に提示可能（locally countably presentable）でありかつ $\Sigma$ が可算のランクを持つ場合は、確かに存在する。類似のケースでも同様である。

例 6.4 インタラクティブな入出力のための可算 Lawvere 理論 $L_{I/O}$ は、操作 $read : I \rightarrow 1$ と $write : 1 \rightarrow O$ によって生成される自由可算 Lawvere 理論である。ここで、$I$ は $input$ の可算集合であり、 $O$ は $output$ の可算集合である。インタラクティブな入出力のモナド $T_{I/O}(X) = \mu Y.(O \times Y + Y^I + X)$ は、この Lawvere 理論によって誘導される。つまり、$T_{I/O}(X)$ は X 上の自由 $\Sigma$-代数である。ここで $\Sigma Y = O \times Y + Y^I$ は 2 つの操作によって決定されるシグネチャ関手（signature functor）とする。そして、$\Sigma$ の代数は、単項操作の $O$ 添字付きの族と一つの $I$-アリティの操作で構成される。これはまた、$Mod(L_S,C)$ から局所的可算的に提示可能圏（locally countably presentable category） C から生じるより一般的な状況における $T_{I/O}$ の形式である。

例 6.5 （二項）非決定性のための可算 Lawvere 理論 $L_N$ は、結合法則、可換法則、冪等性の等式に従う二項操作 $\vee : 2 \rightarrow 1$ によって自由に生成される可算 Lawvere 理論、すなわち半束（semilattice）の可算 Lawvere 理論である。Set上に誘導されるモナドは、有限非空部分集合（finite non-empty subset）モナド $\mathcal{F}+$である。

例 6.6 確率的非決定性のための可算 Lawvere 理論 $L_P$ は、[12] のような結合法則、可換法則、冪等性の等式に従う [0, 1]-多二項操作 $+_r : 2 \rightarrow 1$ によって自由に生成される。$Set$ 上で誘導されるモナドは、有限の台（finite support）を持つ分布のモナド $\mathcal{D}_f$ である。実際には、結合法則は $(a +_r b) +s c = a +{rs}(b +_t c)$ であり、ここで $(1−r)s = (1−rs)t$ である。そして、擬似可換法則（pseudo-commutative law）は $a +r b = b +{(1−r)} a$ であり、冪等性は等式 $a +_r a = a$ の族である。

圏 Set は、表示的意味論において主要な関心のある圏ではない。より関心があるのは $\omega Cpo$ とその変種であり、再帰と非停止をモデル化する。前述のように、有限 Lawvere 理論と有限モナドの間の関係は、可算 Lawvere 理論とモナドの間、そして可算強化された Lawvere 理論と強化されたモナド、同等に強いモナドの間に問題なく一般化される。【As we observed earlier, the relationship between finite Lawvere theories and finitary monads generalises without fuss to one between countable Lawvere theories and monads and then to one between countable enriched Lawvere theories and enriched monads, equivalently strong monads, on the category in which the enrichment takes place.】理論が機能するためには、圏がデカルト閉圏として局所的可算的に提示可能（locally countably presentable）であることで十分である。圏 $\omega Cpo$ は、そのような圏の例である。したがって、ここでの作業は $\omega Cpo$ を含むように一般化される。

Lawvere理論の観点を支持する一つの理由は、計算効果の自然な組み合わせがLawvere理論の自然な組み合わせ、特に和とテンソルに対応することである[14,15]。特に、例外と他の計算効果の組み合わせは、Lawvere理論の和に対応する。これは、インタラクティブな入出力と他の多くの効果の自然な組み合わせについても当てはまる。一方、副作用を組み合わせる場合には、次のようになる[15]。

例 6.7 $L_S$ を副作用のための可算 Lawvere 理論とし、ここで $S = \text{Val}^\text{Loc}$ であり、さらに $L$ を任意の可算 Lawvere 理論とする。このとき、モナド $T_{L_S}\otimes L$ は、 $(T_L(S \times -))^S$ と同型となる。

これは、計算効果のテンソル積が Moggi の副作用モナド変換子の定義と一致することを示している。さらに、次のような好ましい系がある。

系 6.8 $S = \text{Val}^\text{Loc}$ の副作用理論は、$S = Val$ の副作用理論の $Loc$ 重テンソル積（Loc-fold tensor product）である。
　
理論の和の話に手短に戻ると、興味のある非退化（non-degenerate）の場合では、新しい等式をどちら［の理論］にも追加することなく理論を組み合わせる方法が提供されることに注意して欲しい。（再び非退化の場合において、）分配法則を使用することによってモナドの観点から純粋に理論を組み合わせる方法が存在する。分配法則 $TS \rightarrow ST$ から、合成モナド ST が得られる。しかし、Lawvere 理論の観点から見ると、これ［分配法則］は $L_S$ の演算を $L_T$ の演算に分配し、そして、その結果は、和 $L_S+L_T$ に対応するモナドとは非常に異なることになる。さらに、重要な例では、分配法則が存在しないことがある。Plotkin と Varacca によって、確率的選択モナド（probabilistic choice monad）に対する任意の非決定的選択モナド（nondeterministic choice monad）、またはその逆に対する分配法則は存在しないことが示された。この状況を解決するにはかなりの努力が必要である [47]。分配法則の状況とは対照的に、Lawvere 理論のさまざまな種類の合成、例えば和、テンソル、および分配テンソル（distibutive tensor） [17] は常に存在する。我々が知っているものとしては、主な関心のある計算効果の組み合わせが含まれている。また、特に豊穣化（enriched）された設定で発生する可能性のある計算効果のさらなる組み合わせも、Lawvere 理論の観点から最も適切に扱われる可能性が高いようである。

上記の例のリストから欠けているモナドの一つは、継続モナドである。これはランクのないモナドであり、有用な種類の Lawvere 理論と見なすことができない。実際、[13] の議論によれば、継続モナド変換子は、独特なものとして見なされるべきである。少なくとも非常に明白な意味では、継続モナドを他のものと組み合わせた結果であるようには見えないのである。前述の強調の変化は、操作と等式から生じるモナドと他のモナド、他のモナドには継続が含まれる、を区別することにつながる。さらに、結果として得られる観点は、計算効果のための Kleisli 構造の役割を重要視しないことにつながる。つまり、一般的には、Lawvere理論からモナドに移行し、次にそのKleisli構成に移行する必要はなく、むしろまさしくLawvere理論 $L$ から始めて、それが $KL(T_L)^{op}$ の有限制限であることを知りつつ、必要に応じてそれを直接的に拡張すればよいのである[44]。

７今後の展開

最近の発展の観点からすると、MacLaneの本にLawvere理論に関する一文があるモナドの章があるのではなく、モナドの節があるLawvere理論の章があったならば、1987年にMoggiの口頭試問が行われた際、またはその直後に何が起こったのだろうかということを考えるのは魅力的である。HylandやFreydがMoggiの話を聞いたときに、すぐに普遍代数やLawvere理論について尋ねていたら、研究は異なる方向に進んでいたのだろうか？もちろん、それを決して知ることはできないが、2001年に普遍代数の関連が結局は提案されたときに何が起こったのかについては言うことができる。

2001年、Gordon PlotkinはジェノバでのETAPSでの開会招待講演を行い、Moggiは聴衆として参加していた。Plotkinは、計算効果と普遍代数を関連付け始めたPowerとの共同研究を発表した[37]。彼は、普遍代数の一般性のレベルでの構造的操作的意味論（structural operational semantics）を説明し、非決定性や確率的非決定性のさまざまな形式から引き出された例を研究した。講演の最後に、Moggiは彼の副作用モナドが計算的に自然な操作に従ったlookupとupdateの操作によって生成されるかもしれないことを提案した。その後の数ヶ月の間に、PlotkinとPowerはそれを検証し、後にHylandが加わり、その当時計算効果と見なされていたものが、1つの例外を除いて、普遍代数の実例および発展したものとして有益に見なすことができることを確認した：インタラクティブな入出力（interactive input/output）は、等式を含まない例としてすぐに認識された上で、局所状態（local state）を自然に組み込む方法として見られた。そして、計算効果を組み合わせるさまざまな方法は、Lawvere理論を組み合わせる単純な例であることが証明された。例外は継続（continuation）である。そのようなわけで、次のようなことを考える。

1987年に普遍代数との関連が当時認識されていたら、何が起こっていただろうか？より大事なことは、これから何が起こるだろうか？ということである。

これらの質問に対する推測的な回答でこの論文を締めくくることにする。

おそらく計算効果は普遍代数の実例および発展したものとして見なされるかもしれない、ということになるだろうか？継続は計算効果とは見なされず、むしろ別の概念として扱われるだろう。継続は依然として独自の理論体系を持ち、計算効果との関係を研究することになるだろうが、おそらく計算効果とは見なされない、ということになるだろうか？
モナドは継続の研究において非常に直接的に現れる。したがって、モナドの概念は継続の一般化された意味論として見なされるかもしれない、ということになるだろうか？単位（unit）と余単位（counit）は、thunkとforceの一般化された形式として扱われることになる、ということになるだろうか？
おそらくLawvere理論 $L$ をモナド $T_L$ に送る構成は、CPS変換に数学的な支持を提供するものとして見なされるかもしれない、ということになるだろうか？$\lambda_c$-計算と計算メタ言語に対して、それぞれ異なる見た目の意味論を与えることができる。前者は閉Freyd圏（closed Freyd-category）[42,44]に基づき、後者はモナドに基づく。$\lambda_c$-計算の第一階のフラグメント（fragment）に焦点を当てることもできる。Lawvere理論は即座にモデルを提供し、健全で完全なクラスを容易に生成することができる[44]。

参考文献

[1]: Barr, M., and J. Beck, Acyclic models and triples, Proc. Conf. on Categorical Algebra at La Jolla (1966), 336–344.
[2]: Barr, M., and C. Wells, “Toposes, Triples, and Theories,” Grundlehren der math. Wissenschaften 278, Springer-Verlag, 1985.
[3]: Barr, M., and C. Wells, ”Category Theory for Computing Science,” Prentice-Hall, 1990.
[4]: Beck, J., “Triples, Algebra and Cohomology,” PhD thesis, Columbia University, New York, 1967.
[5]: Bunemann, P., S. Naqvi, V. Tannen and L. Wong, Principles of programming with complex objects and collection types, Theoretical Computer Science 149 (1995), 3-48.
[6]: Eckmann, B., and P. Hilton, Group-like structures in general categories i: multiplications and comultiplications, Math. Annalen 145 (1962), 227–255.
[7]: Eilenberg, S., and G. M. Kelly, Closed categories, in Proc. Conf. on Categorical Algebra at La Jolla (1966), 421–562.
[8]: Eilenberg, S., and J. C. Moore, Adjoint Functors and Triples, Illinois J. Math. 9 (1965), 381–398.
[9]: Freyd, P. J., Algebra-valued functors in general and tensor products in particular, Colloq. Math. Wroclaw 14 (1966), 89–106.
[10]: Godement, R., “Th´eorie des faisceaux,” Herman, Paris, 1958.
[11]: Gabriel, P., and F. Ulmer, “Lokal pr¨asentierbare Kategorien,” Lecture Notes in Mathematics 221, Springer-Verlag, Berlin, 1971.
[12]: Heckmann, R., Probabilistic Domains, Proc. CAAP ’94, Lecture Notes in Computer Science 136 (1994), 21-56.
[13]: Hyland, M., P. B. Levy, G. D. Plotkin and A. J. Power, Combining algebraic effects with continuations, Accepted in Theoretical Computer Science.
[14]: Hyland, M., G. D. Plotkin and A. J. Power, Combining computational effects: commutativity and sum, Proc. 2nd IFIP Conf on Theoretical Computer Science, (eds. Ricardo A. Baeza-Yates, Ugo Montanari and Nicola Santoro), Kluwer (2002), 474–484.
[15]: Hyland, M., G. D. Plotkin and A. J. Power, Combining effects: sum and tensor, Theoretical Computer Science, 357 (2006), 70-99.
[16]: Hyland, M., and A. J. Power, Pseudo-closed 2-categories and pseudo-commutativities, J. Pure Appl. Algebra 175 (2002), 141–185.
[17]: Hyland, M., and A. J. Power, Discrete Lawvere theories and computational effects, Theoretical Computer Science, 366 (2006), 144–162.
[18]: Jones, C., and G. D. Plotkin, A probabalistic power domain of evaluations. Proceedings of the 4th Symposium on Logic in Computer Science, IEEE Publications 1989, 186-195.
[19]: Kelly, G. M., “Basic Concepts of Enriched Category Theory,” Cambridge University Press, Cambridge, 1982.
[20]: Kelly, G. M., Structures defined by finite limits in the enriched context I, Cahiers Topologie Geom. Differentielle 23 (1982), 3–41.
[21]: Kinoshita, Y., A. J. Power and M. Takeyama, Sketches, J. Pure Appl. Algebra 143 (1999), 275–291.
[22]: Kleisli H., Every standard construction is induced by a pair of adjoint functors, Proc. Amer. Math. Soc. 16 (1965), 544-546.
[23]: Lawvere, F. W., “Functorial Semantics of Algebraic Theories,” PhD Thesis, Columbia University, 1963. (Available with commentary as TAC Reprint 5.)
[24]: Lawvere, F. W., An elementary theory of the category of sets, Proc. Nat. Acad. Sci. USA 50 (1964), 1506–1511. (Long version with commentary available as TAC Reprint 11.)
[25]: Lawvere, F. W., Some algebraic problems in the context of functorial semantics of algebraic structures, Reports of the Midwest Category Seminar II, (ed. S. Mac Lane), Lecture Notes in Mathematics 61, Springer-Verlag 1968, 41-61. (Available with commentary as addition to [23] in TAC Reprint 5.)
[26]: Lawvere, F. W., Adjointness in Foundations, Dialectica 23, 1969, 281-296. (Available with commentary as TAC Reprint 16.)
[27]: Lawvere, F. W., Equality in hyperdoctrines and the comprehension schema as an adjoint functor, Applications of Categorical Algebra, (ed. A. Heller), Proceedings of Symposia in Pure Mathematics 17, American Mathematical Society 1970, 1-14.
[28]: Lawvere, F. W., and R. Roseburgh, “Sets for Mathematics,” Cambridge University Press, 2003.
[29]: Linton, F. E. J., Some aspects of equational theories, Proc. Conf. on Categorical Algebra at La Jolla (1966), 84–95.
[30]: Linton, F. E. J., An outline of functorial semantics, Seminar on Triples and Categorical Homology Theory, Lecture Notes in Mathematics 80, 7-52.
[31]: Mac Lane, S., “Categories for the Working Mathematician,” Springer-Verlag, Berlin, 1971.
[32]: Makkai, M., and G. Reyes, “First-Order Categorical Logic,” Lecture Notes in Mathematics 611, Springer-Verlag, Berlin, 1977.
[33]: Moggi, E., Computational lambda-calculus and monads, Proc. LICS ’89 (1989), 14–23.
[34]: Moggi, E., An abstract view of programming languages, University of Edinburgh, Report ECS-LFCS- 90-113, 1989.
[35]: Moggi, E., Notions of computation and monads, Inf. and Comp. 93 (1991), 55–92.
[36]: Nishizawa, K., and A. J. Power, Lawvere theories over a general base, J. Pure Appl. Algebra, to appear.
[37]: Plotkin, G. D., and A. J. Power, Adequacy for Algebraic Effects, Proc. FOSSACS 2001, Lecture Notes in Computer Science 2030 (2001), 1–24.
[38]: Plotkin, G. D., and A. J. Power, Semantics for Algebraic Operations, Proc. MFPS XVII, Electronic Notes in Theoretical Computer Science 45 (2001) 1–14.
[39]: Plotkin, G. D., and A. J. Power, Notions of computation determine monads, Proc. FOSSACS 2002, Lecture Notes in Computer Science 2303 (2002), 342–356.
[40]: Plotkin, G. D., and A. J. Power, Computational effects and operations: an overview, Proc. Workshop Domains 2002, Electronic Notes in Theoretical Computer Science 73 (2002), 149–163.
[41]: Plotkin, G. D., and A. J. Power, Algebraic operations and generic effects, Applied Categorical Structures 11 (2003) 69–94.
[42]: Plotkin, G. D., and A. J. Power, Logic for computational effects: work in progress, Proc. IWFM 2003, EWiC (2003).
[43]: Power, A. J., Enriched Lawvere Theories, Theory and Applications of Categories 6 (1999), 83–93.
[44]: Power, A. J., Generic models for Computational Effects, Theoretical Computer Science 364 (2006), 254-269.
[45]: Schubert, H., “Categories,” Springer-Verlag, Berlin, 1972.
[46]: Street, R. H., The formal theory of monads, J. Pure and Applied Algebra 2, 1972, 149-168.
[47]: Varacca, D., The powerdomain of indexed valuations, in Proc. LICS 2002, IEEE Computer Society, 2002, 299-310.
[48]: Wadler, P., Comprehending monads, Mathematical Structures in Computer Science 2, 1992, 461-493.

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up