ユニフィケーション

ユニフィケーション（英: unification）は数理論理学や計算機科学の用語であり、充足性（英語版）問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つの項（英語版）が同一^[1]または同等^[2]であることを示す置換（英語版）を求めるのが目的である。ユニフィケーションは自動推論、論理プログラミング、プログラミング言語の型システムの実装などに幅広く用いられている。

なお、ユニフィケーションを単一化あるいは統一化とも呼ぶ。

主なユニフィケーションは数種類ある。等号を持たない論理（理論）において、2つの項が同一であることを示すためのユニフィケーションは統語論的ユニフィケーション^[3]と呼ばれる。空でない等号を持つ論理（理論）で2つの項の同等性^[4]を示す場合、それを意味論的ユニフィケーション^[5]と呼ぶ。置換は順序集合として順序付けられるので、ユニフィケーションは束における結びを求める手続きとして解釈できる。

ユニフィケーションアルゴリズムはジャック・エルブラン^[6]^[7]^[8]によって最初に発見されたが、ユニフィケーションを初めて形式的に研究したのはジョン・アラン・ロビンソン（英語版）で、一階述語論理の導出手続きを構築する際に一階のユニフィケーションを基盤として使い、組合せ爆発の原因の1つ（項を例化したものの探索）を排除することで自動推論技術への大きな一歩とした。

一階の項の統語論的ユニフィケーション

一階の項

変数記号の集合 X = {x,y,z,...}、個別定数記号の集合 C = {a,b,c,...}、個別関数記号の集合 F = {f,g,h,...} が与えられたとき、「項」は以下のような有限個の規則を適用して得られる式として定義される。

基本: 任意の変数 $x\in X$ および任意の定数 $a\in C$ は、それぞれ項である。
帰納: $t_{1},\ldots ,t_{k}$ が項なら $f(t_{1},\ldots ,t_{k})$ も項である。ただし k は正の有限の整数。

例えば、x、y、a、b は基本規則から項であることが明らかである。f(a,x) や g(b,y,x) は基本規則で項とされたものに帰納規則を一回適用することで得られる。f(a,f(a,x)) は帰納規則を2回適用することで得られる。このように様々な項が生成できる。簡単にするため、定数記号は引数（アリティ）がゼロ個の関数記号とみなすことが多く、帰納規則でゼロ引数の項も許容されるようにする。その場合、a() は a と統語論的に同等である。証明を行う目的では、基本規則と帰納規則を明確に区別するため、定数（ゼロアリティ関数）とアリティがゼロより大きい関数記号とを区別する。数学では関数記号ごとに引数の個数（アリティ）を固定することが多いが、統語論的ユニフィケーション問題では一般に関数記号は（有限の）任意個の引数を持ち、同じ関数記号であっても文脈によって異なる個数の引数をとりうる。例えば、f(f(a),f(x,y,z)) はユニフィケーション問題においては正しい項である。

置換

置換は、変数から項へのマッピングの有限集合 $\{x_{1}\mapsto t_{1},\dots ,x_{k}\mapsto t_{k}\}$ と定義され、1つの変数を2つの異なる項にマッピングすると曖昧さが生じるため、個々のマッピングは一意的でなければならない。項 u への置換の「適用」を $u\{x_{1}\mapsto t_{1},\dots ,x_{k}\mapsto t_{k}\}$ と記述し、項 $u$ に出現する各変数 $x_{i}$ を項 $t_{i}$ で置き換えることを意味する。このとき、 $1\leq i\leq k$ である。例えば、 $f(x,a,g(z),y)\{x\mapsto h(a,y),z\mapsto b\}=f(h(a,y),a,g(b),y)$ となる。

一階の項における統語論的ユニフィケーション問題

一階の項における統語論的ユニフィケーション問題は、同等である可能性のある有限個の式の連言 $t_{1}{\stackrel {?}{=}}u_{1}\And ,\ldots ,\And t_{n}{\stackrel {?}{=}}u_{n}$ で表される。この問題を解くには、それぞれの潜在的等式の左辺と右辺が統語論的に等価となるような置換 $\theta$ を求める必要があり、 $t_{1}\theta =u_{1}\theta \And ,\ldots ,\And t_{n}\theta =u_{n}\theta$ となるようにしなければならない。そのような置換 $\theta$ を「単一子」（ユニフィケーション作用素）と呼ぶ。ユニフィケーション問題には解がない場合もある。例えば、 $x{\stackrel {?}{=}}z\And y{\stackrel {?}{=}}f(x)$ の単一子は $\{x\mapsto z,y\mapsto f(z)\}$ である。この場合、

x\{x\mapsto z,y\mapsto f(z)\}=z=z\{x\mapsto z,y\mapsto f(z)\}=z

y\{x\mapsto z,y\mapsto f(z)\}=f(z)=f(x)\{x\mapsto z,y\mapsto f(z)\}=f(z)

となる。

出現検査

変数 x を x が部分として出現する関数 x=f(...,x,...) とユニフィケーションしようとする場合、x は無限個の項を持たなければならなくなる。これは有限であるとした項の定義と矛盾するため、ユニフィケーションは失敗する。そのためユニフィケーション問題を解くアルゴリズムでは、まず x がユニフィケーションしようとする項の中に出現しないかチェックする。これを出現検査（英語版）^[9]などと呼ぶ。

非形式的概要

2つの項 s と t があるとき、（統語論的）ユニフィケーションは s と t を構造的に等価にする置換を求めるプロセスである。そのような置換が存在する場合、それを s と t の単一子^[10]と呼ぶ。

理論上、入力された2つの項は無数の単一子を持ちうる。しかし一般的用途では1つの最大汎用単一子^[11]を考慮すれば十分である。他の単一子は最大汎用単一子のインスタンスである。

一階のユニフィケーションは、一階の項（変数記号や関数記号で構築される項）の統語論的ユニフィケーションである。一方高階ユニフィケーションは、高階の項（何らかの高階の変数を含む項）のユニフィケーションを指す。

特定のユニフィケーションアルゴリズムの理論的属性は、入力される項の多様性に依存する。たとえば一階のユニフィケーションは決定可能であり、単一化可能な項群は必ず最大汎用単一子を持つ。しかし高階ユニフィケーションは一般に決定不能であり、最大汎用単一子を持たないことが多い。

統語論的ユニフィケーションとは別に、意味論的ユニフィケーション^[12]も広く使われている。この2つは、項を「等しい」とみなす方法が異なる。統語論的ユニフィケーションでは、置換によって項が構造的に等価になるようにする。意味論的ユニフィケーションでは、2つの項が何らかの理論において合同であるかで判定する。例えば、交換性と結合性において合同な項を「等しい」とするユニフィケーションをAC-ユニフィケーションと呼ぶ。

ユニフィケーションは計算機科学の重要なツールである。特に一階のユニフィケーションは論理プログラミング、プログラミング言語の型システム設計、自動推論などに用いられている。高階ユニフィケーションは定理証明支援で使われている。高階ユニフィケーションに制約を加えたものを実装に採用したプログラミング言語^[13]もある。意味論的ユニフィケーションは、背景理論付きSAT (SMT) を解くアルゴリズムや項書き換えアルゴリズムでよく使われている。

一階述語論理でのユニフィケーションの定義

p と q が一階述語論理の文とする。

UNIFY(p,q) = U ここで subst(U,p) = subst(U,q)

subst(U,p) は置換 U を文 p に適用した結果を意味する。したがって U は p と q にとっての単一子である。p と q のユニフィケーションは両者に U を適用した結果である^[14]。

例えば L = {p,q} のような文の集合 L があるとする。L についての全単一子を U' としたとき、L に U を適用したものにある置換 s を適用した結果が L に U' を適用した結果と同じなら、単一子 U は L の最大汎用単一子^[11]と呼ばれる。

subst(U',L) = subst(s,subst(U,L)).

論理プログラミングでのユニフィケーション

単一化(ユニフィケーション)の考え方は Prolog に代表される論理プログラミングの根底を支える重要な概念である。それは変数の内容の束縛であり、項の構成要素の全体の形式から細部までその同一性を検査する機構である。他のプログラム言語とは異なり、Prolog では = という記号はこの意味を表す。Prolog は、質問としての副目標と、これによって呼び出される述語定義の頭部の単一化が試みられ、頭部の単一化の成功した節のみ選択され、その本体が次の質問になる導出と呼ばれるダイナミックで再帰的な機構によって実行される。

一般に型推論アルゴリズムは上記単一化に基づいている。

Prolog では、単一化されるとは、

束縛されていない変数は、原子項、複合項、そして他の束縛されていない変数を、以後同一なものとみなす。この変数の変数名を、変数を含む他の項の一種の別名と解釈することも可能である。全ての形式の項に対して同一のものとみなすことができるのだから、束縛されていない変数の単一化は必ず成功する。(注1)
原子項（アトム）は同じ原子項とだけ単一化可能である。原子項はアルファベット(英文字に限らない)によって構成された文字列なのでこの先頭から最後までの文字とその位置が同一の場合、単一化される。一ヶ所でも異なれば単一化は失敗する。
複合項は関数名(述語名)とアリティ（オペランドの個数）が等しい場合に、対応するオペランド毎に項の単一化が再帰的に試みられる。この単一化が全て成功した場合のみ単一化に成功したことになる。

(注1) 最近の Prolog や一階述語論理では、変数（変項）はそれ自身を含む項と単一化することはできない。それをすると無限の単一化が発生するためである。

型推論

ユニフィケーションは型推論でも使われており、例えば関数型言語 Haskell で使われている。型推論を行う言語では型に関する情報をいちいち記述する必要がなく、ユニフィケーションはデータ型の誤り検出に使われる。Haskellの式 1:['a','b','c'] は型付けが正しくない。なぜならリスト構築関数 : の型は a->[a]->[a] だが、第一引数 1 からポリモルフィックな型変数 a はInt型となるのに対して、['a','b','c'] の型は[Char]であり、a は同時に Char と Int になることはできないからである。

型推論のアルゴリズムは次のようになる:

任意の型変数は任意の型表現と単一化し、その表現をインスタンス化する。理論によっては出現検査でこの規則に制約を課すこともある。
2つの型定数は両者が同じ型のときのみ単一化される。
2つの型構築は、両者が使用する型構築子が同じで、それらのコンポーネント型が再帰的に単一化されるときのみ単一化される。

宣言的特徴から、ユニフィケーションが行われる順序は通常重要ではない。

高階ユニフィケーション

多くの用途で、一階の項ではなく型付きラムダ項のユニフィケーションを考慮する必要がある。そのようなユニフィケーションを「高階ユニフィケーション」と呼ぶことが多い。高階ユニフィケーションで特に研究が進んでいる領域は、αβη変換により単純な型付きラムダ項の等価性を判定する問題である。そのようなユニフィケーション問題は最大汎用単一子を持たない。高階ユニフィケーションは決定不能だが^[15]^[16]^[17]、Gérard Huet は単一子空間の体系的探索を可能にする半決定可能なユニフィケーションアルゴリズム（Martelli-Montanari のユニフィケーションアルゴリズム^[18]に高階の変数を含む項についての規則を加えて一般化したもの）を示した^[19]。Huet^[20] と Gilles Dowek^[21] はこれに関する論文を書いている。

デール・ミラー^[22]は高階パターン・ユニフィケーション^[23]と呼ばれるものを提案した^[24]。この高階ユニフィケーションのサブセットは決定可能であり、これで解けるユニフィケーション問題には最大汎用単一子が存在する。λProlog（英語版）やTwelf（英語版）といった高階の論理プログラミング言語は、完全な高階ユニフィケーションではなくパターン・ユニフィケーションを実装しているものが多い。

計算言語学では、省略法について最も有力な理論として、省略された要素を自由変数で表し高階ユニフィケーション (HOU) を使ってその値を決定するというものがある。例えば、ジョンはメアリーが好きで、ピーターも同様であるという文を like(j; m)R(p) のように意味論表現したとき、R（省略の意味論的表現）の値は like(j; m) = R(j) という等式で決定される。このような式を解くプロセスを高階ユニフィケーションと呼ぶ^[25]。

一階の項の統語論的ユニフィケーションの例

Prolog では、大文字で始まるシンボルは変数名、小文字で始まるシンボルは関数名を表し、カンマは論理積として使われる。数学の慣習では小文字だけを使い、アルファベットの最後の方（たとえば x,y,z）は変数名、f,g,h といった文字は関数記号、a,b,c といった文字は定数を意味し、定数は引数を持たない関数とみなされる。論理積は & または $\land$ で表される。

Prolog の記法	数学の記法	ユニフィケーションに必要な置換	備考
`a = a`	$a=a$	$\{\,\}$	成功（恒真式）
`a = b`	$a=b$	失敗	a と b は一致しない。
`X = X`	$x=x$	$\{\,\}$	成功（恒真式）
`a = X`	$a=x$	$\{x\mapsto a\}$	x は定数 a に単一化される。
`X = Y`	$x=y$	$\{x\mapsto y\}$	x と y は別名である。
`f(a,X) = f(a,b)`	$f(a,x)=f(a,b)$	$\{x\mapsto b\}$	関数記号と定数記号が一致しているので、x を定数 b に単一化する。
`f(a) = g(a)`	$f(a)=g(a)$	失敗	f と g は一致しない。
`f(X) = f(Y)`	$f(x)=f(y)$	$\{x\mapsto y\}$	x と y は別名である。
`f(X) = g(Y)`	$f(x)=g(y)$	失敗	f と g は一致しない。
`f(X) = f(Y,Z)`	$f(x)=f(y,z)$	失敗	アリティが異なる。
`f(g(X)) = f(Y)`	$f(g(x))=f(y)$	$\{y\mapsto g(x)\}$	y を項 g(x) に単一化する。
`f(g(X),X) = f(Y,a)`	$f(g(x),x)=f(y,a)$	$\{x\mapsto a,y\mapsto g(a)\}$	x を定数 a に、y を項 g(a) に単一化する。
`X = f(X)`	$x=f(x)$	失敗とすべき	（出現検査（英語版）により）厳密な一階述語論理では失敗となり、最近のPrologでも失敗する。古い実装のPrologでは x が x=f(f(f(f(...)))) という無限の式に単一化されるが、これは厳密には項ではない。
`X = Y, Y = a`	$x=y\land y=a$	$\{x\mapsto a,y\mapsto a\}$	x と y が共に定数 a に単一化される。
`a = Y, X = Y`	$a=y\land x=y$	$\{x\mapsto a,y\mapsto a\}$	同上（ユニフィケーションは対称的で推移的である）
`X = a, b = X`	$x=a\land b=x$	失敗	a と b は一致しないので、x はどちらとも単一化できない。

アルゴリズム

項 $s_{0},t_{0},\ldots ,s_{n},t_{n}$ についてのユニフィケーション問題 $G$ が ${\text{ }}G=\{s_{1}{\stackrel {\text{?}}{=}}t_{1},\ldots ,s_{n}{\stackrel {\text{?}}{=}}t_{n}\}$ という潜在的等式の多重集合で表されるとき、そのアルゴリズムはそれらの式に以下に示す項書き換え規則を適用し、等価な形式である $\{x_{1}{\stackrel {\text{?}}{=}}u_{1},\ldots ,x_{m}{\stackrel {\text{?}}{=}}u_{m}\}$ に変形しようとする。ここで、 $x_{0},\ldots ,x_{m}$ は一意な変数である（1つの式の左辺に一度だけ現れ、他の部分には出現しない）。この形式の多重集合は置換を表しているとみなすことができる。解がない場合、アルゴリズムは $\bot$ とともに停止する。項 $t$ に含まれる変数群を $Vars(t)$ と表記し、問題 $G$ 内の式の左辺と右辺の全ての項に含まれる変数の集合は $Vars(G)$ と表記する。問題 $G$ 内での変数 $x$ の出現を全て項 $t$ に置換することを $G\{x\mapsto t\}$ と表記する。簡単にするため、定数記号は引数ゼロ個の関数記号とみなす。

$G\cup \{t{\stackrel {\text{?}}{=}}t\}\Rightarrow G$

$G\cup \{f(s_{1},\dots ,s_{k}){\stackrel {\text{?}}{=}}f(t_{1},\ldots ,t_{k})\}\Rightarrow G\cup \{s_{1}{\stackrel {\text{?}}{=}}t_{1},\ldots ,s_{k}{\stackrel {\text{?}}{=}}t_{k}\}$

$G\cup \{f(s_{1},\dots ,s_{k}){\stackrel {\text{?}}{=}}g(t_{1},\ldots ,t_{m})\}\Rightarrow \bot {\text{ if }}f\neq g\lor k\neq m$

$G\cup \{f(s_{1},\dots ,s_{k}){\stackrel {\text{?}}{=}}x\}\Rightarrow G\cup \{x{\stackrel {\text{?}}{=}}f(s_{1},\dots ,s_{k})\}$

$G\cup \{x{\stackrel {\text{?}}{=}}t\}\Rightarrow G\{x\mapsto t\}\cup \{x{\stackrel {\text{?}}{=}}t\}{\text{ if }}x\in Vars(G)\land x\notin Vars(t)$

$G\cup \{x{\stackrel {\text{?}}{=}}f(s_{1},\dots ,s_{k})\}\Rightarrow \bot {\text{ if }}x\in Vars(f(s_{1},\dots ,s_{k}))$

停止することの証明

停止性の証明においては <NUVN,NLHS,EQN> という3タプルを考察する。NVUN は一意でない変数の数^[26]、NLHS は潜在的等式の左辺にある関数記号と定数の数^[27]、EQN は等式の数^[28]である。書き換え規則をどのような順序で適用しても、書き換えの度にNUVNは減るか、減らずに現状維持するかのどちらかなので、最終的に停止する。NUVNが現状維持した場合、NLHSが書き換えによって減るか、減らずに現状維持するかのどちらかである。NUVNとNLHSがどちらも現状維持した場合、EQNが書き換えによって減る。

構造上再帰的なユニフィケーション

コナー・マクブリッジ（英語版）は、Epigram（英語版）のような依存型（英語版）言語で「ユニフィケーションが利用している構造を表現することにより」、ジョン・アラン・ロビンソンのアルゴリズムを再帰的にすることができ、証明の複数の停止条件は不要になることを示した^[29]。

脚注

^ 英: identical
^ 英: equal
^ 英: syntactic unification
^ 英: equality
^ 英: semantic unification
^ 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 (2009). Lectures on Jacques Herbrand as a Logician (SEKI Report). DFKI. arXiv:0902.4682。 Here: p.56
^ 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
^ 英: occurs check
^ 英: unifier
^ ^a ^b 英: most general unifier
^ 英: equational-unification。e-unification とも呼ばれる。
^ lamdaPrologなど
^ Russell, Norvig: Artificial Intelligence, A Modern Approach, p. 277
^ Warren Goldfarb: The undecidability of the second-order unification problem
^ Gérard Huet: The undecidability of unification in third order logic
^ Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)
^ Martelli, Montanari: An Efficient Unification Algorithm
^ Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []
^ Gérard Huet: Higher Order Unification 30 Years Later
^ Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009-1062
^ 英: Dale Miller
^ 英: higher-order pattern unification
^ Dale Miller: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, 1991, pp. 497--536
^ Claire Gardent, Michael Kohlhase, Karsten Konrad, (1997), A multi-level, Higher-Order Unification approach to ellipsis
^ 英: number of non-unique variables
^ 英: number of function symbols and constants on the LHS of potential equations
^ 英: number of equations
^ McBride, Conor (October 2003). “First-Order Unification by Structural Recursion”. Journal of Functional Programming 13 (6): 1061–1076. doi:10.1017/S0956796803004957. ISSN 0956-7968 2012年3月30日閲覧。.

参考文献

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.
Joseph Goguen, What is Unification?.
Alex Sakharov. "Unification". mathworld.wolfram.com (英語).

[1] 英: identical

[2] 英: equal

[3] 英: syntactic unification

[4] 英: equality

[5] 英: semantic unification

[6] 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.

[7] 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

[8] 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

[9] 英: occurs check

[10] 英: unifier

[#1-11] 英: most general unifier

[12] 英: equational-unification。e-unification とも呼ばれる。

[13] Prologなど

[14] Russell, Norvig: Artificial Intelligence, A Modern Approach, p. 277

[15] Warren Goldfarb: The undecidability of the second-order unification problem

[16] Gérard Huet: The undecidability of unification in third order logic

[17] Claudio Lucchesi: The Undecidability of the Unification Problem for Third Order Languages (Research Report CSRR 2059; Department of Computer Science, University of Waterloo, 1972)

[18] Martelli, Montanari: An Efficient Unification Algorithm

[19] Gérard Huet: A Unification Algorithm for typed Lambda-Calculus []

[20] Gérard Huet: Higher Order Unification 30 Years Later

[21] Gilles Dowek: Higher-Order Unification and Matching. Handbook of Automated Reasoning 2001: 1009-1062

[22] 英: Dale Miller

[23] 英: higher-order pattern unification

[24] Dale Miller: A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, 1991, pp. 497--536

[25] Claire Gardent, Michael Kohlhase, Karsten Konrad, (1997), A multi-level, Higher-Order Unification approach to ellipsis

[26] 英: number of non-unique variables

[27] 英: number of function symbols and constants on the LHS of potential equations

[28] 英: number of equations

[29] McBride, Conor (October 2003). “First-Order Unification by Structural Recursion”. Journal of Functional Programming 13 (6): 1061–1076. doi:10.1017/S0956796803004957. ISSN 0956-7968 2012年3月30日閲覧。.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]