定义1：代换是形如{t1/x1,t2/x2,,tn/xn}的有限集合。 ·t/X表示用t:代替x,t1〈)x1,x:不能出现在t中， ·t1,t2,.tn是项，x1,x2.xn是互不相同的变元 例{a/x,f(b)/y,w/z}是一个代换 {g(y)/x,f(x)/y}x与y之间出现了循环代换的情况 {g(a)/x,f(x)/y}y用f(g(a)代换 定义2：设Q-{t1/x1,t2/x2,.tn/xn} 1={u1/y1,u2/y2.u/yn}是两个代表 则{t12/x1,t21/x2,.,tn1/x,u1/y1,u2/y2,.,/yn} 也是一个代换，从中删去两个元素t1入/X1,u/y:后剩下 的元素所构成的集合，记为Q°入 例设有代换Q={f(y)/x,z/y},1={a/x,b/y,y/z} Q°λ={f(b)/x,y/z} 定义1：代换是形如{t1/x1,t2/x2,…,tn/xn}的有限集合。 • ti/xi表示用ti代替xi,ti<>xi,xi不能出现在ti中， • t1,t2,…tn是项，x1,x2..xn是互不相同的变元 例 {a/x,f(b)/y,w/z}是一个代换 {g(y)/x,f(x)/y} x与y之间出现了循环代换的情况 {g(a)/x,f(x)/y} y用f(g(a))代换 定义2：设Q={t1/x1,t2/x2,…tn/xn} λ={u1/y1,u2/y2…um/ym}是两个代表 则{t1λ/x1,t2λ/x2,..,tnλ/xn,u1/y1,u2/y2,..,um/ym} 也是一个代换，从中删去两个元素tiλ/xi,ui/yi后剩下 的元素所构成的集合，记为Qλ 例 设有代换Q={f(y)/x,z/y},λ={a/x,b/y,y/z} Qλ={f(b)/x,y/z}