指標と枠

指標を単なる有向グラフと考えるのはとてもいいとわかってきた。

等式的セオリー

まず、等式的セオリーとグラフのあいだには次の関係がある。

指標	圏の生成グラフ
ソート	対象の生成集合
関数記号	射の生成集合
項形成規則	自由構成
項	射
等式系	グラフの（一般化）合同
リンデンバウム構成	商圏
モデル／代数	商圏からの射

※「商圏」（quotient category）つったら、ビジネス用語と間違われるな。

C-枠

圏Cを固定して、グラフとみなした指標Σと部分関手 K:FreeCat(Σ)→C の組(Σ, K)をC-枠と呼ぶ。部分関手とは、単に部分圏でのみ定義された関手のこと。Kは空部分関手でも全体で定義された普通の関手でもよい。

C-枠(Σ, K)に対して、その代数とは、Kの拡張（延長）になっている関手 F:FreeCat(Σ)→C のこと。(Σ, K)代数の全体をAlg_Σ,Kとすると、Alg_Σ,Kは圏となる。

C-枠(Σ, K)と(Σ', K')のあいだの準同型は、部分関手T:FreeCat(Σ)→FreeCat(Σ')で、T;K' = K を満たすもの。この準同型でC-枠の全体は圏となる。

指標ΔとΔ上の関手K:FreeCat(Δ)→Cを固定する。Δの拡張となっている指標の全体をSign↑Δとして、Σ∈(Sing↑Δ)とKを一緒に考えるとC-枠となる。Sign↑ΔにC-枠の準同型を考えて圏となる。この圏をSign↑Δ[K]とする。より詳しくはSign↑Δ[K:Δ→C]。

プログラミング言語としてのC-枠

C-枠はプログラミング言語機構と解釈できる。Δは言語組み込みの型／関数／演算などの記号（名前）集合。K:Δ→Cはその意味である。圏Cはこの言語を解釈する場となるアンビエント圏。Sign↑Δ[K]に入る指標はユーザー定義の記号集合。ただし、組み込み記号は前もって意味が定まっている。Σ∈|Sign↑Δ[K]|に対してΣ代数（Cに値をとる）を考えれば、それはユーザーによるΣの実装になる。Σ代数F:Σ→CがKの拡張でなければいけないのは、組み込み記号の意味を変えることができない（protected）ことを意味する。

C-枠ΣごとにΣ代数の圏Alg_Σ,Kが対応するので、インスティチューションとなる。ただし、Sen(Σ, K)は別に考えなくてはならない。