2.2.3 合一与匹配
替换是形如{t1/v1,...,tn/vn}的有限集合，其中 vi 是变量符号，ti 是不同于vi 的项，并且 v1,...,vn 互不相同。设替换 θ={t1/v1,. ,tn/vn}，E 是
表达式，将 E 中出现的每个变量符号 vi，都用项 ti 来代替，得到的表达式记为Eθ，称为E 的例。
替换的乘积：设替换 θ={t1/x1,...,tm/xm}，λ={u1/y1,. ,un/yn}，将集合
{t1λ/x1,...,tmλ/xm, u1/y1,. ,un/yn}中任意满足如下条件的元素删除，
（1）ui/yi，当 yi{x1,. ,xm}；，
（2）tjλ/xj，当tjλ=xj 时；
如此得到的替换称为替换 θ 和 λ 的乘积，记为θ∙λ。
替换 θ 称为是表达式集合 {E1,. ,Ek} 的合一， 当且仅当
E1θ=E2θ=...=Ekθ。表达式集合{E1,. ,Ek}的合一σ 被称为最一般合一（匹
配），当且仅当对此集合的任意合一 θ，都存在替换λ 满足 θ=σ∙λ。例如表达式集合{P(a,y), P(x,f(b))}是可合一的，其最一般合一为{a/x, f(b)/y}。对于有限的可合一的表达式集合，存在合一算法返回其最一
般合一。