Improving substitutions
identity functionのインスタンスの集合
$ [ \! [\forall a. a \rightarrow a] \!] = \{ \tau \rightarrow \tau \mid \tau \in Type \}
一般化
$ [ \! [\forall a_1 \cdots a_n. \tau] \!] = \{ S \tau \mid dom \: S \in \{ a_1, \cdots, a_n \} \} ただし$ dom \: S は$ Sa \neq aである型変数 $ aの集合
述語の集合 $ P がSatisfiableである:
$ \lfloor P \rfloor \neq \emptyset ただし $ \lfloor P \rfloor = \{ S P \mid \emptyset \vdash \!\! \vdash S P \} (SPを満たせるような置き換えS (によるsatisfiable instances) が存在する)
条件付き一般化
$ [ \! [\forall a_1 \cdots a_n. P \Rightarrow \tau] \!] = \{ S \tau \mid dom \: S \in \{ a_1, \cdots, a_n \}, \emptyset \vdash \!\! \vdash S P \}
$ S improves $ P:
$ \lfloor P \rfloor = \lfloor SP \rfloor (置き換え$ Sが$ Pのsatisfiable instancesに変化を及ぼさない)
トリビアルなImproving substituionは恒等変換だが、例えば$ [Int/a] improves $ \{ a \subseteq Int \} である。
fundepsのない言語においてもgeneralization時にimproving substitutionを計算することでsatisfiableでない述語を発見し早期にエラーとしたりできる。