Variables in Prolog are a means to name terms that become known at run-time.
A variable's name starts with a capital letter or _ , followed by an arbitrary sequence of letters, digits and _ s. The variable, whose name is just _ , has a special role in Prolog. It is called the anonymous variable.
A variable gets allocated, when the clause (fact or rule) it occurs in is about to be applied. A variable does not get deallocated after successfully satisfying the goals that comprise the successful application of this clause. Rather, it gets deallocated when the application of the clause it got allocated in is cancelled in order, to e.g. resatisfy the goal that launched it, by a backward step.
From its allocation a variable is available for instantiation , i.e. for assigning it a term to stand for. The same variable can be instantiated and then uninstantiated unlimitedly many times. This is so because, after its allocation, the variable in general becomes part of terms, that get passed to subgoals, given rise by the application of the clause which caused the variable to get allocated. Here forward steps and backward steps can cause instantiation and uninstantiation both of locally allocated variables and earlier allocated ones.
A variable loses its value , i.e. gets uninstantiated again, only after backward steps on a clause that caused it to get a value - get instantiated. Note that, a loss of value, and not of allocation, is what happens. The backward step doesn't need to be on the clause that caused allocation.
It is sometimes possible for one variable to get instantiated to a term
that consists of just another variable. This case of unification
is remarkable for its violating the branch-replaces-leaf intuition
for the effect of instantiation on the tree representations of terms. The
definition of sharing of the two variables has been adopted, because
whatever in the future instantiates one of the two, immediately does so
with the other.