# Is Unification "an Implementation of Existential Quantification"?

I read a comment (I've forgotten the source), "Unification is an implementation of existential quantification." (Emphasis mine.)

If true, this point of view clears up many things.

For instance why omitting the "occurs check" in unification can lead to unsound inference: it would be the same as using the assumption of the existence of a thing in your proof(-term) of the existence of that thing.

It would also explain why the algorithms for unification in logic programming language engines I've looked at seem (to me) more arbitrary than other operators such as conjunction and disjunction.

But - is the statement true? Is it an over-simplification?

It's possible you're paraphrasing me. I've certainly said things similar to that e.g. here.

A more precise statement would be that existential quantification in logic programming languages is (typically) handled by introducing a unification variable. To perform existential introduction, you need to have a term $$t$$. The rule looks like: $$\dfrac{\Gamma\vdash P[t/x]}{\Gamma\vdash\exists x.P}$$

One way to implement this is to just guess a term $$t$$ and then see if we can backchain $$P(t)$$. Of course, for a language like Prolog, there are an infinite number of possible terms, and you have no guidance on what term to guess. A different option is to have $$t$$ be a meta-variable that stands for a term and continue execution on the hope that we can constrain $$t$$ enough to know what to decide later. This is essentially what a unification variable is. Unification itself just constrains what possible terms that meta-variable can be. Then, instead of actually enumerating the (now constrained) terms, we usually return the (simplified) constraints themselves as a compact representation of the set of possible terms, assuming they aren't contradictory (i.e. that that set isn't empty).

The occurs-check is simply the enforcement of the fact that usual term languages don't have infinite terms. You can consider other term languages that can represent these terms leading to things like rational tree unification.

Unsurprisingly, the operation unification itself most directly implements is equality. If we did the "exhaustively enumerate terms" approach to handling existential quantification, all the places where we (implicitly) use "unification" could just be straightforward syntactic checks of ground terms. With meta-variables, they instead produce constraints. Of course, this suggests the natural and common generalization of allowing constraints other than syntactic equality, and this leads to constraint logic programming. One generic example of such a constraint is disunification which states what a term (potentially containing meta-variables) cannot be. It is the negation of unification, $$t\not\equiv s$$ states that for all substitutions $$\sigma$$, $$t[\sigma]\neq s[\sigma]$$.

• You're right, that's where I read it and thanks for linking it. As you speak of constraints on terms, another aspect I've puzzled over is whether unification constraining t to a specific value is theoretically significant compared to general constraints like "t < 10" or "t*t == 9", or if it's just that there are efficient implementations (and data representations) for the special case of assigning t a ground value. I suspect one could draw a parallel to how there are efficient (matrix based) solvers for linear constraints, but a different algorithm is required for nonlinear constraints. Commented Jun 6, 2019 at 14:37