構文付き変換手インスティチューション 2/n 実例：モノイド - 檜山正幸のキマイラ飼育記 (はてなBlog)

「構文付き変換手インスティチューション 1/n」で言い残していることはあるのですが、いったんそれは棚上げにして構文付き変換手インスティチューションの実例を挙げます。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\op}{ \mathrm{op} }
\newcommand{\In}{\text{ in }}
%\newcommand{\u}[1]{\underline{#1}}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\twoto}{ \Rightarrow }
\newcommand{\id}{ \mathrm{id} }
\newcommand{\hyp}{\text{－} }
%\newcommand{\DiagI}[1]{ {#1}\text{-}\mathrm{Diag}}
\newcommand{\dimU}[2]{ {{#1}\!\updownarrow^{#2}} }
%\newcommand{\NFProd}[3]{ \mathop{_{#1} \!\underset{#2}{\times}\,\!_{#3} } }
%\newcommand{\dblcat}[1]{\mathbb{#1}}
`$

内容：

構文付き変換手インスティチューションの全体像
自由モノイドの表現
一般論：代入の圏
モノイドの線形表現
モノイドの線形表現続き

ハブ記事：

構文付き変換手インスティチューション 1/n

構文付き変換手インスティチューションの全体像

「構文付き変換手インスティチューション 1/n」の短い復習です。構文付き変換手インスティチューション〈transforial institution with syntax〉は次の構成素からなります。この図全体が可換図式というわけではありません。

$`\quad \xymatrix@C+1pc@R+1pc {
\cat{Sign} \ar@/^1pc/[r]^{F} \ar@/_/[dr]_{J_\mrm{sign}}
\ar@{}[r]|{\bot}
& \cat{Thy} \ar@/^1pc/[l]^{U} \ar[d]^{J_\mrm{thy}}
\\
{}
& \cat{Amb}
} % transforial inst
`$

この図が描かれている“場所／環境”は問題ですが、今はあまり気にしないことにします。構成素の呼び名は次のようです。

$`\cat{Sign}`$ ：指標の圏〈category of signatures〉
$`\cat{Thy}`$ ：セオリーの圏〈category of theories〉
$`F`$ ：構文随伴系の自由関手〈free functor〉
$`U`$ ：構文随伴系の忘却関手〈forgetful functor〉
$`\cat{Amb}`$ ：アンビエント〈ambient〉
$`J_\mrm{thy}`$ ：（セオリーの圏からの）編入関手〈incorporation functor〉
$`J_\mrm{sign}`$ ：（指標の圏からの）編入関手〈incorporation functor〉

$`F \dashv U`$ が作る随伴系は構文随伴系〈syntax adjunction〉です。$`\cat{Amb}`$ の対象はn-圏（n = 0, 1, 2, …）であり、ターゲットと呼びます*1。

圏 $`\cat{Sign}`$ には、有限余完備包含圏〈finitely cocomplete inclusive category〉という条件を課します*2。$`\Sigma \in |\cat{Sign}|`$ と $`\cat{T} \in |\cat{Amb}|`$ に対して、次のホムn-圏は、変換手のn-圏（とりあえずは n = 1, 2）である必要があります。

$`\quad \mrm{Model}(\Sigma, \cat{T}) := \cat{Amb}(J_\mrm{thy}(F(\Sigma)), \cat{T})`$

$`\cat{Amb}`$ が内部ホム $`[\hyp, \hyp]_{\cat{Amb}}`$ を持っている場合は、次の定義もありです。（'$`I`$' は "internal" から。）

$`\quad \mrm{IModel}(\Sigma, \cat{T}) := [J_\mrm{thy}(F(\Sigma)), \cat{T}]_\cat{Amb}`$

$`\cat{Amb}`$ の対象としてデフォルトのターゲット $`\cat{D}`$ が決まっている場合は、一引数のモデル圏関手 $`\mrm{Model}(\Sigma)`$ を次のように定義できます。

$`\quad \mrm{Model}(\Sigma) := \cat{Amb}(J_\mrm{thy}(F(\Sigma)), \cat{D})`$

自由モノイドの表現

$`\text{一般論}`$	$`\text{具体例}`$
$`\cat{Sign}`$	$`{\bf Set}`$
$`\cat{Thy}`$	$`{\bf Mon}`$
$`F`$	$`\mrm{FreeMon}`$
$`U`$	$`\mrm{UnderlSet}`$
$`J_\mrm{thy}`$	$`\mrm{MonAsCat}`$
$`\cat{Amb}`$	$`{\bf CAT}`$
$`\cat{D}`$	$`{\bf Set}`$

指標 $`\Sigma \in |{\bf Set}|`$ は単なる集合です。セオリーとはモノイドのことです。指標＝集合から自由生成されるセオリーは、集合 $`\Sigma`$ を生成系とする自由モノイドです。セオリー＝モノイド $`M`$ の台集合は $`\mrm{UnderlSet}(M)`$ です。次の随伴系があります。

$`\quad \xymatrix@C+1pc@R+1pc {
{\bf Set} \ar@/^1pc/[r]^{ \mrm{FreeMon} }
\ar@{}[r]|{\bot}
& {\bf Mon} \ar@/^1pc/[l]^{\mrm{UnderlSet} }
}\\
\quad \In {\bf CAT} % adjunction exam
`$

セオリー＝モノイド達の圏 $`{\bf Mon}`$ からの編入関手 $`\mrm{MonAsCat}`$ は、モノイドを単一対象の圏とみなす関手です。

$`\quad \mrm{MonAsCat} : {\bf Mon} \to {\bf CAT} \In \mathbb{CAT}`$

ここで、$`\In \mathbb{CAT}`$ があるので、2-圏 $`{\bf CAT}`$ は自動的に次元調整（「圏の次元調整」を参照）されて、$`\dimU{\bf Cat}{1}`$ になると思ってください。

デフォルト・ターゲットは集合圏なので、セオリー＝モノイド $`M`$ に対するモデル圏は次のようになります。

$`\quad {\bf CAT}(\mrm{MonAsCat}(M), {\bf Set})`$

これは、モノイド $`M`$ の表現達の圏です。モノイドが、集合の自己準同型写像〈endomorphism〉達のモノイドにより“表現”されます。表現〈モデル〉達の圏の射は、表現のあいだの繋絡作用素〈けいらくさようそ | intertwiner〉です。

指標＝集合 $`\Sigma`$ に対するモデル圏は：

$`\quad \mrm{Model}(\Sigma) := {\bf CAT}(\mrm{MonAsCat}(\mrm{FreeMon}(M) ), {\bf Set})`$

集合の自由モノイドに対する表現の圏が、その集合〈指標〉のモデル圏となります。指標が $`\Sigma`$ である自由モノイドの表現の別名は、アルファベットが $`\Sigma`$ であるラベル付き状態遷移系〈labeled {state}? transition system〉です。

一般論：代入の圏

前節の自由モノイドの表現を事例に使って、一般論を挟みます。

構文付き変換手インスティチューションには、以下の随伴系〈構文随伴系〉が備わっていました。

$`\quad \xymatrix@C+1pc@R+1pc {
\cat{Sign} \ar@/^1pc/[r]^{F}
\ar@{}[r]|{\bot}
& \cat{Thy} \ar@/^1pc/[l]^{U}
}\\
\quad \In {\bf CAT} % syntax adjunction
`$

この随伴系から、指標の圏 $`\cat{Sign}`$ 上のモナドが誘導されます。このモナドを項生成モナド〈term-generating monad〉、または構文モナド〈syntax monad〉と呼び、記号の乱用で次のように書きます。

$`\quad G = G/\cat{Sign} = (G, \mu, \eta)/\cat{Sign}\\
\text{Where}\\
\quad G: \cat{Sign} \to \cat{Sign} \In {\bf CAT}\\
\quad \mu :: G*G \twoto G : \cat{Sign} \to \cat{Sign}\In {\bf CAT}\\
\quad \eta :: \mrm{Id}_\cat{Sign} \twoto G : \cat{Sign} \to \cat{Sign}\In {\bf CAT}
`$

自由モノイドの表現の場合、構文モナドは集合圏上のリストモナドになります。

$`\quad G = (\mrm{List}, \mrm{flatten}, \mrm{sing})/{\bf Set}`$

構文モナドのクライスリ圏を代入の圏〈category of substitutions〉と呼び、一般的に次のように書きます。

$`\quad \cat{Subst} := \mrm{Kl}(G) = \mrm{Kl}(G/\cat{Sign})`$

圏 $`\cat{Subst}`$ の射、つまり構文モナドのクライスリ射を代入射〈substitution morphism〉、または単に代入〈substitution〉と呼びます。

自由モノイドの表現の場合、代入射 $`s: \Sigma \to \Gamma`$ は、集合 $`\Sigma`$ の要素に $`\mrm{List}(\Gamma)`$ の要素（リスト）を対応させる写像です。$`\Sigma, \Gamma`$ が有限なら、次のような記述構文で指標と代入を書けます。リストは、要素の単なる並び（文字列）として書いています。

$`\text{signature }\Sigma \:\{\\
\quad \text{element }a, b, c\\
\}\\
\text{signature }\Gamma \:\{\\
\quad \text{element }x, y, z, w\\
\}\\
\:\\
\text{substitution } s : \Sigma \to \Gamma \:\{\\
\quad a := yyzxy\\
\quad b := w\\
\quad c := zwz\\
\}
`$

代入の表現に '$`:=`$' を使ってますが、これはタマタマこの記号を選んだだけで、'$`\Leftarrow`$' とか '$`\mapsto`$' とかでもかまいません。なんなら、カンマで区切ったペア $`(a, yyzxy)`$ でも何の問題もありません。記述構文の選択は常に恣意的であって、なんだっていいのです。

モデル圏関手 $`\mrm{Model}(\hyp, \hyp)`$ は、代入の圏に拡張できます。拡張したモデル圏関手は $`\mrm{SubstModel}`$ とします。ただし、対象パートはもとの $`\mrm{Model}`$ と同じです。

$`\quad \mrm{SubstModel} : \cat{Subst}^\op \times \cat{Amb} \to {\bf CAT} \In \mathbb{2CAT}`$

$`\cat{Amb}`$ の内部ホムによりモデル圏関手が定義されている場合は：

$`\quad \mrm{SubstIModel} : \cat{Subst}^\op \times \cat{Amb} \to \cat{Amb} \In \mathbb{2CAT}`$

$`\In \mathbb{2CAT}`$ と書いているので、2-圏達の3-圏内で考えていますが、それが煩雑なら $`\In \mathbb{CAT}`$ として、1-圏達の2-圏内へと次元を落としてもかまいません。

代入 $`s:\Sigma \to \Gamma`$ に対する $`\mrm{SubstModel}(s, \cat{T})`$ は次の手順で定義します。

$`s`$ を $`s:\Sigma \to U(F(\Gamma)) \In \cat{Sign}`$ と考える。
随伴 $`F \dashv U`$ のホムセット同型 $`\cat{Sign}(\Sigma, U(F(\Gamma)) ) \cong \cat{Thy}(F(\Sigma), F(\Gamma))`$ により得られる射を $`s': F(\Sigma)\to F(\Gamma) \In \cat{Thy}`$ とする。
$`\mrm{SubstModel}(s, \cat{T}) := \cat{Amb}(J_\mrm{thy}(s'), \mrm{Id}_{\cat{T}})`$ と定義する。

$`\cat{Subst}`$ の射 $`s`$ は、構文モナド $`G = U(F(\hyp))`$ で定義されるプログラミング言語で書かれたプログラムコードだと解釈することができます。$`\mrm{SubstModel}(s)`$ は、（関手意味論における） $`s`$ の意味〈セマンティクス〉を与えます。

モノイドの線形表現

$`\text{一般論}`$	$`\text{具体例}`$
$`\cat{Sign}`$	$`{\bf MonSign}`$
$`\cat{Thy}`$	$`{\bf Mon}`$
$`F`$	$`\mrm{FreeQuoMon}`$
$`U`$	$`\mrm{FullMonSign}`$
$`J_\mrm{thy}`$	$`\mrm{MonAsCat}`$
$`\cat{Amb}`$	$`{\bf CAT}`$
$`\cat{D}`$	$`{\bf Vect}_{\bf R}`$

セオリーの圏は前々節と同じくモノイドの圏ですが、指標はモノイド向けのコンピュータッドを使います。コンピュータッドについては以下の記事に説明があります。ただし、ここで使うコンピュータッドはだいぶ単純なものです。

ここでの指標 $`\Sigma`$ は、集合 $`A`$ と“モノイド向けの等式”の集合 $`E`$ のペア $`(A, E)`$ です。$`E`$ は次の条件で記述できます。

$`\quad E \subseteq \mrm{List}(A)\times \mrm{List}(A)`$

$`E`$ は空集合でもかまいません。$`\Sigma = (A, E)`$ は、例えば次の構文で記述できます。

$`\text{signature }\Sigma \:\{\\
\quad \text{element }a, b, c\\
\quad \text{equation eq1} : aaa = a\\
\quad \text{equation eq2} : bc = c\\
\}
`$

これは、$`A = \{a, b, c\},\; E = \{(aaa, a), (bc, c)\}`$ をそれらしく書いたものです。

$`{\bf MonSign}`$ の対象（＝指標）の定義は今述べたとおりなので、指標のあいだの射（$`\cat{Sign}`$ の射）について述べます。集合のあいだの写像 $`f:A \to B \In {\bf Set}`$ があると、次の写像が誘導されます。

$`\quad f_* : \mrm{List}(A)\times \mrm{List}(A) \to \mrm{List}(B)\times \mrm{List}(B) \In {\bf Set}`$

さらに、像集合を対応させる写像が誘導されますが、同じ記号で書きます。

$`\quad f_* : \mrm{Pow}( \mrm{List}(A)\times \mrm{List}(A)) \to \mrm{Pow}(\mrm{List}(B)\times \mrm{List}(B) ) \In {\bf Set}`$

指標 $`\Sigma = (A, E)`$ から指標 $`\Gamma = (B, F)`$ への指標射とは、写像 $`\varphi: A \to B`$ であって、次を満たすものです。

$`\quad \varphi_*(E) \subseteq F`$

記述を簡潔にするために、以下のような写像を、いずれも $`\varphi`$ で表します（名前をオーバーロード〈多義的使用〉します）。

$`\varphi : A \to B \In {\bf Set}`$
$`\varphi : \mrm{List}(A) \to \mrm{List}(B) \In {\bf Set}`$
$`\varphi : \mrm{List}(A)\times \mrm{List}(A) \to \mrm{List}(B)\times \mrm{List}(B) \In {\bf Set}`$
$`\varphi : \mrm{Pow}(\mrm{List}(A)\times \mrm{List}(A) ) \to \mrm{Pow}(\mrm{List}(B)\times \mrm{List}(B)) \In {\bf Set}`$
$`\varphi: \Sigma \to \Gamma \In {\bf MonSign}`$

指標 $`\Sigma = (A, E)`$ と指標 $`\Gamma = (B, F)`$ のあいだの包含〈inclusion〉は次のように定義します。

$`\quad \Sigma \sqsubseteq \Gamma \;\mathrel{:\!\!\iff} A \subseteq B \;\land\; E \subseteq F`$

例えば、$`(A, \emptyset) \sqsubseteq (A, E)`$ です。

以上のように定義した、包含が定められた圏を $`{\bf MonSign}`$ とします。この $`{\bf MonSign}`$ が有限余完備包含的圏であることを示すのはけっこう面倒だと思います。たぶんそうなっているでしょ（ちゃんと確認してない）*3。

モノイドの線形表現続き

次のような随伴系を構成する必要があります。

$`\quad \xymatrix@C+1pc@R+1pc {
{\bf MonSign} \ar@/^1pc/[r]^{ \mrm{FreeQuoMon} }
\ar@{}[r]|{\bot}
& {\bf Mon} \ar@/^1pc/[l]^{\mrm{FullMonSign} }
}\\
\quad \In {\bf CAT} % adjunction exam
`$

順に構成していきましょう。

$`\Sigma = (A, E) \in |{\bf MonSign}|`$ に対する $`\mrm{FreeQuoMon}(\Sigma)`$ は次のように作ったモノイドです。

リストの集合 $`A^\star := \mrm{List}(A)`$ を作る。（右肩の星印はクリーネスター。）
すべての $`\alpha = (\alpha_1, \alpha_2) \in E`$ に対して、$`\alpha_1 \sim \alpha_2`$ となるような $`A^\star`$ 上の同値関係で最小の同値関係 $`\sim`$ を作る。
商集合〈quotient set〉 $`A^\star/\!\sim`$ を作る。
リストの集合上の連接モノイド構造（自由モノイド構造）と協調するモノイド構造を、商集合 $`A^\star/\!\sim`$ 上に構成する。
こうして作ったモノイドとその台集合をどちらも（記号の乱用で） $`A^\star/E`$ と書く。

今約束した記法で、次のように書けます。

$`\quad \mrm{FreeQuoMon}(\Sigma) = \mrm{FreeQuoMon}( (A, E) ) := A^\star/E \;\in |{\bf Mon}|`$

同値関係の標準射影を $`\pi: A^\star \to A^\star/E`$ とすると、それぞれの集合に載ったモノイド構造に対して射影 $`\pi`$ はモノイド準同型射になります。

$`\quad \pi = \pi_\Sigma = \pi_{(A, E)} \; : \mrm{FreeMon}(A) \to \mrm{FreeQuoMon}( (A, E) ) \In {\bf Mon}`$

以上で、関手 $`\mrm{FreeQuoMon}`$ の対象パート〈object part〉は定義できました。次は射パート〈morphism part〉です。$`\varphi : (A, E) \to (B, F) \In {\bf MonSign}`$ に対して、$`\mrm{FreeQuoMon}(\varphi)`$ を構成します。

既に、次のような写像とモノイド準同型射はできています。

$`\quad \mrm{List}(\varphi) : \mrm{List}(A) \to \mrm{List}(B) \In {\bf Set}\\
\quad \mrm{FreeMon}(\varphi) : \mrm{FreeMon}(A) \to \mrm{FreeMon}(B) \In {\bf Mon}
`$

これらをどちらも（記号の乱用／オーバーロードで）次のように略記します。

$`\quad \varphi^\star : A^\star \to B^\star
`$

$`\mrm{FreeQuoMon}( (A,E)), \mrm{FreeQuoMon}( (B, F))`$ を作る途中で、同値関係を備えた集合を作りました。それらを次のように置きます。

$`\quad (A, \sim_E), (B, \sim_F)`$

同値関係を備えた集合はセットイド〈setoid | 亜集合〉と呼ぶので、$`(A, \sim_E), (B, \sim_F)`$ はセットイドです。

$`\varphi^\star`$ は同値関係を保存することが示せるので、セットイドのあいだの準同型写像になります。

$`\quad \varphi^\star : (A, \sim_E) \to (B, \sim_F) \In {\bf Setoid}`$

ここでも、同じ記号を使っています（記号の乱用／オーバーロード）。

$`\varphi^\star`$ が同値関係を保存する写像（セットイドのあいだの準同型写像）ならば、以下の可換図式の点線の写像が一意に定まります。

$`\quad \xymatrix{
{(A^\star, \sim_E)} \ar[r]^{\varphi^\star} \ar[d]_{\pi}
\ar@{}[dr]|{\text{commutative}}
& {(B^\star, \sim_F)} \ar[d]^{\pi}
\\
{A^\star/E} \ar@{.>}[r]_{?}
& {B^\star/F}
}`$

一意に決まる写像は、モノイドとしての $`A^\star/E, B^\star/F`$ のあいだのモノイド準同型射になることも確認できます。これを、$`\mrm{FreeQuoMon}( \varphi)`$ とします。

$`\quad \mrm{FreeQuoMon}( \varphi) : \mrm{FreeQuoMon}( (A,E)) \to \mrm{FreeQuoMon}( (B, F))
\In {\bf Mon}
`$

さらに、$`\mrm{FreeQuoMon}(\hyp)`$ の関手性の確認も必要です。まー、なにやかにや細かい作業をすれば、次の関手ができ上がります。

$`\quad \mrm{FreeQuoMon} : {\bf MonSign} \to {\bf Mon} \In {\bf CAT}
`$

さて、逆向きの関手 $`\mrm{FullMonSign}`$ も必要です。これは簡単に触れます。与えられたモノイド $`M`$ に対してモノイド指標 $`(A, E)`$ を次のように定義します。

$`A := \underline{M}`$ （モノイドの台集合）
$`E := \{ (\alpha_1, \alpha_2) \in A^\star\times A^\star \mid \prod_M(\alpha_1) = \prod_M(\alpha_2) \}`$

$`\prod_M(\alpha)`$ は、モノイドの台集合の要素のリスト $`\alpha\in {\underline{M}}^\star`$ の総積をとる操作です。要するに、$`M`$ 上で“ほんとに等しい”リストのペアをすべて集めて $`E`$ を作ります。

なにやかにや細かい作業をすれば、次の関手ができ上がります。

$`\quad \mrm{FullMonSign} : {\bf Mon} \to {\bf MonSign} \In {\bf CAT}
`$

2つの関手が作れてもまだ終わりではなくて、2つの関手が随伴ペアになっていることも示す必要があります。あー、大変。随伴性は割愛ね。

セオリーの圏＝モノイドの圏 $`{\bf Mon}`$ からの編入関手 $`\mrm{MonAsCat}`$ は、モノイドを単一対象の圏とみなす関手です。前の例と同じです。これは簡単。

$`\quad \mrm{MonAsCat} : {\bf Mon} \to {\bf CAT} \In \mathbb{CAT}`$

デフォルト・ターゲットは実数係数ベクトル空間の圏なので、セオリー＝モノイド $`M`$ に対するモデル圏は次のようになります。

$`\quad {\bf CAT}(\mrm{MonAsCat}(M), {\bf Vect}_{\bf R})`$

これは、モノイド $`M`$ に対する、自己線形写像〈linear endomorphism〉モノイドによる表現達の圏です。表現の圏の射は、表現のあいだの線形な繋絡作用素です。

モノイド指標（$`{\bf MonSign}`$ の対象） $`\Sigma`$ に対するモデル圏（線形表現の圏）は次のとおりです。

$`\quad \mrm{Model}(\Sigma) := {\bf CAT}(\mrm{MonAsCat}(\mrm{FreeQuoMon}(\Sigma)), {\bf Vect}_{\bf R})`$

構文付き変換手インスティチューションの事例は、まだ色々あります。が、今日のところはモノイドの例を紹介できたところでおわりにします。

*1:ターゲットは、モデルを作るとき、モデルが展開・配備〈deploy〉される“場所”になります。

*2:この条件はきつ過ぎるかも知れません。もっとゆるい条件に変更するかも知れません。

*3:仮に、有限余完備包含的圏になってなくてもシリアスな問題ではありません。有限余完備包含的という条件がちょっときつ過ぎるかな、と思っているので、必要なら条件をゆるまます。

構文付き変換手インスティチューションの全体像

自由モノイドの表現

一般論： 代入の圏

モノイドの線形表現

モノイドの線形表現 続き

一般論：代入の圏

モノイドの線形表現続き