最汎単一化子
most general unifier
連立方程式を解くときに無限に解が求まることがあるが、その時に用いられる汎用的な解のこと
定義
型代入$ Sが連立方程式$ Eの最汎単一化子であるとは以下を満たすとき $ Sが$ Eの階である
$ Eの任意の解$ S'について、ある型代入$ S''が存在し、$ S'=S''\circ Sが成り立つ
ここで$ S''\circ Sは
型代入を、「型から型への関数」と見なして、それを関数合成したもの つまり「型代入関数」と「型代入関数」の合成関数
参考