モナドと構文と計算 - (保存用) 檜山正幸のキマイラ飼育記メモ編

インスティチューションは概念を整理する枠組みとしては便利だが、中身がまったくないので、インスティチューションから出発してもラチがあかない。なんか実際のモノを作って、後から見たらそれはインスティチューションでした、ってことじゃないとダメだな。

で、抽象的インスティチューションに欠けている実質は、指標が何であるか？指標の圏が何であるか、指標の圏とモデルの圏をごちゃ混ぜにできるメカニズムなど。

構文論がモナドをベースにできることは、非常に確からしい気がする。ので、とりあえず、モナドから出発して、インスティチューションを意識しながらナニカ（何だ？）を作る方針にする。

モナドの例と解釈

モナドの例としては、自由ベクトル空間を作るモナドと自由半群（モノイドである必要はない）を作るモナドを考える。自由ベクトル空間を作るモナドの関手部分は K¹[A]、自由半群モナドでは A |→ A⁺ と書ける。K¹[A]は、K係数の1次多項式、A⁺は空を許さない列を表す。

これらの例からも分かるように、モナドの関手部分は項生成オペレータ（term {forming, production} operator）とみなせる。そして、モナド乗法は、普遍的一般的な項簡約規則を与える。簡約規則は完全に構文的なルールで、個別具体的な項集合には依存しないで記述できるもの；その記述がモナド乗法に他ならない。なんらかの形式的（実体は伴わない）計算ルールを学ぶことはモナド乗法を知ることだ。

アイレンベルク／ムーア構成

(T, μ, η)をC上のモナドとする。アイレンベルク／ムーア構成（Eilenberg-Moore）を考える。

最初に、関手Tに対してT代数の圏Alg_Tを考える。このときTは、代数の類型（similarity type）、または指標を与える。実際、任意の自己関手を指標と定義する流儀もある（代数、余代数の一般論）。ここでは、Tは項生成関手だが、項の全体は指標によって決まるので、指標Σと関手Tは、T = T_Σ により同一視できる。

A = (a:T(X)→X) がT代数のとき、X = |A| と書いて、代数Aの台と呼ぶ。台は最初の圏Cの対象である。台の概念を使えば、代数の圏Alg_TからCに、忘却関手U = U_Tを定めることができる。

A = (a:T(X)→X) に出てくるaは、項（式）に実際の値を対応させる写像のように解釈できるので、領域（みたいなナニカ）X上に「個別具体的な実際の計算機構＝形式的計算の意味」を与える。つまり、文字通りの“代数”である。

Xが何であれ、μ_X:TT(X)→T(X) はX上の形式的な計算を与える。一方で、a:T(X)→X は実質的・具体的な計算を与える。形式的な（構文論的な）計算と実質的（意味論的な）計算の互換性・協調性は次の可換図で示される。



 TT(X) -(μ)→ T(X)  (形式的な計算)

  ｜            ｜

  ｜T(a)        ｜a

  ↓            ↓

  T(X)  -(a)→  X    (実質的な計算)

(T(a);a) : TT(X)→X はXとaで具体化された個別の実際計算を行う（入れ子の内側の実質計算を先にやる）。一方、μ;a は先に形式的な計算を済ませて、最後の最後で実際の計算を行う。call by valueとcall by name に似てる感じもする。

アイレンベルク／ムーア構成を済ませると、モナド(T, μ, η)から随伴対 (F_T -| U_T) ができる。モナド単位ηはそのまま随伴対（関手の双対）の単位となる。さらに、随伴余単位εが定義できる。余単位はev（evaluation）とも書かれるが、実際、ε:(F・U)(A)→A は、U(A) = |A| という台から構成された項に対する個別具体的な実際の計算を遂行することを意味する。

モナド乗法 -- 形式的一般的な項簡約規則
余単位 -- 個別具体的な演算の遂行

クライスリ構成

Kleisliを何とカタカナ表記すべきか？わからーん！が、「クライスリ」を採用することにした。

(T, μ, η)をC上のモナドとして、そのクライスリ圏をK_Tとする。ホントはK_{(T, μ, η)}と書くべきだが少しさぼる。CをK_Tに埋め込むのは簡単。いま、クライスリ射（クライスリ圏の射）f:X→T(Y) があったとき、fの拡張f^#:T(X)→T(Y)を対応させれば、(X |→ T(X), f |→ f^#) により、K_T→Cの関手が定義できる。埋め込みと拡張が随伴対なのだと思う（今、確認してないが）。

クライスリ射とその拡張の構文論的・計算論的意味だが、クライスリ射は、置換（substitution）の定義、またはマクロの定義となる。fがマクロ定義のとき、f^#は、そのマクロ定義を使ったマクロ展開（置換）を与える。

アイレンベルク／ムーア構成では、値の集合（とみなせる）台対象と、“ホントの演算”とみなせる項集合からの射が登場したが、クライスリ構成では、値もホントの演算も出てこないで、マクロの計算だけで済んでしまっている。

確証はまったくないが、クライスリ圏のほうが指標の圏を与えて、アイレンベルク／ムーア圏のほうがモデルの圏を与えるような気がする。インスティチューションの論理文Senに関しても、項から論理式を生成するような論理式生成モナドが介在しているんじゃなからろうか。