Injectivity not required for unification algorithms?

Question

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.

Answer 1

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.

If you like, you can think of it as though every function symbol in a symbolic expression is an injective function; but that's not really accurate, that's just a crude way to think about symbolic expressions.

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).