unification problem というナニで google 先生にお伺いしたら標題の_項書き換え系_という用語がお出ましになった。
たとえば以下。
上記のナニで言うと subst-in-term はダウトっぽいカンジ。今の実装って i が term に変換されるカンジなんですが、逆なのかなぁ。
でも apply-subst が symbol を substitution でナニする、という意味では外してはいないのかどうなのか。Ex.2.25 きちんと確認せい、なんですが現実トウヒベースでは微妙かも。
