2
$\begingroup$

Looking at various examples online, some seem concrete, but some seem to not be explained properly.

Can $f(x)$ be substituted with $g(x)$? I know that $x$ cannot be substituted with $f(x)$, but $x$ can be substituted with $y$ or $a$ or $f(y)$ (assuming $y$ is a variable and $a$ is a constant).

2 Answers 2

4

In short, you can unify two terms only if following conditions are true:

  • $x$ and $y$:
    • always.
  • $x$ and $f(\ldots)$:
    • the second term does not contain $x$.
  • $\alpha(x_1, \ldots, x_n)$ and $\beta(y_1, \ldots, y_m)$:
    • $\alpha = \beta$, e.g. $f = f$, but $f \neq g$,
    • $n = m$,
    • $x_i$ can be unified with $y_i$ for all $1 \leq i \leq n$.

I don't know the context, so this is not precise (e.g. there are some subleties if you have both bound and free variables, some quantifiers or Skolem constants), but it should give you enough intuition to work out any issues yourself.

Cheers!

  • 0
    See also the [Wikipedia](http://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm).2012-12-09
3

you can't unify two terms if no substitution makes them equal.