什么是合一算法介绍
合一算法（unification algorithm），信息科学术语，是一种算法。
定义：E1θ=...=Enθ, 则称置换θ为{E1,...,En}的合一子(unifier).。如果对{E1,...,En}存在这样的合一子, 则称集合{E1,...,En}可合一。
合一算法合一算法简介
非形式地讲，合一就是确定将两个表达式e和f中的变量用相应的表达式替换后能否变成等价表达式的问题。测试表达式相等是合一的特殊情况。如果e和f中只包含常量而没有变量，则当且仅当e和f完全相同时e和f合一。本节的合一算法可以用于带环图，所以该算法可用于测试存在环类型的结构等价。
合一是基于称为代换的函数S(从变量到表达式的映射)来定义的。如果将e中的每个变量a均用S(a)代换，则得到的表达式记为s(e)。如果S(e)=S(f)，则称s为e和f的合一代换。本节的算法旨在确定这样一种代换：它是一对表达式上的最一般的合一代换。
研究集合{P(a)，P(x)}。集合中的两个表达式是不同的，差别是在P(a)中出现a，而在P(x)中出现x。为了求出该集合的合一置换，应首先找出两个表达式的不一致之处，然后再试图消除。对P(a)和P(x)，不一致之处可用集合(a，x)表示。由于x是变量，可以取θ={a/x)，
于是有
即θ是(P(n)，P(z))的合一置换。这就是合一算法所依据的思想。在讨论合一算法之前先讨论差异集的概念。
合一算法差异集
定义：表达式的非空集合W的差异集是按下述方法得出的子表达式的集合。
(1)在w的所有表达式中找出对应符号不全相同的第一个符号(自左算起)。
(2)在w的每个表达式中，提取出占有该符号位置的子表达式。这些子表达式的集合便是W的差异集D。
非空表达式集W的差别集:
从左向右,在W中的所有表达式,遇到第一个不相同符号,提取从这个符号开始的子表达式,由此构成一个集合,称为W的差别集,记为D。
例子:
W={P(x,f(y,z),z，w)，P(x,a),P(x,g(z),z,b)}
D={f(y,z),a,g(z)}
合一算法最一般合一子
最一般合一子(mostgeneralunifier，mgu)
定义：如果对E的每个合一子θ,都存在一个置换λ,使得θ=γ°λ,则称合一子γ是集合{E1,…,En}的最一般合一子.
例子:
E={P(x,y),P(x,f(b))},θ1={a/x,f(b)/y},θ2={b/x,f(b)/y}
最一般合一子γ={f(b)/y}
θ1=γ°{a/x},θ2=γ°{b/x}
合一算法合一算法的考虑
消除两个谓词之间项的差别：{P(x,…),P(a,…)}
W的合一算法：
1、K=0,Wk=W,γk=ε.
2、如果Wk是单一的,停机,γk是W的mgu.
否则，求出Wk的差别集Dk.
3、如果在Dk中存在元素vk与tk,使vk是一个未出
现在tk中的变量,转4；
否则，停机,W是不可合一的.
4、令γk+1=γk°{tk/vk}，Wk+1=Wk
°γk+1.
5、K=K+1.转2.
合一算法算法实现
要将合一的基于图论的形式化描述实现为算法，关键是将最一般的合一代换下等价的两个表达式所对应的结点进行分组。两个表达式由图标记为“→：
1、”的两个结点表示。在结点1被合一之后，结点上的整数表示结点所属的等价类编号。
合一算法等价类
等价类具有如下性质，即同一等价类中的所有内结点表示相同的操作符。在一个等价类中，内部结点对应的子结点也都是等价的。
合一算法过程
一对结点的合一。
输入：一个图和一对要合一的结点m和n。
输出：如果结点m和11所表示的表达式合一，则输出布尔值true，否则输出false。如果算法中的函数不是返回false，而是改为导致失败，那么该算法就是类型检查规则所需的unify(合一)的另一版本。
合一算法方法
结点用图1的记录来表示，该记录包含一个二元操作符域和指向左右儿子的指针。
合一算法等价结点
等价结点的集合用set域来保存。每个等价类都选择一个结点作为该等价类的惟一代表，该结点的set域置为空指针，等价类中其他结点的set域均指向(可能间接地通过集合中的其他结点)这个代表结点。初始时，每个结点n的等价类就是自身，而且n也是其自身的代表结点。
合一算法具体算法
合一算法使用了下面两个作用在结点上的操作。
(1)find(n)。返回结点n当前所在等价类的代表结点。
(2)union(m，n)。合并结点m和n所在的两个等价类。如果两个等价类中的某一代表结点是非变量结点，那么union将该结点作为合并后等价类的代表结点。
否则union任选其中的一个作为新的代表结点。在union的说明中，这种非对称性很重要，因为变量不能当作一个包含类型构造符或基本类型的表达式的等价类代表。否则，两个等价的表达式就可以通过该变量合一。
集合上的union操作可通过修改其中一个等价类的代表上的set域，使其指向另一等价类的代表来实现。为寻找某结点所属的等价类，逐级查找结点的set指针，直到到达代表结点(该结点的set域为空指针)为止。
合一算法注意
r的算法分别使用s=find(m)和t=find(n)，而不是m和n。如果m和n在同一等价类中，则代表结点8和t相等。如果s和t代表同一基本类型，则unify(m，n)返回true。如果S和t都是代表二元类型构造符的内部结点，先试着将其合并，然后递归地检查它们各自的子结点是否等价。通过先进行合并，在递归检查子结点之前，等价类的数目就会减少，所以算法最终会停止。
用表达式代换变量是通过将代表变量的叶结点加到包含该表达式对应结点的等价类中来实现的。如果m或n是代表变量的叶结点，而且已经被加到某结点所属的等价类中，而该结点是一个包含类型构造符或基本类型的表达式所对应的结点，那么其上的find将返回该类型构造符或基本类型的代表，所以此时变量不可能与两个不同的表达式进行合一。
对有限非空可合一的表达式集合给出求取最一般合一置换的合一算法。当集合不可合一时，算法也能给出不可合一的结论，并且结束。
合一算法合一算法
第1步置k=0，Wk=W，σk=ε。
第2步若Wk中只有一个元素，终止，并且σk为W的最一般合一。否则求出Wk的
差异集Dk。
第3步 若Dk中存在元素vk和tk，并且vk是不出现在tk中的变量，则转向第4步。否则终止，并且W是不可合一的。
第4步 置
(注意w胖1=肋抖1)。
第5步置k=k+1，转向第2步。
注意：在第3步，要求vk不出现在tk中的，这称为occur检查，算法的正确性依赖于它。但是由于occur检查，使上述合一算法在最坏的情况下运行时间是输入长度的指数函数，因此在多数Prolog程序设计系统中都省略了occur检查。
合一算法置换和合一的区别
定义:置换是一个形如{t1/v1,…,tn/vn}的有限集,其中每个vi是变量,ti是不同于vi的项（常量、变量或函数）(vi≠ti).当i≠j时，vi≠vj.
无元素组成的置换称为空置换,记为ε;
例子：
{a/x,w/y,f(s)/z},{g(x)/x}是置换;
{x/x},{y/f(x)}不是置换;
概念的理解：
置换：被置换元素必是变量，置换元素是项;
置换元素必不同于被置换元素;
在一次置换中，针对同一元素的置换只能出现一次(单次置换的同时性);
无元素组成的置换，成为空置换;