I am learning unification (Martelli and Montanari 1982 paper). I have a question about how the algorithm (Algorithm 1) deals with constants. Take these two equations:
$$ f(a) = c \\ f(X) = c $$
where $a$ and $c$ are constants (zero-arity functions), $f$ an unary function and $X$ a variable. Note that there are no variables in the first equation.
The paper states: "If the two root function symbols are different, stop with failure; otherwise, apply term reduction." $f$ is different from $c$, I cannot apply term reduction, does that mean I have to stop with failure? My intuition would lead to $f(a)=f(X)$, $a=X$ and finally $X=a$.
Rereading the Wiki page gives me the answer: "So for example 1+2 = 3 is not satisfiable because they are syntactically different."
My example would fail on the first equation.