What precisely is a "logical variable" and what is the general approach for implementing the language feature?

Question

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.

Answer 1

Partial answer, concerning only the notion of logical variable.

A first approximation could be to say that logic variables act like math variables: once their value is learned, it will not change. That leads to the notion of assign-once variables. This contrasts with the notion of variables in imperative programming languages where they symbolically identify memory locations, allowing destructive (and thus) multiple assignment. But, going back to logic variables, it gets better. A logic variable can be unified with a term, but that term may itself contain variables. In turn, these variables can be further unified with other terms later. Consider the following example in Prolog:

?- V = a(Y).
V = a(Y).

?- V = a(Y), V = a(1).
V = a(1),
Y = 1.

In the second query, the variable V is further instantiated by unifying the variable it contains, Y, with the integer 1. The =/2 operator is Prolog unification operator. Unification is a logical operation that is true when you can take two terms and make them equal, possibly by binding variables in one term to a sub-term in the other term.