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 未來方向

盡管反統一研究已有數十年的歷史，但這個領域的大部分工作都是由實際應用驅動的，與統一技術等相比，反統一的理論相對不太發達。為了解決這一不足，我們列出了一些有趣的未來研究方向，我們認為這些方向可以顯著促進反統一/泛化技術的發展。

? 基于問題中允許的函數符號類型（僅限方程式符號、方程式符號+自由常數，或方程式符號+任意自由符號）對方程式理論中的反統一進行特征化。這種選擇可能會影響泛化類型。

? 開發方法，將不相交方程式理論的反統一算法組合成一個組合理論的算法。

? 對表現出泛化問題類似行為和屬性的方程式理論類別進行特征化。

? 研究偏好關系選擇對泛化問題類型和解集的影響。

? 研究計算復雜性和優化。