多項式インスティチューション
思わぬところでインスティチューションに出会うことがある。多項式インスティチューションは典型的なインスティチューションではないが、「こんなところにも」という例にはなる。それに説明が簡単だし。
以下で、インスティチューションの単純化である簡易インスティチューションを定義して、多項式の集合達が簡易インスティチューションの例であることを示す。
簡易インスティチューションの定義
Bを圏として、S:B→Setが共変関手、M:B→Setが反変関手だとする。Bの対象は（習慣に従って）Σ、Γなどの文字で示し、射はσ、ρなどで示す。以下、Bの対象を指標、Bの射を指標射、S(Σ)をΣの文集合、M(Σ)をΣのモデル集合と呼ぶ。
Σ∈|B|ごとに、VΣ⊆M(Σ)×S(Σ)が割り当てられているとして、これをΣの充足関係、または妥当関係と呼ぶ。x∈M(Σ)とp∈S(M)に対して、(x, p)∈VΣ を、x |=Σ p と書くことにする。下添字Σを省略して、x |= p とも書く。
x |= p は、「モデルxは文pを満たす」と読む。さらに、関手S, M、関係の族|= のあいだに次が成立しているとする。
- σ:Σ→Γ in Bとして、y∈M(Γ), p∈S(Σ)に対して、M(y) |= p ⇔ y |= S(p)
上の条件は充足条件と呼ぶ。以上の状況で、(B, S, M, |=)を簡易インスティチューションと呼ぶ。
一般的なインスティチューションは、MがB→Setの関手ではなくて、B→Cat（圏の圏）となっている。集合は対象だけの圏とみなせるので、簡易インスティチューションはインスティチューションである。
一番簡単な多項式インスティチューション
体Kを固定する、例えばKは有理数体。Bは有限集合を対象として、inclusionを射とする圏とする。X⊆YのときX→Yの射がある。K[X]は、有限集合Xを不定元とするK係数多項式の集合とする。X⊆YのときK[X]⊆K[Y]となるから、K[-]は共変関手である。S(-) = K[-]としてS:B→Setを定義する。
KXは、X上に定義されたK値関数の全体とする。X={x1, ..., xn}とすれば、KXの元は{x1:v1, ...., xn:vn}というレコード形式で書ける。よって、KXは、Xを名前の集合とするK値レコード全体だとみなせる。X⊆Yのとき、レコードの制限（射影といってもよい）によってKY→KXが定義できるから、K-は反変関手となる。M(-) = K- として反変M:B→Setを定義する。
a∈M(X)、f∈S(X)に対して、a |= f を 「fにaによる代入をして計算した値が0」と定義する。X={x1, ..., xn}で、a={x1:a1, ..., xn:an}のときf[a1/x1, ..., an/xn] = 0 が a |= f の意味するところである。
以上のsettingで、充足条件を確認すれば、(B, S, M, |=)は簡易インスティチューションとなる。
- 充足条件：X⊆Yだとして、M(b) |= f ⇔ b |= S(f)。
X={x1, ..., xn}, Y={x1, ..., xn, y1, ..., ym}とする。b={x1:a1, ..., xn:an, y1:b1, ..., ym:bm} で、fはx1, ..., xnの多項式である。fにはy1, ..., ymは含まれていないので、
- f[a1/x1, ..., an/xn, b1/y1, ..., bm/ym] = f[a1/x1, ..., an/xn]
これから、f[a1/x1, ..., an/xn] = 0 ⇔ f[a1/x1, ..., an/xn, b1/y1, ..., bm/ym] = 0 が従うが、これは充足条件に他ならない。
多項式インスティチューションの拡張
指標圏Bは、有限集合とinclusionの圏としたが、有限集合とinjectionの圏でも事情はほとんど変わらない。これは、不定元のリネームを許すことになる。
inclusion, injectionだけでなく一般の写像を許しても大丈夫だ。例えば、{x, y}→{t}という写像を考えると、共変関手SによるS(→)は、f(x, y)|→f(t, t) で与えられる。一方、反変関手MによるM(→)は、{t:a}|→{x:a, y:a}で与えられる。充足条件は、{x:a, y:a} |= f(x, y) ⇔ {t:a} |= f(t, t) だから、ほぼ自明だろう。
不定元の集合が有限でなくても多項式は定義できる。よって、Setを指標圏と考えての多項式インスティチューションも定義できる。代入をモナドで定式化するときなどは、このような一般的な定義が必要になる。
多項式インスティチューションの使い道
まず、多項式インスティチューションは簡単で具体的だから、実験や確認を行う事例として役に立つ。特に、モデルが圏でなくて単なる集合（レコードの集合）なので扱いが簡単だ。
個人的には、中学校以来納得がいかなかった不定元（代数的変数）の概念がやっと飲み込めた気がする。不定元は具体的な名前を持っているが、実際には名前が問題になることはない。名前があるが、なくてもいいという奇妙な感じに決着がついた、という思いがある。
ここから先はホラだが； 多項式インスティチューションは、座標による具体的表示を使った代数幾何の舞台といっていいだろう。一方、もともとインスティチューションはソフトウェア工学の概念であり、その起源はバーワイズによるモデル論の抽象化である。となると、多項式インスティチューションは、代数幾何、ソフトウェア工学／計算科学、論理／モデル論の交差点に位置するかもしれない。
