I am trying to write a toy logic programming query language, based on various sources of instruction including SICP and The Art of Prolog (AoP). I am just starting to work out my first sketch of the unification algorithm (the "heart of the computation model of logic programming" according to AoP), and AoP notes that
When implementing the unification algorithm for a particular logic programing language, the explicit substitution in both the equations on the stack and the unifier is avoided. Instead, logical variables and other terms are represented by memory cells with different values, and variable binding is implemented by assigning the memory cell representing a logical variable a reference to the cell containing the representation of the term the variable is bound to. (1st edition, p. 71)
Reading this made me realize that I only have a rough and practical grasp of how logical variables work, but I do not really understand how they are implemented. I'm not even sure what are the precise, formal characteristics that differentiate logical variable from the immutable variables that feature in other regions of the declarative programming paradigm. I will be grateful for all illuminating explanations and instructive references.