# Injectivity not required for unification algorithms?

When learning about a general unification algorithm, we learned the rule decompose, which states unifying

$$G \cup \{f(a_0,...a_k)=f(b_0,...,b_k)\} \Rightarrow G \cup \{a_0=b_0,...a_k=b_k\}.$$

The question of, "What if $$f$$ is not injective?" stood out to me. Say $$f$$ is not injective, and we traverse that branch of computation where $$f(a_0,...a_k)=f(b_0,...,b_k) \Rightarrow \{a_0=b_0,...,a_k=b_k\}$$ and lead to failure. Is it possible that there's another way to assign $$a_0,...,a_k$$ to $$b_0,...b_k$$ such that it's unifiable?

I was thinking maybe of an example to demonstrate what I mean. This may not be a good example, but say we consider $$f(x,y) = x+y$$, and we want to unify $$f(h(a),g(b)) = f(g(c),h(d))$$ then we would fail by assigning $$\{h(a) = g(c), g(b)=h(d)\}$$ by decompose, but succeed in unification if instead we first switch the arguments of $$f$$ (valid since $$f(a,b)=f(b,a)$$), which will yield $$\{a \mapsto d, b \mapsto c\}$$.

I was reading a bit about it in this paper on page 6 where they discuss the idea of strictness in terms of decompose, but I don't quite understand it, and more generally how we can perform this unification step of decompose on a general $$f$$ without somehow backtracking on failure.

• I don’t think unification was intended to resolve based on the semantics of the underlying functions (i.e., this only works bc you know f is commutative). – D. Ben Knoble Mar 25 '20 at 13:13

Here $$f$$ is not a mathematical function. Rather, it is a function symbol. Don't think of $$f(a,b)$$ as the result of evaluating the function at parameters $$a,b$$. Rather, think of it as a term in a symbolic expression -- it is a syntactic object that is not intended to be interpreted in the way you are interpreting it.
You can't define $$f(x)=x+y$$. $$f$$ is an uninterpreted function symbol. You're not allowed to define a particular function. Rather, $$f$$ is a stand-in for a function that is not yet defined. One way to think about it is that any conclusions that you draw from unification, are conclusions that should hold for all functions $$f$$ (not just a single one).