CLTT読書会 - yoshitake-hのブログ

1.6 Fibrations of signatures

集合 $T$ の生成する自由モノイドを $T^\star$ と書く．

集合 $T$ と集合族 $\mathcal{F}=\{ \mathcal{F}(i^\star,\,j) \}_{(i^\star,\,j)\in T^\star\times T}$ の組 $(T,\,\mathcal{F})$ を signature という．

$T$ の元を型とよび， $\mathcal{F}(i^\star,\,j)$ の元を，引き数型 $i^\star$ ，返り値型 $j$ の 関数記号 とよぶ．

signature の間の射が自然に定義でき，圏 $\mathbf{Sign}$ が定義される．

$\mathbf{Sign}\to \mathbf{Set},\; (T,\,\mathcal{F})\mapsto T$ は fibered category である．

2.2 Functorial semantics

signature $(T,\,\mathcal{F})$ と有限積をもつ小圏 $\mathbb{B}$ に対し，
・写像 $X: T\to \mathrm{Ob}(\mathbb{B} ),\; i\mapsto X_i$
・写像 $\mathcal{F}(i^\star,\,j)\to \mathbb{B}(X_{i^\star},\,X_j),\; X_{i^\star}=X_{i(1)}\times \cdots \times X_{i(n)},\; i^\star = (i(1),\,\dots,\,i(n))$
の組を， $\mathbb{B}$ における $(T,\,\mathcal{F})$ の モデル という．

有限積をもつ小圏 $\mathbb{B}$ に対し，
$T_\mathbb{B} =\mathrm{Ob}(\mathbb{B}),\quad ( \mathcal{F}_\mathbb{B} )_{x_1,\,\dots,\,x_n;\,x} =\mathbb{B}(x_1\times \cdots \times x_n,\,x)$
で定義される signature を $\mathrm{Sign}(\mathbb{B})=( T_\mathbb{B},\, \mathcal{F}_\mathbb{B})$ と書く．
これは，有限積をもつ小圏の圏 $\mathbf{FPCat}$ から $\mathbf{Sign}$ への関手をあたえる．

項の定義：(1) 型の指定された変数は項．(2) 項を型にしたがって関数記号に代入したものは項．

signature $(T,\,\mathcal{F})$ に対し，変数の型指定の列（文脈）を対象とし，項の列を射とする，有限積をもつ小圏 $\mathrm{Cl}(T,\,\mathcal{F})$ が定義される．
これは $\mathbf{Sign}$ から $\mathbf{FPCat}$ への関手をあたえる．

$(\mathrm{Cl},\,\mathrm{Sign})$ は随伴対であり，
$\mathbf{Sign}((T,\,\mathcal{F}),\,\mathrm{Sign}(\mathbb{B}) ) \cong \mathbf{FPCat}( \mathrm{Cl}(T,\,\mathcal{F}),\, \mathbb{B})$
の元はモデルに１対１対応する．