合一

在邏輯和計算機科學中，合一（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]