形式言語系の例
この話。
ラベル付き遷移系と多項式の例を出す。（多項式インスティチューションについては、多項式インスティチューション - 檜山正幸のキマイラ飼育記 メモ編参照。）まず全体的な対応。
| 形式言語系 | ラベル付き遷移系 | 多項式 |
|---|---|---|
| 指標Σ | ラベル集合Σ | 変数集合x ={x1, ..., xn}（無限でもいい） |
| 指標の射 | ラベル集合間の写像 | 変数集合間の写像 |
| Mod[Σ] | Σラベル付き遷移系 | X上のK付値=レコード=点 |
| 構文モナドT | クリーネスター | 多項式生成関手 |
| Kleisli射 | ラベルのマクロ定義 | 多項式による変数変換 |
| モデルの自然拡張 | Σ*への拡張 | 多項式上の付値 |
以前に出した多項式インスティチューションでは指標の圏を制限していたが、あまり気にしなくていい。
重要なのはモデルの自然拡張なので、そこを中心に以下にメモ。
ラベル付き遷移系の場合
ラベル集合Σに対して、モデルのアンビアント〈アンビエント〉圏は集合と部分写像の圏だとする。部分写像の圏のt:Σ×S→Sが遷移系を定義する。f:S→SがΣ作用を保つとき、ラベル付き遷移系の射として、ラベル付き遷移系の圏TS(Σ)を定義する。tからt':Σ*×S→Sは自明に定義できる。この拡張を関手と考えて、ξΣ:TS(Σ)→TS(Σ*)とする。
TS(Σ)の形の圏の全体がレルムTSになっている。
ξΣのΣを動かすと、指標の圏（この場合はSet）からレルムTSへの関手の自然変換になる。つまり、Nat(TS(-), TS(-*):Set→TS)。TSは遷移系の圏の圏。
φ:Δ→Σ
以下が可換：
TS(Σ)-(ξΣ)→TS(Σ*)
↓TS(φ) ↓TS(φ*)
TS(Δ)-(ξΔ)→TS(Δ*)
多項式の場合
体Kは固定する。変数の集合Xに対して、Mod[X]（単なる集合）は、X上で定義されたK値関数。X上のK値関数をK付値*1と呼んで、Val(X)と書くことにする。もちろん、Val(X) = Mod[X]。
P(X)を多項式集合とする。付値v∈Val(X)に対して、付値v':P(X)→K も代入計算として自然に定義できる。これにより、ξX:Val(X)→Val(P(X))を定義する。
φ:Y→X
以下が可換：
Val(X)-(ξX)→Val(P(X))
↓Val(φ) ↓Val(P(φ))
Val(Y)-(ξY)→Val(P(Y))
命題論理の簡易インスティチューションの場合も多項式と同じだろう。
*1:全然別な意味の「付値」もあるが。
