合一

在邏輯和電腦科學中，合一（unification），是方程求解表達式之間方程的演算法過程。例如，使用 x, y, z 作為變數，單元素集合解的方程{cons(x, cons(x, nil)) = cons(2, y)}是一個語法一階合一問題，具有替換{x ↦ 2, y ↦ cons(2, nil)}作為其唯一解。

合一演算法首先由雅克·埃爾布朗 ( ^[1] ^[2] ^[3]發現，而第一個正式研究可歸因於John Alan Robinson（英語：John Alan Robinson）^[4] ^[5]，他使用一階句法合一作為基本構建塊他對一階邏輯的歸結過程的研究是自動推理技術的一大進步，因為它消除了組合爆炸（英語：Combinatorial explosion）的一個來源：搜尋專案實例。如今，自動推理仍然是合一的主要應用領域。語法一階合一用於邏輯編程和程式語言型別系統實現，特別是基於 Hindley-Milner 的類型推論演算法。語意合一用於 SMT 求解器、重寫邏輯演算法和安全協定分析。高階合一用於證明助手，例如 Isabelle 和 Twelf ，並且高階合一的受限形式（高階模式合一）用於某些程式語言實現，例如lambdaProlog（英語：λProlog），因為高階模式具有表現力，但它們相關的合一過程保留了更接近一階合一的理論屬性。

例如，對於多項式 X² 和 Y³ 可以透過採納 X = Z³ 和 Y = Z² 而合一到 Z⁶。

Prolog 中的合一的解釋

合一概念是在 Prolog 背後的主要想法。它表示繫結變數的內容的機制並可以看作為一種只一次的(one-time)賦值。在 Prolog 中，這種操作用符號 "=" 來指示。

在傳統 Prolog 中，未實例化的變數 X — 就是說在它上面以前沒有進行合一，可以合一於一個原子、一個項、或另一個未實例化的變數，因此在效果上變成了它的別名。在很多現代 Prolog 方言和一階邏輯演算中，變數不能合一於包含它的項；這叫做出現檢查（英語：Occurs check）。
Prolog 原子只能合一於同一個原子。
類似的，項只能合一於另一個項，如果頂部函式符號和項的元數(arity)和這個項是一樣的，並且參數可以同時合一。注意這是遞迴行為。

由於它的聲明本性，一序列合一的次序(通常)是不重要的。

注意在一階邏輯的術語中，原子是基本命題而且其合一同 Prolog 項一樣。

合一的例子

A = A : 成功(重言式)
A = B, B = abc : A 和 B 二者合一於原子 abc
xyz = C, C = D : 合一是對稱的
abc = 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)
f(g(A), A) = f(B, xyz) : A 合一於原子 xyz 而 B 合一於項 g(xyz)
A = f(A) : 無限合一， A 合一於 f(f(f(f(...))))。在嚴格的一階邏輯和很多現代 Prolog 方言中，這是禁止的(並由出現檢查來強制)
A = abc, xyz = X, A = X : 合一失敗；效果上 abc = xyz

參照

F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.
F. Baader and W. Snyder, Unification Theory（頁面存檔備份，存於網際網路檔案館）. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers, 2001.

^ J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.
^ Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier. Lectures on Jacques Herbrand as a Logician (SEKI Report). 2009. arXiv:0902.4682  . |number=被忽略 (幫助)Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). Lectures on Jacques Herbrand as a Logician (SEKI Report). DFKI. arXiv:0902.4682. Here: p.56
^ Jacques Herbrand. Recherches sur la théorie de la demonstration (PDF) (Ph.D. thesis論文). [2024-01-28]. （原始內容存檔 (PDF)於2023-12-02）. Jacques Herbrand (1930). Recherches sur la théorie de la demonstration （頁面存檔備份，存於網際網路檔案館） (PDF) (Ph.D. thesis). A. Vol. 1252. Université de Paris. Here: p.96-97
^ J.A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. Jan 1965, 12 (1): 23–41. S2CID 14389185. doi:10.1145/321250.321253  . J.A. Robinson (Jan 1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.; Here: sect.5.8, p.32
^ J.A. Robinson. Computational logic: The unification computation. Machine Intelligence. 1971, 6: 63–72. J.A. Robinson (1971). "Computational logic: The unification computation" （頁面存檔備份，存於網際網路檔案館）. Machine Intelligence. 6: 63–72.

[1] J. Herbrand: Recherches sur la théorie de la démonstration. Travaux de la société des Sciences et des Lettres de Varsovie, Class III, Sciences Mathématiques et Physiques, 33, 1930.

[2] Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier. Lectures on Jacques Herbrand as a Logician (SEKI Report). 2009. arXiv:0902.4682  . |number=被忽略 (幫助)Claus-Peter Wirth; Jörg Siekmann; Christoph Benzmüller; Serge Autexier (2009). Lectures on Jacques Herbrand as a Logician (SEKI Report). DFKI. arXiv:0902.4682. Here: p.56

[3] Jacques Herbrand. Recherches sur la théorie de la demonstration (PDF) (Ph.D. thesis論文). [2024-01-28]. （原始內容存檔 (PDF)於2023-12-02）. Jacques Herbrand (1930). Recherches sur la théorie de la demonstration （頁面存檔備份，存於網際網路檔案館） (PDF) (Ph.D. thesis). A. Vol. 1252. Université de Paris. Here: p.96-97

[Robinson.1965-4] J.A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. Jan 1965, 12 (1): 23–41. S2CID 14389185. doi:10.1145/321250.321253  . J.A. Robinson (Jan 1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12 (1): 23–41. doi:10.1145/321250.321253. S2CID 14389185.; Here: sect.5.8, p.32

[5] J.A. Robinson. Computational logic: The unification computation. Machine Intelligence. 1971, 6: 63–72. J.A. Robinson (1971). "Computational logic: The unification computation" （頁面存檔備份，存於網際網路檔案館）. Machine Intelligence. 6: 63–72.

[1]

[2]

[3]

[4]

[5]