純粋型システム

純粋型システム(Pure Type System; PTS)

定義

純粋型システム(pure type system) を、以下から成る組$ \langle \mathcal{S}, \mathcal{A}, \mathcal{R} \rangle とする。

$ \mathcal{S} : 非空な集合

$ \mathcal{A} \subseteq \mathcal{S}^2

$ \mathcal{R} \subseteq \mathcal{S}^2

$ \mathcal{S}^2 : $ \mathcal{S} \times \mathcal{S} の直積集合

内包表記で書くとこんなところ

$ \mathcal{S}_1 \times \mathcal{S_2} = \{ (s_1,s_2) \mid s_1 \in \mathcal{S}_1, s_2 \in \mathcal{S}_2 \}

確認用

Q. 純粋型システム

参考