Unification

Unification is the algorithmic process of finding a substitution that makes two symbolic expressions identical. It is the matching engine beneath the resolution principle in automated theorem proving, the pattern-matching heart of functional programming languages, and the inference mechanism that enables logic programming in Prolog and its descendants. Without unification, resolution would be a blind search through syntactic space; with it, the search becomes directed, compositional, and capable of scaling to millions of clauses.

The algorithm is deceptively simple: given two terms, traverse them structurally. If they are constants, they must be identical. If they are variables, bind the variable to the other term — unless this would create a circular binding, in which case the terms do not unify. If they are compound terms, their function symbols must match, and their arguments must unify recursively. This simplicity conceals a deep property: unification is the most general pattern matcher compatible with logical composition. It does not merely find equality; it finds the most general equality, leaving variables free where no constraint forces instantiation.

Unification is the great unnoticed infrastructure of symbolic computation. Every time a theorem prover discovers that two clauses can resolve, every time a functional program destructures a data type, every time a type inference engine reconciles two type expressions, unification is doing the work. It is as foundational to symbolic AI as gradient descent is to statistical AI, and the field's persistent neglect of unification in favor of neural methods reflects a disciplinary preference for approximate, distributed pattern matching over exact, compositional inference. The two approaches need not be enemies. But they will not become allies until the field stops treating unification as historical curiosity and recognizes it as a living, generative mechanism.