「ν-インスティチューションでは健全性の定義と証明が出来る」で述べた「ν-インスティチューションの健全性」が示せるのは、充足関係の定義がうまいこと働くからです。では、充足関係の定義がどこから来たのでしょうか？ これは具体例を見たり触ったりしていれば思い至るものです。
逆に、具体例がなかったら実験・観察ができないので、何もわからないし何も思いつかないでしょう。
ν-インスティチューションやC-システムの具体例として僕がよく見たり触ったりしているのは、集合圏で解釈する等式的指標達の圏です。このような指標はおそらく一番ポピュラーなもので、特に変わったものではありません。ただし、「指標〈signature〉」ではなくて、仕様〈specification〉とか表示〈presentation〉とかセオリー〈theory〉と呼ぶ人もいます。プログラミング言語では、インターフェイス、型クラス、プロトコル、トレイト、コンセプト … など様々な呼び名があります。概念としてはポピュラーですが、呼び名はバランバランです。
指標については、「構造記述のための指標と名前 1/n 基本」と、そこからリンクされている記事達を見てください。この記事では、さらに具体的な話をします。ほんとに具体的な個別特定の指標をいくつか提示します。それらの具体的な指標は、いずれ説明の素材に使うつもりです。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\In}{\text{ in }}
\newcommand{\Imp}{\Longrightarrow} % for meta prop
%\newcommand{\hyp}{ \text{－} }
\newcommand{\twoto}{\Rightarrow }
%
%
\newcommand{\T}[1]{\text{#1} }
\require{color}
\newcommand{\NX}[1]{ \textcolor{orange}{ {#1}} } % New eXpression
\newcommand{\KX}[1]{ \textcolor{blue}{#1} } % Known eEXpression
\newcommand{\VN}[1]{ \textcolor{violet}{ {#1}} } % Variable Name
\newcommand{\KO}[1]{ \mathop{\textcolor{blue}{ {#1}}} } % Known Operator
`$
内容：
幾つかの指標
指標の書き方は、とりあえずは「構造記述のための指標と名前 1/n 基本」と同じです。ただし、色付けは初出の名前をオレンジ色にするだけです。後で名前を削除するので、そうなると黒一色です。
「構造記述のための指標と名前 1/n 基本」の最初の例は半群の指標でした。
$`\T{signature }\NX{\text{Semigroup}}\:\{\\
\quad \T{sort } \NX{U} \In \mbf{Set}\\
\quad \T{operation }\NX{m} : U \times U \to U \In \mbf{Set}\\
\quad \T{equation } \NX{\text{assoc}} ::
(m\times \id_U);m \twoto \alpha_{U,U,U} ; (\id_U \times m); m \\
\qquad : (M\times M)\times M \to M
\In \mbf{Set}\\
\}
`$
もっと原始的な構造として、集合に二項演算が載っただけで、何の法則も仮定しない構造を考えます。そのような構造はマグマ〈magma〉と呼びます。
$`\T{signature }\NX{\text{Magma}}\:\{\\
\quad \T{sort } \NX{U} \In \mbf{Set}\\
\quad \T{operation }\NX{m} : U \times U \to U \In \mbf{Set}\\
\}
`$
次は、集合に一点が指定されただけの構造です。
$`\T{signature }\NX{\text{PointedSet}}\:\{\\
\quad \T{sort } \NX{A} \In \mbf{Set}\\
\quad \T{operation }\NX{p} : \mbf{1} \to A \In \mbf{Set}\\
\}
`$
次は、マグマと符点集合〈pointed set〉を一緒にした構造です。符点マグマ〈pointed magma〉と呼ぶことにします。
$`\T{signature }\NX{\text{PointedMagma}}\:\{\\
\quad \T{sort } \NX{U} \In \mbf{Set}\\
\quad \T{operation }\NX{m} : U \times U \to U \In \mbf{Set}\\
\quad \T{operation }\NX{p} : \mbf{1} \to U \In \mbf{Set}\\
\}
`$
符点マグマの指定された一点が左単位元になるなら、次のような指標で記述します。後で出てくるラムダ記法と '$`\lambda`$' が被ってしまうので、集合圏の左単位律子〈left unitor〉を $`\boldsymbol{\ell}_{U}`$ としました。
$`\T{signature }\NX{\text{LeftUnitalMagma}}\:\{\\
\quad \T{sort } \NX{U} \In \mbf{Set}\\
\quad \T{operation }\NX{m} : U \times U \to U \In \mbf{Set}\\
\quad \T{operation }\NX{p} : \mbf{1} \to U \In \mbf{Set}\\
\quad \T{equation } \NX{\text{lunit}} ::
(p \times \id_U);m \twoto
\boldsymbol{\ell}_{U} : (\mbf{1} \times U) \to U \In \mbf{Set}\\
\}
`$
キーワードや名前の削除
実際に使う指標の構文ではキーワードや名前は必須ですが、理論的取り扱いではキーワードや名前がとても邪魔になります。キーワード／名前は完全に削除して、指標を（入れ子の）リストデータとして扱います。キーワード／名前を削除すると、可読性がとんでもなく悪くなりますが、その構文を実際に使うわけではないので気にする必要はありません。余計なことは考えずに、とにかく名前を抹殺することが大事です。
我々が考える指標は常に集合圏で解釈するものだとして、各宣言末尾の $`\In \mbf{Set}`$ は取り除きます。宣言先頭のキーワード $`\T{sort}, \T{operation}, \T{equation}`$ も取り除きます。また、型推論で容易に補えるプロファイル情報の一部も取り除きます。半群と左単位的マグマの例は次のようになります。
$`\T{signature }\NX{\text{Semigroup}}\:\{\\
\quad \NX{U}\\
\quad \NX{m} : U \times U \to U\\
\quad \NX{\text{assoc}} ::
(m\times \id_U);m \twoto \alpha_{U,U,U} ; (\id_U \times m); m \\
\}
`$
$`\T{signature }\NX{\text{LeftUnitalMagma}}\:\{\\
\quad \NX{U}\\
\quad \NX{m} : U \times U \to U\\
\quad \NX{p} : \mbf{1} \to U\\
\quad \NX{\text{lunit}} ::
(p \times \id_U);m \twoto
\boldsymbol{\ell}_{U}\\
\}
`$
「指標から名前の削除 その2」で述べた方法で、各宣言の構成素役割り名を番号にします。ひとつの宣言を、番号、プロファイルのラムダ式、ラムダ式の引数である番号リストの3つの項目からなるリストにします。最初のソート宣言は、番号だけの単項目リストです。
$`\T{signature }\NX{\text{Semigroup}}\:\{\\
\quad (1)\\
\quad (2, \lambda\, X.( X\times X \to X), (1) )\\
\quad (3, \lambda\, (f, X).( ( f\times \id_X);f \twoto \alpha_{X,X,X}; (\id_X\times f) ), (2, 1) ) \\
\}
`$
$`\T{signature }\NX{\text{LeftUnitalMagma}}\:\{\\
\quad (1)\\
\quad (2, \lambda\, X.( X\times X \to X), (1) )\\
\quad (3, \lambda\, Y.(\mbf{1} \to Y), (1) )\\
\quad (4, \lambda\, (x, Y, z).( (x \times \id_Y);z \twoto
\boldsymbol{\ell}_{X} ), (3, 1, 2) )\\
\}
`$
出現位置から番号は分かるので、各項目の第1項目の番号も取り除けますが、今回は残しておきます。指標の先頭に空リスト $`()`$ が現れるのが気持ち悪いので。
最後に、指標の名前も削除して、単なるリストデータの形にします。先頭の $`\T{signature}`$ は、そのリストが指標であることを示すために残しておきます。
$`\T{signature }(\\
\quad (1),\\
\quad (2, \lambda\, X.( X\times X \to X), (1) ),\\
\quad (3, \lambda\, (f, X).( (f\times \id_X);f \twoto \alpha_{X,X,X}; (\id_X\times f) ), (2, 1) ) \\
)
`$
$`\T{signature }(\\
\quad (1),\\
\quad (2, \lambda\, X.( X\times X \to X), (1) ),\\
\quad (3, \lambda\, Y.(\mbf{1} \to Y), (1) ),\\
\quad (4, \lambda\, (x, Y, z).( (x \times \id_Y);z \twoto
\boldsymbol{\ell}_{X} ), (3, 1, 2) )\\
)
`$
理論的な扱いでは、以上のようなリストデータを指標だと考えます。指標は名前を持ってないし、指標の項目〈宣言〉にも名前が付いてません。ラムダ式のラムダ変数は名前を持ってますが、好きにリネームしてよい束縛変数なので、識別子としての名前ではありません。ド・ブラウン・インデックス（「ラムダ式のド・ブラウン・インデックス」参照）でラムダ変数も番号にすれば、ラムダ変数名さえ消せます。
可読性の酷さについては次のように考えましょう； 名前を徹底的に消し去ったリストデータこそが指標の実体なのだが、便宜上、人間の都合により、一時的な名前を使って可読性を向上させてもよい。
指標から名前を削除すると、極端に可読性が落ちることは、人間どうしの伝達では、名前が極めて重要なことの証左にもなります。たいていの人は、自然言語由来の名前から、類推や連想をすることにより理解・把握の足しにしているのです。形式的には情報量が同じでも、名前の代わりに番号を使われると、類推や連想が働かなくなって辛いのです。
しかしそれでも、類推や連想が邪魔になることがあるので、名前の削除は必要です。それにそもそも、名前を残しておくと、いちいちリネームの影響を考えなくてはならず、理論的扱いは難解・晦渋になってしまい大きな負担になります。ネーミングのメカニズム自体を解明したいなら別ですが、それ以外では、名前を削除するとスッキリします。
[/補足]
ストリームの例
僕がよく事例に使っている指標のひとつがストリームの指標です。まずは、人間向きに可読性を考慮した構文で書くと：
$`\T{signature }\NX{\text{Stream}}\:\{\\
\quad \T{sort } \NX{V} \In \mbf{Set}\\
\quad \T{sort } \NX{S} \In \mbf{Set}\\
\quad \T{operation }\NX{\mrm{get}} : S \to S\times V\In \mbf{Set}\\
\quad \T{operation }\NX{\mrm{put}} : S \times V \to S \In \mbf{Set}\\
\quad \T{equation } \NX{\text{get-put}} ::
\mrm{get}; \mrm{put} \twoto \id_{S} \In \mbf{Set}\\
\quad \T{equation } \NX{\text{put-get}} ::
\mrm{put}; \mrm{get} \twoto \id_{S\times V} \In \mbf{Set}\\
\}
`$
リストデータとして書けば：
$`\T{signature } (\\
\quad (1),\\
\quad (2),\\
\quad (3, \lambda\,(V, S).(S \to S\times V), (1, 2) ),\\
\quad (4, \lambda\,(V, S).(S \times V \to S), (1, 2) ),\\
\quad (5, \lambda,(V, S, g, p).( g; p \twoto \id_{S}), (1, 2, 3, 4) )\\
\quad (6, \lambda,(V, S, g, p).( p ; g \twoto \id_{S\times V}), (1, 2, 3, 4) )\\
)
`$
ストリームは、概念的には無限にいくらでもデータを出し入れできるデータストアです。$`\mrm{get}`$ で1個分のデータを取得して、$`\mrm{put}`$ で1個分のデータを追加できます。先入れ後出し方式です。1個分のデータの集合が $`V`$ で、全体のデータの状態集合が $`S`$ です。
ストリームの例 その2
ストリームを別なインターフェイスで書いてみましょう。集合 $`V,S`$ は前節と同じです。利用できる関数（あるいはメソッド）は $`\mrm{peek}, \mrm{next}, \mrm{put}`$ です。$`\mrm{peek}`$ は先頭の要素を返しますが、ストリームの状態を変えません。言い方を変えると状態への副作用を持たない関数です。$`\mrm{next}`$ は状態遷移するだけの関数です。プロファイル上は状態を出力しますが、通常の意味での値は返しません。
- $`\mrm{peek} : S \to S\times V`$ （通常の意味の戻り値の型は $`V`$）
- $`\mrm{next} : S \to S`$ （通常の意味の戻り値はない）
$`\mrm{put}`$ は前節の $`\mrm{put}`$ と同じです。
このインターフェイスでの等式的法則は、$`\mrm{peek}`$ が副作用を持たないことと、$`\mrm{peek}`$ と $`\mrm{next}`$ の組み合わせで $`\mrm{put}`$ の逆が構成できることだとします。以下のように書けます。$`V,S`$ の出現順はあえて逆にしています。$`\boldsymbol{r}_S`$ は集合圏の右単位律子〈right unitor〉です。
$`\T{signature }\NX{\text{Stream2}}\:\{\\
\quad \T{sort } \NX{S} \In \mbf{Set}\\
\quad \T{sort } \NX{V} \In \mbf{Set}\\
\quad \T{operation }\NX{\mrm{peek}} : S \to S\times V\In \mbf{Set}\\
\quad \T{operation }\NX{\mrm{next}} : S \to S \In \mbf{Set}\\
\quad \T{operation }\NX{\mrm{put}} : S \times V \to S \In \mbf{Set}\\
\quad \T{equation } \NX{\text{peek}} :: \mrm{peek}; (\id_S \times !_V); \boldsymbol{r}_S \twoto \id_S \In \mbf{Set}\\
\quad \T{equation } \NX{\text{next-peek-put}} ::
\Delta_S ; (\mrm{next} \times \mrm{peek}); \mrm{put} \twoto \id_{S} \In \mbf{Set}\\
\quad \T{equation } \NX{\text{put-next-peek}} ::
\mrm{put}; (\Delta_S ; (\mrm{next} \times \mrm{peek}) )\twoto \id_{S\times V} \In \mbf{Set}\\
\}
`$
リストデータとして書くことは練習問題とします。
おわりに
指標達の圏 $`\cat{S}`$ の具体例として、集合圏で解釈する等式的指標達の圏を選ぶことが出来ます。具体的なコンテキスト達の圏 $`\cat{C} = \cat{S}^\op`$ は反対圏として得られます。この程度の簡単な事例でも、丁寧に調べれば、インスティチューション理論や型理論に関するそれなりの洞察が得られます。他にも事例はありますが、一番ポピュラーな場合を調べるのが先でしょう。
