统一（计算机科学）

在逻辑学和计算机科学中，统一是解决符号表达式之间方程的一个算法过程。根据哪些表达式（也叫术语）允许出现在方程组中（也叫统一问题），以及哪些表达式被认为是相等的，可以区分出几个统一的框架。如果一个表达式中允许出现高阶变量，即代表函数的变量，那么这个过程被称为高阶统一，否则称为一阶统一。如果一个解决方案需要使每个等式的两边都相等，那么这个过程就被称为句法或自由统一，否则就被称为语义或等式统一，或E-统一，或统一模态理论。统一问题的解决方案被称为替换，即为问题表达式中的每个变量分配一个符号值的映射。统一算法应该为一个给定的问题计算出一个完整的、最小的替换集，即一个包含问题的所有解决方案的集合，并且没有多余的成员。根据不同的框架，一个完整的最小替换集可能最多只有一个，最多只有有限的几个，或者可能有无限多的成员，或者根本就不存在。在某些框架中，通常无法决定是否存在任何解决方案。对于一阶句法统一，Martelli和Montanari给出了一种算法，它可以报告不可解性，或者计算出一个完整的、最小的单子替换集，其中包含所谓的最一般的统一器。例如，用x,y,z作为变量，单子方程组{cons(x,cons(x,nil))=cons(2,y)}是一个句法一阶统一问题，它的xxx解是替换{x↦2,y↦cons(2,nil)}。句法一阶统一问题{y=cons(2,y)}在有限项集合上没有解；然而，它在无限树集合上有xxx的解{y↦cons(2,cons(2,cons(2,...))语义一阶统一问题{a⋅x=x⋅a}在半群中，即如果(⋅)被认为是关联的，则每个替换形式{x↦a⋅...⋅a}都是一个解决方案；同样的问题，在非线性群中，即(⋅)被认为是换元的，有任何替换都是一个解决方案。单子集{a=y(x)}是一个语法上的二阶统一问题，因为y是一个函数变量。一个解决方案是{x↦a,y↦(身份函数)}；另一个解决方案是{y↦(常数函数将每个值映射到a),x↦(任何值)}。统一算法最早是由JacquesHerbrand发现的，而xxx次正式研究可以归功于JohnAlanRobinson，他将一阶句法统一作为他的一阶逻辑的解析程序的基本构件，这是自动推理技术的一大进步，因为它消除了组合爆炸的一个来源：搜索术语的实例化。今天，自动推理仍然是统一的主要应用领域。

语法上的一阶统一被用于逻辑编程和编程语言类型系统的实现，特别是基于Hindley-Milner的类型推理算法。语义上的统一被用于SMT求解器、术语重写算法和加密协议分析。高阶统一用于证明助手，例如Isabelle和Twelf，高阶统一的限制形式（高阶模式统一）用于一些编程语言的实现，例如lambdaProlog，因为高阶模式具有表达能力，但其相关的统一程序保留了更接近一阶统一的理论属性。

从形式上看，统一方法的前提是一个无限的集合V{displaystyleV}的变量。的变量。对于高阶统一，方便的做法是选择{displaystyleequiv}反映了关于某些函数符号的背景知识；例如，如果是一个人，那么他就会被认为是一个人。