Anti-unification and Generalization: A Survey
反统一与泛化:一个综述
https://arxiv.org/pdf/2302.00277
摘要
反统一（AU）是归纳推理中用于泛化计算的基本操作。它是统一操作的对偶操作，统一操作是现代自动推理和定理证明的基础[Baader和Snyder，2001]。AI和相关社区对AU的兴趣日益增长，但没有对概念进行系统研究或对现有工作的调查，调查往往不得不开发特定于应用的方法，而现有方法可能已经涵盖了这些方法。我们提供了AU研究及其应用的首次调查，以及用于分类现有和未来发展的通用框架。
1. 引言
反统一（AU），也称为泛化，是归纳推理中使用的基本操作。它抽象地定义为从一组符号表达式中派生出一个新的符号表达式，该表达式具有其成员之间共享的某些共同点。它是统一操作的对偶操作，统一操作是现代自动推理和定理证明的基础[Baader和Snyder，2001]。AU由Plotkin[1970]和Reynolds[1970]引入，可以如下说明：
其中，f(a, g(g(c, a), h(a))) 和 f(a, g(c, h(a))) 是我们希望进行反统一的两个一阶项，而 f(a, g(X, h(a))) 是得到的泛化结果；不匹配的子项被变量替换。注意，f(a, g(X, h(a))) 捕捉了两个项的共同结构，并且通过替换可以推导出任一输入项。此外，f(a, g(X, h(a))) 通常被称为最小一般泛化，因为不存在比它更具体的项可以同时捕捉所有共同结构。而 f(a, X) 更为一般化，仅覆盖一些共同结构。
早期的归纳逻辑程序设计 (ILP) [Cropper et al., 2022] 方法利用泛化之间的关系来学习逻辑程序 [Muggleton, 1995]。现代 ILP 方法（如 Popper [Cropper and Morel, 2021]）利用这一机制迭代简化搜索。通过示例编程 (pbe) [Gulwani, 2016] 范式集成了语法反统一方法来找到满足输入示例的最小一般程序。最近关于库学习和压缩的工作 [Cao et al., 2023] 利用等式反统一来高效地找到合适的程序，并且性能优于 Dreamcoder [Ellis et al., 2021]，即以前的最先进方法。
归纳合成领域之外的应用通常利用以下观察：“语法相似性通常意味着语义相似性”。一个显著的例子是自动并行递归方案检测 [Barwell et al., 2018]，其中开发了模板，在反统一的帮助下，允许将不可并行的递归替换为并行化的高阶函数。其他用途包括从代码库中学习程序修复 [de Sousa et al., 2021]，防止配置错误[Mehta et al., 2020]，以及检测软件克隆 [Vanhoof and Yernaux, 2019]。
对反统一的兴趣日益增长，但现有的大多数工作都是由特定应用推动的。缺乏系统的研究有时导致方法和算法的重新发明。举例来说，Babble 的作者 [Cao et al., 2023] 仅出于 Plotkin [1970] 的开创性工作而开发了 E-图反统一算法。由于反统一文献的零碎性，作者错过了关于等式反统一 [Burghardt, 2005] 和术语图反统一 [Baumgartner et al., 2018] 等方面的相关工作。发现这些早期论文可能会加快、改进和/或简化他们的研究。
与它的对偶统一操作不同，目前还没有全面的调查，并且对于发展强大的理论基础重视不够。相反，以实践为导向的主题主导了当前关于反统一的研究。这种情况并不令人惊讶，因为泛化在各种应用中是一种必不可少的成分：推理、学习、信息提取、知识表示、数据压缩、软件开发和分析，以及前面已经提到的应用。
新的应用带来了新的挑战。有些需要在全新的理论中研究泛化问题，而其他一些问题则可以通过改进现有算法来充分解决。对已知方法及其应用进行分类、分析和调查，对于塑造该领域并帮助研究人员导航当前泛化技术的分散状态至关重要。
在这项调查中，我们提供（i）泛化问题的一般框架，（ii）现有理论结果的概述，（iii）现有应用领域的概述，以及（iv）一些未来研究方向的概述。
2 概括问题：抽象视角
下面的定义以一组语法对象 O 为参数，通常由某种形式语言中的表达式（例如，项、公式等）组成。此外，我们必须考虑从 O 到 O 的映射类 M。我们说 µ(O) 是对象 O 的一个实例，相对于 µ ∈ M。在大多数情况下，变量替换是此类映射的具体实例。我们将 M 的元素称为概括映射。
我们的概括问题定义需要两个关系：基关系，定义一个对象如何成为另一个对象的概括；以及偏好关系，定义概括之间的优先级概念。这些关系是抽象定义的，只有最低要求。我们为每个具体的概括问题提供基关系、偏好关系和概括映射的具体实例。可以将基关系理解为描述我们在说一个对象是另一个对象的概括时的含义，而偏好关系则描述概括之间的质量高低。映射可以理解为描述在给定基关系下对象的概括意味着什么。
此问题可能有零个、一个或多个解。可能有两个原因导致它没有解：要么对象 O1, ..., On 根本没有共同的 BM 概括（即，O1, ..., On 是不可概括的，参见 [Pfenning, 1991] 的示例），要么它们可以概括，但没有最符合 P 偏好的共同 BM 概括。
为了表征“信息丰富的”可能解集，我们引入了两个概念：多个对象的共同 BM 概括的 P-完备集和 P-最小完备集。
如果给定对象 O1, ..., On（分别为所需对象 G）被限制为属于某个子集 S ⊆ O，那么我们讨论的是泛化问题的 S-片段（分别为 S-变体）。还可以考虑问题的 S2-片段的 S1-变体，其中 S1 和 S2 不一定相同。
当 O 是一组术语时，通常会考虑线性变体：泛化术语不包含同一变量的多个出现。
以下章节展示了已知的泛化问题如何符合此框架。为简单起见，当不影响普遍性时，我们仅考虑两个给定对象的泛化问题。此外，在讨论共同泛化时，我们通常省略“共同”一词。
由于篇幅限制，我们不讨论特征术语的反统一 [Aït-Kaci and Sasaki, 2001; Armengol and Plaza, 2000]，术语图的反统一 [Baumgartner et al., 2018]，名义反统一 [Baumgartner et al., 2015; Schmidt-Schauß and Nantes-Sobrinho, 2022]，以及近似反统一 [Aït-Kaci and Pasi, 2020; Kutsia and Pau, 2022; Pau, 2022]。这些工作中研究的泛化问题都适合我们的一般框架。
3 泛化在一阶理论中的应用
3.1 一阶语法泛化 (FOSG)
Plotkin [1970] 和 Reynolds [1970] 引入了 FOSG，它是逻辑中最简单且最知名的泛化问题。对象是一阶项，映射是将变量映射到项的替换，其中除有限个变量外，所有变量都映射到它们自身。对项 t 应用替换 σ 表示为 tσ，即通过将 t 中的所有变量替换为它们在 σ 下的映像所得到的项。
3.2 一阶方程式泛化（FOEG）
一阶方程式泛化（FOEG）需要将句法等式扩展为模一组给定等式的等式。许多代数理论都是通过（隐式地全量化的）等式来刻化函数符号的属性。一些知名的方程式理论包括：
我们可以将这种符号扩展到组合中：例如，(AU)(CU)>1 表示包含至少一个函数符号（例如 f），它是结合和单元的（具有单元元素 ef），以及至少两个函数符号（例如 g 和 h），它们是交换和单元的（具有单元元素 eg 和 eh）。表2展示了一阶方程式反统一如何适应我们在第2节中描述的通用框架。
特定理论的结果总结在表3中。Alpuente等人[2014]在更一般的排序设置中研究了A、C和AC理论的反统一，并提供了相应的算法。在[Alpuente等人，2022]中，他们还考虑了将这些理论与U结合在特定的排序签名中，以确保相应算法的有限性和完备性。
Burghardt[2005]提出了一种基于语法的方法来计算方程式泛化：从一个描述给定项t1和t2的同余类的正则树语法出发，计算出一个描述t1和t2的E泛化完整集的正则树语法。这种方法适用于导致正则同余类的方程式理论。否则，可以使用一些启发式方法来近似答案，但无法保证完备性。
Baader在1991年的研究中考虑了所谓的交换理论的反统一，这个概念包括了交换幺半群（ACU）、交换幂等幺半群（ACUI）和阿贝尔群。在这种设置中，对象集被限制为使用变量和代数运算符构建的术语。在这种设置中的交换理论反统一始终是单元的。
3.3 一阶子句泛化（FOCG）
子句是文字（原子公式或其否定）的析取。一阶子句的泛化可以看作是FOEG的一个特例，其中有一个ACUI符号（析取）只作为所涉及表达式的顶层符号出现。这是最早研究泛化的理论之一（见例如[Plotkin, 1970]）。子句泛化（带有各种基础关系）已成功用于关系学习。较新的工作使用刚性函数构建泛化，并考虑逻辑程序中的克隆检测[Yernaux和Vanhoof, 2022b]。
表征子句泛化的一个重要概念是θ-包含[Plotkin, 1970]：通过将析取视为ACUI符号来定义，但更自然的定义是将子句L1 ∨ ··· ∨ Ln视为文字集合{L1, ... , Ln}。那么我们说子句C θ-包含子句D，记作C ⊑ D，如果存在一个替换θ使得Cθ ⊆ D（其中Sθ的符号定义为对于集合S，Sθ = {sθ | s ∈ S}）。基础关系B是集合包含⊆，泛化映射M中的泛化映射是一阶替换，偏好关系P是θ-包含的逆关系⊏。
Plotkin的博士论文包含了一个计算子句泛化的算法。这个问题是单元的：一个有限的子句集总是拥有一个唯一的lgg，直到θ-包含等价≡P。其大小可以是它泛化子句数量的指数。
Idestam-Almquist在1995年提出了一种子句泛化的新变体，提出了一种不同的基础关系：T-implication ⇒T。这种关系是反射性的非传递关系，它考虑了一组给定的地面术语T，扩展了Plotkin关于在θ-subsumption下的泛化框架，将其推广到一种特殊形式的implication下的泛化。与implication不同，它是可判定的。值得注意的是，Plotkin引入了θ-subsumption作为implication的不完整近似。Idestam-Almquist在1997年还将相对子句泛化提升到T-implication。
Muggleton等人在2009年引入了相对子句泛化的修改版本，称为不对称相对最小泛化，并在ProGolem中实现。Kuzelka等人在2012年研究了子句泛化的有界版本，这是由子句学习中的实际应用驱动的。Yernaux和Vanhoof在2022年考虑了不同的基础关系，用于泛化无序逻辑程序目标。这些研究中研究的泛化问题都符合我们所描述的通用框架。
3.4未分级的一阶推广(UFOG)
在未排序的语言中，符号没有固定的参数数量，通常被称为多样的、多参数的、灵活的、可变参数或者变量参数符号。为了利用这种多样性，未排序的语言包含了hedging变量以及个别变量。后者代表单个术语，而前者代表hedging（可能是空的术语序列）。在本节中，个别变量用x、y、z表示，hedging变量用X、Y、Z表示。形式为f()的术语被写作f。通常将hedging放在括号中，但单个hedging (t)被写作t。替换映射将个别变量映射到术语，将hedging变量映射到hedging，应用后进行扁平化处理。
我们在表 4 中为 UFOG 提供了相对于我们通用框架参数的具体值。
Kutsia 等人 [2014] 研究了非排序泛化，并提出了在泛化中禁止相邻树篱变量的刚性变体。此外，使用了一个称为刚性函数的额外参数来选择树篱顶层函数符号的公共子序列集进行泛化。该集合的元素提供了泛化树篱的顶层函数符号序列，从而简化了泛化的构建。刚性函数最自然的选择是计算其参数的最长公共子序列（lcs）的集合。然而，还有其他具有实际意义的刚性函数（例如，带最小长度限制的 lcs，按照某种标准选择的单个 lcs，最长公共子串等）。刚性变体也是有限的，其最小完整集合记为 mcsgR。Kutsia 等人 [2014] 描述了一个计算该集合的算法。以下示例使用了 lcs 刚性函数。
无序项和树篱可以用于建模半结构化文档、程序代码、执行轨迹等。Yamamoto 等人 [2001] 在与半结构化数据处理相关的树篱逻辑程序的归纳推理背景下，研究了无序反统一。他们考虑了一种特殊情况（没有个体变量），其中树篱不包含相同树篱变量的重复出现，并且任何一组同级参数至多包含一个树篱变量。这样的树篱称为简单树篱。
Kutsia 等人 [2014] 引入了一种（刚性）反统一算法，不仅用于计算无序泛化（包括简单树篱），还用于其他相关理论，如词泛化 [Biere, 1993] 或 AU 泛化。Baumgartner 和 Kutsia [2017] 将无序一阶项的反统一推广到无序二阶项，并在 [Baumgartner 等人, 2018] 中推广到无序项图。相应的算法已被研究。两类问题都是有限的，并符合我们的通用框架，但由于篇幅限制，我们无法详细讨论。
3.5 描述逻辑
描述逻辑（DLs）是知识表示和推理的重要形式主义。它们是一阶逻辑的可判定片段。DLs 中的基本句法构建块是概念名（单元谓词）、角色名（二元谓词）和个体名（常量）。从这些构造开始，通过构造器可以构建复杂的概念和角色，构造器决定了描述逻辑的表达能力。在本节中讨论的描述逻辑中，我们展示了概念描述（用 C 和 D 表示）如何在概念名集 NC 和角色名集 NR 上递归定义。下面我们提供描述逻辑 EL、FLE、ALE 和 ALEN 的定义，其中 P ∈ NC 表示一个基本概念，r ∈ NR 表示一个角色名，n ∈ N。
表5展示了这些关于EL、FLE、ALE和ALEN的结果如何能够适应我们的框架。在描述逻辑（DLs）中计算泛化的一些其他结果包括：根据背景术语计算最小公共子sumer [Baader et al., 2007]，计算知识库中的最小公共子sumer和最具体概念 [Jung et al., 2020]，以及反统一 [Konev and Kutsia, 2016]。
4 高阶泛化
高阶泛化主要涉及在简单类型λ演算中的泛化，尽管它已经在Berendregt的λ-立方体[Barendregt et al., 2013]中的其他理论以及相关设置中被研究（见[Pfenning, 1991]）。
我们考虑由语法t ::= x | c | λx.t | (t t)定义的lambda项，其中x是变量，c是常数。一个简单类型τ要么是一个基本类型δ，要么是一个函数类型τ → τ。我们使用λ-演算的标准概念，如绑定变量和自由变量、子项、α-转换、β-规约、η-长的β-正规形式等（见，例如，[Barendregt et al., 2013]）。
替换是（类型保持的）从变量到lambda项的映射。它们构成了集合M。
在本节中，x、y、z用于绑定变量，X、Y、Z用于自由变量。
4.1 高阶αβη-泛化 (HOGαβη)
在简单类型λ演算中的句法反统一是关于α、β、η规则的泛化（即，基础关系是模αβη的等式，我们在本节中用≈表示）。
假设项处于η-长的β-正规形式。偏好关系是%：如果s ≈ tσ对于某个替换σ，则s % t。它的逆关系用-表示。Cerna和Buran[2022]表明，在这个理论中，不受限制的泛化是零元的：
Cerna和Kutsia在2019年提出了一个通用框架，用于处理简单类型λ演算中的几种特殊单元泛化变体。这个框架的动机是两个期望的泛化属性：最大化地保留给定项的自顶向下公共部分（顶极大性）和避免泛化变量的嵌套（浅层性）。这些约束导致了顶极大浅（tms）泛化变体，它在选择泛化变量下的子项时提供了一定的自由度。可能的单元变体包括：投影（pr：整个项）、公共子项（cs：最大公共子项）、其他cs变体，其中公共子项不一定是最大的，但满足Libal和Miller在2022年讨论的限制，例如（放宽的）函数作为构造器（rfc,fc），以及模式（p）。计算pr和p变体的时间复杂度是输入项大小的线性，而其他情况则是立方。
在高阶泛化中，特别是在简单类型λ演算中，考虑的是λ项的句法反统一，这是关于α、β、η规则的泛化（即，基础关系是模αβη的等式，本节中用≈表示）。术语假设处于η-长的β-正规形式。偏好关系是%：如果s ≈ tσ对于某个替换σ，则s % t。它的逆关系用-表示。Cerna和Buran在2022年展示了在这个理论中，不受限制的泛化是零元的。
表6 将 HOGαβη 与通用框架相关联。αβη-广义化的线性变体被 [Pientka, 2009] 用于开发一个基于替代树的高阶术语索引算法。插入到替代中需要计算给定的高阶模式与已在替代树中的高阶模式的 lgg。Feng 和 Muggleton [1992] 考虑了一个称为 λM 的简单类型 lambda 项的 αβδ0η-广义化，其中 δ0 表示类似于 if-then-else 的额外分解规则。类似于 top-maximal 浅层 lambda 项，λM 允许常量在广义化变量的参数内。由于篇幅限制，我们未详细讨论 [Pfenning, 1991] 关于构造演算中反统一的工作，他描述了一种用于模式变体的算法。将这项工作纳入我们的通用框架需要稍微调整用于 αβη-广义化的参数。
4.2 高阶等式广义化
Cerna 和 Kutsia [2020a] 研究了简单类型 lambda 演算中高阶等式广义化（HOEG）的模式变体，涉及 A、C、U 公理及其组合（表7）。此外，他们还研究了某些片段，其中可以快速计算出某些最佳广义化。研究表明，在 A、C、AC 理论中的模式 HOEG 是有限的。HOEG 在 A、C、U 理论及其组合中的线性模式变体也是如此。考虑的片段在仅考虑最佳解时是单元的。最佳性意味着解应至少与 αβη-lgg 一样好。已识别出允许快速计算最佳解（线性、二次或立方时间）的片段。
4.3 多态高阶泛化
Lu等人[2000]考虑在多态λ演算中的泛化，通常称为λ2（见表8）。
与上述αβη-泛化不同，术语不需要具有相同的类型才能被泛化。虽然[Pfenning, 1991]中也有类似的论述，但Lu等人[2000]不仅限于模式变体，而是限制了偏好关系。他们使用应用顺序的受限形式，即s % t当且仅当存在术语和类型r1, ..., rn使得sr1 ... rn ≈ t，换句话说，sr1 ... rn β-规约到t。他们将r1, ..., rn限制为t的子项，并引入变量冻结来处理绑定变量顺序。映射也基于β-规约。
4.4 二阶组合子泛化
Hasker在1995年考虑了使用组合子而不是λ抽象来表示二阶逻辑的替代表示方法（见表9）。与λ项不同，λ项通过替换将一个术语应用于另一个术语，组合子是特殊的符号，每个符号都与它们对输入术语影响的精确公理定义相关联。请注意，这里的替换涉及术语规范化，而不是泛化问题。在[Hasker, 1995]中引入的泛化问题和算法仍然需要二阶替换。Hasker引入了单体组合子，它们接受单个参数，以及笛卡尔组合子，它们通过引入配对函数来泛化单体组合子，从而允许多个参数。麻烦的是，笛卡尔组合子泛化是零元的，因为配对函数可以作为无关构造的存储。Hasker在1995年通过引入相关性概念来解决这个问题，并展示了由此产生的泛化问题是有限性的。
5 应用
文献中考虑了许多应用。它们通常可以归入以下领域之一：学习与推理、合成与探索、分析与修复。下面我们简要讨论这些领域的最新技术，并在可能的情况下，讨论相关的泛化类型。
5.1 学习与推理
基于逆蕴涵的归纳逻辑编程系统，如ProGolem [Muggleton et al., 2009]、Aleph [Srinivasan, 2001] 和 Progol [Muggleton, 1995] 使用（相对）θ-包含或其变体来搜索最具体的子句（底层子句）的泛化，该子句蕴涵单一示例。由Cropper等人[2022]开发的ILP系统Popper使用基于θ-包含的约束来迭代简化搜索空间。这个系统的最近扩展，如Hopper [Purgal et al., 2022] 和 NOPI [Cerna and Cropper, 2023] 在更具表现力的假设空间上考虑了类似的技术。
几位作者专注于类比推理的泛化和反统一。Krumnack等人[2007]使用高阶泛化的限制形式来发展有用的类比。Weller和Schmid[2006]使用Burghardt[2005]引入的方程式泛化方法来解决比例类比问题，即“A 对 B 如 C 对？”。Sotoudeh和Thakur[2020]讨论了泛化作为类比推理程序的重要工具。泛化在基于案例的推理[Onta ˜n ´on 和 Plaza, 2007]文献中作为一种方法被用来编码给定预测所覆盖的案例范围。
与概念融合和数学推理相关的研究建立在启发式驱动的理论投影基础上，使用高阶反统一的形式[Schwering et al., 2009]。这方面的示例工作包括[Guhe et al., 2011]和[Mart´ınez et al., 2017]。
从准自然语言句子中使用反统一学习推理规则在[Yang and Deng, 2021]中讨论。通过泛化语言结构进行学习在工业聊天机器人的开发中找到了应用[Galitsky, 2019]。
5.2 合成与探索
基于示例的编程（PBE）范式是一种归纳合成范式，涉及在特定领域的语言（DSL）中生成一个程序，该程序泛化输入输出示例[Raza et al., 2014]。通过DSL的有效搜索利用了专门构建的泛化方法[Mitchell, 1982]。这个领域的基础工作包括[Gulwani, 2011]和[Polozov and Gulwani, 2015]。
最近的发展包括[Dong et al., 2022]，其中作者特别提到了在机器人流程自动化中用于合成的未排序方法，以及[Feser et al., 2015]，其中作者合成了数据结构的函数转换。关于函数程序归纳合成的早期工作包括由Hofmann[2010]开发的IGOR II。IGOR II基于[Kitzelmann and Schmid, 2006]中介绍的工作，并利用了Plotkin[1970]引入的基本句法泛化方法。
Johansson等人[2011]使用泛化的一种形式进行猜想合成。
Babble是由Cao等人[2023]引入的一种方法，用于理论探索和压缩，利用一阶方程式反统一和术语图表示来寻找压缩库中其他函数表示的函数。Bowers等人[2023]关注问题的学习能力方面。Singher和Itzhaky[2021]在合成过程中使用泛化模板。
5.3 分析与修复
使用反统一来检测软件和仓库中的克隆问题最初由Bulychev和Minea在2008年讨论（另见[Bulychev et al., 2009]）。这个研究方向针对特定用例进一步发展。例如，Li和Thompson[2010]研究了Erlang中的克隆检测，而Yernaux和Vanhoof[2022b]研究了约束逻辑程序中的克隆检测。
Sinha[2008]，以及最近的Arusoaie和Lucanu[2022]，使用反统一来实现高效的符号执行，这是一种软件验证类型。Hasker[1995]使用基于组合子的高阶反统一方法开发了一种推导重放方法，通过模板化自动化编程的某些方面。与推导重放相关的是Barwell等人[2018]关于并行递归方案检测的工作。Maude[Clavel et al., 2002]是一种用于软件验证任务的声明性编程语言。它已经通过排序、方程式和句法反统一方法得到了扩展。
正如Winter等人[2022]所讨论的，最近的调查利用反统一提供程序修复和错误检测能力。Sakkas等人[2020]使用未排序的hedging反统一变体作为模板机制，基于类型错误提供修复。Getafix的作者[Bader et al., 2019]和REVISAR的作者[de Sousa et al., 2021]也采取了这种方法。由Mehta等人[2020]开发的Rex，对于修复配置错误的服务采取了类似的方法，而[Siddiq et al., 2021]使用未排序的hedging反统一来检测和修复SQL注入漏洞。Zhang等人[2022]使用泛化技术从仓库中的编辑序列开发编辑模板。
6 未来方向
尽管反统一研究已有数十年的历史，但这个领域的大部分工作都是由实际应用驱动的，与统一技术等相比，反统一的理论相对不太发达。为了解决这一不足，我们列出了一些有趣的未来研究方向，我们认为这些方向可以显著促进反统一/泛化技术的发展。
• 基于问题中允许的函数符号类型（仅限方程式符号、方程式符号+自由常数，或方程式符号+任意自由符号）对方程式理论中的反统一进行特征化。这种选择可能会影响泛化类型。
• 开发方法，将不相交方程式理论的反统一算法组合成一个组合理论的算法。
• 对表现出泛化问题类似行为和属性的方程式理论类别进行特征化。
• 研究偏好关系选择对泛化问题类型和解集的影响。
• 研究计算复杂性和优化。
