合一（電腦科學與邏輯）

合一（電腦科學與邏輯）

概述

合一（Unification）是邏輯學與電腦科學中用於求解表達式之間方程式的演算法過程。這一概念在自動推理、邏輯編程、程式語言類型系統等領域具有重要應用。合一的核心目標是找到一個替換（substitution），使得兩個或多個表達式在應用該替換後變得完全相同。

合一的概念是 Prolog 等邏輯編程語言背後的主要思想，它代表了一種變數綁定內容的機制，可視為一種單次賦值操作。

歷史淵源

合一理論的發展可追溯至二十世紀初。1930年，法國數學家雅克·埃爾布朗（Jacques Herbrand）在其博士論文中首次發現了合一演算法的基本原理^[3]^。隨後，1965年，美國邏輯學家約翰·阿蘭·羅賓遜（John Alan Robinson）在其具有里程碑意義的論文《A Machine-Oriented Logic Based on the Resolution Principle》中，首次正式系統地研究了合一理論，並將一階語法合一作為其歸結原理（Resolution Principle）研究的核心構建模塊^[4]^。羅賓遜的工作被視為自動推理技術的重大進步，因為合一技術有效消除了搜尋實例過程中的組合爆炸問題^[1]^。

主要內容

一階語法合一

一階語法合一是最基本且應用最廣泛的合一形式。其核心問題可定義為：給定一組變數和函數符號，找出能將兩個或多個項（terms）統一為相同結構的替換集合。

合一的基本規則：

• 變數可以與原子合一，形成該變數的別名
• 原子只能與相同的原子合一
• 項（Term）只能與具有相同函數符號和元數（Arity）的另一項合一
• 合一過程具有遞迴性，項的參數必須同時可合一

合一的主要類型

類型	應用領域
語法一階合一	邏輯編程、類型推論（如 Hindley-Milner 演算法）
語意合一	SMT 求解器、重寫邏輯、安全協定分析
高階合一	證明助手（如 Isabelle、Twelf）
高階模式合一	程式語言實現（如 λProlog）

Prolog 中的合一機制

在 Prolog 中，合一操作使用符號 = 表示。其行為規則如下^[1]^：

1. 未實例化變數：未綁定的變數可與原子、項或另一未實例化變數合一，形成別名
2. 出現檢查：在嚴格的一階邏輯及現代 Prolog 方言中，變數不能與包含自身的項合一，以避免無限合一的問題
3. 項的合一：僅當項的函數符號、元數相同，且所有參數可同時合一時，兩個項才能合一

合一的理論性質

合一運算具有以下重要理論性質：

• 終結性：合一過程在有限步驟內終止
• 唯一性：最一般合一（Most General Unifier, MGU）是唯一的
• 對稱性：合一關係是對稱的

合一的例子

以下為各類合一情形及其結果^[1]^：

表達式	結果	說明
A = A	成功	重言式
A = B, B = abc	成功	A、B 皆合一於原子 abc
abc = xyz	失敗	原子不同
f(A) = f(B)	成功	A 合一於 B
f(A) = g(B)	失敗	函數符號不同
f(A) = f(B, C)	失敗	元數不同
f(g(A)) = f(B)	成功	B 合一於 g(A)
A = f(A)	失敗	違反出現檢查，產生無限合一

多項式合一的例子

對於多項式 X² 和 Y³，可透過採納替換 X ↦ Z³ 和 Y ↦ Z² 而合一到 Z⁶ ^[1]^。

應用領域

1. 自動推理：合一是歸結原理的核心構建模塊，用於定理證明
2. 邏輯編程：Prolog 等語言的執行機制建立在合一之上
3. 類型系統：特別是基於 Hindley-Milner 的類型推論演算法
4. 安全協定分析：用於驗證密碼學協定的安全性
5. 證明助手：如 Isabelle、Coq 等形式化驗證工具

來源

1. Wikipedia - 合一（電腦科學）. https://zh.wikipedia.org/wiki/%E5%90%88%E4%B8%80
2. Baader, F. and Nipkow, T. Term Rewriting and All That. Cambridge University Press, 1998.
3. Baader, F. and Snyder, W. "Unification Theory." Handbook of Automated Reasoning, Volume I, pp. 447-533. Elsevier Science Publishers, 2001.
4. Robinson, J.A. "A Machine-Oriented Logic Based on the Resolution Principle." Journal of the ACM, 12(1): 23-41, 1965.

校對記錄

• 2026-05-04 確認錯誤：「1930年，法國數學家雅克·埃爾布朗（Jacques Herbrand）在其博士論文中首次發現了合一演算法的基本原理」這句有明顯年代錯誤：Herbrand 於 1931 年去世，且其著名『Herbrand theorem / Herbrand universe』相關工作並非在 1930 年的博士論文中首次提出合一演算法基本原理；合一理論通常不歸功於他『首次發現演算法基本原理』。 → 正確：合一（unification）的奠基性工作通常歸功於 J. Alan Robinson（1965）在自動定理證明中的引入；Herbrand 與其定理、Herbrand universe 相關，但不宜表
• 2026-05-04 確認錯誤：「羅賓遜的工作…因為合一技術有效消除了搜尋實例過程中的組合爆炸問題」表述過度且不準確。合一能大幅降低搜尋負擔，但不能說『有效消除了』組合爆炸問題。 → 正確：合一能顯著減少在推理中枚舉實例的搜尋空間，但不能說已『有效消除』組合爆炸問題；較準確說法是『大幅降低搜尋負擔』或『減少實例化帶來的組合爆炸』。
• 2026-05-04 確認錯誤：「變數可以與原子合一，形成該變數的別名」不夠精確且容易誤導：在一階項合一中，變數可與任意項合一，不只是原子；且這不是『原子』專屬規則。 → 正確：在一階項合一中，變數可以與任意項合一，不限於原子；較精確的表述應是『變數可被替換為某個項，並可與該項合一』。
• 2026-05-04 確認錯誤：「在嚴格的一階邏輯及現代 Prolog 方言中，變數不能與包含自身的項合一」不準確。標準邏輯中的合一通常包含 occurs check，但許多 Prolog 實作為效率會省略 occurs check，並非可直接概括為『現代 Prolog 方言中』都不能。 → 正確：標準的一階合一通常包含 occurs check，故變數不能與含有自身的項合一；但許多 Prolog 實作為效率起見會省略 occurs check，因此不能概括成『現代 Prolog 方言中』一概不
• 2026-05-04 確認錯誤：「合一運算具有以下重要理論性質：唯一性：最一般合一（MGU）是唯一的」表述不嚴謹。MGU 通常是『唯一到變數重命名（renaming）』，不是字面上唯一。 → 正確：最一般合一（MGU）通常是『唯一到變數重命名（renaming）』，不是字面上的唯一。
• 2026-05-04 確認錯誤：「對於多項式 X² 和 Y³，可透過採納替換 X ↦ Z³ 和 Y ↦ Z² 而合一到 Z⁶」這不是典型『合一』的標準例子，因為多項式代數中的同值化與一階項合一是不同概念；此處將多項式等式直接說成合一，概念混淆。 → 正確：將多項式等式 X²、Y³ 的同值化直接稱為『合一』，會混淆代數同值化與一階項合一；兩者是不同概念。