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.