代换是形如{t1/x1,t2/x2,…,tn/xn}的有限集合。其中，t1,t2,…,tn是项；x1,x2,…,xn是可相同的变元。