合一算法

合一（unification algorithm）定义：E1θ=...=Enθ, 则称置换θ为{E1,...,En}的合一子(unifier).。如果对{E1,...,En}存在这样的合一子, 则称集合{E1,...,En}可合一。合一是基于称为代换的函数S(从变量到表达式的映射)来定义的。如果将e中的每个变量a均用S(a)代换，则得到的表达式记为s(e)。如果S(e)=S(f)，则称s为e和f的合一代换。本节的算法旨在确定这样一种代换：它是一对表达式上的最一般的合一代换。