Anti-unification (computer science) とは

反統一は、与えられた2つの記号表現に共通する一般化を構築するプロセスです。統一と同様に、いくつかのフレームワークは、どの表現が(用語とも呼ばれる)、どの表現が等しいとみなされるかによって区別されます。式に関数を表す変数が許されていれば、このプロセスは「高次の反統一」と呼ばれ、そうでなければ「一次の反統一」と呼ばれます。一般化が、各入力式に事実上等しいインスタンスを持つことが要求される場合、プロセスは「統語的反統一」と呼ばれ、そうでなければ「E-反統一」または「反統一モジュロ理論」と呼ばれる。
反統一アルゴリズムは、与えられた式に対して、完全で最小限の一般化集合、すなわち、すべての一般化をカバーする集合であり、冗長なメンバを含まない集合をそれぞれ計算しなければならない。フレームワークによっては、完全で最小限の一般化集合は、1つ、有限に多くの、または無限に多くのメンバーを持つこともあれば、まったく存在しないこともあります。いずれにしても些細な一般化が存在するため、空にすることはできません。一次構文の反統一のために、Gordon Plotkinは、いわゆる「最小一般汎化」(lgg)を含む完全で最小限のシングルトン汎化集合を計算するアルゴリズムを与えました。
反統一は統一されたものと混同されるべきではない。後者は、すべての与えられた不等式が満足されるような変数の値を見つけることである、不等式の系を解くプロセスを意味する。この作業は一般化を見つけることとはかなり異なっています。