통일(컴퓨터과학)

논리학과 컴퓨터 과학에서 통일은 상징적 표현 사이의 방정식을 푸는 알고리즘적 과정이다.

어떤 표현식(일명 용어)이 방정식 집합(통일 문제라고도 함)에서 일어날 수 있도록 허용되고 어떤 표현이 동등하다고 생각하느냐에 따라 통일의 여러 틀이 구분된다.고차 변수, 즉 함수를 나타내는 변수를 표현으로 허용하면 그 과정을 고차 통일, 그렇지 않으면 1차 통일이라고 한다.각 방정식의 양쪽을 문자 그대로 균등하게 만드는 해법이 요구되면 그 과정을 통사적 또는 자유통일, 그렇지 않으면 의미적 또는 등가적 통일, 또는 E-통일 또는 통일모듈로 이론이라고 한다.

통일 문제의 해결책은 대체, 즉 문제의 표현에 대한 각 변수에 상징적 값을 할당하는 매핑으로 표시된다.통일 알고리즘은 주어진 문제에 대한 완전하고 최소한의 대체 집합, 즉 그것의 모든 해결책을 포함하며 중복 구성원을 포함하지 않는 집합을 계산해야 한다.프레임워크에 따라 완전하고 최소한의 대체 집합은 최대 하나, 최대 미세하게 많거나 무한히 많은 구성원을 가질 수도 있고 아예 존재하지 않을 수도 있다.^{[note 1][1]}어떤 프레임워크에서는 일반적으로 어떤 해결책이 존재하는지 결정하는 것이 불가능하다.1차 구문통일의 경우, 마텔리와 몬타나리는^[2] 불능성을 보고하거나 이른바 가장 일반적인 단일기가 포함된 완전하고 최소의 단일톤 치환 세트를 계산하는 알고리즘을 부여했다.

예를 들어 x,y,z를 변수로 사용하는 싱글톤 방정식 집합 { cons(x,cons(x,nil)) = cons(2,y)}은 대체 {x y 2, y cons cons(2,nil)}을 유일한 해법으로 하는 통사적 1차 통일 문제다.통사적 1차 통일 문제 {y = cons(2,y)}은 유한한 용어의 집합에 대해서는 해결책이 없지만, 무한 나무 집합에 대해서는 단일 솔루션 { y ↦ cons(2,cons(2,...) }이 있다.의미론적 1차 통일 문제 { a⋅x = x⋅a }은(는) 형식 { x ... a⋅...을 각각 대체한다.sema }은(는) 세미그룹에서 해결책으로서, 즉 (ㄴ) 연관성이 있는 것으로 간주되는 경우, (ㄴ) 아벨 그룹에서도 볼 수 있는 동일한 문제는 (ㄴ) 역교합성이 있는 것으로 간주되는, 해결책으로서 어떠한 대체도 가지고 있다.싱글톤 집합 { a = y(x) }은 함수 변수인 만큼 통사 2차 통일 문제다.한 솔루션은 { x ↦ a, y ↦ (identity 함수) }이고, 다른 솔루션은 { y ↦ (각 값을 a에 매핑하는 고정 함수), x ↦ (임의 값) }이다.

는 첫번째 공식적인 조사 존 앨런 Robinson,[6][7]로 그것을 제거하는 일차 논리의 자동화된 추론 기술에 커다란 일보 전진해서 그의 해결 절차에 대한 기본적인 건축 블록으로, 일차 언어의 구문을 통일 사용에 기인할 수 있는 통일 알고리즘 먼저 자크 Herbrand,[3][4][5]에 의해 발견되었다.d가 한 근원조합 폭발: 용어의 인스턴스화 검색.오늘날에도 자동화된 추리는 여전히 통일의 주요 적용 분야다.구문 1차 통일은 로직 프로그래밍과 프로그래밍 언어 유형 시스템 구현, 특히 힌들리-밀너 기반 유형 추론 알고리즘에 사용된다.의미론적 통일은 시만텍 해결사, 용어 재쓰기 알고리즘, 암호 프로토콜 분석 등에 사용된다.고차 통일은 ISabelle과 Twel과 같은 교정 보조자에게 사용되며, 제한된 형태의 고차 통일(고차 패턴 통일)은 고차 패턴이 표현되어 있지만, 관련 통일 절차는 이론성을 유지하고 있기 때문에 람다프로로그와 같은 일부 프로그래밍 언어 구현에 사용된다.1차 통일과 가까운 부동산.

일반적인 형식 정의

전제조건

형식적으로는 통일 접근법이 전제된다.

• 변수의 $무한{\displaystyle }$ 세트 V ${\displaystyle$ V$}.$고차 통일의 경우 람다-항 경계 변수 집합에서 $V{\displaystyle }$ ${\displaystyle V}$의 분리를 선택하는 것이 편리하다.
• $V{\displaystyle }$ ${\displaystyle \subseteq }$ ${\displaystyle T}$ ${\displaystyle V\subseteq T}$과 같은 용어의 T ${\displaystyle$ T$}$ 집합$.$ 1차 단일화의 경우 $T{\displaystyle }$ ${\displaystytle T}$은 보통 1차 항(변수와 함수 기호로 작성된 용어) 집합이다$$.고차 통일의 경우 $T{\displaystyle }$ ${\displaystyle T}$은(는) 1차 항과 람다 항(일부 고차 변수를 포함하는 항)으로 구성된다$$.
• 매핑 변수:${\displaystyle T\rightarrow }$ ${\displaystyle \mathbb {P} }$${\displaystyle (V)}$, assigning to each term ${\displaystyle t}$ the set ${\displaystyle {\text{vars}}(t)\subsetneq V}$ of free variables occurring in ${\displaystyle t}$.
• $T{\displaystyle }$ ${\displaystyle T}$의 동등성 관계 $\equiv {\displaystyle }$ ${\displaystyle \equiv$ $\},$ 어떤 항이 동등하다고 간주되는지 표시.1차 E-unity의 경우,${\displaystyle }${$${\$displaystyle$\$equiv$ $}$은(는) 특정 기능 기호에 대한 배경 지식을$$ 반영한다. 예를 들어, ${\displaystyle \{}$ ${\$$displaystyle$$u}$이(가) t$$${\displaystytle$$u$$}$의 인수를 스와핑하여$$ $결과$인 경우 t {\$displaystyt$}${\displaystyle }$일부 발생 시$$\$displaystyle$ $\oplus }$^{[note 2]} 가장 일반적인 경우에서 배경 지식이 전혀 없는 경우, 문자 그대로 또는 구문론적으로만 동일한 용어가 동등하다고 간주된다.이 경우 ≡은 자유이론(자유이론), 빈이론(동일문장의 집합, 또는 배경지식이 비어있기 때문에), 해석되지 않은 함수론(통일이 해석되지 않은 용어로 이루어지기 때문에), 또는 생성자의 이론(모든 함수 기호는 단지 데이터 용어를 쌓기 때문에,(이들 위에서 작동하기 보다는)고차 통일의 경우 $일반적$으로 t$${\$displaystyle t$}과 u$${\$displaystyle u}$이(가) 알파 등가인 경우$$ ${\displaystyle t}$ ${\displaystyle \equiv }$u {\$displaystytle t\equiv u}$을(를) 사용한다.

1차 용어

변수 기호의 $V$ ${\displaystyle V}$ 세트, 상수 $기호$의 C ${\displaystyle C}$ 세트, 연산자 기호라고도 하는 ${\displaystyle {n-ary}_{}}$ 함수 기호의 $F$ ${\$ $F_$${n}$ 설정, 각 자연 숫자 $n{\displaystyle 1}$ 1$$${\displaystyle$ n\$geq$ 1$},$ $T$의 집합.다음 속성을 가진 최소 집합으로 재귀적으로 정의된다.^[8]

• 모든 변수 기호는 용어: $V{\displaystyle }$⊆ ${\displaystyle T}$ ${\displaystyle V\subseteq$ T$\},$
• 모든 상수 기호는 $용어{\displaystyle }$: C ${\displaystyle \subseteq }$ ${\displaystyle T}$ ${\displaystyle C\subseteq$ T$\},$
• 모든 n 용어 $t{\displaystyle {}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$, .${\displaystyle }$. ${\displaystyle {}_{}}$ ${\displaystyle n_{}}$ ${\$$t_{n}}$과$($와) 모든 n-ary ${\displaystyle {함수}_{}}$ 기호 $f{\displaystyle }$ ${\displaystyle \in }$ ${\displaystyle {}_{}}$n {\$displaystyle$ f$\in$F_$\{$$n}},$ 더 큰 용어 $f{\displaystyle ({}_{}}$ ${\displaystyle {1\mathrm{}}_{}}$,${\displaystyle }$.${\displaystyle }$. ${\displaystyle {}_{}}$ $){\displaystyle f(t_{$1}, $..., t_{n}})$를 작성할 수 있다.

For example, if ${\displaystyle x\in V}$ is a variable symbol, ${\displaystyle 1\in C}$ is a constant symbol, and ${\displaystyle {\text{add}}\in F_{2}}$ is a binary function symbol, then ${\displaystyle x\in T,1\in T}$, and (hence) ${\displaystyle {\text{add$$}}}(x,1)\각각$ 1기, 2기, 3기 건물 규칙으로$.$후자는 일반적으로 $x{\displaystyle }$+ ${\displaystyle 1}$ {\$displaystyle x+1}$로 표기되는데$,$ infix 표기법과 보다 일반적인 연산자 기호 +를 사용하여 편리하게 표기한다.

고차항

대체

A substitution is a mapping ${\displaystyle \sigma :V\rightarrow T}$ from variables to terms; the notation ${\displaystyle \{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$ refers to a substitution mapping each variable ${\displaystyle x_{i}}$ to the term ${\displaystyle t_i}$${\displaystyle t_{i$ ${\displaystyle \mathrm{i}}$= 1,${\displaystyle }$. .${\displaystyle }$. ${\displaystyle k}${\$displaystyle i=1,...,k$ 및 다른 모든 변수.Applying that substitution to a term ${\displaystyle t}$ is written in postfix notation as ${\displaystyle t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$; it means to (simultaneously) replace every occurrence of each variable ${\displaystyle x_{i}}$ in the term ${\displaystyle t}$${\displaystyle }$${\$$displaystyle$ $t_{i}$ by$$ ${\displaystyle t_{}}$ i {\$displaystyle$ t_$\}.$$t{\displaystyle }$ ${\displaystyle t}$ 용어에 대체$$ $\tau {\displaystyle }$ ${\displaystyle \tau }$을(를) 적용하는 $결과$를 $t$의 인스턴스$($instance)라고 한다$$$(\{\backslash$$displaystyty$ t$}).$ 첫 번째 예로서 대체 {x ↦ h(a,y), z ↦ b}을(를)라는 용어에 적용한다.

	${\displaystyle f()}$	${\displaystyle {\textbf {x}}$	$(\displaystyle ,a,g()$	${\displaystyle {\textbf {z}$	$(\displaystyle )y)}$
수확하다
	${\displaystyle f()}$	${\displaystyle {\textbf {h}({\textbf {a},{\textbf {y})}$	$(\displaystyle ,a,g()$	${\displaystyle {\textbf{b}}$	$(\displaystyle )y).}$

일반화, 전문화

$t{\displaystyle }$ 용어$${\$displaystyle t}$에 $u{\displaystyle }$ ${\displaystyle u$과 동등한 인스턴스가 있는 경우, 즉, t $substitution$${\displaystyle u}$ ${\$$displaystyle \sigma \$$equiv u}$이$($가) 일부 대체 $\sigma {\displaystyle }$ ${\displaystystyle$ u$\}$보다 일반적이라고 하며$$ u}은 ${\\discal$$.$led more special than, or subsumed by, ${\displaystyle t}$. For example, ${\displaystyle x\oplus a}$ is more general than ${\displaystyle a\oplus b}$ if ⊕ is commutative, since then ${\displaystyle (x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b}$.

만약 ≡이 용어의 문자적(합성적) 정체성인 경우, 두 용어가 통사적 구조가 아닌 가변적 이름만 다를 경우에만 용어는 다른 용어보다 더 일반적이고 더 특별할 수 있다. 이러한 용어를 변형 또는 상호 명칭 변경이라고 한다.예를 들어 f${\displaystyle }$( ${\displaystyle {x\mathrm{}}_{}}$ 1,${\displaystyle {}_{}a}$, g (${\displaystyle {z\mathrm{}}_{}}$ ${\displaystyle {}_{}}$)${\displaystyle }$, ${\displaystyle {y\mathrm{}}_{}}$ ${\displaystyle {}_{}}$) ${\displaystyle f(x_{1},a,g(z_{1}),$${\displaystyle {y\_\mathrm{}}_{}}$${1}}$은(는) 이후$$f${\displaystyle ({x\mathrm{}}_{}}$2 , ${\displaystyle a,}$ ${\displaystyle g}$ (${\displaystyle {}_{}}$ ${\displaystyle {2\mathrm{}}_{}}$)${\displaysty f(x_{2}),y_{$2}}}의$변형이다.$

, 그리고

However, ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$ is not a variant of ${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$, since no substitution can transform the latter term into the former one.그러므로 후기는 전기에 비해 적절하게 더 특별하다.

임의의 $\equiv {\displaystyle }$ ${\displaystyle \equiv }$의 경우$,$ 용어는 구조적으로 다른 용어보다 더 일반적이고 더 특별할 수 있다.For example, if ⊕ is idempotent, that is, if always ${\displaystyle x\oplus x\equiv x}$, then the term ${\displaystyle x\oplus y}$ is more general than ${\displaystyle z}$,^{[note 3]} and vice versa,^{[note 4]} although ${\displaystyle x\oplus y}$ and ${\displaystyle z}$ are of different structure.

A substitution ${\displaystyle \sigma }$ is more special than, or subsumed by, a substitution ${\displaystyle \tau }$ if ${\displaystyle t\sigma }$ is more special than ${\displaystyle t\tau }$ for each term ${\displaystyle t}$. We also say that ${\displaystyle \tau }$ is more general than ${\displaystyle \sigma }$${\displaystyle \sigma }$. For instance ${\displaystyle \{x\mapsto a,y\mapsto a\}}$ is more special than ${\displaystyle \tau =\{x\mapsto y\}}$, but ${\displaystyle \sigma =\{x\mapsto a\}}$ is not, as ${\displaystyle f(x,y)\sigma =f(a,y)}$ is not mo${\displaystyle f}$( ${\displaystyle x}$, y${\displaystyle }$) ${\displaystyle \tau }$= ${\displaystyle f}$( ${\displaystyle y}$, y${\displaystyle }$) ${\displaystyle f(x,y)\tau =f(y,y)}$보다 특별함$.$^[9]

통일 문제, 솔루션 세트

통일문제는 전위 방정식의 유한 집합 { l₁ ≐ r₁, ..., l_n ≐ r_n }이다. 여기서 l_ii, r ∈ T. 대체 σ은 $i{\displaystyle }$= ${\displaystyle 1}$,${\displaystyle }$.${\displaystyle }$, ${\displaystyle n}$ ${\displaystyle$i=1, $...n}$에 대한_i l r rσ_i rσ이 그 문제의 해결책이다$.$ 이러한 대체는 통일문제의 통일문제의 통일문제의 통일문제의 통일문안자라고도 한다.예를 들어 ⊕이 연관성이 있는 경우 통일 문제 {x ⊕ a ≐ a },, {x ↦ a ⊕ a}, {x ↦ a ⊕ a }, a} 등의 해결책이 있는 반면, 문제 {x ↦ a ⊕ a },}은 해결책이 없다.

주어진 통일 문제의 경우, 각 해결책 대체가 일부 대체 σ S에 의해 요약되는 경우, 집합 S는 그 구성원 중 어느 누구도 다른 것을 흡수하지 않는 경우 최소라고 불린다.

1차 용어의 통사적 통일

1차 용어의 통사적 통일은 가장 널리 사용되는 통일의 틀이다.그것은 1차 항(일부 주어진 변수 V, 상수의 C, n-ary 함수 기호의 F_n)의 집합인 T와 구문적 동일성에 기초한다.이 프레임워크에서 해결 가능한 각 통일 문제 {l₁ ≐ r₁, ..., l_n ≐ r_n}에는 완전하고 분명히 최소의 싱글톤 솔루션 집합 {σ}이(가) 있다.그 멤버인 σ은 문제의 가장 일반적인 단결자(mgu)로 불린다.각 전위 방정식의 왼쪽과 오른쪽의 항은 mgu를 적용할 때 구문론적으로 동일해진다. 즉, lσ₁ = rσ₁ ∧ ... ∧ l_nσ = r_nσ.문제의 모든 단결자는 mgu σ에 의해^{[note 5]} 요약된다.mgu는 변형에 따라 고유하다: S와₁ S가₂ 모두 동일한 구문 통일 문제의 완전하고 최소 솔루션 집합인 경우, 일부 대체 and과₁₁₂ for에 대해₁ S = { } }과₂ S = { } } }이며₂, xσ은₁ 문제에서 발생하는 각 변수 x에 대한 xσ의₂ 변종이다.

예를 들어 통일 문제 { x ≐ z, y ≐ f(x) }에는 통일 문제 { x ↦ z, y ↦ f(z)}이(가) 있기 때문에 unifier { 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 f(x₁), y f f(x₁), z f f(x₁) }, { x f f(f(x₁)), y f f(f(x₁)), z f f(f(x₁) } 등이 있으며, 이와 유사한 고유어가 무한히 많다.

또 다른 예로, problem f(y) literal f(y)는 ≡이 문자 그대로의 정체성과 관련하여 해답이 없다. 왜냐하면 좌우에 적용되는 대체는 각각 가장 바깥쪽 g와 f를 유지하며, 가장 바깥쪽 함수 기호가 다른 항은 구문론적으로 다르기 때문이다.

통일 알고리즘

로빈슨(1965)이 준 첫 번째 알고리즘은 다소 비효율적이었다; cf. box.다음의 더 빠른 알고리즘은 마텔리 몬타나리(1982)에서 비롯되었다.^{[note 6]}본 논문에는 효율적인 구문 통일 알고리즘을 찾기 위한 선행 시도도 나열되어 있으며,^{[13][14][15][16][17][18]} 선형 시간 알고리즘은 마르텔리 몬타나리(1976년)^[15]와 패터슨 웨그만(1976년,^[19] 1978년^[16])에 의해 독자적으로 발견되었다고 기술되어 있다.^{[note 7]}

감안할 때들은 한정된),{\displaystyle G=\{s_{1}\doteq t_{1}{s1≐ t1,..., sn≐ tn}G설정...잠재적인 방정식(t_{n}\}}, 알고리즘 형태의 방정식이 x1,..., xm는 별개의 변수와 u1,..., 음 있는 용어들{x1 ≐ u1,...,xm ≐)}의 등가 세트 이렇게 변형에 규칙을 적용합니다. containing x 중_i 어느 것도. 이 형식의 집합은 대체물로 읽을 수 없다.해결책이 없을 경우 알고리즘은 ⊥으로 종료된다. 다른 저자는 이 경우 "Ω", "{}" 또는 "fail"을 사용한다.문제 G에서 발생하는 모든 변수 x를 용어 t로 대체하는 작업은 G {x ↦ t}로 표시된다.단순성을 위해 상수 기호는 인수가 0인 함수 기호로 간주된다.

${\displaystyle G\cup \{t\doteq t\}}$	${\displaystyle \Rightarrow }$	$(\displaystyle G}$		삭제하다
${\displaystyle G\cup \{f(s_{0},...,s_{k})\doteq f(t_{0},...,t_{k}}\}}}}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\cup \{0}\doteq t_{0}}\doteq t_{0}},...,s_{k}\doteq t_{k}\}\}}}}}}$		분해하다
${\displaystyle G\cup \{f(s_{0},\ldots ,s_{k})\doteq g(t_{0}, ...,t_{m}\}}}}}}}$	${\displaystyle \Rightarrow }$	$\displaystyle \bot }$	$f{\displaystyle }$ ${\displaystyle \ne }$ ${\displaystyle g}$ ${\displaystyle f\neq g}$ 또는$$ $k{\displaystyle }$ ${\displaystyle \ne }$ ${\displaystyle m}$ ${\displaystyle k\neq m}$인 경우	갈등을 빚다
${\displaystyle G\cup \{f_{0},...,s_{k}\doteq x\}}$	${\displaystyle \Rightarrow }$	${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k}\}}}}}$		바꾸다
${\displaystyle G\cup \{x\doteq t\}}$	${\displaystyle \Rightarrow }$	$\\displaystyle G\{x\mapsto t\}\cup \{x\doteq t\}}}컵 \{x\doteq t$	$x{\displaystyle }$ ${\displaystyle \notin \text{vars}(t}$) ${\displaystyle x\not \in {\text{vars}(t)$ 및 $x$ ${\displaystyle \in \text{vars}(G}$) ${\displaystyle$ x$\in {\text{vars}(G)$인 경우	없애다[주 8]
${\displaystyle G\cup \{x\doteq f(s_{0},...,s_{k}\}}}}}$	${\displaystyle \Rightarrow }$	$\displaystyle \bot }$	$x{\displaystyle }$ ${\displaystyle \in \text{vars}(f}$(${\displaystyle {}_{}}$ ${\displaystyle {0\mathrm{}}_{}}$.${\displaystyle }$. . . s ${\displaystyle k_{}}$)${\displaystyle x\in {\text{vars}}(f(s_{0},...,s_{k$})})인 경우$}$	수표

발생 확인

x를 포함하는 항을 엄격한 하위항 x f f(..., x, ...)로 하여 변수 x를 통일하려는 시도는 x 자체의 하위항으로서 발생하기 때문에 x에 대한 솔루션으로서 무한의 항으로 이어질 것이다.위에서 정의한 (최종) 1차 항 집합에서 x ≐ f(..., x, ...) 방정식은 해법이 없으므로, 제거 규칙은 x ∉ var(t)일 경우에만 적용될 수 있다.발생 점검이라고 불리는 추가 점검은 알고리즘을 느리게 하기 때문에 대부분의 Prolog 시스템에서 생략된다.이론적인 관점에서, 체크 양을 생략하는 것은 무한 나무에 대한 방정식을 푸는 것과 같다. 아래를 참조하라.

해지증빙

이 알고리즘의 해지의 증명을 위해서 삼중⟨ nv을 고려한 r, n나는 h, neq n⟩{\displaystyle\langle n_{},n_{lhs},n_{유닉스}\rangle}이 nvar은 숫자의 변수 발생하는 한번 이상의 방정식 집합, nlhs은 숫자의 함수 기호와 상수에 왼손 측면들의 잠재적인 equa.결함,그리고_eqn n은 방정식의 수입니다.규칙 제거가 적용되면 n은_var 감소하는데, 이는 x가 G에서 제거되고 { x t t }에만 유지되기 때문이다. 다른 규칙을 적용하면 n이_var 다시 증가하지 않는다.규칙이 분해, 충돌 또는 스왑을 적용할 때 n은_lhs 감소하는데, 적어도 왼쪽의 가장 바깥쪽 f는 사라지기 때문이다.나머지 규칙 중 하나를 삭제하거나 확인하는 것은 n을_lhs 증가시킬 수 없지만 n은_eqn 감소한다.따라서 모든 규칙 애플리케이션은 한정된 횟수만큼만 가능한 사전적 순서와 관련하여$$ 트리플 $⟨{\displaystyle }$ n ${\displaystyle {}_{}}$ ${\displaystyle a_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle l_{}}$ h ${\displaystyle s_{}}$ n ${\displaystyle e_{}}$ ${\displaystyle q_{}}$ ${\displaystyle {}_{}}$ ${\displaystyle \langle n_{var},n_{lhs},n_{eqn}\rangele }$를 감소시킨다.

코너 맥브라이드는 "통일이 악용하는 구조를 에피그램과 같이 의존적으로 입력된 언어로 표현함으로써 로빈슨의 알고리즘은 변수 수에 따라 재귀적으로 만들어질 수 있으며, 이 경우 별도의 종료 증명이 불필요하게 된다"고 관측한다^[20].

1차 용어의 통사적 통일 예제

프롤로그 통념에서 대문자로 시작하는 기호는 변수 이름, 소문자로 시작하는 기호는 함수 기호, 쉼표는 논리 및 연산자로 사용된다.수학 표기법의 경우 x,y,z는 변수로, f,g는 함수 기호로, a,b는 상수로 사용된다.

프롤로그 표기법	수학적 표기법	통합 대체	설명
a = a	{ a = }	{}	성공하다.(자동학)
a = b	{ a = b }	⊥	a와 b가 일치하지 않다
X = X	{ x = x }	{}	성공하다.(자동학)
a = X	{ a = x }	{ x x ↦ a }	x는 상수 a와 통일된다.
X = Y	{ x = y }	{ x ↦ y }	x와 y는 별칭임
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는 별칭임
f(X) = g(Y)	{ f(x) = g(y) }	⊥	f와 g가 일치하지 않음
f(X) = f(Y,Z)	{ f(x) = f(y,z) }	⊥	실패함. f 함수 기호는 서로 다른 아성을 갖는다.
f(g(X)) = f(Y)	{ f(g(x) = f(y) }	{ y ↦ g(x) }	$y$를${\displaystyle g(}$ x$$) {\$displaystyle$ g$(x)}$ 용어와 통합
f(g(X),X) = f(Y,a)	{ f(g(x),x) = f(y,a) }	{ x x a a, y g g(a) }	상수 ${\displaystyle a}$로 x를 통합하고, $g{\displaystyle (}$) ${\displaystyle g(a)}$이라는 용어로 y를 통합한다.
X = f(X)	{ x = f(x) }	⊥여야 한다	1차 로직과 많은 최신 프롤로그 방언(발생 확인에 의해 강제 적용)으로 returns을 반환한다. 기존 프롤로그와 프롤로그 II에서 성공, x를 무한 용어로 통일x=f(f(f(f(...)))).
X = Y, Y = a	{ x = y, y = a }	{ x x ↦ a, y ↦ a }	x와 y는 모두 상수 a로 통일된다.
a = Y, X = Y	{ a = y, x = y }	{ x x ↦ a, y ↦ a }	위와 같이(세트 방정식의 순서는 중요하지 않음)
X = a, b = X	{ x = a, b = x }	⊥	실패. a와 b가 일치하지 않기 때문에 x는 둘 다와 통일될 수 없다.

n 크기의 통사적 1차 통일 문제의 가장 일반적인 단일화는 2의ⁿ 크기를 가질 수 있다.For example, the problem ${\displaystyle (((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))}$ has the most general unifier ${\displaystyle \{z\mapsto a,y\mapsto a*a,x\mapsto (a*a)$$*(a*a),w\mapsto((a*a)*(a*a)*(a*a)*(a*a)*(a*a)*(a*a))$$\}}},$cf. 사진.이러한 블로업으로 인한 기하급수적인 시간 복잡성을 피하기 위해 고급 통일 알고리즘은 나무보다는 지시된 반복 그래프(다그)에 작용한다.^[21]

응용 프로그램: 로직 프로그래밍에서의 통일

통일의 개념은 로직 프로그래밍의 주요 아이디어 중 하나로, 프롤로그 언어를 통해 가장 잘 알려져 있다.변수의 내용을 구속하는 메커니즘을 나타내며 일종의 일회성 할당으로 볼 수 있다.Prolog에서 이 연산은 동일 기호(Equality 기호로 표시됨=, 그러나 변수를 인스턴스화할 때도 수행된다(아래 참조).그것은 또한 평등 기호를 사용함으로써 다른 언어에서도 사용된다.=, 그러나 또한 다음을 포함한 많은 운영과 함께.+,-,*,/. 형식 추론 알고리즘은 일반적으로 단일화에 기반한다.

프롤로그에서:

1. 인스턴스화되지 않은 변수(즉, 이전에 단일화가 수행되지 않은 변수)는 원자, 용어 또는 다른 인스턴스화되지 않은 변수와 통일될 수 있으므로 사실상 그 별칭이 된다.현대의 많은 프롤로그 방언과 1차 논리에서는 변수를 포함하는 용어로 통일할 수 없다. 이것이 소위 발생 점검이다.
2. 두 원자는 동일해야 통일할 수 있다.
3. 마찬가지로 항은 상위 함수 기호와 용어의 아성이 동일하고 매개변수가 동시에 통일될 수 있는 경우 다른 항과 통일될 수 있다.이것은 반복적인 행동이라는 점에 유의한다.

응용 프로그램: 유형 추론

통일은 예를 들어 기능 프로그래밍 언어 하스켈에서 유형 추론 중에 사용된다.한편, 프로그래머는 모든 기능에 대한 형식 정보를 제공할 필요가 없고, 다른 한편으로 그것은 타이핑 오류를 감지하는 데 사용된다.하스켈 표현True : ['x', 'y', 'z']올바르게 입력되지 않음.목록 작성 기능(:)형식이다.a -> [a] -> [a], 그리고 첫 번째 논쟁에 대해서.True다형체형 변수a와 통일되어야 한다.True의 유형,Bool두번째 논쟁은,['x', 'y', 'z']는 유형이다.[Char]그렇지만a둘 다일 수는 없다Bool, 그리고Char동시에

Prolog와 마찬가지로 유형 추론을 위한 알고리즘을 제공할 수 있다.

1. 모든 형식 변수는 모든 형식 표현식과 통합되며 해당 표현식에 인스턴스화된다.특정 이론은 발생 체크로 이 규칙을 제한할 수 있다.
2. 두 유형 상수는 유형이 같은 경우에만 통일된다.
3. 두 가지 유형구조는 동일한 유형구축자의 애플리케이션인 경우에만 통일되고 모든 구성요소 유형은 반복적으로 통일된다.

선언적인 성격 때문에 일련의 통일의 순서는 (보통) 중요하지 않다.

1차 논리학의 용어에서 원자는 기본 명제로서 프롤로그 용어와 유사하게 통일된다는 점에 유의한다.

질서정연한 통일

순서 정렬 논리학에서는 각 용어에 분류 또는 유형을 할당하고₁, 일반적으로₁ s s₂ s로 표기된 다른₂ 종류의 하위 집합을 선언할 수 있다.예를 들어 생물학적 생물에 대해 재도약할 때, 분류된 개를 분류된 동물의 하위집단이라고 선언하는 것이 유용하다.어떤 종류의 용어가 필요한 경우, s의 하위 용어가 대신 제공될 수 있다.예를 들어 함수 선언 어미: 동물 → 동물, 그리고 상수 선언 래시: 개를 가정하면 어미(래시)라는 용어는 완벽하게 유효하며 종류별 동물을 가지고 있다.개 엄마가 개라는 정보를 차례대로 공급하기 위해 개 → 개라는 또 다른 선언적 어미인 개 → 개를 발행할 수 있는데, 이를 프로그래밍 언어의 과부하와 비슷하게 함수 과부하라고 한다.

발터order-sorted 논리에 조건을, 어떤 두개를 선언한 종류 s1을 의무화하는 선고를 받기 교차 s1∩ s2 s2도 바로 종류 s1과 s2의 x1과 미국은 변수, 각각, 방정식 x1 ≐ 미국은 해결책{x1=-1, 미국))}, x:∩ s2 s1 통일 알고리즘을 주었다.한clause-based 자동화로 이 알고리즘을 통합한 후[22].정리 프로베르는 벤치마크 문제를 순서 결정 논리로 번역하여 해결할 수 있었고, 그에 따라 많은 단수 술어들이 분류로 변함에 따라 그 크기를 줄였다.

스몰카는 파라메트릭 다형성을 허용하기 위해 순서 편중 논리를 일반화했다.^[23] 그의 틀에서 하위집단 선언은 복잡한 유형 표현으로 전파된다.프로그래밍 예로서 파라메트릭 정렬 리스트(X)를 선언할 수 있으며(X는 C++ 템플릿에서와 같은 형식 매개변수임), 서브포트 선언 int에서 관계 리스트(int) ⊆ 리스트(float)는 자동으로 유추되며, 이는 각 정수 리스트도 플로트의 리스트라는 것을 의미한다.

슈미트-샤우프는 용어 선언을 허용하기 위해 주문-변형 논리를 일반화했다.^[24] 예를 들어, 하위 항목이 even int 및 odd int int까지 선언한다고 가정하면, ∀ i : int. (i + i) : 일반적인 과부하로 표현할 수 없는 정수 덧셈의 속성까지 선언할 수 있다.

무한한 용어의 통일

이 구간은 확장이 필요하다.덧셈으로 도와줘도 된다(2021년 12월)

무한 나무의 배경:

• B. Courcelle (1983). "Fundamental Properties of Infinite Trees" (PDF). Theoret. Comput. Sci. 25 (2): 95–169. doi:10.1016/0304-3975(83)90059-2. Archived from the original (PDF) on 2014-04-21. Retrieved 2013-06-28.
• 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. pp. 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.

통일 알고리즘, Prolog II:

• A. Colmerauer (1982). K.L. Clark; S.-A. Tarnlund (eds.). Prolog and Infinite Trees. Academic Press.
• Alain Colmerauer (1984). "Equations and Inequations on Finite and Infinite Trees". In ICOT (ed.). Proc. Int. Conf. on Fifth Generation Computer Systems. pp. 85–99.

응용 프로그램:

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

E-통일

E-통일(E-unified)은 어떤 등가적 배경지식 E를 고려하여 주어진 방정식 집합에 대한 해결책을 찾는 문제다.후자는 보편적 평등의 집합으로 주어진다.일부 특정 집합 E에서는 방정식 해결 알고리즘(예: E-통일 알고리즘)이 고안되었고, 다른 집합에서는 그러한 알고리즘이 존재할 수 없다는 것이 증명되었다.

예를 들어 a와 b가 구별되는 상수인 경우, $방정식{\displaystyle }$ x x ${\displaystyle a}$ ${\displaystyle \doteq }$ ${\displaystyle y}$ ${\displaystyle \ast }$ b ${\displaystyle$ x$*a\doteq$ y$*b}$은(는) 연산자에 대해 알려진 것이 없는 순수 통사적 통일과 관련하여 해법이 없다$$$.$ 그러나, 만일 $\ast {\displaystyle }$ ${\displaystyle *}$이 교호작용적인 것으로 알려지면$$ 치환 {x { b, y, y, y,↦ a}은(는) 다음부터 위의 방정식을 해결한다.

	$(\displaystyle x*a}$	{x ↦ b, y ↦ a}
=	$디스플레이 스타일 b*a}$		대체 적용으로
=	$(\displaystyle a*b)$		$\ast {\displaystyle }$ ${\displaystyle *}$의 동시 사용률로
=	$(\displaystyle y*b)$	{x ↦ b, y ↦ a}	대체적용에 의하여.

배경지식 E는 만유평등 " ${\displaystyle v}$v = ${\displaystyle v}$u ${\displaystyle u}$ ${\$$displaystyle$ u$*v=v*u}$에 의한${\displaystyle }${$${\$displaystyle$u}의 공통성을 모든 u, v"에$$ 대해 진술할 수 있다.

특정 배경 지식 집합 E

사용된 명명 규칙

∀ u,v,w:	${\displaystyle u*(v*w)}$	=	${\디스플레이 스타일(u*v)*w}$	A	$\ast {\displaystyle }$ ${\displaystyle *}$의 연관성
∀ u,v:	$(\디스플레이 스타일 uplaystyle u*v)$	=	${\displaystyle v*u}$	C	$\ast {\displaystyle }$ ${\displaystyle *}$의 동일성
∀ u,v,w:	${\displaystyle u*(v+w)}$	=	${\디스플레이 스타일 u*v+u*v+u*w}$	Dl	$+{\displaystyle }$ ${\displaystyle +}$에 대한 $\ast {\displaystyle }$ ${\displaystyle *}$의 왼쪽 분포
∀ u,v,w:	${\displaystyle(v+w)*u}$	=	${\displaystyle v*u+w*u}$	Dr	$+{\displaystyle }$ ${\displaystyle +}$에 대한 $\ast {\displaystyle }$ ${\displaystyle *}$의 올바른 분포
∀ u:	$u*u}$	=	u	I	$\ast {\displaystyle }$ ${\displaystyle *}$의 IDempotence
∀ u:	$디스플레이 스타일 n*u}$	=	u	Nl	$\ast {\displaystyle }$ ${\displaystyle *}$에 대한 좌측 중립 요소 n
∀ u:	$(\displaystyle u*n}$	=	u	Nr	$\ast {\displaystyle }$ ${\displaystyle *}$에 대한 우측 중립 요소 n

어떤 입력 문제에 대해 종결되는 통일 알고리즘이 고안되었다면, 어떤 이론에 대해서도 통일은 결정 가능하다고 한다.어떤 해결 가능한 입력 문제에 대해 종결되는 통일 알고리즘이 고안되었다면, 통일은 이론에 대해 반 결정적으로 가능하지만, 풀 수 없는 입력 문제의 해결책을 계속해서 찾을 수 있을 것이다.

통일은 다음과 같은 이론에 대해 결정 가능하다.

• A^[25]
• A,C^[26]
• A,C,I^[27]
• A,C,N_l^{[note 9][27]}
• A,I^[28]
• A,N_l,N_r(단조형)^[29]
• C^[30]
• 부울 링^[31][32]
• 임의의 추가 기호에 의해 서명이 확장되더라도(^[33]공리는 아님) 아벨 그룹
• K4 모달 알헤브라스^[34]

통일은 다음과 같은 이론에 대해 반결정가능하다.

• A,D_l,D_r^[35]
• A,C,D_l^{[note 9][36]}
• 정류 링^[33]

단측 파라미터

E에 사용할 수 있는 수렴 용어 재쓰기 시스템 R이 있는 경우, 단측 매개변수 알고리즘을^[37] 사용하여 주어진 방정식의 모든 해결책을 열거할 수 있다.

단측 매개변수 규칙

G ∪ {f,s1...sn ≐ f(t1,...,t) } f(t,...,tn) }	; S	⇒	G ∪ { s1 ≐ t1, ..., sn ≐ tn } }	; S		분해하다
G ∪ { x ≐ t }	; S	⇒	G { x ↦ t }	; S{x↦t} ∪ {x↦t}	변수 x가 t에서 발생하지 않는 경우	없애다
G ∪ {f1,...sn ≐ t }	; S	⇒	G ∪ { s1 ≐ u1, ..., sn ≐ un, r ≐ t }	; S	f(u1, ...,un) → r이 R의 규칙이라면	돌연변이를 일으키다
G ∪ {f1,...sn ≐ y }	; S	⇒	G ∪ { s1 ≐ y1, ..., sn ≐ yn, y ≐ f(y1,...,yn) }	; S	만약1 y,...y가n 새로운 변수라면	흉내를 내다

G가 해결해야 할 통일문제, S가 정체성 대체문제인 것을 시작으로 빈 세트가 실제 G로 나타날 때까지 비결정론적으로 규칙이 적용되는데, 이 경우 실제 S는 통일성 대체다.매개 변수 규칙을 적용하는 순서에 따라, G로부터 실제 방정식의 선택, 돌연변이에 있어서의 R의 규칙의 선택에 따라, 다른 계산 경로가 가능하다.일부만 해결책으로 이어지는 반면 다른 일부는 더 이상의 규칙이 적용되지 않는 G ≠ {}에서 종료된다(예: G = { f(...) ≐ g(...) ≐ g(...) }).

예시 용어 재작성 시스템 R

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

For an example, a term rewrite system R is used defining the append operator of lists built from cons and nil; where cons(x,y) is written in infix notation as x.y for brevity; e.g. 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 demonstrates the concatenation of the lists a.b.nil and c.d.nil, employing the rewrite rule 2, 2, 1.R에 해당하는 등가 이론 E는 R의 합치성 폐쇄로, 둘 다 용어로 이항관계로 간주된다.예를 들어, app(a.b.nil, c.d.nil) app(a.b.c.d.nil,nil) app(a.b.c.d.nil,nil) app.매개변수 알고리즘은 예 R을 사용할 때 E에 대한 방정식에 대한 해결책을 열거한다.

통일 문제 {app(x,app(y,x) ≐ a.a.nil }에 대한 성공적인 계산 경로가 아래와 같다.가변 이름 충돌을 피하기 위해 규칙 변경에 의해 사용되기 전에 항상 다시 쓰기 규칙의 이름을 변경한다. v₂, v₃, ...는 이러한 목적을 위해 컴퓨터에서 생성된 변수 이름이다.각 선에서 G에서 선택한 방정식은 빨간색으로 강조 표시된다.돌연변이 규칙을 적용할 때마다 선택한 다시 쓰기 규칙(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) ≡ a.app(nil,a.nil) ≡ a.a.nil이 주어진 문제를 해결한다."mutate(1), mutate(2), mutate(2), mutate(2), mutate(1)"를 선택하여 얻을 수 있는 두 번째 성공적인 계산 경로는 대체 S = { y y a.a.nil, x ↦nil }을(를) 유도하며, 여기에는 표시되지 않는다.다른 길은 성공으로 이어지지 않는다.

유니퍼 계산 예제

사용된 규칙		G	S
		{ app(x,app(y,x)) ≐ a.a.nil }	{}
돌연변이(2)	⇒	{ x ≐ v2.v3, app(y,x) ≐ v4, v2.app(v3,v4) ≐ a.a.nil }	{}
분해하다	⇒	{ x ≐ v2.v3, app(y,x) ≐ v4, v2 ≐ a, app(v3,v4) ≐ a.nil }	{}
없애다	⇒	{ app(y,v2.v3) ≐ v4, v2 ≐ a, app(v3,v4) ≐ a.nil }	{ x ↦ v2.v3 }
없애다	⇒	{ app(y,a.v3) ≐ v4, app(v3,v4) ≐ a.nil }	{ x ↦ a.v3 }
돌연변이(1)	⇒	{ y ≐nil, a.v3 ≐ v5, v5 ≐ v4, app(v3,v4) ≐ a.nil }	{ x ↦ a.v3 }
없애다	⇒	{ y ≐nil, a.v3 ≐ v4, app(v3,v4) ≐ a.nil }	{ x ↦ a.v3 }
없애다	⇒	{ a.v3 ≐ v4, app(v3,v4) ≐ a.nil }	{ y ↦nil, x ↦ a.v3 }
돌연변이(1)	⇒	{ a.v3 ≐ v4, v3 ≐ nil, v4 ≐ v6, v6 ≐ a.nil }	{ y ↦nil, x ↦ a.v3 }
없애다	⇒	{ a.v3 ≐ v4, v3 ≐ nil, v4 ≐ a.nil }	{ y ↦nil, x ↦ a.v3 }
없애다	⇒	{ a.nil ≐ v4, v4 ≐ a.nil }	{ y ↦nil, x ↦ a.nil }
없애다	⇒	{ a.nil ≐ a.nil }	{ y ↦nil, x ↦ a.nil }
분해하다	⇒	{ a ≐ a, nil ≐ nil }	{ y ↦nil, x ↦ a.nil }
분해하다	⇒	{nil ≐ nil }	{ y ↦nil, x ↦ a.nil }
분해하다	⇒	{}	{ y ↦nil, x ↦ a.nil }

좁히기

R이 E를 위한 융합 용어 재작성 시스템인 경우, 이전 절의 접근 대안은 "경사적 단계"의 연속적인 적용으로 구성된다. 이는 결국 주어진 방정식의 모든 해결책을 열거할 것이다.좁은 단계(cf. picture)는

• 당기의 비변수 하위항 선택,
• R에서 규칙의 왼쪽과 구문적으로 통일하고, 그리고
• 즉석 규칙의 오른손을 즉석 용어로 대체한다.

형식적으로 l → r이 R에서 다시쓰기 규칙의 개명본으로, 용어의 s와 공통적으로 변수가 없고, 하위 용어 s가 변수가 아니며 mgu σ을 통해 l와 함께 사용할 수 없는 경우, s는 t = s[[rσ],_p 즉 sσ라는 용어로 좁혀질 수 있으며, s는 rσ으로 대체된 p에서 하위 용어로 좁혀질 수 있다.s가 t로 좁혀질 수 있는 상황은 일반적으로 s ↝ t로 표시된다.직관적으로, 일련의 좁은 단계 t₁ ↝ t₂ ↝ ...↝ t는_n rewrite step 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 ↦ 닐

v2.app(v3,app)

못을 박다

,v2.v3)))

→

v2.app.

v3

,v2.

v3

)

↓

↓

v3 ↦nil.

v2.app.

못을 박다

,v2.

못을 박다

)

→

v2.v2.nil

마지막 용어인 v₂.v₂.nil은 원래 오른쪽 측면 용어인 a.a.nil과 구문적으로 통일될 수 있다.

축소 보조정리법은^[38] 융합적 용어 재작성 시스템에 의해 s라는 용어의 한 인스턴스를 t라는 용어로 다시 쓸 수 있을 때마다 s와 t를 각각 s narrowed와 twritten라는 용어로 좁히고 다시 쓸 수 있도록 보장한다.

형식적: sσ → ∗ t가 어떤 대체 σ에 대해 보유할 때마다 s′, t′, s terms, t′, s′ = t′ 등의 용어가 존재하게 된다.

고차통일

많은 응용 프로그램에서는 1차 용어 대신 람다-단어의 통일성을 고려해야 한다.이런 통일을 흔히 고차적 통일이라고 부른다.고차 통일의 잘 연구된 분과는 단순히 입력된 람다 용어를 αββ 변환에 의해 결정되는 동등성으로 통일하는 문제다.그러한 통일 문제는 대부분의 일반적인 통일 문제를 가지고 있지 않다.반면higher-order 통일 undecidable,[39][40][41]은 제라르 후 에트는 unifiers의(조건을 Martelli-Montanari[2]의 규칙으로 통일 알고리즘을 일반화 고차 변수가 들어 있는)그 충분히 practic에서 일하는 것처럼 보이는 우주의 유기적인 검색할 수 있는semi-decidable(전송)unification algorithm[42]을 주었다.eHuet과^[43] Gilles Dowek은^[44] 이 주제에 관한 기사를 썼다.

데일 밀러는 현재 고차 패턴 통일이라고 불리는 것을 묘사했다.^[45]고차 통일의 이 부분집합은 해독이 가능하며 해결 가능한 통일 문제는 대부분의 일반적인 통일자를 가지고 있다.고차 로직 프로그래밍 언어인 proProlog와 Tweel과 같이 고차 통일을 포함하는 많은 컴퓨터 시스템은 완전 고차 통일은 아닌 패턴 단편만 구현하는 경우가 많다.

계산언어학에서 가장 영향력 있는 줄임표 이론 중 하나는 타원이 자유 변수에 의해 표현되고 그 값은 HOU(High-Order Uniform)를 사용하여 결정된다는 것이다.예를 들어 "존은 메리를 좋아하고 베드로도 좋아한다"는 의미표현은 (j, m)∧ R(p)과 같으며, R(타원의 의미표현)의 값은 (j, m) = R(j)와 같은 방정식에 의해 결정된다.그런 방정식을 푸는 과정을 고차 통일이라고 한다.^[46]

For example, the unification problem { f(a, b, a) ≐ d(b, a, c) }, where the only variable is f, has the solutions {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) } and {f ↦ λx.λy.λz.d(b, a, c) }.

웨인 스나이더는 고차 통일과 E-통일의 일반화, 즉 람다-단어 모듈로를 평준화 이론으로 통일하는 알고리즘을 제공했다.^[47]

참고 항목

• 재작성
• 인정규정
• 람다 미적분에서의 명시적 대체
• 수학 방정식 풀이
• 통일 해제: 상징적 표현 사이의 불평등 해소
• 반통일: 두 용어의 최소 일반화(lgg)를 계산하고, 가장 일반적인 인스턴스(mgu)를 계산한다.
• 온톨로지 정렬(의미적 등가성을 가진 통일 사용)

메모들

참조

추가 읽기

• 프란츠 바데르와 웨인 스나이더(2001)이다."통일 이론" 웨이백 머신에 2015-06-08 보관.John Alan Robinson and Andrei Voronkov, 편집자, 자동 추론 핸드북 1권, 447–533페이지.엘스비에 과학 출판사.^{[dead link]}
• 길레스 다우크(2001)"고차 통일과 매칭"자동 추론 핸드북.
• 프란츠 바데르와 토비아스 닙코우(1998년).용어 재작성과 모든 것.케임브리지 대학교 출판부
• 프란츠 바데르와 요르그 H. 시크만[de](1993년)."통일론".인공지능과 논리 프로그래밍의 논리학 핸드북에서.
• 장 피에르 주안노와 클로드 키르치네르(1991)."추상 알헤브라의 해결방정식: 통일에 대한 규칙에 근거한 조사"컴퓨터 논리학에서: 앨런 로빈슨을 기리는 에세이들.
• 나첨 더쇼위츠와 장 피에르 주안노우드, 리프레드 시스템스, in: 잔 반 리우웬(ed.), 이론 컴퓨터 과학 핸드북, B권 형식 모델과 의미론, 엘스비에르, 1990, 페이지 243–320
• 요르그 H. 시크만(1990)."통일론".클로드 키르치네르(편집자) 통일에서.학술 출판사.
• Kevin Knight (Mar 1989). "Unification: A Multidisciplinary Survey" (PDF). ACM Computing Surveys. 21 (1): 93–124. CiteSeerX 10.1.1.64.8967. doi:10.1145/62029.62030. S2CID 14619034.
• 제라드 휴에와 데릭 C. 오펜(1980)."평준화 및 재작성 규칙: 설문 조사"기술 보고서.스탠퍼드 대학교
• 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 (2): 14–20. doi:10.1145/1089208.1089210. S2CID 17033087.
• 클로드 키르치너와 헨 키르치너재작성, 해결, 증명.준비 중.