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

随伴系、モナド、モナドのアイレンベルク／ムーア代数、自己関手のランベック代数、ベックの分配法則などを扱っていると、こういうモノ達を系統的に組織化したい、という気持ちになります。

代数的構造の組織化のためには、ゴグエン／バーストル〈Joseph Goguen, Rod Burstall〉のインスティチューションが優れたフレームワークです。が、上記のような構造を扱うには幾つかの問題があります。

抽象的過ぎる。
構文を表現する手段が貧弱。
高次元のサポートがない。

そこで、具象的で構文を表現できて高次元（当面は2次元）を扱えるインスティチューションを考えようと思い立つわけです。もう何年も前からそう思っています。

が、なかなかうまくいかない。素材がうまく噛み合ってくれないのですよ。最近になって、「なにがマズいのだろう？」とかえりみると、次元・サイズ・形状ポリシー（いずれ説明するでしょう）にこだわり過ぎだった気がします。「そこらへんはテキトーでいいや」と割り切るとうまくいきそうです（たぶん）。

タイトルに「1/n」を付けているのは、この記事の続きがあることを示唆しています。が、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}}
`$

内容：

インスティチューション
等式的関手インスティチューション
指標と仕様
包含構造を持つ指標の圏
構文付き変換手インスティチューション
構文論と意味論

関連記事：

インスティチューション

インスティチューションの創始者・ゴグエン〈Joseph Goguen〉先生は2006年7月3日にお亡くなりになりました。インスティチューションのホームページはそのまま残っています。

https://cseweb.ucsd.edu/~goguen/projs/inst.html

インスティチューションに関する最初の論文 "Introducing Institutions" はインターネット上では見つからないようですが、"Institutions: Abstract model theory for specification and programming" は上記サイトからPostScript形式のファイルとしてダウンロードできます。PDFが欲しいなら、次があります。

[GB92]
Title: Institutions: Abstract Model Theory for Specification and Programming
Authors: Joseph Goguen and Rod Burstall
Date: Jan. 1992
Pages: 52p
URL: https://dl.acm.org/doi/pdf/10.1145/147508.147524 （PDFファイル）

インスティチューション〈institution〉は次の構成素からなります。（おいおい説明していきます。）

	ゴグエン／バーストル	この記事
指標の圏	$`{\bf Sign}`$	$`\cat{Sign}`$
モデル圏関手	$`{\bf Mod}`$	$`\mrm{Model}`$
文集合関手	$`Sen`$	$`\mrm{Prop}`$
充足関係	$`\models_\Sigma`$

オリジナル〈ゴグエン／バーストル〉のインスティチューションの構成素達のプロファイル（域・余域の仕様）は：

$`{\bf Sign} \in |{\bf CAT}|`$
$`{\bf Mod} : {\bf Sign}^\op \to \dimU{\bf CAT}{1} \In \mathbb{CAT}`$
$`Sen : {\bf Sign} \to {\bf Set} \In {\bf CAT}`$

$`\dimU{\bf CAT}{1}`$ は、小さいとは限らない圏達の2-圏から2-射〈自然変換〉を捨てた1-圏です。$`\dimU{\hyp}{1}`$ という書き方については、「圏の次元調整」を参照してください。

充足関係〈satisfaction relation〉の定義は、指標 $`\Sigma \in |{\bf Sign}|`$ ごとに：

$`(\models_\Sigma) \subseteq |{\bf Mod}(\Sigma)|\times Sen(\Sigma)`$

この記事（と引き続く記事）で述べる構文付き変換手インスティチューションでは、充足関係はまったく違った形になります。

インスティチューションの定義に登場する $`{\bf Sign}, {\bf Mod}, Sen, \models`$ は、抽象的なモノで、「具体的にそれはなに？」と聞かれても答えようがありません。もちろん、抽象的な公理系から言えることも多々あり、それは任意のインスティチューションに適用できる一般的な結果となります。

実際にインスティチューションを使うときは、$`{\bf Sign}, {\bf Mod}, Sen, \models`$ を具体化する必要があります。完全に具体化してしまうと融通が効かないので、抽象的な定義と個別具体例の中間的な構造があると便利です。そのような、ある程度は具体化した構造を半具象インスティチューション〈semi-concrete institution〉と呼びましょう。

以下の（3日間で書かれた）過去記事は、半具象インスティチューションを模索した記録として読めます。

等式的関手インスティチューション

前節の最後に挙げた過去記事達では、半具象インスティチューションの一形態として、等式的関手インスティチューション〈equational functorial institution〉を提案しています。この節では、等式的関手インスティチューションについて、現時点からみて整理した形で要約します*1。

形容詞「関手〈functorial〉」は、モデルの構成にローヴェア流の関手意味論〈functorial semantics〉を使う、ということを表現しています。説明しましょう；インスティチューションにおけるモデル圏関手〈category-of-models functor〉$`{\bf Mod}`$ は抽象的・公理的に存在が要請されるものです。多くの具体例では、モデル圏が関手圏として作られます。つまり、次のように定義されるのです。

$`\quad {\bf Mod}(\Sigma) := {\bf CAT}(\Sigma^\diamondsuit, {\bf Set}) \;\in |{\bf CAT}|`$

ここで、$`(\hyp)^\diamondsuit`$ は、指標から“なんらかの圏”を生成するオペレーターです。

$`\quad |{\bf Sign}| \ni \Sigma \mapsto \Sigma^\diamondsuit \in |{\bf CAT}|`$

そうであるなら、オペレーター $`(\hyp)^\diamondsuit`$ の存在を要請すれば、モデル圏関手 $`{\bf Mod}`$ は構成可能となるので、インスティチューションの公理的定義からは削除できます。

オペレーター $`(\hyp)^\diamondsuit`$ をうまく定義するために（他の理由もありますが）、過去記事では、指標の圏も完全に具体的な圏として定義しています。具象的な指標〈concrete signature〉とは、有向グラフです。オペレーター $`(\hyp)^\diamondsuit`$ は、有向グラフから自由圏〈パスの圏〉を生成する自由関手の余域を $`{\bf CAT}`$ に広げたものです。（以下の $`\mrm{Inc}`$ は包含です。）

$`\quad \mrm{FreeCat} : {\bf Graph} \to \dimU{\bf Cat}{1} \In {\bf CAT}\\
\quad \mrm{Inc}\; : \dimU{\bf Cat}{1} \to {\bf CAT} \In \mathbb{2CAT}\\
\quad (\hyp)^\diamondsuit = \mrm{FreeCat}* \mrm{Inc}\; :{\bf Graph} \to {\bf CAT} \In \mathbb{2CAT}
`$

形容詞「等式的〈equational〉」は、論理式として等式の連言〈AND結合〉を使う、ということを表現しています。射のあいだの等式を、集合圏（あるいは他の圏でも）の2-射と考えれば、等式的論理〈equational logic〉はすべての圏に組み込みで存在していて、タダで使えます。タダで使えるものは遠慮なく使おう、という方針です。

具体的な指標（有向グラフ）の圏がある状況では、インスティチューションにおける文〈論理文 | {logical}? sentence〉の集合 $`Sen(\Sigma)`$ は、指標（有向グラフ）のすべてのパス同値関係達の集合です。パス同値関係は等式に対応するので、$`Sen(\Sigma)`$ は $`\Sigma`$ に追加可能な等式の集合とみなせます。有向グラフにパス同値関係の集合（空集合でもよい）を付け足したものは仕様〈specification〉と呼びます。ただし、仕様のことも（広義に）指標と呼ぶことも多いです -- この点は次節で議論します。

指標の圏を具体的な圏（有向グラフの圏）とすることで、指標 $`\Sigma`$ （有向グラフ）に対する文はパス同値関係（等式と同じ）として具体的に与えられます。文集合関手 $`Sen`$ も構成可能となるので、インスティチューションの公理的定義からは削除できます。

指標と仕様

インスティチューションにおいて、指標〈signature〉と仕様〈specificatio〉を区別すべきか、一律に扱うべきかは悩みのタネです。例えば以下は、半群〈semigroup〉の定義を単一の指標（仕様との区別なし）で書く例と、指標と仕様を区別して書く例です。

$`
\text{signature Semigroup }\{\\
\quad \text{sort }A\\
\quad \text{operation }m : A\times A \to A\\
\quad \text{equation assoc} :: (m \times \id_A); m = \alpha_{A,A,A}; (\id_A \times m); m\\
\}
`$

$`
\text{signature SemigroupSig }\{\\
\quad \text{sort }A\\
\quad \text{operation }m : A\times A \to A\\
\}\\
\text{specification Semigroup }\{ \\
\quad \text{signature SemigroupSig} \\
\quad (m \times \id_A); m = \alpha_{A,A,A}; (\id_A \times m); m\\
\}
`$

ゴグエン／バーストルのインスティチューションは、指標と仕様を分けることを想定しているようです。指標 $`\Sigma`$ はソート〈型 | 台集合〉と演算〈オペレーション〉の宣言だけで、指標に $`Sen(\Sigma)`$ の文を幾つか追加して仕様を作る、という方式です。

しかし、指標と仕様を区別する方式はけっこう不便なんですよ。「指標と仕様」では多パート指標〈multipart signature〉という概念を導入しました。仕様の内部をいくつかのパートに分けてよい、というものです。例えばデータパートと公理パートに分けると次のようです。

$`
\text{signature Semigroup }\{\\
\:\: \text{Data }\{\\
\quad \text{sort }A\\
\quad \text{operation }m : A\times A \to A\\
\:\: \}\\
\:\: \text{Axioms }\{\\
\quad \text{equation assoc} :: (m \times \id_A); m = \alpha_{A,A,A}; (\id_A \times m); m\\
\:\: \}\\
\}
`$

ひとつの指標を複数のパートに分けるやり方は色々ありますが、経験上、上記の分け方のように、台集合と演算でひとつのパート、要求される法則〈公理 | 条件〉でもうひとつのパートが多いです。

パートに分けるのではなくて、指標を拡大〈拡張 | extend〉する機能を導入するテもあります。

$`
\text{signature SemigroupData }\{\\
\quad \text{sort }A\\
\quad \text{operation }m : A\times A \to A\\
\}\\
\text{signature Semigroup extends SemigroupData }\{\\
\quad \text{equation assoc} :: (m \times \id_A); m = \alpha_{A,A,A}; (\id_A \times m); m\\
\}
`$

以下の過去記事（古い順）では、実際に指標を拡大〈拡張〉する方式を使っています。

結局、指標と仕様の明示的な区別は設けずに、指標の拡大〈拡張〉を使うのが融通が効いて便利だと思います。そのためには、指標の圏には拡大〈extension〉をサポートする構造が必要になります。

包含構造を持つ指標の圏

等式的関手インスティチューションでは、指標は有向グラフ、またはパス同値関係の集合を追加した有向グラフだと具体的に定義しています。これは具体化し過ぎでした。カバーできる範囲が狭すぎるし一般化もできないし ‥‥ ここはある程度抽象的にすべきです。

抽象的な構造としての指標の圏を $`\cat{Sign}`$ とします。ゴグエン／バーストルの記法とはフォントを変えています。その理由は：

太字の名前（$`{\bf Set}`$ や $`{\bf CAT}`$ など）は、圏（高次圏も含む）の固有名に使う習慣があるので、$`{\bf Sign}`$ だと固有特定の圏のように思えてしまう。
一般的な圏はカリグラフィー体の名前（$`\cat{C}`$ や $`\cat{D}`$ など）にしているが、Sign という綴りは使いたい。それで $`\cat{Sign}`$ 。

というわけで、指標の圏 $`\cat{Sign}`$ は固有特定の圏ではありません。が、まったく勝手な圏というわけでもありません。前節で述べた指標の拡大をサポートするには、それなりの構造を持つ必要があります。指標の圏に要求される性質・構造は有限余完備性と包含構造〈inclusion {structure | system}〉です。

指標の圏に包含構造を導入することは、ゴグエン／ロス〈Joseph Goguen, Grigore Rosu〉、ダイアコネスク〈Razvan Diaconescu〉、カザネスク／ロス〈Virgil Emil Cazanescu, Grigore Rosu〉などにより行われています。そのことについては以下の過去記事で書いています。

圏の束構造と包含的圏

圏 $`\cat{C}`$ とその部分圏 $`\cat{I}\subseteq \cat{C}`$ の組 $`(\cat{C}, \cat{I})`$ が有限余完備包含的圏〈finitely cocomplete inclusive category〉であるとは：

$`\cat{C}`$ は、始対象と任意のプッシュアウト（スパンの余極限）を持つ。（結果的に、有限余極限を持つ。）
$`(\cat{C}, \cat{I})`$ は、ゴグエン／ロスの意味での包含的圏〈inclusive category〉となる。「圏の束構造と包含的圏」参照。

半具象インスティチューションの指標の圏 $`\cat{Sign}`$ は、有限余完備包含的圏であることを要請します。対象の集合 $`|\cat{Sign}|`$ は最小元（始対象でもある） $`{\bf 0}`$ を持つ束構造を持ちます。それは次のように書けます。

$`\quad (|\cat{Sign}|, \sqsubseteq, \wedge, \vee, {\bf 0})`$

$`\Sigma, \Gamma \in |\cat{Sign}|`$ が $`\Sigma \sqsubseteq \Gamma`$ であるとき、このペアを指標の拡大〈extension of signatures | signature extension | 指標拡大〉と呼びましょう。$`\Sigma`$ はベース指標〈base signature〉、$`\Gamma`$ は拡大指標〈extended signature〉です。

$`\Sigma_1 \sqsubseteq \Sigma_2 \sqsubseteq \cdots \sqsubseteq \Sigma_n`$ のような指標の拡大の列は、「指標と仕様」で述べた多パート指標の表現になります。

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

オリジナルのインスティチューションでは「構文の記述がうまくいかない」と言いました。構文記述のための構造をインスティチューションに付け加えることにします。それは、随伴系〈adjunction | adjoint system〉によって与えられます。

$`\cat{Sign}`$ は指標の圏（有限余完備包含的圏）だとして、もうひとつの圏（同じ圏でもよい） $`\cat{Thy}`$ を準備します。"Thy" は、ローヴェアの意味でのセオリー〈theory〉にちなみます。セオリーの圏〈category of theories〉と呼んでおきます。指標の圏とセオリーの圏のあいだに次の随伴系があるとします。

$`\quad \xymatrix@C+1pc {
\cat{Sign} \ar@/^1pc/[r]^{F}
\ar@{}[r]|{\bot}
& \cat{Thy} \ar@/^1pc/[l]^{U}
}
`$

自明な例として、$`\cat{Thy} := \cat{Sign}`$ と置いて、$`F = G := \mrm{Id}_{\cat{Sign}}`$ とすると、随伴系となります。

随伴系があると、なぜ構文記述が出来るのかは後で話すとして、インスティチューションとしての残りの構造を揃えてしまいましょう。

$`\cat{Amb}`$ を、圏を対象とする2-圏だとします（典型例は $`{\bf CAT}`$）。"Amb" は "ambient" からです。次のような関手を考えます。

$`\quad J_\mrm{thy} : \cat{Thy} \to \cat{Amb}`$

$`\cat{Thy}`$ と $`\cat{Amb}`$ は次元が違うので、そのあいだの関手とは何か？が問題になります。圏の次元調整（「圏の次元調整」参照）を使うと、次の2つの候補があります。

$`\quad J_\mrm{thy} : \cat{Thy} \to \dimU{\cat{Amb}}{1} \In \mathbb{CAT}\\
\quad J_\mrm{thy} : \dimU{\cat{Thy}}{2} \to \cat{Amb} \In \mathbb{2CAT}
`$

どちらにするかはここでは規定しないで、用途・目的に応じて選ぶとします。

以上で、構文付き変換手インスティチューション〈transforial institution with syntax〉を構成する素材は出揃いました。構成素名（構造における役割り名）と共にまとめて列挙します。

$`\cat{Sign}`$ ： 指標の圏、有限余完備包含的圏
$`\cat{Thy}`$ ： セオリーの圏
$`F`$ ： 自由関手〈free functor〉、随伴系の左関手
$`U`$ ： 忘却関手〈forgetful functor〉、随伴系の右関手
$`\cat{Amb}`$ ： アンビエント〈ambient〉、圏を対象とする2-圏
$`J_\mrm{thy}`$ ：（セオリーの圏からの）編入関手〈incorporation functor〉

$`F \dashv U`$ が作る随伴系は構文随伴系〈syntax adjunction〉と呼ぶことにします。指標の圏からの編入関手は次のように定義します。

$`\quad J_\mrm{sign} := F * J_\mrm{thy} \; : \cat{Sign}\to \cat{Amb}`$

この $`J_\mrm{sign}`$ は、先に $`(\hyp)^\diamondsuit`$ という記号で出したオペレーターと同じものです。

これらの構成素達をまとめて図示すると次のようになります（全体が可換図式というわけではありません）。

$`\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}
}
`$

インスティチューションのモデル圏関手は、Diag構成で定義できます。

$`\text{For }\Sigma \in |\cat{Sign}|\\
\text{For }\cat{T} \in |\cat{Amb}|\\
\quad \mrm{Model}(\Sigma , \cat{T}) := \cat{Amb}\text{-}\mrm{Diag}^{\cat{Sign}, J_\mrm{sign}}[\Sigma](\cat{T})
= \cat{Amb}(J_\mrm{sign}(\Sigma), \cat{T})
`$

Diag構成については以下の記事で説明しています。

通常のインスティチューションと違うのは、$`\mrm{Model}`$ の引数が2つあることです。第一引数は指標、第二引数はターゲット〈target〉です。デフォルトのターゲットを決めているときは、第二引数を省略することができます。

今のセッティングでは、$`\mrm{Model}(\Sigma , \cat{T})`$ は関手圏なので関手意味論ですが、圏の次元を上げると、モデル達の高次圏は変換手〈transfor〉達の高次圏になります。つまり、変換手意味論〈transforial semantics〉となるので、形容詞「変換手」を使って名付けています。なお、関手意味論〈関手モデル〉については次の過去記事で書いています。

指数関手と構文論・意味論

変換手については：

変換手n-圏のブラケット記法

インスティチューションとして必要な $`Sen`$ 関手（に相当する関手）や充足関係についてはまだ述べてません。が、素材は上の図で尽きていて増えることはありません。

構文論と意味論

構文付き変換手インスティチューションの構文論は、構文随伴系 $`F \dashv U`$ が担います。例えば、構文随伴系が誘導する $`\cat{Sign}`$ 上のモナドを $`G = (G, \mu, \eta)/\cat{Sign}`$ とすると、$`G`$ は項生成モナド〈term-generating monad）です。$`G(\Sigma)`$ は指標 $`G(\Sigma)`$ から生成された項（あるいは式〈expression〉）の集合となります。

一方、意味論は、編入関手 $`J_\mrm{sign}`$ とアンビエント $`\cat{Amb}`$ だけで構成できます。モデル圏関手の定義が、$`J_\mrm{sign}`$ と $`\cat{Amb}`$ のホム圏だけから構成されているからです。

構文論と意味論を別々に展開することが出来ますが、インスティチューションの醍醐味は構文論と意味論の相互関係を議論できることです。なかでも重要なトピックは、指標拡大を分類する事と、構文の論理パートを抽出することです。

モデルのターゲット圏 $`T\in |\cat{Amb}|`$ を固定して、モデル圏を $`\mrm{Model}(\Sigma) := \mrm{Model}(\Sigma, \cat{T})`$ と書くことにします。$`(\Sigma \sqsubseteq \Gamma)`$ が指標拡大のとき、モデル圏のあいだの関手が反変に誘導されます。

$`\quad \mrm{Model}(\Gamma) \to \mrm{Model}(\Sigma) \In {\bf CAT}`$

この関手は、モデルのあいだの忘却関手ですが、指標拡大（指標の包含射）から誘導されている場合はモデル射影関手〈model projection functor〉、または単に射影〈projection〉と呼ぶことにします。

射影がどのような関手であるかで指標拡大を分類できます。例えば、射影が充満忠実〈fully faithful〉なら、拡大は性質〈プロパティ〉拡大〈property extension〉と呼んでいいでしょう。これは、次のnLab項目「付属物、構造、性質」に基づく分類です。