title: Prolog: Is f(X) = X unifiable or not?
body: <p>My understanding of unification is a little patchy. I understand basic unification, but I'm having issues getting my head round terms which are not unifiable.</p>
  
  <p>I was watching a youtube tutorial on unification which stated if a variable is trying to be unified against a term which contains that variable, then it is not unifiable.</p>
  
  <p>However when I type <code>?- f(X) = X</code> into prolog, it returns something along the lines of... <code>f(f(f(f(f(f(...)))))) ?</code></p>
  
  <p>I understand why this is... but I don't understand if this means it is unifiable or not, as I would have expected it just to return 'no' if it wasn't unifiable. Am I right in thinking that trying to unify f(X) = X fails the occurs check, thus making them not unifiable?</p>