Unifiable

Unifiable is a term used in logic, computer science, and related fields to describe two expressions (usually terms with variables) that can be made identical by applying a substitution to their variables. A substitution assigns a term to each variable, and applying the substitution to both expressions yields the same result. If such a substitution exists, the expressions are unifiable; if not, they are not unifiable. The most general substitution that makes the expressions identical is called the most general unifier (MGU), because any other unifier can be obtained by composing the MGU with another substitution.

A simple example: the terms f(x, a) and f(b, y) are unifiable with the substitution {x -> b, y -> a}. The occurs check is a technical refinement used in some unification procedures to prevent solutions where a variable is unified with a term containing that same variable (for example, x = f(x)). Without the occurs check, such equations can lead to infinite structures or non-terminating processes.

In first-order logic, unification is studied through Robinson’s unification algorithm, which computes an MGU when one exists and reports failure otherwise. This algorithm underpins many practical systems: Prolog and other logic programming languages rely on unification to match goals with clauses, and type inference in functional programming languages frequently uses unification to determine common types.

Higher-order unification (unifying terms with functions, lambdas, or lambda abstractions) is more complex; in general, it is undecidable, though restricted forms (such as higher-order pattern unification) are decidable and used in some proof and type systems. Unification modulo equational theories (like associativity or commutativity) also introduces additional complexity.