단일화

논리학 및 컴퓨터 과학, 특히 자동화된 추론에서 단일화 또는 유니피케이션(unification)은 기호적 수식 사이의 방정식을 푸는 알고리즘 프로세스로, 각 방정식은 좌변 = 우변의 형태를 갖는다. 예를 들어, x,y,z를 변수로 사용하고 f를 해석되지 않는 함수로 간주할 때, 한원소 집합 방정식 집합 { f(1,y) = f(x,2) }는 치환 { x ↦ 1, y ↦ 2 }를 유일한 해로 갖는 구문적 1차 단일화 문제이다.

변수가 취할 수 있는 값과 어떤 식이 동등한 것으로 간주되는지에 대한 관례는 다르다. 1차 구문 단일화에서는 변수가 1차 항을 범위로 하고 동등성은 구문적이다. 이 버전의 단일화는 고유한 "최적의" 답을 가지며 논리형 프로그래밍 및 프로그래밍 언어의 자료형 체계 구현, 특히 힌들리–밀너 기반의 자료형 추론 알고리즘에 사용된다. 고차 단일화에서는 고차 패턴 단일화로 제한될 수 있으며, 항에 람다 식이 포함될 수 있고 동등성은 베타-환원(beta-reduction)까지 고려된다. 이 버전은 증명 보조기 및 고차 논리형 프로그래밍(예: Isabelle, Twelf 및 lambdaProlog)에 사용된다. 마지막으로 의미론적 단일화 또는 E-단일화에서는 등식이 배경 지식에 따라 달라지며 변수는 다양한 도메인을 범위로 한다. 이 버전은 SMT 솔버, 항 재작성 알고리즘 및 암호화 프로토콜 분석에 사용된다.

형식 정의

단일화 문제는 유한 집합 E= l₁ ≐ r₁, ..., l_n ≐ r_n }의 방정식이다. 여기서 l_i, r_i는 항 또는 식의 집합 $T$에 속한다. 방정식 집합 또는 단일화 문제에 어떤 식이나 항이 허용될 수 있는지, 어떤 식이 동등한 것으로 간주되는지에 따라 여러 단일화 프레임워크가 구별된다. 고차 변수, 즉 함수를 나타내는 변수가 식에 허용되는 경우, 이 과정은 고차 단일화라고 불리며, 그렇지 않으면 1차 단일화라고 불린다. 해가 각 방정식의 양변을 문자적으로 같게 만들어야 하는 경우, 이 과정은 구문적 또는 자유 단일화라고 불리며, 그렇지 않으면 의미론적 또는 방정식 단일화, 즉 E-단일화 또는 이론 모듈로 단일화라고 불린다.

각 방정식의 우변이 닫혀 있는 경우(자유 변수가 없는 경우) 이 문제는 (패턴) 매칭이라고 불린다. 각 방정식의 좌변(변수를 포함하는)은 패턴이라고 불린다.

전제 조건

형식적으로, 단일화 접근 방식은 다음을 전제한다.

• 무한 변수 집합 $V$. 고차 단일화의 경우, $V$를 람다 항 속박 변수 집합과 서로소로 선택하는 것이 편리하다.
• $V\subseteq T$를 만족하는 항 집합 $T$. 1차 단일화의 경우, $T$는 일반적으로 1차 항 집합(변수와 함수 기호로 구성된 항)이다. 고차 단일화의 경우 $T$는 1차 항과 람다 항(고차 변수를 포함하는 항)으로 구성된다.
• 각 항 $t$에 $t$에 나타나는 자유 변수 집합 ${\text{vars}}(t)\subsetneq V$를 할당하는 매핑 ${\text{vars}}\colon T\rightarrow$ $\mathbb {P}$$(V)$.
• $T$에 대한 이론 또는 동치 관계 $\equiv$는 어떤 항이 동일한 것으로 간주되는지를 나타낸다. 1차 E-단일화의 경우, $\equiv$는 특정 함수 기호에 대한 배경 지식을 반영한다. 예를 들어, $\oplus$가 교환적이라고 간주되면, $u$가 $t$에서 $\oplus$의 인수를 일부(possibly all) 발생에서 교환하여 얻어지는 경우 $t\equiv u$이다. 배경 지식이 전혀 없는 가장 일반적인 경우, 문자적으로 또는 구문적으로 동일한 항만 동일한 것으로 간주된다. 이 경우 ≡는 자유 이론(자유 대상이기 때문에), 빈 이론(방정식 문장 집합 또는 배경 지식이 비어 있기 때문에), 해석되지 않는 함수 이론(단일화가 해석되지 않는 항에 대해 수행되기 때문에), 또는 생성자 이론(모든 함수 기호가 데이터 항을 생성할 뿐, 항에 대해 작동하지 않기 때문에)이라고 불린다. 고차 단일화의 경우, 일반적으로 $t\equiv u$는 $t$와 $u$가 알파 동치인 경우이다.

항 집합과 이론이 해 집합에 어떻게 영향을 미치는지의 예로, 1차 구문 단일화 문제 { y = cons(2,y) }는 유한항 집합에서는 해가 없다. 그러나 무한 나무 항 집합에서는 단일 해 { y ↦ cons(2,cons(2,cons(2,...))) }를 갖는다. 유사하게, 의미론적 1차 단일화 문제 { a⋅x = x⋅a }는 각 치환 { x ↦ a⋅...⋅a }를 반군에서 해로 갖는다. 즉, (⋅)가 결합적으로 간주되는 경우이다. 그러나 (⋅)가 교환적으로도 간주되는 아벨 군에서 동일한 문제를 보면 어떤 치환이든 해가 된다.

고차 단일화의 예로, 한원소 집합 { a = y(x) }는 y가 함수 변수이므로 구문적 2차 단일화 문제이다. 한 가지 해는 { x ↦ a, y ↦ (항등 함수) }이며, 다른 해는 { y ↦ (상수 함수 매핑 각 값을 a로), x ↦ (임의의 값) }이다.

치환

 이 부분의 본문은 치환 실례입니다.

치환은 변수에서 항으로의 매핑 $\sigma :V\rightarrow T$이다. 표기법 $\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$는 $i=1,...,k$에 대해 각 변수 $x_{i}$를 항 $t_{i}$로 매핑하고, 다른 모든 변수를 자기 자신으로 매핑하는 치환을 나타낸다. $x_{i}$는 서로 구별되어야 한다. 그 치환을 항 $t$에 적용하는 것은 후위 표기법으로 $t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}$로 작성된다. 이는 항 $t$에서 각 변수 $x_{i}$의 모든 발생을 $t_{i}$로 (동시에) 대체하는 것을 의미한다. 치환 $\tau$를 항 $t$에 적용한 결과 $t\tau$를 그 항 $t$의 인스턴스(instance)라고 한다. 1차 예로, 치환 x ↦ h(a,y), z ↦ b }를 항에 적용하면

	$f($	${\textbf {x}}$	$,a,g($	${\textbf {z}}$	$),y)$
결과를 얻는다.
	$f($	${\textbf {h}}({\textbf {a}},{\textbf {y}})$	$,a,g($	${\textbf {b}}$	$),y).$

일반화, 특수화

항 $t$가 항 $u$와 동등한 인스턴스를 가지는 경우, 즉 일부 치환 $\sigma$에 대해 $t\sigma \equiv u$인 경우, $t$는 $u$보다 더 일반적이라고 하며, $u$는 $t$보다 더 특수하거나 $t$에 의해 포괄된다고 한다. 예를 들어, $x\oplus a$는 $a\oplus b$보다 더 일반적이다. ⊕가 교환적인 경우, $(x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b$이기 때문이다.

≡가 항의 문자적(구문적) 동일성인 경우, 한 항이 다른 항보다 더 일반적이면서 동시에 더 특수한 경우는 두 항이 구문적 구조가 아닌 변수 이름에서만 차이가 날 때뿐이다. 이러한 항을 서로의 변형(variants) 또는 재명명(renamings)이라고 한다. 예를 들어, $f(x_{1},a,g(z_{1}),y_{1})$ 은 다음의 변형이다. $f(x_{2},a,g(z_{2}),y_{2})$ 왜냐하면 $$f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})$$ 이고 $$f(x_{2},a,g(z_{2}),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1},a,g(z_{1}),y_{1}).$$ 그러나, $f(x_{1},a,g(z_{1}),y_{1})$은 $f(x_{2},a,g(x_{2}),x_{2})$의 변형이 아니다. 어떤 치환도 후자의 항을 전자의 항으로 변환할 수 없기 때문이다. 따라서 후자의 항은 전자 항보다 엄밀히 더 특수하다.

임의의 $\equiv$에 대해, 구조적으로 다른 항보다 더 일반적이고 더 특수할 수 있다. 예를 들어, ⊕가 멱등적인 경우, 즉 항상 $x\oplus x\equiv x$인 경우, 항 $x\oplus y$는 $z$보다 더 일반적이고, 그 반대도 마찬가지이다. 비록 $x\oplus y$와 $z$는 구조가 다르더라도 말이다.

치환 $\sigma$는 각 항 $t$에 대해 $t\sigma$가 $t\tau$에 의해 포괄되는 경우 치환 $\tau$에 의해 포괄되거나 $\tau$보다 더 특수하다. 우리는 또한 $\tau$가 $\sigma$보다 더 일반적이라고 말한다. 더 형식적으로, 무한 변수 집합 $V$를 취하는데, 단일화 문제의 어떤 방정식 $l_{i}\doteq r_{i}$도 $V$의 변수를 포함하지 않도록 한다. 그러면 치환 $\sigma$는 다른 치환 $\tau$에 의해 포괄된다. 만약 모든 항 $X\notin V$에 대해 $X\sigma \equiv X\tau \theta$를 만족하는 치환 $\theta$가 있다면 말이다. 예를 들어 $\{x\mapsto a,y\mapsto a\}$는 $\theta =\{y\mapsto a\}$를 사용하여 $\tau =\{x\mapsto y\}$에 의해 포괄되지만, $\sigma =\{x\mapsto a\}$는 $\tau =\{x\mapsto y\}$에 의해 포괄되지 않는다. $f(x,y)\sigma =f(a,y)$가 $f(x,y)\tau =f(y,y)$의 인스턴스가 아니기 때문이다.

해집합

치환 σ는 $i=1,...,n$에 대해 l_iσ ≡ r_iσ이면 단일화 문제 E의 해이다. 이러한 치환은 E의 단일자(unifier)라고도 불린다. 예를 들어, ⊕가 결합적인 경우, 단일화 문제 { x ⊕ a ≐ a ⊕ x }는 {x ↦ a}, {x ↦ a ⊕ a}, {x ↦ a ⊕ a ⊕ a} 등의 해를 가지며, 문제 { x ⊕ a ≐ a }는 해가 없다.

주어진 단일화 문제 E에 대해, 단일자의 집합 S는 각 해 치환이 S의 일부 치환에 의해 포괄되는 경우 완전하다고 불린다. 완전한 치환 집합은 항상 존재하지만(예: 모든 해의 집합), 일부 프레임워크(예: 제한되지 않은 고차 단일화)에서는 해의 존재 여부(즉, 완전한 치환 집합이 비어 있지 않은지)를 결정하는 문제가 결정 불가능하다.

집합 S는 그 구성원 중 어떤 것도 다른 구성원을 포괄하지 않는 경우 최소(minimal)라고 불린다. 프레임워크에 따라 완전하고 최소인 치환 집합은 0개, 1개, 유한개, 또는 무한개의 구성원을 가질 수 있으며, 무한히 중복되는 구성원의 사슬 때문에 전혀 존재하지 않을 수도 있다. 따라서 일반적으로 단일화 알고리즘은 완전한 집합의 유한 근사치를 계산하며, 이는 최소일 수도 있고 아닐 수도 있지만, 대부분의 알고리즘은 가능한 경우 중복된 단일자를 피한다. 1차 구문 단일화의 경우, 마르텔리(Martelli)와 몬타나리(Montanari)는 해결 불가능성을 보고하거나 그 자체가 완전하고 최소인 치환 집합을 형성하는 단일자, 즉 가장 일반적인 단일자(most general unifier)를 계산하는 알고리즘을 제시했다.

1차 항의 구문 단일화

1차 항 t₁과 t₂를 치환 σ에 의해 구문적으로 단일화하는 삼각형 도표

1차 항의 구문 단일화는 가장 널리 사용되는 단일화 프레임워크이다. 이것은 $T$가 (주어진 변수 집합 $V$, 상수 집합 $C$, $n$항 함수 기호 집합 $F_{n}$에 대한) 1차 항의 집합이고 $\equiv$가 구문적 등호인 것에 기반을 둔다. 이 프레임워크에서 해결 가능한 각 단일화 문제 l₁ ≐ r₁, ..., l_n ≐ r_n}는 완전하고 분명히 최소인 한원소 해집합 σ}을 갖는다. 그 구성원 σ는 문제의 가장 일반적인 단일자(mgu)라고 불린다. 각 잠재적 방정식의 좌변과 우변의 항은 mgu가 적용될 때 구문적으로 동일하게 된다. 즉 l₁σ = r₁σ ∧ ... ∧ l_nσ = r_nσ이다. 문제의 어떤 단일자도 mgu σ에 의해 포괄된다. mgu는 변형(variants)에 따라 고유하다. 만약 S₁과 S₂가 동일한 구문적 단일화 문제의 완전하고 최소인 해집합이라면, S₁ = { σ₁ }이고 S₂ = { σ₂ }이다 (일부 치환 σ₁ 및 σ₂에 대해). 그리고 xσ₁는 문제에 나타나는 각 변수 x에 대해 xσ₂의 변형이다.

예를 들어, 단일화 문제 { x ≐ z, y ≐ f(x) }는 단일자 { x ↦ z, y ↦ f(z) }를 갖는다. 왜냐하면

x	{ x ↦ z, y ↦ f(z) }	=	z	=	z	{ x ↦ z, y ↦ f(z) }	, 그리고
y	{ x ↦ z, y ↦ f(z) }	=	f(z)	=	f(x)	{ x ↦ z, y ↦ f(z) }	.

이것은 또한 가장 일반적인 단일자이다. 동일한 문제에 대한 다른 단일자는 예를 들어 { x ↦ f(x₁), y ↦ f(f(x₁)), z ↦ f(x₁) }, { x ↦ f(f(x₁)), y ↦ f(f(f(x₁))), z ↦ f(f(x₁)) } 등이며, 무한히 많은 유사한 단일자가 있다.

다른 예로, 문제 g(x,x) ≐ f(y)는 ≡가 문자적 동일성일 때 해가 없다. 좌변과 우변에 적용된 어떤 치환도 각각 가장 바깥의 g와 f를 유지할 것이며, 가장 바깥의 함수 기호가 다른 항은 구문적으로 다르기 때문이다.

단일화 알고리즘

로빈슨의 1965년 단일화 알고리즘

기호는 변수가 함수 기호보다 선행하도록 정렬된다. 항은 작성된 길이 증가 순으로 정렬되며, 길이가 같은 항은 사전식으로 정렬된다. 항 집합 T에 대해, 그 불일치 경로 p는 T의 두 구성원 항이 다른 사전식으로 가장 작은 경로이다. 그 불일치 집합은 p에서 시작하는 부분항의 집합이다. 형식적으로: { t|_p : t ∈ T }.

알고리즘:

주어진 항 집합 T를 단일화
σ를 초기에 항등 치환으로 설정
무한 루프
    만약 Tσ가 한원소 집합이면
        σ 반환
    끝
    D를 Tσ의 불일치 집합으로 설정
    s, t를 D에서 사전식으로 가장 작은 두 항으로 설정
    만약 s가 변수가 아니거나 s가 t에 나타나면
        "NONUNIFIABLE" 반환
    끝
     $\sigma :=\sigma \{s\mapsto t\}$
종료

자크 에르브랑은 1930년에 단일화의 기본 개념을 논하고 알고리즘을 스케치했다. 그러나 대부분의 저자들은 최초의 단일화 알고리즘을 존 앨런 로빈슨에게 귀속시킨다 (상자 참조). 로빈슨의 알고리즘은 시간과 공간 모두에서 최악의 경우 지수적 성능을 보였다. 수많은 저자들이 더 효율적인 단일화 알고리즘을 제안했다. 최악의 경우 선형 시간 성능을 가진 알고리즘은 Martelli & Montanari (1976)와 Paterson & Wegman (1976)에 의해 독립적으로 발견되었다. Baader & Snyder (2001)는 패터슨-웨그먼과 유사한 기술을 사용하므로 선형이다. 그러나 대부분의 선형 시간 단일화 알고리즘과 마찬가지로 입력 전처리 및 DAG 표현 구성과 같은 출력 후처리 오버헤드 때문에 작은 크기의 입력에서는 로빈슨 버전보다 느리다. de Champeaux (2022) 또한 입력 크기에 대해 선형 복잡도를 갖지만 작은 크기의 입력에서는 로빈슨 알고리즘과 경쟁한다. 속도 향상은 술어 계산의 객체 지향 표현을 사용하여 전처리 및 후처리 필요성을 피하고 대신 변수 객체가 치환을 생성하고 별칭을 처리하는 역할을 하도록 함으로써 얻어진다. 드 샴포는 프로그래밍적 객체로 표현된 술어 계산에 기능을 추가할 수 있는 능력이 다른 논리 연산도 최적화할 기회를 제공한다고 주장한다.

다음 알고리즘은 일반적으로 제시되며 Martelli & Montanari (1982)에서 유래한다. 유한 집합 $G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}$의 잠재적 방정식이 주어지면, 이 알고리즘은 규칙을 적용하여 다음 형식의 동등한 방정식 집합으로 변환한다. { x₁ ≐ u₁, ..., x_m ≐ u_m } 여기서 x₁, ..., x_m은 서로 다른 변수이고 u₁, ..., u_m은 x_i를 포함하지 않는 항이다. 이 형식의 집합은 치환으로 읽을 수 있다. 만약 해가 없으면 알고리즘은 ⊥로 종료한다. 다른 저자들은 그 경우 "Ω" 또는 "fail"을 사용한다. 문제 G에서 변수 x의 모든 발생을 항 t로 치환하는 연산은 G {x ↦ t}로 표기된다. 간단하게 하기 위해 상수 기호는 0개의 인수를 갖는 함수 기호로 간주된다.

$G\cup \{t\doteq t\}$	$\Rightarrow$	$G$			delete
$G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k})\}$	$\Rightarrow$	$G\cup \{s_{0}\doteq t_{0},...,s_{k}\doteq t_{k}\}$			decompose
$G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0},...,t_{m})\}$	$\Rightarrow$	$\bot$	if $f\neq g$ or $k\neq m$		conflict
$G\cup \{f(s_{0},...,s_{k})\doteq x\}$	$\Rightarrow$	$G\cup \{x\doteq f(s_{0},...,s_{k})\}$			swap
$G\cup \{x\doteq t\}$	$\Rightarrow$	$G\{x\mapsto t\}\cup \{x\doteq t\}$	if $x\not \in {\text{vars}}(t)$ and $x\in {\text{vars}}(G)$		eliminate
$G\cup \{x\doteq f(s_{0},...,s_{k})\}$	$\Rightarrow$	$\bot$	if $x\in {\text{vars}}(f(s_{0},...,s_{k}))$		check

발생 확인(Occurs check)

 이 부분의 본문은 발생 확인입니다.

변수 x를 x를 엄밀한 부분항으로 포함하는 항 x ≐ f(..., x, ...)와 단일화하려고 시도하면 x에 대한 해로 무한 항이 생성된다. x가 자기 자신의 부분항으로 나타나기 때문이다. 위에서 정의한 (유한) 1차 항 집합에서는 방정식 x ≐ f(..., x, ...)는 해가 없다. 따라서 eliminate 규칙은 x ∉ vars(t)인 경우에만 적용될 수 있다. 이 추가적인 확인(occur check라고 불림)이 알고리즘 속도를 늦추기 때문에, 예를 들어 대부분의 프롤로그 시스템에서는 생략된다. 이론적 관점에서, 이 확인을 생략하는 것은 무한 트리(tree)에 대한 방정식을 푸는 것과 같다. 아래의 #무한 항의 단일화를 참조하라.

종료 증명

알고리즘의 종료를 증명하기 위해 세 개의 튜플 $\langle n_{var},n_{lhs},n_{eqn}\rangle$을 고려한다. 여기서 n_var는 방정식 집합에 두 번 이상 나타나는 변수의 수이고, n_lhs는 잠재적 방정식의 좌변에 있는 함수 기호와 상수의 수이며, n_eqn는 방정식의 수이다. eliminate 규칙이 적용될 때, x가 G에서 제거되고 { x ≐ t }에만 유지되므로 n_var는 감소한다. 다른 어떤 규칙을 적용해도 n_var는 다시 증가할 수 없다. decompose, conflict 또는 swap 규칙이 적용될 때, 적어도 좌변의 가장 바깥쪽 f가 사라지므로 n_lhs는 감소한다. 나머지 delete 또는 check 규칙 중 어느 것도 n_lhs를 증가시키지 않지만, n_eqn을 감소시킨다. 따라서 어떤 규칙 적용도 사전식 순서에 대해 튜플 $\langle n_{var},n_{lhs},n_{eqn}\rangle$을 감소시키며, 이는 유한한 횟수만큼만 가능하다.

코너 맥브라이드는 "단일화가 활용하는 구조를 의존형 언어 (예: 에피그램)로 표현함으로써, 로빈슨의 단일화 알고리즘은 변수의 수에 대한 재귀로 만들 수 있으며, 이 경우 별도의 종료 증명이 불필요해진다"고 언급한다.

1차 항의 구문 단일화 예시

프롤로그 구문 규칙에서는 대문자로 시작하는 기호는 변수 이름이고, 소문자로 시작하는 기호는 함수 기호이며, 쉼표는 논리적 AND 연산자로 사용된다. 수학적 표기법에서는 x,y,z를 변수로, f,g를 함수 기호로, a,b를 상수로 사용한다.

프롤로그 표기법	수학적 표기법	단일화 치환	설명
a = a	{ a = a }	{}	성공. (항진식)
a = b	{ a = b }	⊥	a와 b가 일치하지 않음
X = X	{ x = x }	{}	성공. (항진식)
a = X	{ a = x }	{ x ↦ a }	x는 상수 a와 단일화됨
X = Y	{ x = y }	{ x ↦ y }	x와 y는 별칭(alias)됨
f(a,X) = f(a,b)	{ f(a,x) = f(a,b) }	{ x ↦ b }	함수 및 상수 기호 일치, x는 상수 b와 단일화됨
f(a) = g(a)	{ f(a) = g(a) }	⊥	f와 g가 일치하지 않음
f(X) = f(Y)	{ f(x) = f(y) }	{ x ↦ y }	x와 y는 별칭(alias)됨
f(X) = g(Y)	{ f(x) = g(y) }	⊥	f와 g가 일치하지 않음
f(X) = f(Y,Z)	{ f(x) = f(y,z) }	⊥	실패. f 함수 기호의 인자 수가 다름 (arity)
f(g(X)) = f(Y)	{ f(g(x)) = f(y) }	{ y ↦ g(x) }	y를 항 $g(x)$와 단일화
f(g(X),X) = f(Y,a)	{ f(g(x),x) = f(y,a) }	{ x ↦ a, y ↦ g(a) }	x를 상수 a와, y를 항 $g(a)$와 단일화
X = f(X)	{ x = f(x) }	⊥이어야 함	1차 논리와 많은 현대 프롤로그 방언에서는 ⊥를 반환함(발생 확인에 의해 강제됨). 전통적인 프롤로그와 프롤로그 II에서는 성공하며, x를 무한 항 x=f(f(f(f(...))))와 단일화함.
X = Y, Y = a	{ x = y, y = a }	{ x ↦ a, y ↦ a }	x와 y 모두 상수 a와 단일화됨
a = Y, X = Y	{ a = y, x = y }	{ x ↦ a, y ↦ a }	위와 동일 (집합 내 방정식 순서는 중요하지 않음)
X = a, b = X	{ x = a, b = x }	⊥	실패. a와 b가 일치하지 않으므로 x는 둘 다와 단일화될 수 없음

가장 작은 공통 인스턴스에 대해 지수적으로 더 큰 트리를 가진 두 항. 그 dag 표현 (가장 오른쪽, 주황색 부분)은 여전히 선형 크기이다.

크기 n인 구문적 1차 단일화 문제의 가장 일반적인 단일자는 2ⁿ의 크기를 가질 수 있다. 예를 들어, 문제 $(((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))$는 그림과 같이 가장 일반적인 단일자 $\{z\mapsto a,y\mapsto a*a,x\mapsto (a*a)*(a*a),w\mapsto ((a*a)*(a*a))*((a*a)*(a*a))\}$를 갖는다. 이러한 폭발로 인한 지수 시간 복잡도를 피하기 위해 고급 단일화 알고리즘은 트리 대신 유향 비순환 그래프(dag)를 사용한다.

응용: 논리형 프로그래밍에서의 단일화

단일화 개념은 논리형 프로그래밍의 주요 아이디어 중 하나이다. 특히, 단일화는 공식 만족도를 결정하기 위한 추론 규칙인 분해의 기본 구성 요소이다. 프롤로그에서 등호 =는 1차 구문 단일화를 의미한다. 이는 변수 내용 바인딩 메커니즘을 나타내며 일종의 일회성 할당으로 볼 수 있다.

프롤로그에서:

1. 변수는 상수, 항 또는 다른 변수와 단일화될 수 있으며, 사실상 해당 변수의 별칭이 된다. 많은 현대 프롤로그 방언과 1차 논리에서 변수는 자신을 포함하는 항과 단일화될 수 없다. 이를 소위 발생 확인이라고 한다.
2. 두 상수는 동일한 경우에만 단일화될 수 있다.
3. 유사하게, 한 항은 최상위 함수 기호와 항의 인자 개수가 동일하고 매개변수가 동시에 단일화될 수 있는 경우에만 다른 항과 단일화될 수 있다. 이는 재귀적 동작이라는 점에 유의하라.
4. +, -, *, /를 포함한 대부분의 연산은 =에 의해 평가되지 않는다. 예를 들어 1+2 = 3은 구문적으로 다르기 때문에 만족할 수 없다. 정수 산술 제약 조건 #=의 사용은 이러한 연산이 해석되고 평가되는 E-단일화 형식을 도입한다.

응용: 자료형 추론

자료형 추론 알고리즘은 일반적으로 단일화에 기반을 두며, 특히 함수형 언어인 하스켈과 ML에서 사용되는 힌들리-밀너 자료형 추론이 그러하다. 예를 들어, 하스켈 식 True : ['x']의 자료형을 추론하려고 할 때, 컴파일러는 리스트 구성 함수 (:)의 자료형 a -> [a] -> [a], 첫 번째 인자 True의 자료형 Bool, 두 번째 인자 ['x']의 자료형 [Char]를 사용한다. 다형 자료형 변수 a는 Bool과 단일화될 것이고 두 번째 인자 [a]는 [Char]와 단일화될 것이다. a는 동시에 Bool과 Char일 수 없으므로, 이 식은 올바른 자료형이 아니다.

프롤로그와 마찬가지로 자료형 추론을 위한 알고리즘은 다음과 같이 주어진다.

1. 모든 자료형 변수는 모든 자료형 표현식과 단일화되며, 해당 표현식으로 인스턴스화된다. 특정 이론은 발생 확인을 통해 이 규칙을 제한할 수 있다.
2. 두 자료형 상수는 동일한 자료형인 경우에만 단일화된다.
3. 두 자료형 구성은 동일한 자료형 생성자의 응용이고 모든 구성 요소 자료형이 재귀적으로 단일화되는 경우에만 단일화된다.

응용: 특징 구조 단일화

 특징 구조 문서를 참고하십시오.

단일화는 계산 언어학의 여러 연구 분야에서 사용되었다.

순서정렬 단일화

순서정렬 논리는 각 항에 정렬(sort) 또는 자료형(type)을 할당하고, 정렬 s₁을 다른 정렬 s₂의 하위 정렬로 선언하는 것을 허용하며, 일반적으로 s₁ ⊆ s₂로 작성된다. 예를 들어, 생물에 대해 추론할 때 dog 정렬을 animal 정렬의 하위 정렬로 선언하는 것이 유용하다. 특정 정렬 s의 항이 필요한 곳에는 s의 모든 하위 정렬의 항이 대신 제공될 수 있다. 예를 들어, 함수 선언 mother: animal → animal, 상수 선언 lassie: dog을 가정하면, 항 mother(lassie)는 완벽하게 유효하며 animal 정렬을 갖는다. 개의 어미가 다시 개라는 정보를 제공하기 위해, 다른 선언 mother: dog → dog이 발행될 수 있다. 이는 프로그래밍 언어의 오버로딩과 유사한 함수 오버로딩이라고 불린다.

크리스토프 발터는 순서정렬 논리에서 항에 대한 단일화 알고리즘을 제시했는데, 임의의 두 선언된 정렬 s₁, s₂에 대해 그들의 교집합 s₁ ∩ s₂도 선언되어야 한다고 요구했다. 즉, x₁과 x₂가 각각 정렬 s₁과 s₂의 변수라면, 방정식 x₁ ≐ x₂는 { x₁ = x, x₂ = x }라는 해를 가지며, 여기서 x: s₁ ∩ s₂이다. 이 알고리즘을 절 기반 자동화된 정리 증명기에 통합한 후, 그는 벤치마크 문제를 순서정렬 논리로 번역하여 그 크기를 한 단계 줄임으로써 해결할 수 있었다. 많은 단항 술어가 정렬로 바뀌었기 때문이다.

스몰카(Smolka)는 매개변수 다형성을 허용하도록 순서정렬 논리를 일반화했다. 그의 프레임워크에서 하위 정렬 선언은 복잡한 자료형 표현식으로 전파된다. 프로그래밍 예시로, 매개변수 정렬 list(X)가 선언될 수 있고(X는 C++ 템플릿과 같은 자료형 매개변수임), 하위 정렬 선언 int ⊆ float로부터 관계 list(int) ⊆ list(float)가 자동으로 추론된다. 이는 정수 리스트가 또한 부동소수점 리스트임을 의미한다.

슈미트-샤우스(Schmidt-Schauß)는 항 선언을 허용하도록 순서정렬 논리를 일반화했다. 예를 들어, 하위 정렬 선언 even ⊆ int와 odd ⊆ int를 가정하면, ∀ i : int. (i + i) : even과 같은 항 선언은 일반적인 오버로딩으로는 표현할 수 없는 정수 덧셈의 속성을 선언할 수 있게 한다.

무한 항의 단일화

무한 트리에 대한 배경:

• B. Courcelle (1983). 《Fundamental Properties of Infinite Trees》. 《Theoret. Comput. Sci.》 25. 95–169쪽. doi:10.1016/0304-3975(83)90059-2. 
• Michael J. Maher (Jul 1988). 〈Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees〉. 《Proc. IEEE 3rd Annual Symp. on Logic in Computer Science, Edinburgh》. 348–357쪽. 
• Joxan Jaffar; Peter J. Stuckey (1986). 《Semantics of Infinite Tree Logic Programming》. 《Theoretical Computer Science》 46. 141–158쪽. doi:10.1016/0304-3975(86)90027-7. 

단일화 알고리즘, 프롤로그 II:

• A. Colmerauer (1982). K.L. Clark; S.-A. Tarnlund (편집). 《Prolog and Infinite Trees》. Academic Press. 
• Alain Colmerauer (1984). 〈Equations and Inequations on Finite and Infinite Trees〉. ICOT (편집). 《Proc. Int. Conf. on Fifth Generation Computer Systems》. 85–99쪽. 

응용:

• Francis Giannesini; Jacques Cohen (1984). 《Parser Generation and Grammar Manipulation using Prolog's Infinite Trees》. 《Journal of Logic Programming》 1. 253–265쪽. doi:10.1016/0743-1066(84)90013-X. 

E-단일화

E-단일화는 주어진 방정식 집합의 해를 찾는 문제이며, 일부 방정식적 배경 지식 E를 고려한다. 후자는 보편 등식 집합으로 주어진다. 특정 E 집합에 대해 방정식 풀이 알고리즘(일명 E-단일화 알고리즘)이 고안되었다. 다른 E 집합에 대해서는 그러한 알고리즘이 존재할 수 없음이 증명되었다.

예를 들어, a와 b가 서로 다른 상수인 경우, 연산자 $*$에 대해 아무것도 알려지지 않은 순수 구문적 단일화에 대해서는 방정식 $x*a\doteq y*b$에 해가 없다. 그러나 $*$가 교환적임이 알려져 있다면, 치환 x ↦ b, y ↦ a}가 위 방정식을 해결한다. 왜냐하면

	$x*a$	x ↦ b, y ↦ a}
=	$b*a$		치환 적용에 의해
=	$a*b$		$*$의 교환성에 의해
=	$y*b$	x ↦ b, y ↦ a}	(역) 치환 적용에 의해

배경 지식 E는 보편 등식 "모든 u, v에 대해 $u*v=v*u$"에 의해 $*$의 교환성을 명시할 수 있다.

특정 배경 지식 집합 E

사용된 명명 규칙

∀ u,v,w:	$u*(v*w)$	=	$(u*v)*w$	A	$*$의 결합성
∀ u,v:	$u*v$	=	$v*u$	C	$*$의 교환성
∀ u,v,w:	$u*(v+w)$	=	$u*v+u*w$	Dl	$*$의 $+$에 대한 좌 분배성
∀ u,v,w:	$(v+w)*u$	=	$v*u+w*u$	Dr	$*$의 $+$에 대한 우 분배성
∀ u:	$u*u$	=	u	I	$*$의 멱등성
∀ u:	$n*u$	=	u	Nl	$*$에 대한 좌 항등원 n
∀ u:	$u*n$	=	u	Nr	$*$에 대한 우 항등원 n

어떤 이론에 대해 단일화 알고리즘이 임의의 입력 문제에 대해 종료하는 경우, 그 이론에 대해 단일화가 결정 가능하다고 말한다. 어떤 이론에 대해 단일화 알고리즘이 모든 해결 가능한 입력 문제에 대해 종료하지만, 해결 불가능한 입력 문제에 대해서는 영원히 해를 찾을 수 있는 경우, 그 이론에 대해 단일화가 반결정 가능하다고 말한다.

단일화는 다음 이론에 대해 결정 가능하다.

• A
• A,C
• A,C,I
• A,C,N_l
• A,I
• A,N_l,N_r (모노이드)
• C
• 불 대수 환
• 아벨 군, 심지어 서명이 임의의 추가 기호(그러나 공리는 아님)로 확장되어도
• K4 모달 대수

단일화는 다음 이론에 대해 반결정 가능하다.

• A,D_l,D_r
• A,C,D_l
• 가환환

단측 매개 변수화

E에 대한 수렴항 재작성 시스템 R을 사용할 수 있는 경우, 단측 매개 변수화 알고리즘 을 사용하여 주어진 방정식의 모든 해를 열거할 수 있다.

단측 매개 변수화 규칙

G ∪ { f(s1,...,sn) ≐ f(t1,...,tn) }	; S	⇒	G ∪ { s1 ≐ t1, ..., sn ≐ tn }	; S		decompose
G ∪ { x ≐ t }	; S	⇒	G { x ↦ t }	; S{x↦t} ∪ {x↦t}	만약 변수 x가 t에 나타나지 않는다면	eliminate
G ∪ { f(s1,...,sn) ≐ t }	; S	⇒	G ∪ { s1 ≐ u1, ..., sn ≐ un, r ≐ t }	; S	만약 f(u1,...,un) → r이 R의 규칙이라면	mutate
G ∪ { f(s1,...,sn) ≐ y }	; S	⇒	G ∪ { s1 ≐ y1, ..., sn ≐ yn, y ≐ f(y1,...,yn) }	; S	만약 y1,...,yn이 새로운 변수라면	imitate

G를 풀려는 단일화 문제로, S를 항등 치환으로 시작하여, G가 빈 집합이 될 때까지 규칙을 비결정적으로 적용한다. 이 경우 현재의 S가 단일화 치환이 된다. 매개 변수화 규칙이 적용되는 순서, G에서 실제 방정식을 선택하는 방법, mutate에서 R의 규칙을 선택하는 방법에 따라 다른 계산 경로가 가능하다. 일부만 해로 이어지고, 다른 일부는 더 이상 규칙을 적용할 수 없는 G ≠ {}에서 끝난다 (예: G = { f(...) ≐ g(...) }).

예시 항 재작성 시스템 R

1	app(nil,z)	→ z
2	app(x.y,z)	→ x.app(y,z)

예를 들어, cons와 nil로 구성된 리스트의 append 연산자를 정의하는 항 재작성 시스템 R이 사용된다. 여기서 cons(x,y)는 간결하게 x.y로 중위 표기된다. 예를 들어, app(a.b.nil,c.d.nil) → a.app(b.nil,c.d.nil) → a.b.app(nil,c.d.nil) → a.b.c.d.nil은 재작성 규칙 2,2,1을 사용하여 리스트 a.b.nil과 c.d.nil의 연결을 보여준다. R에 해당하는 방정식 이론 E는 용어에 대한 이진 관계로 본 R의 합동 폐포이다. 예를 들어, app(a.b.nil,c.d.nil) ≡ a.b.c.d.nil ≡ app(a.b.c.d.nil,nil). 매개 변수화 알고리즘은 예시 R이 주어졌을 때 해당 E에 대한 방정식의 해를 열거한다.

단일화 문제 { app(x,app(y,x)) ≐ a.a.nil }에 대한 성공적인 예시 계산 경로는 아래와 같다. 변수 이름 충돌을 피하기 위해, 재작성 규칙은 mutate 규칙을 사용하기 전에 매번 일관되게 이름을 변경한다. v₂, v₃, ...는 이 목적을 위해 컴퓨터 생성된 변수 이름이다. 각 줄에서 G에서 선택된 방정식은 빨간색으로 강조 표시된다. mutate 규칙이 적용될 때마다 선택된 재작성 규칙(1 또는 2)이 괄호 안에 표시된다. 마지막 줄에서 단일화 치환 S = { y ↦ nil, x ↦ a.nil }을 얻을 수 있다. 사실, app(x,app(y,x)) {y↦nil, x↦ a.nil } = app(a.nil,app(nil,a.nil)) ≡ app(a.nil,a.nil) ≡ a.app(nil,a.nil) ≡ a.a.nil은 주어진 문제를 해결한다. "mutate(1), mutate(2), mutate(2), mutate(1)"을 선택하여 얻을 수 있는 두 번째 성공적인 계산 경로는 치환 S = { y ↦ a.a.nil, x ↦ nil }로 이어진다. 여기서는 보여주지 않는다. 다른 어떤 경로도 성공으로 이어지지 않는다.

단일자 계산 예시

사용된 규칙		G	S
		{ app(x,app(y,x)) ≐ a.a.nil }	{}
mutate(2)	⇒	{ x ≐ v2.v3, app(y,x) ≐ v4, v2.app(v3,v4) ≐ a.a.nil }	{}
decompose	⇒	{ x ≐ v2.v3, app(y,x) ≐ v4, v2 ≐ a, app(v3,v4) ≐ a.nil }	{}
eliminate	⇒	{ app(y,v2.v3) ≐ v4, v2 ≐ a, app(v3,v4) ≐ a.nil }	{ x ↦ v2.v3 }
eliminate	⇒	{ app(y,a.v3) ≐ v4, app(v3,v4) ≐ a.nil }	{ x ↦ a.v3 }
mutate(1)	⇒	{ y ≐ nil, a.v3 ≐ v5, v5 ≐ v4, app(v3,v4) ≐ a.nil }	{ x ↦ a.v3 }
eliminate	⇒	{ y ≐ nil, a.v3 ≐ v4, app(v3,v4) ≐ a.nil }	{ x ↦ a.v3 }
eliminate	⇒	{ a.v3 ≐ v4, app(v3,v4) ≐ a.nil }	{ y ↦ nil, x ↦ a.v3 }
mutate(1)	⇒	{ a.v3 ≐ v4, v3 ≐ nil, v4 ≐ v6, v6 ≐ a.nil }	{ y ↦ nil, x ↦ a.v3 }
eliminate	⇒	{ a.v3 ≐ v4, v3 ≐ nil, v4 ≐ a.nil }	{ y ↦ nil, x ↦ a.v3 }
eliminate	⇒	{ a.nil ≐ v4, v4 ≐ a.nil }	{ y ↦ nil, x ↦ a.nil }
eliminate	⇒	{ a.nil ≐ a.nil }	{ y ↦ nil, x ↦ a.nil }
decompose	⇒	{ a ≐ a, nil ≐ nil }	{ y ↦ nil, x ↦ a.nil }
decompose	⇒	{ nil ≐ nil }	{ y ↦ nil, x ↦ a.nil }
decompose	⇒	{}	{ y ↦ nil, x ↦ a.nil }

좁히기(Narrowing)

항 s의 위치 p에서 항 s ↝ t를 좁히는 삼각형 다이어그램. 재작성 규칙 l → r (상단 행)을 사용하여 단일화 치환 σ (하단 행)와 함께.

E에 대한 수렴항 재작성 시스템 R이 있다면, 이전 섹션에 대한 대안적인 접근 방식은 "좁히기(narrowing)" 단계의 연속적인 적용으로 구성된다. 이것은 결국 주어진 방정식의 모든 해를 열거할 것이다. 좁히기 단계(그림 참조)는 다음으로 구성된다.

• 현재 항의 비변수 부분항을 선택하고,
• R의 규칙 중 하나의 좌변과 구문적으로 단일화하고,
• 인스턴스화된 규칙의 우변을 인스턴스화된 항으로 대체한다.

형식적으로, l → r이 R의 재작성 규칙의 이름 변경된 사본이고, 항 s와 공통 변수가 없으며, 부분항 s|_p가 변수가 아니고 mgu σ를 통해 l과 단일화될 수 있다면, s는 항 t = sσ[rσ]_p로 좁혀질 수 있다. 즉, sσ의 항에서 p 위치의 부분항이 rσ로 대체된 항이다. s가 t로 좁혀질 수 있는 상황은 일반적으로 s ↝ t로 표기된다. 직관적으로, 좁히기 단계의 순서 t₁ ↝ t₂ ↝ ... ↝ t_n은 재작성 단계의 순서 t₁ → t₂ → ... → t_n으로 생각할 수 있지만, 사용된 각 규칙이 적용될 수 있도록 초기 항 t₁이 필요에 따라 계속 인스턴스화된다.

위의 예시 매개 변수화 계산은 다음 좁히기 순서에 해당한다 ("↓"은 여기서 인스턴스화를 나타낸다).

app(

x

,app(y,

x

))

↓

↓

x ↦ v2.v3

app(

v2.v3

,app(y,

v2.v3

))

→

v2.app(v3,app(

y

,v2.v3))

↓

y ↦ nil

v2.app(v3,app(

nil

,v2.v3))

→

v2.app(

v3

,v2.

v3

)

↓

↓

v3 ↦ nil

v2.app(

nil

,v2.

nil

)

→

v2.v2.nil

마지막 항인 v₂.v₂.nil은 원래 우변 항 a.a.nil과 구문적으로 단일화될 수 있다.

좁히기 렘마(narrowing lemma)는 항 s의 인스턴스가 수렴 항 재작성 시스템에 의해 항 t로 재작성될 수 있을 때마다, s와 t는 각각 항 s′와 t′로 좁혀지고 재작성될 수 있으며, t′는 일부 치환 τ에 대해 s′ τ = t′를 만족하는 s′의 인스턴스임을 보장한다.

형식적으로: 일부 치환 σ에 대해 sσ →∗ t가 성립할 때마다, s′, t′와 같은 항들이 존재하여 s ↝∗ s′ 및 t →∗ t′이고 일부 치환 τ에 대해 s′ τ = t′가 성립한다.

고차 단일화

힐베르트의 10번째 문제를 2차 단일화 가능성으로 환원한 골드파브의 방식에서, 방정식 $X_{1}*X_{2}=X_{3}$는 함수 변수 $F_{i}$가 $X_{i}$에 해당하고 $G$가 새로운 변수에 해당하며 도표화된 단일화 문제에 대응된다.

많은 응용 분야에서는 1차 항 대신에 타입이 지정된 람다 항의 단일화를 고려해야 한다. 이러한 단일화는 종종 고차 단일화라고 불린다. 고차 단일화는 결정 불가능하며, 이러한 단일화 문제는 가장 일반적인 단일자를 갖지 않는다. 예를 들어, 유일한 변수가 f인 단일화 문제 { f(a,b,a) ≐ d(b,a,c) }는 다음과 같은 해를 갖는다. {f ↦ λx.λy.λz. d(y,x,c) }, {f ↦ λx.λy.λz. d(y,z,c) }, {f ↦ λx.λy.λz. d(y,a,c) }, {f ↦ λx.λy.λz. d(b,x,c) }, {f ↦ λx.λy.λz. d(b,z,c) }, {f ↦ λx.λy.λz. d(b,a,c) }. αβη 변환에 의해 결정되는 등식 모듈로 단순 타입 람다 항을 단일화하는 문제는 고차 단일화의 잘 연구된 분야이다. 제라르 위트는 체계적인 단일자 공간 탐색을 허용하는 반결정 가능한 (전)단일화 알고리즘을 제시했는데(고차 변수를 포함하는 항에 대한 규칙을 통해 마르텔리-몬타나리의 단일화 알고리즘을 일반화함), 이는 실제 적용에서 충분히 잘 작동하는 것으로 보인다. 위트와 질 도벡은 이 주제를 다룬 논문을 작성했다.

고차 단일화의 여러 부분 집합은 잘 동작하며, 이는 결정 가능하고 해결 가능한 문제에 대해 가장 일반적인 단일자를 갖는다는 의미이다. 그러한 부분 집합 중 하나는 이전에 설명된 1차 항이다. 데일 밀러(Dale Miller)가 제시한 고차 패턴 단일화도 그러한 부분 집합이다. 고차 논리형 프로그래밍 언어인 λProlog와 Twelf는 전체 고차 단일화에서 패턴 조각만 구현하는 것으로 전환했다. 놀랍게도 패턴 단일화는 거의 모든 프로그램에 충분하며, 각 비패턴 단일화 문제가 후속 치환이 단일화를 패턴 조각으로 만들 때까지 유보된다면 말이다. 패턴 단일화의 상위 집합인 함수-생성자 단일화도 잘 동작한다. Zipperposition 정리 증명기는 이러한 잘 동작하는 부분 집합을 전체 고차 단일화 알고리즘에 통합하는 알고리즘을 가지고 있다.

계산언어학에서 생략 구조의 가장 영향력 있는 이론 중 하나는 생략이 자유 변수로 표현되며, 그 값은 고차 단일화를 사용하여 결정된다는 것이다. 예를 들어, "존은 메리를 좋아하고 피터도 그렇다"의 의미론적 표현은 like(j, m) ∧ R(p) 이며, R의 값(생략의 의미론적 표현)은 방정식 like(j, m) = R(j) 에 의해 결정된다. 이러한 방정식을 푸는 과정을 고차 단일화라고 한다.

웨인 스나이더는 고차 단일화와 E-단일화의 일반화를 제시했는데, 즉 방정식 이론 모듈로 람다 항을 단일화하는 알고리즘이다.

같이 보기

• 재작성
• 허용 규칙
• 람다 계산에서의 명시적 치환
• 수학적 방정식 풀기
• 불단일화 (컴퓨터 과학): 기호식 사이의 부등식 풀기
• 반단일화 (컴퓨터 과학): 두 항의 최소 일반화(lgg) 계산, 가장 일반적인 인스턴스(mgu) 계산의 이중
• 포괄 격자, 단일화를 만남(meet)으로, 반단일화를 조인(join)으로 갖는 격자
• 온톨로지 정렬 (의미론적 동등성과 단일화 사용)

더 읽어보기

• Franz Baader 및 Wayne Snyder (2001). "Unification Theory". John Alan Robinson 및 Andrei Voronkov, 편집, 자동화된 추론 핸드북, Volume I, 447–533쪽. Elsevier Science Publishers.
• Gilles Dowek (2001). "Higher-order Unification and Matching" 보관됨 2019-05-15 - 웨이백 머신. In Handbook of Automated Reasoning.
• 프란츠 바더 및 Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press.
• 프란츠 바더 및 외르크 H. 지크만 (1993). "Unification Theory". In Handbook of Logic in Artificial Intelligence and Logic Programming.
• 장피에르 주아노 및 Claude Kirchner (1991). "Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification". In Computational Logic: Essays in Honor of Alan Robinson.
• Nachum Dershowitz 및 Jean-Pierre Jouannaud, Rewrite Systems, in: Jan van Leeuwen (ed.), 이론 컴퓨터 과학 핸드북, volume B Formal Models and Semantics, Elsevier, 1990, pp. 243–320
• 외르크 H. 지크만 (1990). "Unification Theory". In Claude Kirchner (editor) Unification. Academic Press.
• Kevin Knight (Mar 1989). 《Unification: A Multidisciplinary Survey》 (PDF). 《ACM Computing Surveys》 21. 93–124쪽. CiteSeerX 10.1.1.64.8967. doi:10.1145/62029.62030. S2CID 14619034. 
• Gérard Huet 및 Derek C. Oppen (1980). "Equations and Rewrite Rules: A Survey". Technical report. Stanford University.
• Raulefs, Peter; Siekmann, Jörg; Szabó, P.; Unvericht, E. (1979). 《A short survey on the state of the art in matching and unification problems》. 《ACM SIGSAM Bulletin》 13. 14–20쪽. doi:10.1145/1089208.1089210. S2CID 17033087. 
• 클로드 키르슈너 및 헬렌 키르슈너. Rewriting, Solving, Proving. 준비 중.