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.

  • $\begingroup$ 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). $\endgroup$ – D. Ben Knoble Mar 25 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.

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

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.